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 (ℙ ∖ \{2\}) \to (-1 /_{L} P = 1 \leftrightarrow P \mod 4 = 1)$

Proof

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

Metamath Proof Explorer

Theorem m1lgs

Proof