Proof
let is_diff z ↔ (∃m. ∃n. m ∈ ℕ ∧ n ∈ ℕ ∧ z = m - n).
01. 1 ⊢ a ∈ ℤ, hypo.
02. 2 ⊢ b ∈ ℤ, hypo.
03. 1 ⊢ a ∈ {z | z ∈ ℝ ∧ is_diff z},
eq_subst int_eq 1, P t ↔ a ∈ t.
04. 2 ⊢ b ∈ {z | z ∈ ℝ ∧ is_diff z},
eq_subst int_eq 2, P t ↔ b ∈ t.
05. 1 ⊢ a ∈ ℝ ∧ is_diff a, comp_elim 3.
06. 2 ⊢ b ∈ ℝ ∧ is_diff b, comp_elim 4.
07. 1 ⊢ is_diff a, conj_elimr 5.
08. 2 ⊢ is_diff b, conj_elimr 6.
09. 9 ⊢ ∃n. m ∈ ℕ ∧ n ∈ ℕ ∧ a = m - n, hypo.
10. 10 ⊢ ∃n. m' ∈ ℕ ∧ n ∈ ℕ ∧ b = m' - n, hypo.
11. 11 ⊢ m ∈ ℕ ∧ n ∈ ℕ ∧ a = m - n, hypo.
12. 12 ⊢ m' ∈ ℕ ∧ n' ∈ ℕ ∧ b = m' - n', hypo.
13. 11 ⊢ a = m - n, conj_elimr 11.
14. 12 ⊢ b = m' - n', conj_elimr 12.
15. ⊢ m - n = m + -n, rsub_eq.
16. ⊢ m' - n' = m' + -n', rsub_eq.
17. 11 ⊢ a = m + -n, eq_trans 13 15.
18. 12 ⊢ b = m' + -n', eq_trans 14 16.
19. 11, 12 ⊢ a⋅b = (m + -n)⋅(m' + -n'),
eq_cong_ii 17 18, f x y = x⋅y.
20. 11 ⊢ m ∈ ℕ, conj_elimll 11.
21. 11 ⊢ n ∈ ℕ, conj_elimlr 11.
22. 12 ⊢ m' ∈ ℕ, conj_elimll 12.
23. 12 ⊢ n' ∈ ℕ, conj_elimlr 12.
24. 11 ⊢ m ∈ ℝ, incl_elim nat_incl_in_real 20.
25. 11 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 21.
26. 12 ⊢ m' ∈ ℝ, incl_elim nat_incl_in_real 22.
27. 12 ⊢ n' ∈ ℝ, incl_elim nat_incl_in_real 23.
28. 11 ⊢ -n ∈ ℝ, rneg_closed 25.
29. 12 ⊢ -n' ∈ ℝ, rneg_closed 27.
30. 11, 12 ⊢ (m + -n)⋅(m' + -n')
= m⋅m' + (-n)⋅m' + m⋅(-n') + (-n)⋅(-n'),
rmul_expand_add_add 24 28 26 29.
31. 11, 12 ⊢ a⋅b = m⋅m' + (-n)⋅m' + m⋅(-n') + (-n)⋅(-n'),
eq_trans 19 30.
32. 11, 12 ⊢ (-n)⋅(-n') = n⋅n', rmul_cancel_neg 25 27.
33. 11, 12 ⊢ a⋅b = m⋅m' + (-n)⋅m' + m⋅(-n') + n⋅n',
eq_subst 32 31, P t ↔ a⋅b = m⋅m' + (-n)⋅m' + m⋅(-n') + t.
34. 11, 12 ⊢ m⋅m' ∈ ℝ, rmul_closed 24 26.
35. 11, 12 ⊢ (-n)⋅m' ∈ ℝ, rmul_closed 28 26.
36. 11, 12 ⊢ m⋅(-n') ∈ ℝ, rmul_closed 24 29.
37. 11, 12 ⊢ n⋅n' ∈ ℝ, rmul_closed 25 27.
38. 11, 12 ⊢ m⋅m' + (-n)⋅m' + m⋅(-n') + n⋅n'
= m⋅m' + n⋅n' + (-n)⋅m' + m⋅(-n'),
radd_perm_1423 34 35 36 37.
39. 11, 12 ⊢ a⋅b = m⋅m' + n⋅n' + (-n)⋅m' + m⋅(-n'),
eq_trans 33 38.
40. 11, 12 ⊢ m⋅m' + n⋅n' + (-n)⋅m' + m⋅(-n')
= (m⋅m' + n⋅n') + ((-n)⋅m' + m⋅(-n')),
radd_assoc_llolloo 34 37 35 36.
41. 11, 12 ⊢ a⋅b = (m⋅m' + n⋅n') + ((-n)⋅m' + m⋅(-n')),
eq_trans 39 40.
42. 11, 12 ⊢ -(n⋅m') = (-n)⋅m', rmul_compatl_neg 25 26.
43. 11, 12 ⊢ -(m⋅n') = m⋅(-n'), rmul_compatr_neg 24 27.
44. 11, 12 ⊢ -(n⋅m') + -(m⋅n') = (-n)⋅m'+ m⋅(-n'),
eq_cong_ii 42 43, f x y = x + y.
45. 11, 12 ⊢ n⋅m' ∈ ℝ, rmul_closed 25 26.
46. 11, 12 ⊢ m⋅n' ∈ ℝ, rmul_closed 24 27.
47. 11, 12 ⊢ -(n⋅m' + m⋅n') = -(n⋅m') + -(m⋅n'),
rneg_dist_add 45 46.
48. 11, 12 ⊢ -(n⋅m' + m⋅n') = (-n)⋅m'+ m⋅(-n'),
eq_trans 47 44.
49. 11, 12 ⊢ a⋅b = (m⋅m' + n⋅n') + -(n⋅m' + m⋅n'),
eq_subst_rev 48 41, P t ↔ a⋅b = (m⋅m' + n⋅n') + t.
50. ⊢ (m⋅m' + n⋅n') - (n⋅m' + m⋅n')
= (m⋅m' + n⋅n') + -(n⋅m' + m⋅n'), rsub_eq.
51. 11, 12 ⊢ a⋅b = (m⋅m' + n⋅n') - (n⋅m' + m⋅n'),
eq_trans_rr 49 50.
52. 11, 12 ⊢ m⋅m' ∈ ℕ, nmul_closed 20 22.
53. 11, 12 ⊢ n⋅n' ∈ ℕ, nmul_closed 21 23.
54. 11, 12 ⊢ n⋅m' ∈ ℕ, nmul_closed 21 22.
55. 11, 12 ⊢ m⋅n' ∈ ℕ, nmul_closed 20 23.
56. 11, 12 ⊢ m⋅m' + n⋅n' ∈ ℕ, nadd_closed 52 53.
57. 11, 12 ⊢ n⋅m' + m⋅n' ∈ ℕ, nadd_closed 54 55.
58. 11, 12 ⊢ m⋅m' + n⋅n' ∈ ℕ ∧ n⋅m' + m⋅n' ∈ ℕ,
conj_intro 56 57.
59. 11, 12 ⊢ m⋅m' + n⋅n' ∈ ℕ ∧ n⋅m' + m⋅n' ∈ ℕ ∧
a⋅b = (m⋅m' + n⋅n') - (n⋅m' + m⋅n'), conj_intro 58 51.
60. 11, 12 ⊢ ∃n''. m⋅m' + n⋅n' ∈ ℕ ∧ n'' ∈ ℕ ∧
a⋅b = (m⋅m' + n⋅n') - n'', ex_intro 59.
61. 11, 12 ⊢ is_diff (a⋅b), ex_intro 60.
62. 1 ⊢ a ∈ ℝ, conj_eliml 5.
63. 2 ⊢ b ∈ ℝ, conj_eliml 6.
64. 1, 2 ⊢ a⋅b ∈ ℝ, rmul_closed 62 63.
65. 1, 2 ⊢ set (a⋅b), set_intro 64.
66. 1, 2, 11, 12 ⊢ a⋅b ∈ ℝ ∧ is_diff (a⋅b),
conj_intro 64 61.
67. 1, 2, 11, 12 ⊢ a⋅b ∈ {z | z ∈ ℝ ∧ is_diff z},
comp_intro 65 66, P z ↔ z ∈ ℝ ∧ is_diff z.
68. 1, 2, 11, 12 ⊢ a⋅b ∈ ℤ,
eq_subst_rev int_eq 67, P t ↔ a⋅b ∈ t.
69. 1, 2, 10, 11 ⊢ a⋅b ∈ ℤ, ex_elim 10 68.
70. 1, 2, 9, 10 ⊢ a⋅b ∈ ℤ, ex_elim 9 69.
71. 1, 2, 9 ⊢ a⋅b ∈ ℤ, ex_elim 8 70.
72. 1, 2 ⊢ a⋅b ∈ ℤ, ex_elim 7 71.
imul_closed. ⊢ a ∈ ℤ → b ∈ ℤ → a⋅b ∈ ℤ, subj_intro_ii 72.
Dependencies
The given proof depends on 16 axioms:
comp, eq_refl, eq_subst, ext, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, real_is_set, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed, subset.