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 27727

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 12742	. . . . . . . . 9 ⊢ -1 ∈ ℤ
2		oddprm 17000	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
3	2	nnnn0d 12677	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ₀)
4		zexpcl 14229	. . . . . . . . 9 ⊢ (( -1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → ( -1↑((𝑃 − 1) / 2)) ∈ ℤ)
5	1, 3, 4	sylancr 599	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ( -1↑((𝑃 − 1) / 2)) ∈ ℤ)
6	5	peano2zd 12816	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (( -1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
7		eldifi 4069	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 16861	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	7, 8	syl 18	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
10	6, 9	zmodcld 14042	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℕ₀)
11	10	nn0cnd 12679	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℂ)
12		1cnd 11312	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℂ)
13	11, 12, 12	subaddd 11697	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
14		2re 12427	. . . . . . . 8 ⊢ 2 ∈ ℝ
15	14	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℝ)
16	9	nnrpd 13172	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ⁺)
17		0le2 12455	. . . . . . . 8 ⊢ 0 ≤ 2
18	17	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 ≤ 2)
19		oddprmgt2 16887	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
20		modid 14046	. . . . . . 7 ⊢ (((2 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
21	15, 16, 18, 19, 20	syl22anc 852	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = 2)
22		df-2 12415	. . . . . 6 ⊢ 2 = (1 + 1)
23	21, 22	eqtrdi 2814	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = (1 + 1))
24	23	eqeq1d 2765	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ (1 + 1) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
25		eldifsni 4752	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
26	25	neneqd 2963	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 = 2)
27		prmuz2 16883	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
28	7, 27	syl 18	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ_≥‘2))
29		2prm 16879	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
30		dvdsprm 16891	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
31	28, 29, 30	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
32	26, 31	mtbird 328	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 ∥ 2)
33	32	adantr 486	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ 2)
34		1cnd 11312	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → 1 ∈ ℂ)
35	2	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
36		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 2 ∥ ((𝑃 − 1) / 2))
37		oexpneg 16527	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ( -1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
38	34, 35, 36, 37	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ( -1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
39	35	nnzd 12729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℤ)
40		1exp 14244	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 − 1) / 2) ∈ ℤ → (1↑((𝑃 − 1) / 2)) = 1)
41	39, 40	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1)
42	41	negeqd 11561	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1)
43	38, 42	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ( -1↑((𝑃 − 1) / 2)) = -1)
44	43	oveq1d 7442	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (( -1↑((𝑃 − 1) / 2)) + 1) = ( -1 + 1))
45		ax-1cn 11268	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
46		neg1cn 12315	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
47		1pneg1e0 12470	. . . . . . . . . . . . . 14 ⊢ (1 + -1) = 0
48	45, 46, 47	addcomli 11512	. . . . . . . . . . . . 13 ⊢ ( -1 + 1) = 0
49	44, 48	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (( -1↑((𝑃 − 1) / 2)) + 1) = 0)
50	49	oveq2d 7443	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − (( -1↑((𝑃 − 1) / 2)) + 1)) = (2 − 0))
51		2cn 12428	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
52	51	subid1i 11640	. . . . . . . . . . 11 ⊢ (2 − 0) = 2
53	50, 52	eqtrdi 2814	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − (( -1↑((𝑃 − 1) / 2)) + 1)) = 2)
54	53	breq2d 5117	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (𝑃 ∥ (2 − (( -1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2))
55	33, 54	mtbird 328	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ (2 − (( -1↑((𝑃 − 1) / 2)) + 1)))
56	55	ex 418	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ ((𝑃 − 1) / 2) → ¬ 𝑃 ∥ (2 − (( -1↑((𝑃 − 1) / 2)) + 1))))
57	56	con4d 116	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 − (( -1↑((𝑃 − 1) / 2)) + 1)) → 2 ∥ ((𝑃 − 1) / 2)))
58		2z 12738	. . . . . . . 8 ⊢ 2 ∈ ℤ
59	58	a1i 11	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℤ)
60		moddvds 16445	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (( -1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − (( -1↑((𝑃 − 1) / 2)) + 1))))
61	9, 59, 6, 60	syl3anc 1398	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − (( -1↑((𝑃 − 1) / 2)) + 1))))
62		4z 12740	. . . . . . . . 9 ⊢ 4 ∈ ℤ
63		4ne0 12464	. . . . . . . . 9 ⊢ 4 ≠ 0
64		nnm1nn0 12657	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
65	9, 64	syl 18	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℕ₀)
66	65	nn0zd 12728	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℤ)
67		dvdsval2 16437	. . . . . . . . 9 ⊢ ((4 ∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
68	62, 63, 66, 67	mp3an12i 1494	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
69	65	nn0cnd 12679	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℂ)
70	51	a1i 11	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℂ)
71		2ne0 12459	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
72	71	a1i 11	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ≠ 0)
73	69, 70, 70, 72, 72	divdiv1d 12134	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / (2 · 2)))
74		2t2e4 12516	. . . . . . . . . . 11 ⊢ (2 · 2) = 4
75	74	oveq2i 7438	. . . . . . . . . 10 ⊢ ((𝑃 − 1) / (2 · 2)) = ((𝑃 − 1) / 4)
76	73, 75	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / 4))
77	76	eleq1d 2848	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((𝑃 − 1) / 2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈ ℤ))
78	68, 77	bitr4d 285	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
79	2	nnzd 12729	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℤ)
80		dvdsval2 16437	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
81	58, 71, 79, 80	mp3an12i 1494	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
82	78, 81	bitr4d 285	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ 2 ∥ ((𝑃 − 1) / 2)))
83	57, 61, 82	3imtr4d 297	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) → 4 ∥ (𝑃 − 1)))
84	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → -1 ∈ ℂ)
85		neg1ne0 12317	. . . . . . . . . . . 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 482	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (((𝑃 − 1) / 2) / 2) ∈ ℤ)
89		expmulz 14261	. . . . . . . . . . 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 852	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ( -1↑(2 · (((𝑃 − 1) / 2) / 2))) = (( -1↑2)↑(((𝑃 − 1) / 2) / 2)))
91	2	nncnd 12361	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℂ)
92	91, 70, 72	divcan2d 12105	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 · (((𝑃 − 1) / 2) / 2)) = ((𝑃 − 1) / 2))
93	92	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (2 · (((𝑃 − 1) / 2) / 2)) = ((𝑃 − 1) / 2))
94	93	oveq2d 7443	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ( -1↑(2 · (((𝑃 − 1) / 2) / 2))) = ( -1↑((𝑃 − 1) / 2)))
95		neg1sqe1 14349	. . . . . . . . . . . 12 ⊢ ( -1↑2) = 1
96	95	oveq1i 7437	. . . . . . . . . . 11 ⊢ (( -1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) / 2))
97		1exp 14244	. . . . . . . . . . . 12 ⊢ ((((𝑃 − 1) / 2) / 2) ∈ ℤ → (1↑(((𝑃 − 1) / 2) / 2)) = 1)
98	88, 97	syl 18	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (1↑(((𝑃 − 1) / 2) / 2)) = 1)
99	96, 98	eqtrid 2810	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (( -1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1)
100	90, 94, 99	3eqtr3d 2806	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ( -1↑((𝑃 − 1) / 2)) = 1)
101	100	oveq1d 7442	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (( -1↑((𝑃 − 1) / 2)) + 1) = (1 + 1))
102	22, 101	eqtr4id 2817	. . . . . . 7 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 = (( -1↑((𝑃 − 1) / 2)) + 1))
103	102	oveq1d 7442	. . . . . 6 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃))
104	103	ex 418	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) → (2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
105	83, 104	impbid 215	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = ((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 4 ∥ (𝑃 − 1)))
106	13, 24, 105	3bitr2d 310	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ 4 ∥ (𝑃 − 1)))
107		lgsval3 27654	. . . . 5 ⊢ (( -1 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ( -1 /_L 𝑃) = (((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
108	1, 107	mpan 703	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ( -1 /_L 𝑃) = (((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
109	108	eqeq1d 2765	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (( -1 /_L 𝑃) = 1 ↔ (((( -1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1))
110		4nn 12436	. . . . 5 ⊢ 4 ∈ ℕ
111	110	a1i 11	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 4 ∈ ℕ)
112		prmz 16862	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
113	7, 112	syl 18	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
114		1zzd 12737	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℤ)
115		moddvds 16445	. . . 4 ⊢ ((4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
116	111, 113, 114, 115	syl3anc 1398	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
117	106, 109, 116	3bitr4d 314	. 2 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (( -1 /_L 𝑃) = 1 ↔ (𝑃 mod 4) = (1 mod 4)))
118		1re 11318	. . . 4 ⊢ 1 ∈ ℝ
119		nnrp 13142	. . . . 5 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
120	110, 119	ax-mp 5	. . . 4 ⊢ 4 ∈ ℝ⁺
121		0le1 11849	. . . 4 ⊢ 0 ≤ 1
122		1lt4 12531	. . . 4 ⊢ 1 < 4
123		modid 14046	. . . 4 ⊢ (((1 ∈ ℝ ∧ 4 ∈ ℝ⁺) ∧ (0 ≤ 1 ∧ 1 < 4)) → (1 mod 4) = 1)
124	118, 120, 121, 122, 123	mp4an 706	. . 3 ⊢ (1 mod 4) = 1
125	124	eqeq2i 2776	. 2 ⊢ ((𝑃 mod 4) = (1 mod 4) ↔ (𝑃 mod 4) = 1)
126	117, 125	bitrdi 290	1 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (( -1 /_L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2146 ≠ wne 2958 ∖ cdif 4047 {csn 4587 class class class wbr 5105 ‘cfv 6546 (class class class)co 7427 ℂcc 11208 ℝcr 11209 0cc0 11210 1c1 11211 + caddc 11213 · cmul 11215 < clt 11353 ≤ cle 11354 − cmin 11551 -cneg 11552 / cdiv 11983 ℕcn 12345 2c2 12407 4c4 12409 ℕ₀cn0 12616 ℤcz 12703 ℤ_≥cuz 12975 ℝ⁺crp 13130 mod cmo 14019 ↑cexp 14214 ∥ cdvds 16434 ℙcprime 16858 /_L clgs 27633

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287 ax-pre-sup 11288

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-int 4910 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-om 7885 df-1st 8008 df-2nd 8009 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-2o 8488 df-oadd 8491 df-er 8728 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9444 df-inf 9445 df-dju 9992 df-card 10030 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-div 11984 df-nn 12346 df-2 12415 df-3 12416 df-4 12417 df-n0 12617 df-xnn0 12690 df-z 12704 df-uz 12976 df-q 13086 df-rp 13131 df-fz 13650 df-fzo 13799 df-fl 13942 df-mod 14020 df-seq 14155 df-exp 14215 df-hash 14485 df-cj 15278 df-re 15279 df-im 15280 df-sqrt 15414 df-abs 15415 df-dvds 16435 df-gcd 16677 df-prm 16859 df-phi 16955 df-pc 17027 df-lgs 27634

This theorem is used by: 2sqlem11 27768 2sqblem 27770

W3C validator