m1lgs - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > m1lgs		Structured version Visualization version GIF version

Theorem m1lgs 27297

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

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

**Proof of Theorem m1lgs**
Step	Hyp	Ref	Expression
1		neg1z 12511	. . . . . . . . 9 ⊢ -1 ∈ ℤ
2		oddprm 16722	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
3	2	nnnn0d 12445	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ₀)
4		zexpcl 13983	. . . . . . . . 9 ⊢ ((-1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
5	1, 3, 4	sylancr 587	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
6	5	peano2zd 12583	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
7		eldifi 4082	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 16585	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	7, 8	syl 17	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
10	6, 9	zmodcld 13796	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℕ₀)
11	10	nn0cnd 12447	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℂ)
12		1cnd 11110	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℂ)
13	11, 12, 12	subaddd 11493	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
14		2re 12202	. . . . . . . 8 ⊢ 2 ∈ ℝ
15	14	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℝ)
16	9	nnrpd 12935	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ⁺)
17		0le2 12230	. . . . . . . 8 ⊢ 0 ≤ 2
18	17	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 ≤ 2)
19		oddprmgt2 16610	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
20		modid 13800	. . . . . . 7 ⊢ (((2 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
21	15, 16, 18, 19, 20	syl22anc 838	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = 2)
22		df-2 12191	. . . . . 6 ⊢ 2 = (1 + 1)
23	21, 22	eqtrdi 2780	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = (1 + 1))
24	23	eqeq1d 2731	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
25		eldifsni 4741	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
26	25	neneqd 2930	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 = 2)
27		prmuz2 16607	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
28	7, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ_≥‘2))
29		2prm 16603	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
30		dvdsprm 16614	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
31	28, 29, 30	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
32	26, 31	mtbird 325	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 ∥ 2)
33	32	adantr 480	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ 2)
34		1cnd 11110	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → 1 ∈ ℂ)
35	2	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
36		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 2 ∥ ((𝑃 − 1) / 2))
37		oexpneg 16256	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
38	34, 35, 36, 37	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
39	35	nnzd 12498	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℤ)
40		1exp 13998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 − 1) / 2) ∈ ℤ → (1↑((𝑃 − 1) / 2)) = 1)
41	39, 40	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1)
42	41	negeqd 11357	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1)
43	38, 42	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -1)
44	43	oveq1d 7364	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (-1 + 1))
45		ax-1cn 11067	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
46		neg1cn 12113	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
47		1pneg1e0 12242	. . . . . . . . . . . . . 14 ⊢ (1 + -1) = 0
48	45, 46, 47	addcomli 11308	. . . . . . . . . . . . 13 ⊢ (-1 + 1) = 0
49	44, 48	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = 0)
50	49	oveq2d 7365	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = (2 − 0))
51		2cn 12203	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
52	51	subid1i 11436	. . . . . . . . . . 11 ⊢ (2 − 0) = 2
53	50, 52	eqtrdi 2780	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = 2)
54	53	breq2d 5104	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2))
55	33, 54	mtbird 325	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)))
56	55	ex 412	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ ((𝑃 − 1) / 2) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
57	56	con4d 115	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) → 2 ∥ ((𝑃 − 1) / 2)))
58		2z 12507	. . . . . . . 8 ⊢ 2 ∈ ℤ
59	58	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℤ)
60		moddvds 16174	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
61	9, 59, 6, 60	syl3anc 1373	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
62		4z 12509	. . . . . . . . 9 ⊢ 4 ∈ ℤ
63		4ne0 12236	. . . . . . . . 9 ⊢ 4 ≠ 0
64		nnm1nn0 12425	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
65	9, 64	syl 17	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℕ₀)
66	65	nn0zd 12497	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℤ)
67		dvdsval2 16166	. . . . . . . . 9 ⊢ ((4 ∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
68	62, 63, 66, 67	mp3an12i 1467	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
69	65	nn0cnd 12447	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℂ)
70	51	a1i 11	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℂ)
71		2ne0 12232	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
72	71	a1i 11	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ≠ 0)
73	69, 70, 70, 72, 72	divdiv1d 11931	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / (2 · 2)))
74		2t2e4 12287	. . . . . . . . . . 11 ⊢ (2 · 2) = 4
75	74	oveq2i 7360	. . . . . . . . . 10 ⊢ ((𝑃 − 1) / (2 · 2)) = ((𝑃 − 1) / 4)
76	73, 75	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / 4))
77	76	eleq1d 2813	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((𝑃 − 1) / 2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈ ℤ))
78	68, 77	bitr4d 282	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
79	2	nnzd 12498	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℤ)
80		dvdsval2 16166	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
81	58, 71, 79, 80	mp3an12i 1467	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
82	78, 81	bitr4d 282	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ 2 ∥ ((𝑃 − 1) / 2)))
83	57, 61, 82	3imtr4d 294	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) → 4 ∥ (𝑃 − 1)))
84	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → -1 ∈ ℂ)
85		neg1ne0 12115	. . . . . . . . . . . 12 ⊢ -1 ≠ 0
86	85	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → -1 ≠ 0)
87	58	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 ∈ ℤ)
88	78	biimpa 476	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (((𝑃 − 1) / 2) / 2) ∈ ℤ)
89		expmulz 14015	. . . . . . . . . . 11 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (((𝑃 − 1) / 2) / 2) ∈ ℤ)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
90	84, 86, 87, 88, 89	syl22anc 838	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
91	2	nncnd 12144	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℂ)
92	91, 70, 72	divcan2d 11902	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 · (((𝑃 − 1) / 2) / 2)) = ((𝑃 − 1) / 2))
93	92	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (2 · (((𝑃 − 1) / 2) / 2)) = ((𝑃 − 1) / 2))
94	93	oveq2d 7365	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = (-1↑((𝑃 − 1) / 2)))
95		neg1sqe1 14103	. . . . . . . . . . . 12 ⊢ (-1↑2) = 1
96	95	oveq1i 7359	. . . . . . . . . . 11 ⊢ ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) / 2))
97		1exp 13998	. . . . . . . . . . . 12 ⊢ ((((𝑃 − 1) / 2) / 2) ∈ ℤ → (1↑(((𝑃 − 1) / 2) / 2)) = 1)
98	88, 97	syl 17	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (1↑(((𝑃 − 1) / 2) / 2)) = 1)
99	96, 98	eqtrid 2776	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1)
100	90, 94, 99	3eqtr3d 2772	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑((𝑃 − 1) / 2)) = 1)
101	100	oveq1d 7364	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (1 + 1))
102	22, 101	eqtr4id 2783	. . . . . . 7 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 = ((-1↑((𝑃 − 1) / 2)) + 1))
103	102	oveq1d 7364	. . . . . 6 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃))
104	103	ex 412	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) → (2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
105	83, 104	impbid 212	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 4 ∥ (𝑃 − 1)))
106	13, 24, 105	3bitr2d 307	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ 4 ∥ (𝑃 − 1)))
107		lgsval3 27224	. . . . 5 ⊢ ((-1 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (-1 /_L 𝑃) = ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
108	1, 107	mpan 690	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1 /_L 𝑃) = ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
109	108	eqeq1d 2731	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1))
110		4nn 12211	. . . . 5 ⊢ 4 ∈ ℕ
111	110	a1i 11	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 4 ∈ ℕ)
112		prmz 16586	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
113	7, 112	syl 17	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
114		1zzd 12506	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℤ)
115		moddvds 16174	. . . 4 ⊢ ((4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
116	111, 113, 114, 115	syl3anc 1373	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
117	106, 109, 116	3bitr4d 311	. 2 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ (𝑃 mod 4) = (1 mod 4)))
118		1re 11115	. . . 4 ⊢ 1 ∈ ℝ
119		nnrp 12905	. . . . 5 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
120	110, 119	ax-mp 5	. . . 4 ⊢ 4 ∈ ℝ⁺
121		0le1 11643	. . . 4 ⊢ 0 ≤ 1
122		1lt4 12299	. . . 4 ⊢ 1 < 4
123		modid 13800	. . . 4 ⊢ (((1 ∈ ℝ ∧ 4 ∈ ℝ⁺) ∧ (0 ≤ 1 ∧ 1 < 4)) → (1 mod 4) = 1)
124	118, 120, 121, 122, 123	mp4an 693	. . 3 ⊢ (1 mod 4) = 1
125	124	eqeq2i 2742	. 2 ⊢ ((𝑃 mod 4) = (1 mod 4) ↔ (𝑃 mod 4) = 1)
126	117, 125	bitrdi 287	1 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3900 {csn 4577 class class class wbr 5092 ‘cfv 6482 (class class class)co 7349 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 ≤ cle 11150 − cmin 11347 -cneg 11348 / cdiv 11777 ℕcn 12128 2c2 12183 4c4 12185 ℕ₀cn0 12384 ℤcz 12471 ℤ_≥cuz 12735 ℝ⁺crp 12893 mod cmo 13773 ↑cexp 13968 ∥ cdvds 16163 ℙcprime 16582 /_L clgs 27203

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-n0 12385 df-xnn0 12458 df-z 12472 df-uz 12736 df-q 12850 df-rp 12894 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-prm 16583 df-phi 16677 df-pc 16749 df-lgs 27204

This theorem is referenced by: 2sqlem11 27338 2sqblem 27340

W3C validator