Proof 01. 1 ⊢ a ∈ ℤ, hypo. 02. 2 ⊢ m ∈ ℤ, hypo. 03. 1 ⊢ a - a = 0, isub_self 1. 04. ⊢ 0 ∈ ℤ, calc. 05. 2 ⊢ m⋅0 = 0, imul_rzero 2. 06. 1, 2 ⊢ a - a = m⋅0, eq_trans_rr 3 5. 07. 1, 2 ⊢ cong a a m, cong_intro 4 6. cong_refl. ⊢ a ∈ ℤ → m ∈ ℤ → cong a a m, subj_intro_ii 7.
Dependencies
The given proof depends on 11 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_distl_add, rneg_closed.