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 
|- ( P e. ( Prime \ { 2 } ) -> ( ( -u 1 /L P ) = 1 <-> ( P mod 4 ) = 1 ) )

Proof

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