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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B x. D ) - ( C x. E ) ) )

Proof

Step Hyp Ref Expression
1 simp11 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A e. ZZ )
2 simp12 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> B e. ZZ )
3 simp2l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> D e. ZZ )
4 2 3 zmulcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( B x. D ) e. ZZ )
5 simp2r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> E e. ZZ )
6 2 5 zmulcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( B x. E ) e. ZZ )
7 simp13 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> C e. ZZ )
8 7 5 zmulcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( C x. E ) e. ZZ )
9 simp3r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( D - E ) )
10 zsubcl 
 |-  ( ( D e. ZZ /\ E e. ZZ ) -> ( D - E ) e. ZZ )
11 10 3ad2ant2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( D - E ) e. ZZ )
12 dvdsmultr2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( D - E ) e. ZZ ) -> ( A || ( D - E ) -> A || ( B x. ( D - E ) ) ) )
13 1 2 11 12 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( A || ( D - E ) -> A || ( B x. ( D - E ) ) ) )
14 9 13 mpd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( B x. ( D - E ) ) )
15 zcn 
 |-  ( B e. ZZ -> B e. CC )
16 15 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. CC )
17 16 3ad2ant1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> B e. CC )
18 zcn 
 |-  ( D e. ZZ -> D e. CC )
19 18 adantr 
 |-  ( ( D e. ZZ /\ E e. ZZ ) -> D e. CC )
20 19 3ad2ant2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> D e. CC )
21 zcn 
 |-  ( E e. ZZ -> E e. CC )
22 21 adantl 
 |-  ( ( D e. ZZ /\ E e. ZZ ) -> E e. CC )
23 22 3ad2ant2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> E e. CC )
24 17 20 23 subdid 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( B x. ( D - E ) ) = ( ( B x. D ) - ( B x. E ) ) )
25 14 24 breqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B x. D ) - ( B x. E ) ) )
26 simp3l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( B - C ) )
27 2 7 zsubcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( B - C ) e. ZZ )
28 dvdsmultr1 
 |-  ( ( A e. ZZ /\ ( B - C ) e. ZZ /\ E e. ZZ ) -> ( A || ( B - C ) -> A || ( ( B - C ) x. E ) ) )
29 1 27 5 28 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( A || ( B - C ) -> A || ( ( B - C ) x. E ) ) )
30 26 29 mpd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B - C ) x. E ) )
31 zcn 
 |-  ( C e. ZZ -> C e. CC )
32 31 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. CC )
33 32 3ad2ant1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> C e. CC )
34 17 33 23 subdird 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> ( ( B - C ) x. E ) = ( ( B x. E ) - ( C x. E ) ) )
35 30 34 breqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B x. E ) - ( C x. E ) ) )
36 congtr 
 |-  ( ( ( A e. ZZ /\ ( B x. D ) e. ZZ ) /\ ( ( B x. E ) e. ZZ /\ ( C x. E ) e. ZZ ) /\ ( A || ( ( B x. D ) - ( B x. E ) ) /\ A || ( ( B x. E ) - ( C x. E ) ) ) ) -> A || ( ( B x. D ) - ( C x. E ) ) )
37 1 4 6 8 25 35 36 syl222anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B x. D ) - ( C x. E ) ) )