Metamath Proof Explorer

Theorem lgsquad3

Description: Extend lgsquad2 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion lgsquad3 
|- ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) -> ( M /L N ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )

Proof

Step Hyp Ref Expression
1 simplrl 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> N e. NN )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 1 2 syl 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> N e. ZZ )
4 nnz 
 |-  ( M e. NN -> M e. ZZ )
5 4 ad3antrrr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> M e. ZZ )
6 lgscl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N /L M ) e. ZZ )
7 3 5 6 syl2anc 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( N /L M ) e. ZZ )
8 7 zred 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( N /L M ) e. RR )
9 absresq 
 |-  ( ( N /L M ) e. RR -> ( ( abs ` ( N /L M ) ) ^ 2 ) = ( ( N /L M ) ^ 2 ) )
10 8 9 syl 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( abs ` ( N /L M ) ) ^ 2 ) = ( ( N /L M ) ^ 2 ) )
11 3 5 gcdcomd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( N gcd M ) = ( M gcd N ) )
12 simpr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( M gcd N ) = 1 )
13 11 12 eqtrd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( N gcd M ) = 1 )
14 lgsabs1 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( abs ` ( N /L M ) ) = 1 <-> ( N gcd M ) = 1 ) )
15 3 5 14 syl2anc 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( abs ` ( N /L M ) ) = 1 <-> ( N gcd M ) = 1 ) )
16 13 15 mpbird 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( abs ` ( N /L M ) ) = 1 )
17 16 oveq1d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( abs ` ( N /L M ) ) ^ 2 ) = ( 1 ^ 2 ) )
18 sq1 
 |-  ( 1 ^ 2 ) = 1
19 17 18 eqtrdi 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( abs ` ( N /L M ) ) ^ 2 ) = 1 )
20 7 zcnd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( N /L M ) e. CC )
21 20 sqvald 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( N /L M ) ^ 2 ) = ( ( N /L M ) x. ( N /L M ) ) )
22 10 19 21 3eqtr3d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> 1 = ( ( N /L M ) x. ( N /L M ) ) )
23 22 oveq2d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( M /L N ) x. 1 ) = ( ( M /L N ) x. ( ( N /L M ) x. ( N /L M ) ) ) )
24 lgscl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M /L N ) e. ZZ )
25 5 3 24 syl2anc 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( M /L N ) e. ZZ )
26 25 zcnd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( M /L N ) e. CC )
27 26 20 20 mulassd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( ( M /L N ) x. ( N /L M ) ) x. ( N /L M ) ) = ( ( M /L N ) x. ( ( N /L M ) x. ( N /L M ) ) ) )
28 23 27 eqtr4d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( M /L N ) x. 1 ) = ( ( ( M /L N ) x. ( N /L M ) ) x. ( N /L M ) ) )
29 26 mulridd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( M /L N ) x. 1 ) = ( M /L N ) )
30 simplll 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> M e. NN )
31 simpllr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> -. 2 || M )
32 simplrr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> -. 2 || N )
33 30 31 1 32 12 lgsquad2 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
34 33 oveq1d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( ( ( M /L N ) x. ( N /L M ) ) x. ( N /L M ) ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )
35 28 29 34 3eqtr3d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ ( M gcd N ) = 1 ) -> ( M /L N ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )
36 neg1cn 
 |-  -u 1 e. CC
37 36 a1i 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> -u 1 e. CC )
38 neg1ne0 
 |-  -u 1 =/= 0
39 38 a1i 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> -u 1 =/= 0 )
40 4 ad3antrrr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> M e. ZZ )
41 simpllr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> -. 2 || M )
42 1zzd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> 1 e. ZZ )
43 2prm 
 |-  2 e. Prime
44 nprmdvds1 
 |-  ( 2 e. Prime -> -. 2 || 1 )
45 43 44 mp1i 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> -. 2 || 1 )
46 omoe 
 |-  ( ( ( M e. ZZ /\ -. 2 || M ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( M - 1 ) )
47 40 41 42 45 46 syl22anc 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> 2 || ( M - 1 ) )
48 2z 
 |-  2 e. ZZ
49 2ne0 
 |-  2 =/= 0
50 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
51 40 50 syl 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( M - 1 ) e. ZZ )
52 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( M - 1 ) e. ZZ ) -> ( 2 || ( M - 1 ) <-> ( ( M - 1 ) / 2 ) e. ZZ ) )
53 48 49 51 52 mp3an12i 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( 2 || ( M - 1 ) <-> ( ( M - 1 ) / 2 ) e. ZZ ) )
54 47 53 mpbid 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( ( M - 1 ) / 2 ) e. ZZ )
55 2 adantr 
 |-  ( ( N e. NN /\ -. 2 || N ) -> N e. ZZ )
56 55 ad2antlr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> N e. ZZ )
57 simplrr 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> -. 2 || N )
58 omoe 
 |-  ( ( ( N e. ZZ /\ -. 2 || N ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( N - 1 ) )
59 56 57 42 45 58 syl22anc 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> 2 || ( N - 1 ) )
60 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
61 56 60 syl 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( N - 1 ) e. ZZ )
62 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( N - 1 ) e. ZZ ) -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
63 48 49 61 62 mp3an12i 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
64 59 63 mpbid 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( ( N - 1 ) / 2 ) e. ZZ )
65 54 64 zmulcld 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) e. ZZ )
66 37 39 65 expclzd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) e. CC )
67 66 mul01d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. 0 ) = 0 )
68 lgsne0 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N /L M ) =/= 0 <-> ( N gcd M ) = 1 ) )
69 gcdcom 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N gcd M ) = ( M gcd N ) )
70 69 eqeq1d 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N gcd M ) = 1 <-> ( M gcd N ) = 1 ) )
71 68 70 bitrd 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N /L M ) =/= 0 <-> ( M gcd N ) = 1 ) )
72 2 4 71 syl2anr 
 |-  ( ( M e. NN /\ N e. NN ) -> ( ( N /L M ) =/= 0 <-> ( M gcd N ) = 1 ) )
73 72 necon1bbid 
 |-  ( ( M e. NN /\ N e. NN ) -> ( -. ( M gcd N ) = 1 <-> ( N /L M ) = 0 ) )
74 73 ad2ant2r 
 |-  ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) -> ( -. ( M gcd N ) = 1 <-> ( N /L M ) = 0 ) )
75 74 biimpa 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( N /L M ) = 0 )
76 75 oveq2d 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. 0 ) )
77 lgsne0 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M /L N ) =/= 0 <-> ( M gcd N ) = 1 ) )
78 77 necon1bbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M gcd N ) = 1 <-> ( M /L N ) = 0 ) )
79 4 2 78 syl2an 
 |-  ( ( M e. NN /\ N e. NN ) -> ( -. ( M gcd N ) = 1 <-> ( M /L N ) = 0 ) )
80 79 ad2ant2r 
 |-  ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) -> ( -. ( M gcd N ) = 1 <-> ( M /L N ) = 0 ) )
81 80 biimpa 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( M /L N ) = 0 )
82 67 76 81 3eqtr4rd 
 |-  ( ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) /\ -. ( M gcd N ) = 1 ) -> ( M /L N ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )
83 35 82 pm2.61dan 
 |-  ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) -> ( M /L N ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )