Theorem nmul_closed

Proof
01. 1 ⊢ a ∈ ℕ, hypo.
02. 1 ⊢ a⋅0 = 0, nmul_rzero 1.
03. 1 ⊢ a⋅0 ∈ ℕ, eq_subst_rev 2 zero_in_nat,
  P t ↔ t ∈ ℕ.
04. 4 ⊢ n ∈ ℕ, hypo.
05. 5 ⊢ a⋅n ∈ ℕ, hypo.
06. 1, 5 ⊢ a⋅n + a ∈ ℕ, nadd_closed 5 1.
07. 1 ⊢ a⋅1 = a, nmul_neutr 1.
08. 1 ⊢ a⋅n + a⋅1 = a⋅n + a, eq_cong 7, f t = a⋅n + t.
09. ⊢ 1 ∈ ℕ, calc.
10. 1, 4 ⊢ a⋅(n + 1) = a⋅n + a⋅1, nmul_distl_add 1 4 9.
11. 1, 4 ⊢ a⋅(n + 1) = a⋅n + a, eq_trans 10 8.
12. 1, 4, 5 ⊢ a⋅(n + 1) ∈ ℕ, eq_subst_rev 11 6, P t ↔ t ∈ ℕ.
13. 1 ⊢ n ∈ ℕ → a⋅n ∈ ℕ → a⋅(n + 1) ∈ ℕ, subj_intro_ii 12.
14. 1 ⊢ ∀n. n ∈ ℕ → a⋅n ∈ ℕ → a⋅(n + 1) ∈ ℕ, uq_intro 13.
15. 1 ⊢ ∀n. n ∈ ℕ → a⋅n ∈ ℕ,
  nat_induction 3 14, P n ↔ a⋅n ∈ ℕ.
16. 16 ⊢ b ∈ ℕ, hypo.
17. 1, 16 ⊢ a⋅b ∈ ℕ, uq_bounded_elim 15 16.
nmul_closed. ⊢ a ∈ ℕ → b ∈ ℕ → a⋅b ∈ ℕ, subj_intro_ii 17.

Dependencies
The given proof depends on 15 axioms:
comp, eq_refl, eq_subst, ext, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, real_is_set, rmul_closed, rmul_distl_add, rmul_neutr, rneg_closed, subset.