Metamath Proof Explorer

Theorem gausslemma2dlem0i

Description: Auxiliary lemma 9 for gausslemma2d . (Contributed by AV, 14-Jul-2021)

Ref Expression
Hypotheses gausslemma2dlem0.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2dlem0.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
gausslemma2dlem0.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2dlem0.n ⊢ 𝑁 = ( 𝐻 − 𝑀 )
Assertion gausslemma2dlem0i ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2dlem0.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
3 gausslemma2dlem0.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
4 gausslemma2dlem0.n ⊢ 𝑁 = ( 𝐻 − 𝑀 )
5 2z ⊢ 2 ∈ ℤ
6 id ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
7 6 gausslemma2dlem0a ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℕ )
8 7 nnzd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℤ )
9 1 8 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
10 lgscl1 ⊢ ( ( 2 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 2 /L 𝑃 ) ∈ { - 1 , 0 , 1 } )
11 5 9 10 sylancr ⊢ ( 𝜑 → ( 2 /L 𝑃 ) ∈ { - 1 , 0 , 1 } )
12 ovex ⊢ ( 2 /L 𝑃 ) ∈ V
13 12 eltp ⊢ ( ( 2 /L 𝑃 ) ∈ { - 1 , 0 , 1 } ↔ ( ( 2 /L 𝑃 ) = - 1 ∨ ( 2 /L 𝑃 ) = 0 ∨ ( 2 /L 𝑃 ) = 1 ) )
14 1 2 3 4 gausslemma2dlem0h ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15 14 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16 m1expcl2 ⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )
17 15 16 syl ⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )
18 ovex ⊢ ( - 1 ↑ 𝑁 ) ∈ V
19 18 elpr ⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } ↔ ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) )
20 eqcom ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 ↔ - 1 = ( - 1 ↑ 𝑁 ) )
21 20 biimpi ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → - 1 = ( - 1 ↑ 𝑁 ) )
22 21 2a1d ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
23 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
24 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
25 24 nnred ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
26 prmgt1 ⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
27 25 26 jca ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
28 23 27 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
29 1mod ⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
30 1 28 29 3syl ⊢ ( 𝜑 → ( 1 mod 𝑃 ) = 1 )
31 30 eqeq2d ⊢ ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = 1 ) )
32 oddprmge3 ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 3 ) )
33 m1modge3gt1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( - 1 mod 𝑃 ) )
34 breq2 ⊢ ( ( - 1 mod 𝑃 ) = 1 → ( 1 < ( - 1 mod 𝑃 ) ↔ 1 < 1 ) )
35 1re ⊢ 1 ∈ ℝ
36 35 ltnri ⊢ ¬ 1 < 1
37 36 pm2.21i ⊢ ( 1 < 1 → - 1 = 1 )
38 34 37 syl6bi ⊢ ( ( - 1 mod 𝑃 ) = 1 → ( 1 < ( - 1 mod 𝑃 ) → - 1 = 1 ) )
39 33 38 syl5com ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 3 ) → ( ( - 1 mod 𝑃 ) = 1 → - 1 = 1 ) )
40 1 32 39 3syl ⊢ ( 𝜑 → ( ( - 1 mod 𝑃 ) = 1 → - 1 = 1 ) )
41 31 40 sylbid ⊢ ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) → - 1 = 1 ) )
42 oveq1 ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
43 42 eqeq2d ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) ) )
44 eqeq2 ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( - 1 = ( - 1 ↑ 𝑁 ) ↔ - 1 = 1 ) )
45 43 44 imbi12d ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ↔ ( ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) → - 1 = 1 ) ) )
46 41 45 syl5ibr ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
47 22 46 jaoi ⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
48 19 47 sylbi ⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
49 17 48 mpcom ⊢ ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) )
50 oveq1 ⊢ ( ( 2 /L 𝑃 ) = - 1 → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
51 50 eqeq1d ⊢ ( ( 2 /L 𝑃 ) = - 1 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
52 eqeq1 ⊢ ( ( 2 /L 𝑃 ) = - 1 → ( ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ↔ - 1 = ( - 1 ↑ 𝑁 ) ) )
53 51 52 imbi12d ⊢ ( ( 2 /L 𝑃 ) = - 1 → ( ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ↔ ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
54 49 53 syl5ibr ⊢ ( ( 2 /L 𝑃 ) = - 1 → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
55 1 gausslemma2dlem0a ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
56 55 nnrpd ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
57 0mod ⊢ ( 𝑃 ∈ ℝ+ → ( 0 mod 𝑃 ) = 0 )
58 56 57 syl ⊢ ( 𝜑 → ( 0 mod 𝑃 ) = 0 )
59 58 eqeq1d ⊢ ( 𝜑 → ( ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
60 oveq1 ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
61 60 eqeq2d ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( - 1 mod 𝑃 ) ) )
62 61 adantr ⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( - 1 mod 𝑃 ) ) )
63 negmod0 ⊢ ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( 1 mod 𝑃 ) = 0 ↔ ( - 1 mod 𝑃 ) = 0 ) )
64 eqcom ⊢ ( ( - 1 mod 𝑃 ) = 0 ↔ 0 = ( - 1 mod 𝑃 ) )
65 63 64 bitrdi ⊢ ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( 1 mod 𝑃 ) = 0 ↔ 0 = ( - 1 mod 𝑃 ) ) )
66 35 56 65 sylancr ⊢ ( 𝜑 → ( ( 1 mod 𝑃 ) = 0 ↔ 0 = ( - 1 mod 𝑃 ) ) )
67 30 eqeq1d ⊢ ( 𝜑 → ( ( 1 mod 𝑃 ) = 0 ↔ 1 = 0 ) )
68 ax-1ne0 ⊢ 1 ≠ 0
69 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → 0 = ( - 1 ↑ 𝑁 ) ) )
70 68 69 mpi ⊢ ( 1 = 0 → 0 = ( - 1 ↑ 𝑁 ) )
71 67 70 syl6bi ⊢ ( 𝜑 → ( ( 1 mod 𝑃 ) = 0 → 0 = ( - 1 ↑ 𝑁 ) ) )
72 66 71 sylbird ⊢ ( 𝜑 → ( 0 = ( - 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
73 72 adantl ⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ 𝜑 ) → ( 0 = ( - 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
74 62 73 sylbid ⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
75 74 ex ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
76 42 eqeq2d ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( 1 mod 𝑃 ) ) )
77 76 adantr ⊢ ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( 1 mod 𝑃 ) ) )
78 eqcom ⊢ ( 0 = ( 1 mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = 0 )
79 78 67 syl5bb ⊢ ( 𝜑 → ( 0 = ( 1 mod 𝑃 ) ↔ 1 = 0 ) )
80 79 70 syl6bi ⊢ ( 𝜑 → ( 0 = ( 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
81 80 adantl ⊢ ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ 𝜑 ) → ( 0 = ( 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
82 77 81 sylbid ⊢ ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
83 82 ex ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
84 75 83 jaoi ⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
85 19 84 sylbi ⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
86 17 85 mpcom ⊢ ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
87 59 86 sylbid ⊢ ( 𝜑 → ( ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
88 oveq1 ⊢ ( ( 2 /L 𝑃 ) = 0 → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( 0 mod 𝑃 ) )
89 88 eqeq1d ⊢ ( ( 2 /L 𝑃 ) = 0 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
90 eqeq1 ⊢ ( ( 2 /L 𝑃 ) = 0 → ( ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ↔ 0 = ( - 1 ↑ 𝑁 ) ) )
91 89 90 imbi12d ⊢ ( ( 2 /L 𝑃 ) = 0 → ( ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ↔ ( ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
92 87 91 syl5ibr ⊢ ( ( 2 /L 𝑃 ) = 0 → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
93 30 eqeq1d ⊢ ( 𝜑 → ( ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
94 eqcom ⊢ ( 1 = ( - 1 mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = 1 )
95 eqcom ⊢ ( 1 = - 1 ↔ - 1 = 1 )
96 40 94 95 3imtr4g ⊢ ( 𝜑 → ( 1 = ( - 1 mod 𝑃 ) → 1 = - 1 ) )
97 60 eqeq2d ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 1 = ( - 1 mod 𝑃 ) ) )
98 eqeq2 ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( 1 = ( - 1 ↑ 𝑁 ) ↔ 1 = - 1 ) )
99 97 98 imbi12d ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ↔ ( 1 = ( - 1 mod 𝑃 ) → 1 = - 1 ) ) )
100 96 99 syl5ibr ⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
101 eqcom ⊢ ( ( - 1 ↑ 𝑁 ) = 1 ↔ 1 = ( - 1 ↑ 𝑁 ) )
102 101 biimpi ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → 1 = ( - 1 ↑ 𝑁 ) )
103 102 2a1d ⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
104 100 103 jaoi ⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
105 19 104 sylbi ⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
106 17 105 mpcom ⊢ ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) )
107 93 106 sylbid ⊢ ( 𝜑 → ( ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) )
108 oveq1 ⊢ ( ( 2 /L 𝑃 ) = 1 → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
109 108 eqeq1d ⊢ ( ( 2 /L 𝑃 ) = 1 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
110 eqeq1 ⊢ ( ( 2 /L 𝑃 ) = 1 → ( ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ↔ 1 = ( - 1 ↑ 𝑁 ) ) )
111 109 110 imbi12d ⊢ ( ( 2 /L 𝑃 ) = 1 → ( ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ↔ ( ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
112 107 111 syl5ibr ⊢ ( ( 2 /L 𝑃 ) = 1 → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
113 54 92 112 3jaoi ⊢ ( ( ( 2 /L 𝑃 ) = - 1 ∨ ( 2 /L 𝑃 ) = 0 ∨ ( 2 /L 𝑃 ) = 1 ) → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
114 13 113 sylbi ⊢ ( ( 2 /L 𝑃 ) ∈ { - 1 , 0 , 1 } → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
115 11 114 mpcom ⊢ ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) )