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 φM
lgsquad2.2 φ¬2M
lgsquad2.3 φN
lgsquad2.4 φ¬2N
lgsquad2.5 φMgcdN=1
Assertion lgsquad2 φM/LNN/LM=1M12N12

Proof

Step Hyp Ref Expression
1 lgsquad2.1 φM
2 lgsquad2.2 φ¬2M
3 lgsquad2.3 φN
4 lgsquad2.4 φ¬2N
5 lgsquad2.5 φMgcdN=1
6 3 adantr φm2mgcdN=1N
7 4 adantr φm2mgcdN=1¬2N
8 simprl φm2mgcdN=1m2
9 eldifi m2m
10 8 9 syl φm2mgcdN=1m
11 prmnn mm
12 10 11 syl φm2mgcdN=1m
13 eldifsni m2m2
14 8 13 syl φm2mgcdN=1m2
15 14 necomd φm2mgcdN=12m
16 15 neneqd φm2mgcdN=1¬2=m
17 2z 2
18 uzid 222
19 17 18 ax-mp 22
20 dvdsprm 22m2m2=m
21 19 10 20 sylancr φm2mgcdN=12m2=m
22 16 21 mtbird φm2mgcdN=1¬2m
23 6 nnzd φm2mgcdN=1N
24 12 nnzd φm2mgcdN=1m
25 23 24 gcdcomd φm2mgcdN=1Ngcdm=mgcdN
26 simprr φm2mgcdN=1mgcdN=1
27 25 26 eqtrd φm2mgcdN=1Ngcdm=1
28 simprl φm2mgcdN=1n2ngcdm=1n2
29 8 adantr φm2mgcdN=1n2ngcdm=1m2
30 eldifi n2n
31 prmrp nmngcdm=1nm
32 30 10 31 syl2anr φm2mgcdN=1n2ngcdm=1nm
33 32 biimpd φm2mgcdN=1n2ngcdm=1nm
34 33 impr φm2mgcdN=1n2ngcdm=1nm
35 lgsquad n2m2nmn/Lmm/Ln=1n12m12
36 28 29 34 35 syl3anc φm2mgcdN=1n2ngcdm=1n/Lmm/Ln=1n12m12
37 biid x1yxgcd2m=1x/Lmm/Lx=1x12m12x1yxgcd2m=1x/Lmm/Lx=1x12m12
38 6 7 12 22 27 36 37 lgsquad2lem2 φm2mgcdN=1N/Lmm/LN=1N12m12
39 lgscl mNm/LN
40 24 23 39 syl2anc φm2mgcdN=1m/LN
41 lgscl NmN/Lm
42 23 24 41 syl2anc φm2mgcdN=1N/Lm
43 zcn m/LNm/LN
44 zcn N/LmN/Lm
45 mulcom m/LNN/Lmm/LNN/Lm=N/Lmm/LN
46 43 44 45 syl2an m/LNN/Lmm/LNN/Lm=N/Lmm/LN
47 40 42 46 syl2anc φm2mgcdN=1m/LNN/Lm=N/Lmm/LN
48 12 nncnd φm2mgcdN=1m
49 ax-1cn 1
50 subcl m1m1
51 48 49 50 sylancl φm2mgcdN=1m1
52 51 halfcld φm2mgcdN=1m12
53 6 nncnd φm2mgcdN=1N
54 subcl N1N1
55 53 49 54 sylancl φm2mgcdN=1N1
56 55 halfcld φm2mgcdN=1N12
57 52 56 mulcomd φm2mgcdN=1m12N12=N12m12
58 57 oveq2d φm2mgcdN=11m12N12=1N12m12
59 38 47 58 3eqtr4d φm2mgcdN=1m/LNN/Lm=1m12N12
60 biid x1yxgcd2 N=1x/LNN/Lx=1x12N12x1yxgcd2 N=1x/LNN/Lx=1x12N12
61 1 2 3 4 5 59 60 lgsquad2lem2 φM/LNN/LM=1M12N12