Proof
let is_diff z ↔ (∃m. ∃n. m ∈ ℕ ∧ n ∈ ℕ ∧ z = m - n).
01. 1 ⊢ a ∈ ℤ, hypo.
02. 1 ⊢ a ∈ {z | z ∈ ℝ ∧ is_diff z},
eq_subst int_eq 1, P t ↔ a ∈ t.
03. 1 ⊢ a ∈ ℝ ∧ is_diff a, comp_elim 2.
04. 1 ⊢ a ∈ ℝ, conj_eliml 3.
05. 1 ⊢ is_diff a, conj_elimr 3.
06. 6 ⊢ ∃n. m ∈ ℕ ∧ n ∈ ℕ ∧ a = m - n, hypo.
07. 7 ⊢ m ∈ ℕ ∧ n ∈ ℕ ∧ a = m - n, hypo.
08. 7 ⊢ m ∈ ℕ, conj_elimll 7.
09. 7 ⊢ n ∈ ℕ, conj_elimlr 7.
10. 7 ⊢ m ∈ ℝ, incl_elim nat_incl_in_real 8.
11. 7 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 9.
12. 7 ⊢ a = m - n, conj_elimr 7.
13. 7 ⊢ -a = -(m - n), eq_cong 12, f t = -t.
14. 7 ⊢ -(m - n) = n - m, rsub_neg 10 11.
15. 7 ⊢ -a = n - m, eq_trans 13 14.
16. 7 ⊢ n ∈ ℕ ∧ m ∈ ℕ, conj_intro 9 8.
17. 7 ⊢ n ∈ ℕ ∧ m ∈ ℕ ∧ -a = n - m, conj_intro 16 15.
18. 7 ⊢ ∃m. n ∈ ℕ ∧ m ∈ ℕ ∧ -a = n - m, ex_intro 17.
19. 7 ⊢ is_diff (-a), ex_intro 18.
20. 1 ⊢ -a ∈ ℝ, rneg_closed 4.
21. 1 ⊢ set (-a), set_intro 20.
22. 1, 7 ⊢ -a ∈ ℝ ∧ is_diff (-a), conj_intro 20 19.
23. 1, 7 ⊢ -a ∈ {z | z ∈ ℝ ∧ is_diff z},
comp_intro 21 22, P z ↔ z ∈ ℝ ∧ is_diff z.
24. 1, 7 ⊢ -a ∈ ℤ, eq_subst_rev int_eq 23, P t ↔ -a ∈ t.
25. 1, 6 ⊢ -a ∈ ℤ, ex_elim 6 24.
26. 1 ⊢ -a ∈ ℤ, ex_elim 5 25.
ineg_closed. ⊢ a ∈ ℤ → -a ∈ ℤ, subj_intro 26.
Dependencies
The given proof depends on 14 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, real_is_set, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed.