cong_symm

Theorem cong_symm

Theorem. cong_symm
a ∈ ℤ → b ∈ ℤ → m ∈ ℤ → cong a b m → cong b a m

Proof
01. 1 ⊢ a ∈ ℤ, hypo.
02. 2 ⊢ b ∈ ℤ, hypo.
03. 3 ⊢ m ∈ ℤ, hypo.
04. 4 ⊢ cong a b m, hypo.
05. 4 ⊢ ∃k. k ∈ ℤ ∧ (a - b) = m⋅k, cong_elim 4.
06. 6 ⊢ k ∈ ℤ ∧ (a - b) = m⋅k, hypo.
07. 6 ⊢ k ∈ ℤ, conj_eliml 6.
08. 6 ⊢ (a - b) = m⋅k, conj_elimr 6.
09. 6 ⊢ -(a - b) = -(m⋅k), eq_cong 8, f t = -t.
10. 1, 2 ⊢ -(a - b) = b - a, isub_neg 1 2.
11. 3, 6 ⊢ -(m⋅k) = m⋅(-k), imul_compatr_neg 3 7.
12. 1, 2, 6 ⊢ b - a = -(m⋅k), eq_trans_ll 10 9.
13. 1, 2, 3, 6 ⊢ b - a = m⋅(-k), eq_trans 12 11.
14. 6 ⊢ -k ∈ ℤ, ineg_closed 7.
16. 1, 2, 3, 6 ⊢ cong b a m, cong_intro 14 13.
17. 1, 2, 3, 4 ⊢ cong b a m, ex_elim 5 16.
cong_symm. ⊢ a ∈ ℤ → b ∈ ℤ → m ∈ ℤ →
  cong a b m → cong b a m, subj_intro_iv 17.

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.