# 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}\in \left(ℙ\setminus \left\{2\right\}\right)\to \left(-1{/}_{L}{P}=1↔{P}\mathrm{mod}4=1\right)$

### Proof

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