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 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧D∈ℤ∧E∈ℤ∧A∥B−C∧A∥D−E→A∥B⁢D−C⁢E

Proof

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