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 1mod ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
29 1 23 27 28 4syl ( 𝜑 → ( 1 mod 𝑃 ) = 1 )
30 29 eqeq2d ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = 1 ) )
31 oddprmge3 ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ ‘ 3 ) )
32 m1modge3gt1 ( 𝑃 ∈ ( ℤ ‘ 3 ) → 1 < ( - 1 mod 𝑃 ) )
33 breq2 ( ( - 1 mod 𝑃 ) = 1 → ( 1 < ( - 1 mod 𝑃 ) ↔ 1 < 1 ) )
34 1re 1 ∈ ℝ
35 34 ltnri ¬ 1 < 1
36 35 pm2.21i ( 1 < 1 → - 1 = 1 )
37 33 36 biimtrdi ( ( - 1 mod 𝑃 ) = 1 → ( 1 < ( - 1 mod 𝑃 ) → - 1 = 1 ) )
38 32 37 syl5com ( 𝑃 ∈ ( ℤ ‘ 3 ) → ( ( - 1 mod 𝑃 ) = 1 → - 1 = 1 ) )
39 1 31 38 3syl ( 𝜑 → ( ( - 1 mod 𝑃 ) = 1 → - 1 = 1 ) )
40 30 39 sylbid ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) → - 1 = 1 ) )
41 oveq1 ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
42 41 eqeq2d ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) ) )
43 eqeq2 ( ( - 1 ↑ 𝑁 ) = 1 → ( - 1 = ( - 1 ↑ 𝑁 ) ↔ - 1 = 1 ) )
44 42 43 imbi12d ( ( - 1 ↑ 𝑁 ) = 1 → ( ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ↔ ( ( - 1 mod 𝑃 ) = ( 1 mod 𝑃 ) → - 1 = 1 ) ) )
45 40 44 imbitrrid ( ( - 1 ↑ 𝑁 ) = 1 → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
46 22 45 jaoi ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
47 19 46 sylbi ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
48 17 47 mpcom ( 𝜑 → ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) )
49 oveq1 ( ( 2 /L 𝑃 ) = - 1 → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
50 49 eqeq1d ( ( 2 /L 𝑃 ) = - 1 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
51 eqeq1 ( ( 2 /L 𝑃 ) = - 1 → ( ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ↔ - 1 = ( - 1 ↑ 𝑁 ) ) )
52 50 51 imbi12d ( ( 2 /L 𝑃 ) = - 1 → ( ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ↔ ( ( - 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → - 1 = ( - 1 ↑ 𝑁 ) ) ) )
53 48 52 imbitrrid ( ( 2 /L 𝑃 ) = - 1 → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
54 1 gausslemma2dlem0a ( 𝜑𝑃 ∈ ℕ )
55 54 nnrpd ( 𝜑𝑃 ∈ ℝ+ )
56 0mod ( 𝑃 ∈ ℝ+ → ( 0 mod 𝑃 ) = 0 )
57 55 56 syl ( 𝜑 → ( 0 mod 𝑃 ) = 0 )
58 57 eqeq1d ( 𝜑 → ( ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
59 oveq1 ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
60 59 eqeq2d ( ( - 1 ↑ 𝑁 ) = - 1 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( - 1 mod 𝑃 ) ) )
61 60 adantr ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( - 1 mod 𝑃 ) ) )
62 negmod0 ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( 1 mod 𝑃 ) = 0 ↔ ( - 1 mod 𝑃 ) = 0 ) )
63 eqcom ( ( - 1 mod 𝑃 ) = 0 ↔ 0 = ( - 1 mod 𝑃 ) )
64 62 63 bitrdi ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( 1 mod 𝑃 ) = 0 ↔ 0 = ( - 1 mod 𝑃 ) ) )
65 34 55 64 sylancr ( 𝜑 → ( ( 1 mod 𝑃 ) = 0 ↔ 0 = ( - 1 mod 𝑃 ) ) )
66 29 eqeq1d ( 𝜑 → ( ( 1 mod 𝑃 ) = 0 ↔ 1 = 0 ) )
67 ax-1ne0 1 ≠ 0
68 eqneqall ( 1 = 0 → ( 1 ≠ 0 → 0 = ( - 1 ↑ 𝑁 ) ) )
69 67 68 mpi ( 1 = 0 → 0 = ( - 1 ↑ 𝑁 ) )
70 66 69 biimtrdi ( 𝜑 → ( ( 1 mod 𝑃 ) = 0 → 0 = ( - 1 ↑ 𝑁 ) ) )
71 65 70 sylbird ( 𝜑 → ( 0 = ( - 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
72 71 adantl ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ 𝜑 ) → ( 0 = ( - 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
73 61 72 sylbid ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
74 73 ex ( ( - 1 ↑ 𝑁 ) = - 1 → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
75 41 eqeq2d ( ( - 1 ↑ 𝑁 ) = 1 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( 1 mod 𝑃 ) ) )
76 75 adantr ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 0 = ( 1 mod 𝑃 ) ) )
77 eqcom ( 0 = ( 1 mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = 0 )
78 77 66 bitrid ( 𝜑 → ( 0 = ( 1 mod 𝑃 ) ↔ 1 = 0 ) )
79 78 69 biimtrdi ( 𝜑 → ( 0 = ( 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
80 79 adantl ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ 𝜑 ) → ( 0 = ( 1 mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
81 76 80 sylbid ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ 𝜑 ) → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
82 81 ex ( ( - 1 ↑ 𝑁 ) = 1 → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
83 74 82 jaoi ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
84 19 83 sylbi ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
85 17 84 mpcom ( 𝜑 → ( 0 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
86 58 85 sylbid ( 𝜑 → ( ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) )
87 oveq1 ( ( 2 /L 𝑃 ) = 0 → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( 0 mod 𝑃 ) )
88 87 eqeq1d ( ( 2 /L 𝑃 ) = 0 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
89 eqeq1 ( ( 2 /L 𝑃 ) = 0 → ( ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ↔ 0 = ( - 1 ↑ 𝑁 ) ) )
90 88 89 imbi12d ( ( 2 /L 𝑃 ) = 0 → ( ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ↔ ( ( 0 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 0 = ( - 1 ↑ 𝑁 ) ) ) )
91 86 90 imbitrrid ( ( 2 /L 𝑃 ) = 0 → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
92 29 eqeq1d ( 𝜑 → ( ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
93 eqcom ( 1 = ( - 1 mod 𝑃 ) ↔ ( - 1 mod 𝑃 ) = 1 )
94 eqcom ( 1 = - 1 ↔ - 1 = 1 )
95 39 93 94 3imtr4g ( 𝜑 → ( 1 = ( - 1 mod 𝑃 ) → 1 = - 1 ) )
96 59 eqeq2d ( ( - 1 ↑ 𝑁 ) = - 1 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ 1 = ( - 1 mod 𝑃 ) ) )
97 eqeq2 ( ( - 1 ↑ 𝑁 ) = - 1 → ( 1 = ( - 1 ↑ 𝑁 ) ↔ 1 = - 1 ) )
98 96 97 imbi12d ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ↔ ( 1 = ( - 1 mod 𝑃 ) → 1 = - 1 ) ) )
99 95 98 imbitrrid ( ( - 1 ↑ 𝑁 ) = - 1 → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
100 eqcom ( ( - 1 ↑ 𝑁 ) = 1 ↔ 1 = ( - 1 ↑ 𝑁 ) )
101 100 biimpi ( ( - 1 ↑ 𝑁 ) = 1 → 1 = ( - 1 ↑ 𝑁 ) )
102 101 2a1d ( ( - 1 ↑ 𝑁 ) = 1 → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
103 99 102 jaoi ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
104 19 103 sylbi ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
105 17 104 mpcom ( 𝜑 → ( 1 = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) )
106 92 105 sylbid ( 𝜑 → ( ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) )
107 oveq1 ( ( 2 /L 𝑃 ) = 1 → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
108 107 eqeq1d ( ( 2 /L 𝑃 ) = 1 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) ) )
109 eqeq1 ( ( 2 /L 𝑃 ) = 1 → ( ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ↔ 1 = ( - 1 ↑ 𝑁 ) ) )
110 108 109 imbi12d ( ( 2 /L 𝑃 ) = 1 → ( ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ↔ ( ( 1 mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → 1 = ( - 1 ↑ 𝑁 ) ) ) )
111 106 110 imbitrrid ( ( 2 /L 𝑃 ) = 1 → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
112 53 91 111 3jaoi ( ( ( 2 /L 𝑃 ) = - 1 ∨ ( 2 /L 𝑃 ) = 0 ∨ ( 2 /L 𝑃 ) = 1 ) → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
113 13 112 sylbi ( ( 2 /L 𝑃 ) ∈ { - 1 , 0 , 1 } → ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) ) )
114 11 113 mpcom ( 𝜑 → ( ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( - 1 ↑ 𝑁 ) mod 𝑃 ) → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) ) )