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 2 -1 / L P = 1 P mod 4 = 1

Proof

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