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