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