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	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐶 − 𝐷 ) ) ) → 𝐴 ∥ ( 𝐵 − 𝐷 ) )

Proof

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