Metamath Proof Explorer

Theorem jm2.19lem1

Description: Lemma for jm2.19 . X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion jm2.19lem1 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmX M ) gcd ( A rmY M ) ) = 1 )

Proof

Step Hyp Ref Expression
1 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
2 1 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmX M ) e. NN0 )
3 2 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmX M ) e. CC )
4 3 sqcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmX M ) ^ 2 ) e. CC )
5 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
6 5 eldifad 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
7 6 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. NN )
8 7 nncnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. CC )
9 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
10 9 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. ZZ )
11 10 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. CC )
12 11 sqcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmY M ) ^ 2 ) e. CC )
13 8 12 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) e. CC )
14 4 13 negsubd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( ( A rmX M ) ^ 2 ) + -u ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) ) = ( ( ( A rmX M ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) ) )
15 3 sqvald 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmX M ) ^ 2 ) = ( ( A rmX M ) x. ( A rmX M ) ) )
16 11 sqvald 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmY M ) ^ 2 ) = ( ( A rmY M ) x. ( A rmY M ) ) )
17 16 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( -u ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) = ( -u ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY M ) ) ) )
18 8 12 mulneg1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( -u ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) = -u ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) )
19 nnnegz 
 |-  ( ( ( A ^ 2 ) - 1 ) e. NN -> -u ( ( A ^ 2 ) - 1 ) e. ZZ )
20 7 19 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> -u ( ( A ^ 2 ) - 1 ) e. ZZ )
21 20 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> -u ( ( A ^ 2 ) - 1 ) e. CC )
22 21 11 11 mul12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( -u ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) x. ( A rmY M ) ) ) = ( ( A rmY M ) x. ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) ) )
23 17 18 22 3eqtr3d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> -u ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) = ( ( A rmY M ) x. ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) ) )
24 15 23 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( ( A rmX M ) ^ 2 ) + -u ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) ) = ( ( ( A rmX M ) x. ( A rmX M ) ) + ( ( A rmY M ) x. ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) ) ) )
25 rmxynorm 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( ( A rmX M ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY M ) ^ 2 ) ) ) = 1 )
26 14 24 25 3eqtr3d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( ( A rmX M ) x. ( A rmX M ) ) + ( ( A rmY M ) x. ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) ) ) = 1 )
27 2 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmX M ) e. ZZ )
28 20 10 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) e. ZZ )
29 bezoutr1 
 |-  ( ( ( ( A rmX M ) e. ZZ /\ ( A rmY M ) e. ZZ ) /\ ( ( A rmX M ) e. ZZ /\ ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) e. ZZ ) ) -> ( ( ( ( A rmX M ) x. ( A rmX M ) ) + ( ( A rmY M ) x. ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) ) ) = 1 -> ( ( A rmX M ) gcd ( A rmY M ) ) = 1 ) )
30 27 10 27 28 29 syl22anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( ( ( A rmX M ) x. ( A rmX M ) ) + ( ( A rmY M ) x. ( -u ( ( A ^ 2 ) - 1 ) x. ( A rmY M ) ) ) ) = 1 -> ( ( A rmX M ) gcd ( A rmY M ) ) = 1 ) )
31 26 30 mpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A rmX M ) gcd ( A rmY M ) ) = 1 )