Metamath Proof Explorer

Theorem jm2.19lem2

Description: Lemma for jm2.19 . (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion jm2.19lem2 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + M ) ) ) )

Proof

Step Hyp Ref Expression
1 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
2 1 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. ZZ )
3 2 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY M ) e. ZZ )
4 1 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
5 4 3adant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
6 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
7 6 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmX M ) e. NN0 )
8 7 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX M ) e. NN0 )
9 8 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX M ) e. ZZ )
10 3 9 gcdcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) gcd ( A rmX M ) ) = ( ( A rmX M ) gcd ( A rmY M ) ) )
11 jm2.19lem1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmX M ) gcd ( A rmY M ) ) = 1 )
12 11 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) gcd ( A rmY M ) ) = 1 )
13 10 12 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) gcd ( A rmX M ) ) = 1 )
14 coprmdvdsb 
 |-  ( ( ( A rmY M ) e. ZZ /\ ( A rmY N ) e. ZZ /\ ( ( A rmX M ) e. ZZ /\ ( ( A rmY M ) gcd ( A rmX M ) ) = 1 ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( ( A rmX M ) x. ( A rmY N ) ) ) )
15 3 5 9 13 14 syl112anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( ( A rmX M ) x. ( A rmY N ) ) ) )
16 8 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX M ) e. CC )
17 5 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY N ) e. CC )
18 16 17 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX M ) x. ( A rmY N ) ) = ( ( A rmY N ) x. ( A rmX M ) ) )
19 18 breq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( ( A rmX M ) x. ( A rmY N ) ) <-> ( A rmY M ) || ( ( A rmY N ) x. ( A rmX M ) ) ) )
20 15 19 bitrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( ( A rmY N ) x. ( A rmX M ) ) ) )
21 5 9 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmX M ) ) e. ZZ )
22 6 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
23 22 3adant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
24 23 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX N ) e. ZZ )
25 24 3 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY M ) ) e. ZZ )
26 dvdsmul2 
 |-  ( ( ( A rmX N ) e. ZZ /\ ( A rmY M ) e. ZZ ) -> ( A rmY M ) || ( ( A rmX N ) x. ( A rmY M ) ) )
27 24 3 26 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY M ) || ( ( A rmX N ) x. ( A rmY M ) ) )
28 dvdsadd2b 
 |-  ( ( ( A rmY M ) e. ZZ /\ ( ( A rmY N ) x. ( A rmX M ) ) e. ZZ /\ ( ( ( A rmX N ) x. ( A rmY M ) ) e. ZZ /\ ( A rmY M ) || ( ( A rmX N ) x. ( A rmY M ) ) ) ) -> ( ( A rmY M ) || ( ( A rmY N ) x. ( A rmX M ) ) <-> ( A rmY M ) || ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmY N ) x. ( A rmX M ) ) ) ) )
29 3 21 25 27 28 syl112anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( ( A rmY N ) x. ( A rmX M ) ) <-> ( A rmY M ) || ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmY N ) x. ( A rmX M ) ) ) ) )
30 rmyadd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ M e. ZZ ) -> ( A rmY ( N + M ) ) = ( ( ( A rmY N ) x. ( A rmX M ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) )
31 30 3com23 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY ( N + M ) ) = ( ( ( A rmY N ) x. ( A rmX M ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) )
32 17 16 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmX M ) ) e. CC )
33 23 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmX N ) e. CC )
34 3 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A rmY M ) e. CC )
35 33 34 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY M ) ) e. CC )
36 32 35 addcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmY N ) x. ( A rmX M ) ) + ( ( A rmX N ) x. ( A rmY M ) ) ) = ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmY N ) x. ( A rmX M ) ) ) )
37 31 36 eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmY N ) x. ( A rmX M ) ) ) = ( A rmY ( N + M ) ) )
38 37 breq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( ( ( A rmX N ) x. ( A rmY M ) ) + ( ( A rmY N ) x. ( A rmX M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + M ) ) ) )
39 20 29 38 3bitrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + M ) ) ) )