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 ⊢ φ → M gcd N = 1
Assertion lgsquad2 ⊢ φ → M / L N ⁢ N / L M = − 1 M − 1 2 ⁢ N − 1 2

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 ⊢ φ → M gcd N = 1
6 3 adantr ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N ∈ ℕ
7 4 adantr ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → ¬ 2 ∥ N
8 simprl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m ∈ ℙ ∖ 2
9 eldifi ⊢ m ∈ ℙ ∖ 2 → m ∈ ℙ
10 8 9 syl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m ∈ ℙ
11 prmnn ⊢ m ∈ ℙ → m ∈ ℕ
12 10 11 syl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m ∈ ℕ
13 eldifsni ⊢ m ∈ ℙ ∖ 2 → m ≠ 2
14 8 13 syl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m ≠ 2
15 14 necomd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → 2 ≠ m
16 15 neneqd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 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 ∧ m gcd N = 1 → 2 ∥ m ↔ 2 = m
22 16 21 mtbird ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → ¬ 2 ∥ m
23 6 nnzd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N ∈ ℤ
24 12 nnzd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m ∈ ℤ
25 23 24 gcdcomd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N gcd m = m gcd N
26 simprr ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m gcd N = 1
27 25 26 eqtrd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N gcd m = 1
28 simprl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 ∧ n ∈ ℙ ∖ 2 ∧ n gcd m = 1 → n ∈ ℙ ∖ 2
29 8 adantr ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 ∧ n ∈ ℙ ∖ 2 ∧ n gcd m = 1 → m ∈ ℙ ∖ 2
30 eldifi ⊢ n ∈ ℙ ∖ 2 → n ∈ ℙ
31 prmrp ⊢ n ∈ ℙ ∧ m ∈ ℙ → n gcd m = 1 ↔ n ≠ m
32 30 10 31 syl2anr ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 ∧ n ∈ ℙ ∖ 2 → n gcd m = 1 ↔ n ≠ m
33 32 biimpd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 ∧ n ∈ ℙ ∖ 2 → n gcd m = 1 → n ≠ m
34 33 impr ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 ∧ n ∈ ℙ ∖ 2 ∧ n gcd m = 1 → n ≠ m
35 lgsquad ⊢ n ∈ ℙ ∖ 2 ∧ m ∈ ℙ ∖ 2 ∧ n ≠ m → n / L m ⁢ m / L n = − 1 n − 1 2 ⁢ m − 1 2
36 28 29 34 35 syl3anc ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 ∧ n ∈ ℙ ∖ 2 ∧ n gcd m = 1 → n / L m ⁢ m / L n = − 1 n − 1 2 ⁢ m − 1 2
37 biid ⊢ ∀ x ∈ 1 … y x gcd 2 ⁢ m = 1 → x / L m ⁢ m / L x = − 1 x − 1 2 ⁢ m − 1 2 ↔ ∀ x ∈ 1 … y x gcd 2 ⁢ m = 1 → x / L m ⁢ m / L x = − 1 x − 1 2 ⁢ m − 1 2
38 6 7 12 22 27 36 37 lgsquad2lem2 ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N / L m ⁢ m / L N = − 1 N − 1 2 ⁢ m − 1 2
39 lgscl ⊢ m ∈ ℤ ∧ N ∈ ℤ → m / L N ∈ ℤ
40 24 23 39 syl2anc ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m / L N ∈ ℤ
41 lgscl ⊢ N ∈ ℤ ∧ m ∈ ℤ → N / L m ∈ ℤ
42 23 24 41 syl2anc ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N / L m ∈ ℤ
43 zcn ⊢ m / L N ∈ ℤ → m / L N ∈ ℂ
44 zcn ⊢ N / L m ∈ ℤ → N / L m ∈ ℂ
45 mulcom ⊢ m / L N ∈ ℂ ∧ N / L m ∈ ℂ → m / L N ⁢ N / L m = N / L m ⁢ m / L N
46 43 44 45 syl2an ⊢ m / L N ∈ ℤ ∧ N / L m ∈ ℤ → m / L N ⁢ N / L m = N / L m ⁢ m / L N
47 40 42 46 syl2anc ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m / L N ⁢ N / L m = N / L m ⁢ m / L N
48 12 nncnd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m ∈ ℂ
49 ax-1cn ⊢ 1 ∈ ℂ
50 subcl ⊢ m ∈ ℂ ∧ 1 ∈ ℂ → m − 1 ∈ ℂ
51 48 49 50 sylancl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m − 1 ∈ ℂ
52 51 halfcld ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m − 1 2 ∈ ℂ
53 6 nncnd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N ∈ ℂ
54 subcl ⊢ N ∈ ℂ ∧ 1 ∈ ℂ → N − 1 ∈ ℂ
55 53 49 54 sylancl ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N − 1 ∈ ℂ
56 55 halfcld ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → N − 1 2 ∈ ℂ
57 52 56 mulcomd ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m − 1 2 ⁢ N − 1 2 = N − 1 2 ⁢ m − 1 2
58 57 oveq2d ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → − 1 m − 1 2 ⁢ N − 1 2 = − 1 N − 1 2 ⁢ m − 1 2
59 38 47 58 3eqtr4d ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m / L N ⁢ N / L m = − 1 m − 1 2 ⁢ N − 1 2
60 biid ⊢ ∀ x ∈ 1 … y x gcd 2 ⋅ N = 1 → x / L N ⁢ N / L x = − 1 x − 1 2 ⁢ N − 1 2 ↔ ∀ x ∈ 1 … y x gcd 2 ⋅ N = 1 → x / L N ⁢ N / L x = − 1 x − 1 2 ⁢ N − 1 2
61 1 2 3 4 5 59 60 lgsquad2lem2 ⊢ φ → M / L N ⁢ N / L M = − 1 M − 1 2 ⁢ N − 1 2