Metamath Proof Explorer

Theorem congtr

Description: A wff of the form A || ( B - C ) is interpreted as a congruential equation. This is similar to ( B mod A ) = ( C mod A ) , but is defined such that behavior is regular for zero and negative values of A . To use this concept effectively, we need to show that congruential equations behave similarly to normal equations; first a transitivity law. Idea for the future: If there was a congruential equation symbol, it could incorporate type constraints, so that most of these would not need them. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion congtr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → A ∥ B − D

Proof

Step Hyp Ref Expression
1 simp1l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → A ∈ ℤ
2 simp1r ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → B ∈ ℤ
3 simp2l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → C ∈ ℤ
4 2 3 zsubcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → B − C ∈ ℤ
5 zsubcl ⊢ C ∈ ℤ ∧ D ∈ ℤ → C − D ∈ ℤ
6 5 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → C − D ∈ ℤ
7 simp3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → A ∥ B − C ∧ A ∥ C − D
8 dvds2add ⊢ A ∈ ℤ ∧ B − C ∈ ℤ ∧ C − D ∈ ℤ → A ∥ B − C ∧ A ∥ C − D → A ∥ B − C + C - D
9 8 imp ⊢ A ∈ ℤ ∧ B − C ∈ ℤ ∧ C − D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → A ∥ B − C + C - D
10 1 4 6 7 9 syl31anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → A ∥ B − C + C - D
11 zcn ⊢ B ∈ ℤ → B ∈ ℂ
12 11 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∈ ℂ
13 12 3ad2ant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → B ∈ ℂ
14 zcn ⊢ C ∈ ℤ → C ∈ ℂ
15 14 adantr ⊢ C ∈ ℤ ∧ D ∈ ℤ → C ∈ ℂ
16 15 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → C ∈ ℂ
17 zcn ⊢ D ∈ ℤ → D ∈ ℂ
18 17 adantl ⊢ C ∈ ℤ ∧ D ∈ ℤ → D ∈ ℂ
19 18 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → D ∈ ℂ
20 13 16 19 npncand ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → B − C + C - D = B − D
21 10 20 breqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∧ A ∥ C − D → A ∥ B − D