Metamath Proof Explorer

Theorem lgsquad2

Description: Extend lgsquad to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses lgsquad2.1 
|- ( ph -> M e. NN )
lgsquad2.2 
|- ( ph -> -. 2 || M )
lgsquad2.3 
|- ( ph -> N e. NN )
lgsquad2.4 
|- ( ph -> -. 2 || N )
lgsquad2.5 
|- ( ph -> ( M gcd N ) = 1 )
Assertion lgsquad2 
|- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsquad2.1 
 |-  ( ph -> M e. NN )
2 lgsquad2.2 
 |-  ( ph -> -. 2 || M )
3 lgsquad2.3 
 |-  ( ph -> N e. NN )
4 lgsquad2.4 
 |-  ( ph -> -. 2 || N )
5 lgsquad2.5 
 |-  ( ph -> ( M gcd N ) = 1 )
6 3 adantr 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> N e. NN )
7 4 adantr 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> -. 2 || N )
8 simprl 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> m e. ( Prime \ { 2 } ) )
9 eldifi 
 |-  ( m e. ( Prime \ { 2 } ) -> m e. Prime )
10 8 9 syl 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> m e. Prime )
11 prmnn 
 |-  ( m e. Prime -> m e. NN )
12 10 11 syl 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> m e. NN )
13 eldifsni 
 |-  ( m e. ( Prime \ { 2 } ) -> m =/= 2 )
14 8 13 syl 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> m =/= 2 )
15 14 necomd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> 2 =/= m )
16 15 neneqd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> -. 2 = m )
17 2z 
 |-  2 e. ZZ
18 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
19 17 18 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
20 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ m e. Prime ) -> ( 2 || m <-> 2 = m ) )
21 19 10 20 sylancr 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( 2 || m <-> 2 = m ) )
22 16 21 mtbird 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> -. 2 || m )
23 6 nnzd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> N e. ZZ )
24 12 nnzd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> m e. ZZ )
25 23 24 gcdcomd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( N gcd m ) = ( m gcd N ) )
26 simprr 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( m gcd N ) = 1 )
27 25 26 eqtrd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( N gcd m ) = 1 )
28 simprl 
 |-  ( ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) /\ ( n e. ( Prime \ { 2 } ) /\ ( n gcd m ) = 1 ) ) -> n e. ( Prime \ { 2 } ) )
29 8 adantr 
 |-  ( ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) /\ ( n e. ( Prime \ { 2 } ) /\ ( n gcd m ) = 1 ) ) -> m e. ( Prime \ { 2 } ) )
30 eldifi 
 |-  ( n e. ( Prime \ { 2 } ) -> n e. Prime )
31 prmrp 
 |-  ( ( n e. Prime /\ m e. Prime ) -> ( ( n gcd m ) = 1 <-> n =/= m ) )
32 30 10 31 syl2anr 
 |-  ( ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) /\ n e. ( Prime \ { 2 } ) ) -> ( ( n gcd m ) = 1 <-> n =/= m ) )
33 32 biimpd 
 |-  ( ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) /\ n e. ( Prime \ { 2 } ) ) -> ( ( n gcd m ) = 1 -> n =/= m ) )
34 33 impr 
 |-  ( ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) /\ ( n e. ( Prime \ { 2 } ) /\ ( n gcd m ) = 1 ) ) -> n =/= m )
35 lgsquad 
 |-  ( ( n e. ( Prime \ { 2 } ) /\ m e. ( Prime \ { 2 } ) /\ n =/= m ) -> ( ( n /L m ) x. ( m /L n ) ) = ( -u 1 ^ ( ( ( n - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) ) )
36 28 29 34 35 syl3anc 
 |-  ( ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) /\ ( n e. ( Prime \ { 2 } ) /\ ( n gcd m ) = 1 ) ) -> ( ( n /L m ) x. ( m /L n ) ) = ( -u 1 ^ ( ( ( n - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) ) )
37 biid 
 |-  ( A. x e. ( 1 ... y ) ( ( x gcd ( 2 x. m ) ) = 1 -> ( ( x /L m ) x. ( m /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) ) ) <-> A. x e. ( 1 ... y ) ( ( x gcd ( 2 x. m ) ) = 1 -> ( ( x /L m ) x. ( m /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) ) ) )
38 6 7 12 22 27 36 37 lgsquad2lem2 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( N /L m ) x. ( m /L N ) ) = ( -u 1 ^ ( ( ( N - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) ) )
39 lgscl 
 |-  ( ( m e. ZZ /\ N e. ZZ ) -> ( m /L N ) e. ZZ )
40 24 23 39 syl2anc 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( m /L N ) e. ZZ )
41 lgscl 
 |-  ( ( N e. ZZ /\ m e. ZZ ) -> ( N /L m ) e. ZZ )
42 23 24 41 syl2anc 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( N /L m ) e. ZZ )
43 zcn 
 |-  ( ( m /L N ) e. ZZ -> ( m /L N ) e. CC )
44 zcn 
 |-  ( ( N /L m ) e. ZZ -> ( N /L m ) e. CC )
45 mulcom 
 |-  ( ( ( m /L N ) e. CC /\ ( N /L m ) e. CC ) -> ( ( m /L N ) x. ( N /L m ) ) = ( ( N /L m ) x. ( m /L N ) ) )
46 43 44 45 syl2an 
 |-  ( ( ( m /L N ) e. ZZ /\ ( N /L m ) e. ZZ ) -> ( ( m /L N ) x. ( N /L m ) ) = ( ( N /L m ) x. ( m /L N ) ) )
47 40 42 46 syl2anc 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( ( N /L m ) x. ( m /L N ) ) )
48 12 nncnd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> m e. CC )
49 ax-1cn 
 |-  1 e. CC
50 subcl 
 |-  ( ( m e. CC /\ 1 e. CC ) -> ( m - 1 ) e. CC )
51 48 49 50 sylancl 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( m - 1 ) e. CC )
52 51 halfcld 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m - 1 ) / 2 ) e. CC )
53 6 nncnd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> N e. CC )
54 subcl 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N - 1 ) e. CC )
55 53 49 54 sylancl 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( N - 1 ) e. CC )
56 55 halfcld 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( N - 1 ) / 2 ) e. CC )
57 52 56 mulcomd 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( N - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) )
58 57 oveq2d 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( N - 1 ) / 2 ) x. ( ( m - 1 ) / 2 ) ) ) )
59 38 47 58 3eqtr4d 
 |-  ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
60 biid 
 |-  ( A. x e. ( 1 ... y ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> A. x e. ( 1 ... y ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
61 1 2 3 4 5 59 60 lgsquad2lem2 
 |-  ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )