Metamath Proof Explorer

Theorem congmul

Description: If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion congmul ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 · 𝐷 ) − ( 𝐶 · 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 simp11 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∈ ℤ )
2 simp12 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐵 ∈ ℤ )
3 simp2l ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐷 ∈ ℤ )
4 2 3 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐵 · 𝐷 ) ∈ ℤ )
5 simp2r ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐸 ∈ ℤ )
6 2 5 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐵 · 𝐸 ) ∈ ℤ )
7 simp13 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐶 ∈ ℤ )
8 7 5 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐶 · 𝐸 ) ∈ ℤ )
9 simp3r ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( 𝐷 − 𝐸 ) )
10 zsubcl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( 𝐷 − 𝐸 ) ∈ ℤ )
11 10 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐷 − 𝐸 ) ∈ ℤ )
12 dvdsmultr2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝐷 − 𝐸 ) ∈ ℤ ) → ( 𝐴 ∥ ( 𝐷 − 𝐸 ) → 𝐴 ∥ ( 𝐵 · ( 𝐷 − 𝐸 ) ) ) )
13 1 2 11 12 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐴 ∥ ( 𝐷 − 𝐸 ) → 𝐴 ∥ ( 𝐵 · ( 𝐷 − 𝐸 ) ) ) )
14 9 13 mpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐷 − 𝐸 ) ) )
15 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
16 15 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℂ )
17 16 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐵 ∈ ℂ )
18 zcn ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
19 18 adantr ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) → 𝐷 ∈ ℂ )
20 19 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐷 ∈ ℂ )
21 zcn ⊢ ( 𝐸 ∈ ℤ → 𝐸 ∈ ℂ )
22 21 adantl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) → 𝐸 ∈ ℂ )
23 22 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐸 ∈ ℂ )
24 17 20 23 subdid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐵 · ( 𝐷 − 𝐸 ) ) = ( ( 𝐵 · 𝐷 ) − ( 𝐵 · 𝐸 ) ) )
25 14 24 breqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 · 𝐷 ) − ( 𝐵 · 𝐸 ) ) )
26 simp3l ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( 𝐵 − 𝐶 ) )
27 2 7 zsubcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
28 dvdsmultr1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) → 𝐴 ∥ ( ( 𝐵 − 𝐶 ) · 𝐸 ) ) )
29 1 27 5 28 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) → 𝐴 ∥ ( ( 𝐵 − 𝐶 ) · 𝐸 ) ) )
30 26 29 mpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 − 𝐶 ) · 𝐸 ) )
31 zcn ⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
32 31 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
33 32 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐶 ∈ ℂ )
34 17 33 23 subdird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → ( ( 𝐵 − 𝐶 ) · 𝐸 ) = ( ( 𝐵 · 𝐸 ) − ( 𝐶 · 𝐸 ) ) )
35 30 34 breqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 · 𝐸 ) − ( 𝐶 · 𝐸 ) ) )
36 congtr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · 𝐷 ) ∈ ℤ ) ∧ ( ( 𝐵 · 𝐸 ) ∈ ℤ ∧ ( 𝐶 · 𝐸 ) ∈ ℤ ) ∧ ( 𝐴 ∥ ( ( 𝐵 · 𝐷 ) − ( 𝐵 · 𝐸 ) ) ∧ 𝐴 ∥ ( ( 𝐵 · 𝐸 ) − ( 𝐶 · 𝐸 ) ) ) ) → 𝐴 ∥ ( ( 𝐵 · 𝐷 ) − ( 𝐶 · 𝐸 ) ) )
37 1 4 6 8 25 35 36 syl222anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∧ 𝐴 ∥ ( 𝐷 − 𝐸 ) ) ) → 𝐴 ∥ ( ( 𝐵 · 𝐷 ) − ( 𝐶 · 𝐸 ) ) )