Theorem nat_zero_or_succ

Proof
let A n ↔ n = 0 ∨ (∃m. m ∈ ℕ ∧ n = m + 1).
01. ⊢ 0 = 0, calc.
02. ⊢ A 0, disj_introl 1.
03. 3 ⊢ A n, hypo.
04. 4 ⊢ n = 0, hypo.
05. ⊢ 0 ∈ ℕ, zero_in_nat.
06. 4 ⊢ n ∈ ℕ, eq_subst_rev 4 5, P t ↔ t ∈ ℕ.
07. ⊢ n + 1 = n + 1, eq_refl.
08. 4 ⊢ n ∈ ℕ ∧ n + 1 = n + 1, conj_intro 6 7.
09. 4 ⊢ ∃m. m ∈ ℕ ∧ n + 1 = m + 1, ex_intro 8.
10. 4 ⊢ A (n + 1), disj_intror 9.
11. 11 ⊢ ∃m. m ∈ ℕ ∧ n = m + 1, hypo.
12. 12 ⊢ k ∈ ℕ ∧ n = k + 1, hypo.
13. 12 ⊢ k ∈ ℕ, conj_eliml 12.
14. 12 ⊢ n = k + 1, conj_elimr 12.
15. 12 ⊢ k + 1 ∈ ℕ, succ_in_nat 13.
16. 12 ⊢ n + 1 = k + 1 + 1, eq_cong 14, f t = t + 1.
17. 12 ⊢ k + 1 ∈ ℕ ∧ n + 1 = k + 1 + 1, conj_intro 15 16.
18. 12 ⊢ ∃m. m ∈ ℕ ∧ n + 1 = m + 1, ex_intro 17.
19. 12 ⊢ A (n + 1), disj_intror 18.
20. 11 ⊢ A (n + 1), ex_elim 11 19.
21. 3 ⊢ A (n + 1), disj_elim 3 10 20.
22. ⊢ A n → A (n + 1), subj_intro 21.
23. 23 ⊢ n ∈ ℕ, hypo.
24. 23 ⊢ A n → A (n + 1), wk 22.
25. ⊢ n ∈ ℕ → A n → A (n + 1), subj_intro 24.
26. ⊢ ∀n. n ∈ ℕ → A n → A (n + 1), uq_intro 25.
27. ⊢ ∀n. n ∈ ℕ → A n, nat_induction 2 26, P n ↔ A n.
28. 23 ⊢ A n, uq_bounded_elim 27 23.
nat_zero_or_succ. ⊢ n ∈ ℕ → n = 0 ∨ ∃m. m ∈ ℕ ∧ n = m + 1,
  subj_intro 28.

Dependencies
The given proof depends on seven axioms:
comp, eq_refl, eq_subst, ext, radd_closed, real_is_set, subset.