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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lgsquad2.2 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑀 )
lgsquad2.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lgsquad2.4 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
lgsquad2.5 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
Assertion lgsquad2 ( 𝜑 → ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) = ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsquad2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 lgsquad2.2 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑀 )
3 lgsquad2.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 lgsquad2.4 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
5 lgsquad2.5 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
6 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑁 ∈ ℕ )
7 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ¬ 2 ∥ 𝑁 )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑚 ∈ ( ℙ ∖ { 2 } ) )
9 eldifi ⊢ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) → 𝑚 ∈ ℙ )
10 8 9 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑚 ∈ ℙ )
11 prmnn ⊢ ( 𝑚 ∈ ℙ → 𝑚 ∈ ℕ )
12 10 11 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑚 ∈ ℕ )
13 eldifsni ⊢ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) → 𝑚 ≠ 2 )
14 8 13 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑚 ≠ 2 )
15 14 necomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 2 ≠ 𝑚 )
16 15 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ¬ 2 = 𝑚 )
17 2z ⊢ 2 ∈ ℤ
18 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
19 17 18 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
20 dvdsprm ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 ∈ ℙ ) → ( 2 ∥ 𝑚 ↔ 2 = 𝑚 ) )
21 19 10 20 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 2 ∥ 𝑚 ↔ 2 = 𝑚 ) )
22 16 21 mtbird ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ¬ 2 ∥ 𝑚 )
23 6 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑁 ∈ ℤ )
24 12 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑚 ∈ ℤ )
25 23 24 gcdcomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑁 gcd 𝑚 ) = ( 𝑚 gcd 𝑁 ) )
26 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑚 gcd 𝑁 ) = 1 )
27 25 26 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑁 gcd 𝑚 ) = 1 )
28 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑛 gcd 𝑚 ) = 1 ) ) → 𝑛 ∈ ( ℙ ∖ { 2 } ) )
29 8 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑛 gcd 𝑚 ) = 1 ) ) → 𝑚 ∈ ( ℙ ∖ { 2 } ) )
30 eldifi ⊢ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) → 𝑛 ∈ ℙ )
31 prmrp ⊢ ( ( 𝑛 ∈ ℙ ∧ 𝑚 ∈ ℙ ) → ( ( 𝑛 gcd 𝑚 ) = 1 ↔ 𝑛 ≠ 𝑚 ) )
32 30 10 31 syl2anr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) ∧ 𝑛 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑛 gcd 𝑚 ) = 1 ↔ 𝑛 ≠ 𝑚 ) )
33 32 biimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) ∧ 𝑛 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑛 gcd 𝑚 ) = 1 → 𝑛 ≠ 𝑚 ) )
34 33 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑛 gcd 𝑚 ) = 1 ) ) → 𝑛 ≠ 𝑚 )
35 lgsquad ⊢ ( ( 𝑛 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑛 ≠ 𝑚 ) → ( ( 𝑛 /L 𝑚 ) · ( 𝑚 /L 𝑛 ) ) = ( - 1 ↑ ( ( ( 𝑛 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) ) )
36 28 29 34 35 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑛 gcd 𝑚 ) = 1 ) ) → ( ( 𝑛 /L 𝑚 ) · ( 𝑚 /L 𝑛 ) ) = ( - 1 ↑ ( ( ( 𝑛 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) ) )
37 biid ⊢ ( ∀ 𝑥 ∈ ( 1 ... 𝑦 ) ( ( 𝑥 gcd ( 2 · 𝑚 ) ) = 1 → ( ( 𝑥 /L 𝑚 ) · ( 𝑚 /L 𝑥 ) ) = ( - 1 ↑ ( ( ( 𝑥 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝑦 ) ( ( 𝑥 gcd ( 2 · 𝑚 ) ) = 1 → ( ( 𝑥 /L 𝑚 ) · ( 𝑚 /L 𝑥 ) ) = ( - 1 ↑ ( ( ( 𝑥 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) ) ) )
38 6 7 12 22 27 36 37 lgsquad2lem2 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( 𝑁 /L 𝑚 ) · ( 𝑚 /L 𝑁 ) ) = ( - 1 ↑ ( ( ( 𝑁 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) ) )
39 lgscl ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑚 /L 𝑁 ) ∈ ℤ )
40 24 23 39 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑚 /L 𝑁 ) ∈ ℤ )
41 lgscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑁 /L 𝑚 ) ∈ ℤ )
42 23 24 41 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑁 /L 𝑚 ) ∈ ℤ )
43 zcn ⊢ ( ( 𝑚 /L 𝑁 ) ∈ ℤ → ( 𝑚 /L 𝑁 ) ∈ ℂ )
44 zcn ⊢ ( ( 𝑁 /L 𝑚 ) ∈ ℤ → ( 𝑁 /L 𝑚 ) ∈ ℂ )
45 mulcom ⊢ ( ( ( 𝑚 /L 𝑁 ) ∈ ℂ ∧ ( 𝑁 /L 𝑚 ) ∈ ℂ ) → ( ( 𝑚 /L 𝑁 ) · ( 𝑁 /L 𝑚 ) ) = ( ( 𝑁 /L 𝑚 ) · ( 𝑚 /L 𝑁 ) ) )
46 43 44 45 syl2an ⊢ ( ( ( 𝑚 /L 𝑁 ) ∈ ℤ ∧ ( 𝑁 /L 𝑚 ) ∈ ℤ ) → ( ( 𝑚 /L 𝑁 ) · ( 𝑁 /L 𝑚 ) ) = ( ( 𝑁 /L 𝑚 ) · ( 𝑚 /L 𝑁 ) ) )
47 40 42 46 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( 𝑚 /L 𝑁 ) · ( 𝑁 /L 𝑚 ) ) = ( ( 𝑁 /L 𝑚 ) · ( 𝑚 /L 𝑁 ) ) )
48 12 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑚 ∈ ℂ )
49 ax-1cn ⊢ 1 ∈ ℂ
50 subcl ⊢ ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑚 − 1 ) ∈ ℂ )
51 48 49 50 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑚 − 1 ) ∈ ℂ )
52 51 halfcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( 𝑚 − 1 ) / 2 ) ∈ ℂ )
53 6 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → 𝑁 ∈ ℂ )
54 subcl ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℂ )
55 53 49 54 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( 𝑁 − 1 ) ∈ ℂ )
56 55 halfcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℂ )
57 52 56 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝑚 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) = ( ( ( 𝑁 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) )
58 57 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( - 1 ↑ ( ( ( 𝑚 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = ( - 1 ↑ ( ( ( 𝑁 − 1 ) / 2 ) · ( ( 𝑚 − 1 ) / 2 ) ) ) )
59 38 47 58 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑚 gcd 𝑁 ) = 1 ) ) → ( ( 𝑚 /L 𝑁 ) · ( 𝑁 /L 𝑚 ) ) = ( - 1 ↑ ( ( ( 𝑚 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
60 biid ⊢ ( ∀ 𝑥 ∈ ( 1 ... 𝑦 ) ( ( 𝑥 gcd ( 2 · 𝑁 ) ) = 1 → ( ( 𝑥 /L 𝑁 ) · ( 𝑁 /L 𝑥 ) ) = ( - 1 ↑ ( ( ( 𝑥 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝑦 ) ( ( 𝑥 gcd ( 2 · 𝑁 ) ) = 1 → ( ( 𝑥 /L 𝑁 ) · ( 𝑁 /L 𝑥 ) ) = ( - 1 ↑ ( ( ( 𝑥 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
61 1 2 3 4 5 59 60 lgsquad2lem2 ⊢ ( 𝜑 → ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) = ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )