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 ⊢φ→¬2∥M
lgsquad2.3 ⊢φ→N∈ℕ
lgsquad2.4 ⊢φ→¬2∥N
lgsquad2.5 ⊢φ→MgcdN=1
Assertion lgsquad2 ⊢φ→M/LN⁢N/LM=−1M−12⁢N−12

Proof

Step Hyp Ref Expression
1 lgsquad2.1 ⊢φ→M∈ℕ
2 lgsquad2.2 ⊢φ→¬2∥M
3 lgsquad2.3 ⊢φ→N∈ℕ
4 lgsquad2.4 ⊢φ→¬2∥N
5 lgsquad2.5 ⊢φ→MgcdN=1
6 3 adantr ⊢φ∧m∈ℙ∖2∧mgcdN=1→N∈ℕ
7 4 adantr ⊢φ∧m∈ℙ∖2∧mgcdN=1→¬2∥N
8 simprl ⊢φ∧m∈ℙ∖2∧mgcdN=1→m∈ℙ∖2
9 eldifi ⊢m∈ℙ∖2→m∈ℙ
10 8 9 syl ⊢φ∧m∈ℙ∖2∧mgcdN=1→m∈ℙ
11 prmnn ⊢m∈ℙ→m∈ℕ
12 10 11 syl ⊢φ∧m∈ℙ∖2∧mgcdN=1→m∈ℕ
13 eldifsni ⊢m∈ℙ∖2→m≠2
14 8 13 syl ⊢φ∧m∈ℙ∖2∧mgcdN=1→m≠2
15 14 necomd ⊢φ∧m∈ℙ∖2∧mgcdN=1→2≠m
16 15 neneqd ⊢φ∧m∈ℙ∖2∧mgcdN=1→¬2=m
17 2z ⊢2∈ℤ
18 uzid ⊢2∈ℤ→2∈ℤ≥2
19 17 18 ax-mp ⊢2∈ℤ≥2
20 dvdsprm ⊢2∈ℤ≥2∧m∈ℙ→2∥m↔2=m
21 19 10 20 sylancr ⊢φ∧m∈ℙ∖2∧mgcdN=1→2∥m↔2=m
22 16 21 mtbird ⊢φ∧m∈ℙ∖2∧mgcdN=1→¬2∥m
23 6 nnzd ⊢φ∧m∈ℙ∖2∧mgcdN=1→N∈ℤ
24 12 nnzd ⊢φ∧m∈ℙ∖2∧mgcdN=1→m∈ℤ
25 23 24 gcdcomd ⊢φ∧m∈ℙ∖2∧mgcdN=1→Ngcdm=mgcdN
26 simprr ⊢φ∧m∈ℙ∖2∧mgcdN=1→mgcdN=1
27 25 26 eqtrd ⊢φ∧m∈ℙ∖2∧mgcdN=1→Ngcdm=1
28 simprl ⊢φ∧m∈ℙ∖2∧mgcdN=1∧n∈ℙ∖2∧ngcdm=1→n∈ℙ∖2
29 8 adantr ⊢φ∧m∈ℙ∖2∧mgcdN=1∧n∈ℙ∖2∧ngcdm=1→m∈ℙ∖2
30 eldifi ⊢n∈ℙ∖2→n∈ℙ
31 prmrp ⊢n∈ℙ∧m∈ℙ→ngcdm=1↔n≠m
32 30 10 31 syl2anr ⊢φ∧m∈ℙ∖2∧mgcdN=1∧n∈ℙ∖2→ngcdm=1↔n≠m
33 32 biimpd ⊢φ∧m∈ℙ∖2∧mgcdN=1∧n∈ℙ∖2→ngcdm=1→n≠m
34 33 impr ⊢φ∧m∈ℙ∖2∧mgcdN=1∧n∈ℙ∖2∧ngcdm=1→n≠m
35 lgsquad ⊢n∈ℙ∖2∧m∈ℙ∖2∧n≠m→n/Lm⁢m/Ln=−1n−12⁢m−12
36 28 29 34 35 syl3anc ⊢φ∧m∈ℙ∖2∧mgcdN=1∧n∈ℙ∖2∧ngcdm=1→n/Lm⁢m/Ln=−1n−12⁢m−12
37 biid ⊢∀x∈1…yxgcd2⁢m=1→x/Lm⁢m/Lx=−1x−12⁢m−12↔∀x∈1…yxgcd2⁢m=1→x/Lm⁢m/Lx=−1x−12⁢m−12
38 6 7 12 22 27 36 37 lgsquad2lem2 ⊢φ∧m∈ℙ∖2∧mgcdN=1→N/Lm⁢m/LN=−1N−12⁢m−12
39 lgscl ⊢m∈ℤ∧N∈ℤ→m/LN∈ℤ
40 24 23 39 syl2anc ⊢φ∧m∈ℙ∖2∧mgcdN=1→m/LN∈ℤ
41 lgscl ⊢N∈ℤ∧m∈ℤ→N/Lm∈ℤ
42 23 24 41 syl2anc ⊢φ∧m∈ℙ∖2∧mgcdN=1→N/Lm∈ℤ
43 zcn ⊢m/LN∈ℤ→m/LN∈ℂ
44 zcn ⊢N/Lm∈ℤ→N/Lm∈ℂ
45 mulcom ⊢m/LN∈ℂ∧N/Lm∈ℂ→m/LN⁢N/Lm=N/Lm⁢m/LN
46 43 44 45 syl2an ⊢m/LN∈ℤ∧N/Lm∈ℤ→m/LN⁢N/Lm=N/Lm⁢m/LN
47 40 42 46 syl2anc ⊢φ∧m∈ℙ∖2∧mgcdN=1→m/LN⁢N/Lm=N/Lm⁢m/LN
48 12 nncnd ⊢φ∧m∈ℙ∖2∧mgcdN=1→m∈ℂ
49 ax-1cn ⊢1∈ℂ
50 subcl ⊢m∈ℂ∧1∈ℂ→m−1∈ℂ
51 48 49 50 sylancl ⊢φ∧m∈ℙ∖2∧mgcdN=1→m−1∈ℂ
52 51 halfcld ⊢φ∧m∈ℙ∖2∧mgcdN=1→m−12∈ℂ
53 6 nncnd ⊢φ∧m∈ℙ∖2∧mgcdN=1→N∈ℂ
54 subcl ⊢N∈ℂ∧1∈ℂ→N−1∈ℂ
55 53 49 54 sylancl ⊢φ∧m∈ℙ∖2∧mgcdN=1→N−1∈ℂ
56 55 halfcld ⊢φ∧m∈ℙ∖2∧mgcdN=1→N−12∈ℂ
57 52 56 mulcomd ⊢φ∧m∈ℙ∖2∧mgcdN=1→m−12⁢N−12=N−12⁢m−12
58 57 oveq2d ⊢φ∧m∈ℙ∖2∧mgcdN=1→−1m−12⁢N−12=−1N−12⁢m−12
59 38 47 58 3eqtr4d ⊢φ∧m∈ℙ∖2∧mgcdN=1→m/LN⁢N/Lm=−1m−12⁢N−12
60 biid ⊢∀x∈1…yxgcd2⋅ N=1→x/LN⁢N/Lx=−1x−12⁢N−12↔∀x∈1…yxgcd2⋅ N=1→x/LN⁢N/Lx=−1x−12⁢N−12
61 1 2 3 4 5 59 60 lgsquad2lem2 ⊢φ→M/LN⁢N/LM=−1M−12⁢N−12