Proof
let is_diff n ↔ (∃a. ∃b. a ∈ ℕ ∧ b ∈ ℕ ∧ n = a - b).
01. 1 ⊢ n ∈ ℕ, hypo.
02. 1 ⊢ n - 0 = n, nsub_zero 1.
03. 1 ⊢ n = n - 0, eq_symm 2.
04. ⊢ 0 ∈ ℕ, zero_in_nat.
05. 1 ⊢ n ∈ ℕ ∧ 0 ∈ ℕ, conj_intro 1 4.
06. 1 ⊢ n ∈ ℕ ∧ 0 ∈ ℕ ∧ n = n - 0, conj_intro 5 3.
07. 1 ⊢ ∃b. n ∈ ℕ ∧ b ∈ ℕ ∧ n = n - b, ex_intro 6.
08. 1 ⊢ is_diff n, ex_intro 7.
09. 1 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 1.
10. 1 ⊢ n ∈ ℝ ∧ is_diff n, conj_intro 9 8.
11. 1 ⊢ set n, set_intro 1.
12. 1 ⊢ n ∈ {z | z ∈ ℝ ∧ is_diff z}, comp_intro 11 10.
13. 1 ⊢ n ∈ ℤ, eq_subst_rev int_eq 12, P t ↔ n ∈ t.
14. ⊢ n ∈ ℕ → n ∈ ℤ, subj_intro 13.
15. ⊢ ∀n. n ∈ ℕ → n ∈ ℤ, uq_intro 14.
nat_incl_in_int. ⊢ ℕ ⊆ ℤ, incl_intro 15.
Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, radd_closed, radd_neutr, real_is_set.