Metamath Proof Explorer

Theorem lgseisen

Description: Eisenstein's lemma, an expression for ( P /L Q ) when P , Q are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
lgseisen.2 ⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
lgseisen.3 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion lgseisen ( 𝜑 → ( 𝑄 /L 𝑃 ) = ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 lgseisen.2 ⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
3 lgseisen.3 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
4 2 eldifad ⊢ ( 𝜑 → 𝑄 ∈ ℙ )
5 prmz ⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
6 4 5 syl ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
7 lgsval3 ⊢ ( ( 𝑄 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑄 /L 𝑃 ) = ( ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
8 6 1 7 syl2anc ⊢ ( 𝜑 → ( 𝑄 /L 𝑃 ) = ( ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
9 2 gausslemma2dlem0a ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
10 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
11 1 10 syl ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
12 11 nnnn0d ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
13 9 12 nnexpcld ⊢ ( 𝜑 → ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℕ )
14 13 nnred ⊢ ( 𝜑 → ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℝ )
15 neg1rr ⊢ - 1 ∈ ℝ
16 15 a1i ⊢ ( 𝜑 → - 1 ∈ ℝ )
17 neg1ne0 ⊢ - 1 ≠ 0
18 17 a1i ⊢ ( 𝜑 → - 1 ≠ 0 )
19 fzfid ⊢ ( 𝜑 → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin )
20 9 nnred ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
21 1 gausslemma2dlem0a ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
22 20 21 nndivred ⊢ ( 𝜑 → ( 𝑄 / 𝑃 ) ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑄 / 𝑃 ) ∈ ℝ )
24 2re ⊢ 2 ∈ ℝ
25 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℕ )
27 26 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑥 ∈ ℝ )
28 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 2 · 𝑥 ) ∈ ℝ )
29 24 27 28 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ℝ )
30 23 29 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ∈ ℝ )
31 30 flcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ )
32 19 31 fsumzcl ⊢ ( 𝜑 → Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ )
33 16 18 32 reexpclzd ⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∈ ℝ )
34 1re ⊢ 1 ∈ ℝ
35 34 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
36 21 nnrpd ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
37 eqid ⊢ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 )
38 eqid ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ) · ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ) mod 𝑃 ) / 2 ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ( ( - 1 ↑ ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ) · ( ( 𝑄 · ( 2 · 𝑥 ) ) mod 𝑃 ) ) mod 𝑃 ) / 2 ) )
39 eqid ⊢ ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 ) = ( ( 𝑄 · ( 2 · 𝑦 ) ) mod 𝑃 )
40 eqid ⊢ ( ℤ/nℤ ‘ 𝑃 ) = ( ℤ/nℤ ‘ 𝑃 )
41 eqid ⊢ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑃 ) )
42 eqid ⊢ ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑃 ) )
43 1 2 3 37 38 39 40 41 42 lgseisenlem4 ⊢ ( 𝜑 → ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) mod 𝑃 ) )
44 modadd1 ⊢ ( ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℝ ∧ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∈ ℝ ) ∧ ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) mod 𝑃 ) ) → ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) mod 𝑃 ) )
45 14 33 35 36 43 44 syl221anc ⊢ ( 𝜑 → ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) mod 𝑃 ) )
46 peano2re ⊢ ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∈ ℝ → ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) ∈ ℝ )
47 33 46 syl ⊢ ( 𝜑 → ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) ∈ ℝ )
48 df-neg ⊢ - 1 = ( 0 − 1 )
49 neg1cn ⊢ - 1 ∈ ℂ
50 absexpz ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ ) → ( abs ‘ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ) = ( ( abs ‘ - 1 ) ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
51 49 17 32 50 mp3an12i ⊢ ( 𝜑 → ( abs ‘ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ) = ( ( abs ‘ - 1 ) ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
52 ax-1cn ⊢ 1 ∈ ℂ
53 52 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
54 abs1 ⊢ ( abs ‘ 1 ) = 1
55 53 54 eqtri ⊢ ( abs ‘ - 1 ) = 1
56 55 oveq1i ⊢ ( ( abs ‘ - 1 ) ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) = ( 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) )
57 1exp ⊢ ( Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ∈ ℤ → ( 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) = 1 )
58 32 57 syl ⊢ ( 𝜑 → ( 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) = 1 )
59 56 58 syl5eq ⊢ ( 𝜑 → ( ( abs ‘ - 1 ) ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) = 1 )
60 51 59 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ) = 1 )
61 1le1 ⊢ 1 ≤ 1
62 60 61 eqbrtrdi ⊢ ( 𝜑 → ( abs ‘ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ) ≤ 1 )
63 absle ⊢ ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ) ≤ 1 ↔ ( - 1 ≤ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∧ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ≤ 1 ) ) )
64 33 34 63 sylancl ⊢ ( 𝜑 → ( ( abs ‘ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ) ≤ 1 ↔ ( - 1 ≤ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∧ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ≤ 1 ) ) )
65 62 64 mpbid ⊢ ( 𝜑 → ( - 1 ≤ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∧ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ≤ 1 ) )
66 65 simpld ⊢ ( 𝜑 → - 1 ≤ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
67 48 66 eqbrtrrid ⊢ ( 𝜑 → ( 0 − 1 ) ≤ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
68 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
69 68 35 33 lesubaddd ⊢ ( 𝜑 → ( ( 0 − 1 ) ≤ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ↔ 0 ≤ ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) ) )
70 67 69 mpbid ⊢ ( 𝜑 → 0 ≤ ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) )
71 21 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
72 peano2rem ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
73 71 72 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
74 65 simprd ⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ≤ 1 )
75 df-2 ⊢ 2 = ( 1 + 1 )
76 24 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
77 1 eldifad ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
78 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
79 eluzle ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑃 )
80 77 78 79 3syl ⊢ ( 𝜑 → 2 ≤ 𝑃 )
81 eldifsni ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
82 1 81 syl ⊢ ( 𝜑 → 𝑃 ≠ 2 )
83 76 71 80 82 leneltd ⊢ ( 𝜑 → 2 < 𝑃 )
84 75 83 eqbrtrrid ⊢ ( 𝜑 → ( 1 + 1 ) < 𝑃 )
85 35 35 71 ltaddsubd ⊢ ( 𝜑 → ( ( 1 + 1 ) < 𝑃 ↔ 1 < ( 𝑃 − 1 ) ) )
86 84 85 mpbid ⊢ ( 𝜑 → 1 < ( 𝑃 − 1 ) )
87 33 35 73 74 86 lelttrd ⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) < ( 𝑃 − 1 ) )
88 33 35 71 ltaddsubd ⊢ ( 𝜑 → ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) < 𝑃 ↔ ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) < ( 𝑃 − 1 ) ) )
89 87 88 mpbird ⊢ ( 𝜑 → ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) < 𝑃 )
90 modid ⊢ ( ( ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) ∧ ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) < 𝑃 ) ) → ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) mod 𝑃 ) = ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) )
91 47 36 70 89 90 syl22anc ⊢ ( 𝜑 → ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) mod 𝑃 ) = ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) )
92 45 91 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) )
93 92 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) − 1 ) )
94 33 recnd ⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∈ ℂ )
95 pncan ⊢ ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) − 1 ) = ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
96 94 52 95 sylancl ⊢ ( 𝜑 → ( ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) + 1 ) − 1 ) = ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
97 93 96 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )
98 8 97 eqtrd ⊢ ( 𝜑 → ( 𝑄 /L 𝑃 ) = ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) )