m1lgs - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > m1lgs		GIF version

Theorem m1lgs 14613

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 9288	. . . . . . . . 9 ⊢ -1 ∈ ℤ
2		oddprm 12262	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
3	2	nnnn0d 9232	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ₀)
4		zexpcl 10538	. . . . . . . . 9 ⊢ ((-1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
5	1, 3, 4	sylancr 414	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
6	5	peano2zd 9381	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
7		eldifi 3259	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 12113	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	7, 8	syl 14	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
10	6, 9	zmodcld 10348	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℕ₀)
11	10	nn0cnd 9234	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℂ)
12		1cnd 7976	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℂ)
13	11, 12, 12	subaddd 8289	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
14		2z 9284	. . . . . . . . 9 ⊢ 2 ∈ ℤ
15		zq 9629	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
16	14, 15	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ ℚ
17	16	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℚ)
18		prmz 12114	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
19		zq 9629	. . . . . . . 8 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
20	7, 18, 19	3syl 17	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℚ)
21		0le2 9012	. . . . . . . 8 ⊢ 0 ≤ 2
22	21	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 ≤ 2)
23		oddprmgt2 12137	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
24		modqid 10352	. . . . . . 7 ⊢ (((2 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
25	17, 20, 22, 23, 24	syl22anc 1239	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = 2)
26		df-2 8981	. . . . . 6 ⊢ 2 = (1 + 1)
27	25, 26	eqtrdi 2226	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = (1 + 1))
28	27	eqeq1d 2186	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
29		2nn 9083	. . . . . . . 8 ⊢ 2 ∈ ℕ
30	2	nnzd 9377	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℤ)
31		dvdsdc 11808	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℤ) → DECID 2 ∥ ((𝑃 − 1) / 2))
32	29, 30, 31	sylancr 414	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → DECID 2 ∥ ((𝑃 − 1) / 2))
33		eldifsni 3723	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
34	33	neneqd 2368	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 = 2)
35		prmuz2 12134	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ_≥‘2))
37		2prm 12130	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
38		dvdsprm 12140	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
39	36, 37, 38	sylancl 413	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
40	34, 39	mtbird 673	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 ∥ 2)
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ 2)
42		1cnd 7976	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → 1 ∈ ℂ)
43	2	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
44		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 2 ∥ ((𝑃 − 1) / 2))
45		oexpneg 11885	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
46	42, 43, 44, 45	syl3anc 1238	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
47	43	nnzd 9377	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℤ)
48		1exp 10552	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 − 1) / 2) ∈ ℤ → (1↑((𝑃 − 1) / 2)) = 1)
49	47, 48	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1)
50	49	negeqd 8155	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1)
51	46, 50	eqtrd 2210	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -1)
52	51	oveq1d 5893	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (-1 + 1))
53		ax-1cn 7907	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
54		neg1cn 9027	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
55		1pneg1e0 9033	. . . . . . . . . . . . . 14 ⊢ (1 + -1) = 0
56	53, 54, 55	addcomli 8105	. . . . . . . . . . . . 13 ⊢ (-1 + 1) = 0
57	52, 56	eqtrdi 2226	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = 0)
58	57	oveq2d 5894	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = (2 − 0))
59		2cn 8993	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
60	59	subid1i 8232	. . . . . . . . . . 11 ⊢ (2 − 0) = 2
61	58, 60	eqtrdi 2226	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = 2)
62	61	breq2d 4017	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2))
63	41, 62	mtbird 673	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)))
64	63	ex 115	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ ((𝑃 − 1) / 2) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
65		condc 853	. . . . . . 7 ⊢ (DECID 2 ∥ ((𝑃 − 1) / 2) → ((¬ 2 ∥ ((𝑃 − 1) / 2) → ¬ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) → 2 ∥ ((𝑃 − 1) / 2))))
66	32, 64, 65	sylc 62	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) → 2 ∥ ((𝑃 − 1) / 2)))
67	14	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℤ)
68		moddvds 11809	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
69	9, 67, 6, 68	syl3anc 1238	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
70		4z 9286	. . . . . . . . 9 ⊢ 4 ∈ ℤ
71		4ne0 9020	. . . . . . . . 9 ⊢ 4 ≠ 0
72		nnm1nn0 9220	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
73	9, 72	syl 14	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℕ₀)
74	73	nn0zd 9376	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℤ)
75		dvdsval2 11800	. . . . . . . . 9 ⊢ ((4 ∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
76	70, 71, 74, 75	mp3an12i 1341	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
77	73	nn0cnd 9234	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℂ)
78	59	a1i 9	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℂ)
79	29	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℕ)
80	79	nnap0d 8968	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 # 0)
81	77, 78, 78, 80, 80	divdivap1d 8782	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / (2 · 2)))
82		2t2e4 9076	. . . . . . . . . . 11 ⊢ (2 · 2) = 4
83	82	oveq2i 5889	. . . . . . . . . 10 ⊢ ((𝑃 − 1) / (2 · 2)) = ((𝑃 − 1) / 4)
84	81, 83	eqtrdi 2226	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / 4))
85	84	eleq1d 2246	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((𝑃 − 1) / 2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈ ℤ))
86	76, 85	bitr4d 191	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
87		2ne0 9014	. . . . . . . 8 ⊢ 2 ≠ 0
88		dvdsval2 11800	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
89	14, 87, 30, 88	mp3an12i 1341	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
90	86, 89	bitr4d 191	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ 2 ∥ ((𝑃 − 1) / 2)))
91	66, 69, 90	3imtr4d 203	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) → 4 ∥ (𝑃 − 1)))
92	54	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → -1 ∈ ℂ)
93		neg1ap0 9031	. . . . . . . . . . . 12 ⊢ -1 # 0
94	93	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → -1 # 0)
95	14	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 ∈ ℤ)
96	86	biimpa 296	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (((𝑃 − 1) / 2) / 2) ∈ ℤ)
97		expmulzap 10569	. . . . . . . . . . 11 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (2 ∈ ℤ ∧ (((𝑃 − 1) / 2) / 2) ∈ ℤ)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
98	92, 94, 95, 96, 97	syl22anc 1239	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
99	2	nncnd 8936	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℂ)
100	99, 78, 80	divcanap2d 8752	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 · (((𝑃 − 1) / 2) / 2)) = ((𝑃 − 1) / 2))
101	100	adantr 276	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (2 · (((𝑃 − 1) / 2) / 2)) = ((𝑃 − 1) / 2))
102	101	oveq2d 5894	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = (-1↑((𝑃 − 1) / 2)))
103		neg1sqe1 10618	. . . . . . . . . . . 12 ⊢ (-1↑2) = 1
104	103	oveq1i 5888	. . . . . . . . . . 11 ⊢ ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) / 2))
105		1exp 10552	. . . . . . . . . . . 12 ⊢ ((((𝑃 − 1) / 2) / 2) ∈ ℤ → (1↑(((𝑃 − 1) / 2) / 2)) = 1)
106	96, 105	syl 14	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (1↑(((𝑃 − 1) / 2) / 2)) = 1)
107	104, 106	eqtrid 2222	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1)
108	98, 102, 107	3eqtr3d 2218	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑((𝑃 − 1) / 2)) = 1)
109	108	oveq1d 5893	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (1 + 1))
110	26, 109	eqtr4id 2229	. . . . . . 7 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 = ((-1↑((𝑃 − 1) / 2)) + 1))
111	110	oveq1d 5893	. . . . . 6 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃))
112	111	ex 115	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) → (2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
113	91, 112	impbid 129	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 4 ∥ (𝑃 − 1)))
114	13, 28, 113	3bitr2d 216	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ 4 ∥ (𝑃 − 1)))
115		lgsval3 14580	. . . . 5 ⊢ ((-1 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (-1 /_L 𝑃) = ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
116	1, 115	mpan 424	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1 /_L 𝑃) = ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
117	116	eqeq1d 2186	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1))
118		4nn 9085	. . . . 5 ⊢ 4 ∈ ℕ
119	118	a1i 9	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 4 ∈ ℕ)
120	7, 18	syl 14	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
121		1zzd 9283	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℤ)
122		moddvds 11809	. . . 4 ⊢ ((4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
123	119, 120, 121, 122	syl3anc 1238	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
124	114, 117, 123	3bitr4d 220	. 2 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ (𝑃 mod 4) = (1 mod 4)))
125		1z 9282	. . . . 5 ⊢ 1 ∈ ℤ
126		zq 9629	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
127	125, 126	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
128		zq 9629	. . . . 5 ⊢ (4 ∈ ℤ → 4 ∈ ℚ)
129	70, 128	ax-mp 5	. . . 4 ⊢ 4 ∈ ℚ
130		0le1 8441	. . . 4 ⊢ 0 ≤ 1
131		1lt4 9096	. . . 4 ⊢ 1 < 4
132		modqid 10352	. . . 4 ⊢ (((1 ∈ ℚ ∧ 4 ∈ ℚ) ∧ (0 ≤ 1 ∧ 1 < 4)) → (1 mod 4) = 1)
133	127, 129, 130, 131, 132	mp4an 427	. . 3 ⊢ (1 mod 4) = 1
134	133	eqeq2i 2188	. 2 ⊢ ((𝑃 mod 4) = (1 mod 4) ↔ (𝑃 mod 4) = 1)
135	124, 134	bitrdi 196	1 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 834 = wceq 1353 ∈ wcel 2148 ≠ wne 2347 ∖ cdif 3128 {csn 3594 class class class wbr 4005 ‘cfv 5218 (class class class)co 5878 ℂcc 7812 0cc0 7814 1c1 7815 + caddc 7817 · cmul 7819 < clt 7995 ≤ cle 7996 − cmin 8131 -cneg 8132 # cap 8541 / cdiv 8632 ℕcn 8922 2c2 8973 4c4 8975 ℕ₀cn0 9179 ℤcz 9256 ℤ_≥cuz 9531 ℚcq 9622 mod cmo 10325 ↑cexp 10522 ∥ cdvds 11797 ℙcprime 12110 /_L clgs 14559

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589 ax-cnex 7905 ax-resscn 7906 ax-1cn 7907 ax-1re 7908 ax-icn 7909 ax-addcl 7910 ax-addrcl 7911 ax-mulcl 7912 ax-mulrcl 7913 ax-addcom 7914 ax-mulcom 7915 ax-addass 7916 ax-mulass 7917 ax-distr 7918 ax-i2m1 7919 ax-0lt1 7920 ax-1rid 7921 ax-0id 7922 ax-rnegex 7923 ax-precex 7924 ax-cnre 7925 ax-pre-ltirr 7926 ax-pre-ltwlin 7927 ax-pre-lttrn 7928 ax-pre-apti 7929 ax-pre-ltadd 7930 ax-pre-mulgt0 7931 ax-pre-mulext 7932 ax-arch 7933 ax-caucvg 7934

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-xor 1376 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-po 4298 df-iso 4299 df-iord 4368 df-on 4370 df-ilim 4371 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-isom 5227 df-riota 5834 df-ov 5881 df-oprab 5882 df-mpo 5883 df-1st 6144 df-2nd 6145 df-recs 6309 df-irdg 6374 df-frec 6395 df-1o 6420 df-2o 6421 df-oadd 6424 df-er 6538 df-en 6744 df-dom 6745 df-fin 6746 df-sup 6986 df-inf 6987 df-pnf 7997 df-mnf 7998 df-xr 7999 df-ltxr 8000 df-le 8001 df-sub 8133 df-neg 8134 df-reap 8535 df-ap 8542 df-div 8633 df-inn 8923 df-2 8981 df-3 8982 df-4 8983 df-5 8984 df-6 8985 df-7 8986 df-8 8987 df-n0 9180 df-z 9257 df-uz 9532 df-q 9623 df-rp 9657 df-fz 10012 df-fzo 10146 df-fl 10273 df-mod 10326 df-seqfrec 10449 df-exp 10523 df-ihash 10759 df-cj 10854 df-re 10855 df-im 10856 df-rsqrt 11010 df-abs 11011 df-clim 11290 df-proddc 11562 df-dvds 11798 df-gcd 11947 df-prm 12111 df-phi 12214 df-pc 12288 df-lgs 14560

This theorem is referenced by: (None)

W3C validator