Metamath Proof Explorer

Theorem m1lgs

Description: The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime P iff P == 1 (mod 4 ). See first case of theorem 9.4 in ApostolNT p. 181. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion m1lgs ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 neg1z ⊢ - 1 ∈ ℤ
2 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
3 2 nnnn0d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
4 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
5 1 3 4 sylancr ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
6 5 peano2zd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℤ )
7 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 7 8 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℕ )
10 6 9 zmodcld ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ ℂ )
12 1cnd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 1 ∈ ℂ )
13 11 12 12 subaddd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ) )
14 2re ⊢ 2 ∈ ℝ
15 14 a1i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 ∈ ℝ )
16 9 nnrpd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℝ+ )
17 0le2 ⊢ 0 ≤ 2
18 17 a1i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 0 ≤ 2 )
19 oddprmgt2 ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 < 𝑃 )
20 modid ⊢ ( ( ( 2 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 2 ∧ 2 < 𝑃 ) ) → ( 2 mod 𝑃 ) = 2 )
21 15 16 18 19 20 syl22anc ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 2 mod 𝑃 ) = 2 )
22 df-2 ⊢ 2 = ( 1 + 1 )
23 21 22 eqtrdi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 2 mod 𝑃 ) = ( 1 + 1 ) )
24 23 eqeq1d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ↔ ( 1 + 1 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ) )
25 eldifsni ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
26 25 neneqd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑃 = 2 )
27 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
28 7 27 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
29 2prm ⊢ 2 ∈ ℙ
30 dvdsprm ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 2 ∈ ℙ ) → ( 𝑃 ∥ 2 ↔ 𝑃 = 2 ) )
31 28 29 30 sylancl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∥ 2 ↔ 𝑃 = 2 ) )
32 26 31 mtbird ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑃 ∥ 2 )
33 32 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ¬ 𝑃 ∥ 2 )
34 1cnd ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → 1 ∈ ℂ )
35 2 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
36 simpr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) )
37 oexpneg ⊢ ( ( 1 ∈ ℂ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = - ( 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
38 34 35 36 37 syl3anc ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = - ( 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
39 35 nnzd ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
40 1exp ⊢ ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ → ( 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = 1 )
41 39 40 syl ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = 1 )
42 41 negeqd ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → - ( 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = - 1 )
43 38 42 eqtrd ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = - 1 )
44 43 oveq1d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) = ( - 1 + 1 ) )
45 ax-1cn ⊢ 1 ∈ ℂ
46 neg1cn ⊢ - 1 ∈ ℂ
47 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
48 45 46 47 addcomli ⊢ ( - 1 + 1 ) = 0
49 44 48 eqtrdi ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) = 0 )
50 49 oveq2d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) = ( 2 − 0 ) )
51 2cn ⊢ 2 ∈ ℂ
52 51 subid1i ⊢ ( 2 − 0 ) = 2
53 50 52 eqtrdi ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) = 2 )
54 53 breq2d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝑃 ∥ ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) ↔ 𝑃 ∥ 2 ) )
55 33 54 mtbird ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) → ¬ 𝑃 ∥ ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) )
56 55 ex ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ¬ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) → ¬ 𝑃 ∥ ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) ) )
57 56 con4d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∥ ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) → 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) )
58 2z ⊢ 2 ∈ ℤ
59 58 a1i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 ∈ ℤ )
60 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℤ ) → ( ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ↔ 𝑃 ∥ ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) ) )
61 9 59 6 60 syl3anc ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ↔ 𝑃 ∥ ( 2 − ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ) ) )
62 4z ⊢ 4 ∈ ℤ
63 4ne0 ⊢ 4 ≠ 0
64 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
65 9 64 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − 1 ) ∈ ℕ0 )
66 65 nn0zd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − 1 ) ∈ ℤ )
67 dvdsval2 ⊢ ( ( 4 ∈ ℤ ∧ 4 ≠ 0 ∧ ( 𝑃 − 1 ) ∈ ℤ ) → ( 4 ∥ ( 𝑃 − 1 ) ↔ ( ( 𝑃 − 1 ) / 4 ) ∈ ℤ ) )
68 62 63 66 67 mp3an12i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 4 ∥ ( 𝑃 − 1 ) ↔ ( ( 𝑃 − 1 ) / 4 ) ∈ ℤ ) )
69 65 nn0cnd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − 1 ) ∈ ℂ )
70 51 a1i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 ∈ ℂ )
71 2ne0 ⊢ 2 ≠ 0
72 71 a1i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 ≠ 0 )
73 69 70 70 72 72 divdiv1d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) = ( ( 𝑃 − 1 ) / ( 2 · 2 ) ) )
74 2t2e4 ⊢ ( 2 · 2 ) = 4
75 74 oveq2i ⊢ ( ( 𝑃 − 1 ) / ( 2 · 2 ) ) = ( ( 𝑃 − 1 ) / 4 )
76 73 75 eqtrdi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) = ( ( 𝑃 − 1 ) / 4 ) )
77 76 eleq1d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ ↔ ( ( 𝑃 − 1 ) / 4 ) ∈ ℤ ) )
78 68 77 bitr4d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 4 ∥ ( 𝑃 − 1 ) ↔ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ ) )
79 2 nnzd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
80 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) → ( 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ↔ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ ) )
81 58 71 79 80 mp3an12i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ↔ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ ) )
82 78 81 bitr4d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 4 ∥ ( 𝑃 − 1 ) ↔ 2 ∥ ( ( 𝑃 − 1 ) / 2 ) ) )
83 57 61 82 3imtr4d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) → 4 ∥ ( 𝑃 − 1 ) ) )
84 46 a1i ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → - 1 ∈ ℂ )
85 neg1ne0 ⊢ - 1 ≠ 0
86 85 a1i ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → - 1 ≠ 0 )
87 58 a1i ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → 2 ∈ ℤ )
88 78 biimpa ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ )
89 expmulz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ ) ) → ( - 1 ↑ ( 2 · ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) )
90 84 86 87 88 89 syl22anc ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( - 1 ↑ ( 2 · ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) )
91 2 nncnd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℂ )
92 91 70 72 divcan2d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 2 · ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) = ( ( 𝑃 − 1 ) / 2 ) )
93 92 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( 2 · ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) = ( ( 𝑃 − 1 ) / 2 ) )
94 93 oveq2d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( - 1 ↑ ( 2 · ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) ) = ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
95 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
96 95 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) = ( 1 ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) )
97 1exp ⊢ ( ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ∈ ℤ → ( 1 ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) = 1 )
98 88 97 syl ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( 1 ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) = 1 )
99 96 98 syl5eq ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( ( - 1 ↑ 2 ) ↑ ( ( ( 𝑃 − 1 ) / 2 ) / 2 ) ) = 1 )
100 90 94 99 3eqtr3d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = 1 )
101 100 oveq1d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) = ( 1 + 1 ) )
102 22 101 eqtr4id ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → 2 = ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) )
103 102 oveq1d ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 4 ∥ ( 𝑃 − 1 ) ) → ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) )
104 103 ex ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 4 ∥ ( 𝑃 − 1 ) → ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ) )
105 83 104 impbid ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 2 mod 𝑃 ) = ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ↔ 4 ∥ ( 𝑃 − 1 ) ) )
106 13 24 105 3bitr2d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = 1 ↔ 4 ∥ ( 𝑃 − 1 ) ) )
107 lgsval3 ⊢ ( ( - 1 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( - 1 /L 𝑃 ) = ( ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
108 1 107 mpan ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( - 1 /L 𝑃 ) = ( ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
109 108 eqeq1d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( ( ( ( - 1 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = 1 ) )
110 4nn ⊢ 4 ∈ ℕ
111 110 a1i ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 4 ∈ ℕ )
112 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
113 7 112 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℤ )
114 1zzd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 1 ∈ ℤ )
115 moddvds ⊢ ( ( 4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑃 mod 4 ) = ( 1 mod 4 ) ↔ 4 ∥ ( 𝑃 − 1 ) ) )
116 111 113 114 115 syl3anc ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 mod 4 ) = ( 1 mod 4 ) ↔ 4 ∥ ( 𝑃 − 1 ) ) )
117 106 109 116 3bitr4d ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = ( 1 mod 4 ) ) )
118 1re ⊢ 1 ∈ ℝ
119 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
120 110 119 ax-mp ⊢ 4 ∈ ℝ+
121 0le1 ⊢ 0 ≤ 1
122 1lt4 ⊢ 1 < 4
123 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 4 ) ) → ( 1 mod 4 ) = 1 )
124 118 120 121 122 123 mp4an ⊢ ( 1 mod 4 ) = 1
125 124 eqeq2i ⊢ ( ( 𝑃 mod 4 ) = ( 1 mod 4 ) ↔ ( 𝑃 mod 4 ) = 1 )
126 117 125 bitrdi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = 1 ) )