Proof 01. 1 ⊢ a ∈ ℤ, hypo. 02. 2 ⊢ b ∈ ℤ, hypo. 03. 3 ⊢ c ∈ ℤ, hypo. 04. 4 ⊢ m ∈ ℤ, hypo. 05. 5 ⊢ cong a b m, hypo. 06. 6 ⊢ cong b c m, hypo. 07. 5 ⊢ ∃k. k ∈ ℤ ∧ a - b = m⋅k, cong_elim 5. 08. 6 ⊢ ∃k'. k' ∈ ℤ ∧ b - c = m⋅k', cong_elim 6. 09. 9 ⊢ k ∈ ℤ ∧ a - b = m⋅k, hypo. 10. 10 ⊢ k' ∈ ℤ ∧ b - c = m⋅k', hypo. 11. 9 ⊢ k ∈ ℤ, conj_eliml 9. 12. 10 ⊢ k' ∈ ℤ, conj_eliml 10. 13. 9 ⊢ a - b = m⋅k, conj_elimr 9. 14. 10 ⊢ b - c = m⋅k', conj_elimr 10. 15. 9, 10 ⊢ (a - b) + (b - c) = m⋅k + m⋅k', eq_cong_ii 13 14, f x y = x + y. 16. 1, 2, 3 ⊢ (a - b) + (b - c) = a - c, isub_cancel_middle 1 2 3. 17. 1, 2, 3, 9, 10 ⊢ a - c = m⋅k + m⋅k', eq_trans_ll 16 15. 18. 4, 9, 10 ⊢ m⋅(k + k') = m⋅k + m⋅k', imul_distl_add 4 11 12. 19. 1, 2, 3, 4, 9, 10 ⊢ a - c = m⋅(k + k'), eq_trans_rr 17 18. 20. 9, 10 ⊢ k + k' ∈ ℤ, iadd_closed 11 12. 21. 1, 2, 3, 4, 9, 10 ⊢ cong a c m, cong_intro 20 19. 22. 1, 2, 3, 4, 6, 9 ⊢ cong a c m, ex_elim 8 21. 23. 1, 2, 3, 4, 5, 6 ⊢ cong a c m, ex_elim 7 22. 24. 1, 2, 3, 4 ⊢ cong a b m → cong b c m → cong a c m, subj_intro_ii 23. cong_trans. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → m ∈ ℤ → cong a b m → cong b c m → cong a c m, subj_intro_iv 24.
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.