m1lgs - Intuitionistic Logic Explorer

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

Theorem m1lgs 15813

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 9510	. . . . . . . . 9 ⊢ -1 ∈ ℤ
2		oddprm 12831	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
3	2	nnnn0d 9454	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ₀)
4		zexpcl 10815	. . . . . . . . 9 ⊢ ((-1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
5	1, 3, 4	sylancr 414	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
6	5	peano2zd 9604	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
7		eldifi 3329	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 12681	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	7, 8	syl 14	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
10	6, 9	zmodcld 10606	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℕ₀)
11	10	nn0cnd 9456	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℂ)
12		1cnd 8194	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℂ)
13	11, 12, 12	subaddd 8507	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
14		2z 9506	. . . . . . . . 9 ⊢ 2 ∈ ℤ
15		zq 9859	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
16	14, 15	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ ℚ
17	16	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℚ)
18		prmz 12682	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
19		zq 9859	. . . . . . . 8 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
20	7, 18, 19	3syl 17	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℚ)
21		0le2 9232	. . . . . . . 8 ⊢ 0 ≤ 2
22	21	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 ≤ 2)
23		oddprmgt2 12705	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
24		modqid 10610	. . . . . . 7 ⊢ (((2 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
25	17, 20, 22, 23, 24	syl22anc 1274	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = 2)
26		df-2 9201	. . . . . 6 ⊢ 2 = (1 + 1)
27	25, 26	eqtrdi 2280	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = (1 + 1))
28	27	eqeq1d 2240	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
29		2nn 9304	. . . . . . . 8 ⊢ 2 ∈ ℕ
30	2	nnzd 9600	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℤ)
31		dvdsdc 12358	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℤ) → DECID 2 ∥ ((𝑃 − 1) / 2))
32	29, 30, 31	sylancr 414	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → DECID 2 ∥ ((𝑃 − 1) / 2))
33		eldifsni 3802	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
34	33	neneqd 2423	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 = 2)
35		prmuz2 12702	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ_≥‘2))
37		2prm 12698	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
38		dvdsprm 12708	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
39	36, 37, 38	sylancl 413	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
40	34, 39	mtbird 679	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 ∥ 2)
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ 2)
42		1cnd 8194	. . . . . . . . . . . . . . . 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 12437	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
46	42, 43, 44, 45	syl3anc 1273	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
47	43	nnzd 9600	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℤ)
48		1exp 10829	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 − 1) / 2) ∈ ℤ → (1↑((𝑃 − 1) / 2)) = 1)
49	47, 48	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1)
50	49	negeqd 8373	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1)
51	46, 50	eqtrd 2264	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -1)
52	51	oveq1d 6032	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (-1 + 1))
53		ax-1cn 8124	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
54		neg1cn 9247	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
55		1pneg1e0 9253	. . . . . . . . . . . . . 14 ⊢ (1 + -1) = 0
56	53, 54, 55	addcomli 8323	. . . . . . . . . . . . 13 ⊢ (-1 + 1) = 0
57	52, 56	eqtrdi 2280	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = 0)
58	57	oveq2d 6033	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = (2 − 0))
59		2cn 9213	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
60	59	subid1i 8450	. . . . . . . . . . 11 ⊢ (2 − 0) = 2
61	58, 60	eqtrdi 2280	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = 2)
62	61	breq2d 4100	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2))
63	41, 62	mtbird 679	. . . . . . . 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 860	. . . . . . 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 12359	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
69	9, 67, 6, 68	syl3anc 1273	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
70		4z 9508	. . . . . . . . 9 ⊢ 4 ∈ ℤ
71		4ne0 9240	. . . . . . . . 9 ⊢ 4 ≠ 0
72		nnm1nn0 9442	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
73	9, 72	syl 14	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℕ₀)
74	73	nn0zd 9599	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℤ)
75		dvdsval2 12350	. . . . . . . . 9 ⊢ ((4 ∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
76	70, 71, 74, 75	mp3an12i 1377	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
77	73	nn0cnd 9456	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℂ)
78	59	a1i 9	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℂ)
79	29	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℕ)
80	79	nnap0d 9188	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 # 0)
81	77, 78, 78, 80, 80	divdivap1d 9001	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / (2 · 2)))
82		2t2e4 9297	. . . . . . . . . . 11 ⊢ (2 · 2) = 4
83	82	oveq2i 6028	. . . . . . . . . 10 ⊢ ((𝑃 − 1) / (2 · 2)) = ((𝑃 − 1) / 4)
84	81, 83	eqtrdi 2280	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / 4))
85	84	eleq1d 2300	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((𝑃 − 1) / 2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈ ℤ))
86	76, 85	bitr4d 191	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
87		2ne0 9234	. . . . . . . 8 ⊢ 2 ≠ 0
88		dvdsval2 12350	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
89	14, 87, 30, 88	mp3an12i 1377	. . . . . . 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 9251	. . . . . . . . . . . 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 10846	. . . . . . . . . . 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 1274	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
99	2	nncnd 9156	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℂ)
100	99, 78, 80	divcanap2d 8971	. . . . . . . . . . . 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 6033	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = (-1↑((𝑃 − 1) / 2)))
103		neg1sqe1 10895	. . . . . . . . . . . 12 ⊢ (-1↑2) = 1
104	103	oveq1i 6027	. . . . . . . . . . 11 ⊢ ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) / 2))
105		1exp 10829	. . . . . . . . . . . 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 2276	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1)
108	98, 102, 107	3eqtr3d 2272	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑((𝑃 − 1) / 2)) = 1)
109	108	oveq1d 6032	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (1 + 1))
110	26, 109	eqtr4id 2283	. . . . . . 7 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 = ((-1↑((𝑃 − 1) / 2)) + 1))
111	110	oveq1d 6032	. . . . . 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 15746	. . . . 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 2240	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1))
118		4nn 9306	. . . . 5 ⊢ 4 ∈ ℕ
119	118	a1i 9	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 4 ∈ ℕ)
120	7, 18	syl 14	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
121		1zzd 9505	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℤ)
122		moddvds 12359	. . . 4 ⊢ ((4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
123	119, 120, 121, 122	syl3anc 1273	. . 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 9504	. . . . 5 ⊢ 1 ∈ ℤ
126		zq 9859	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
127	125, 126	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
128		zq 9859	. . . . 5 ⊢ (4 ∈ ℤ → 4 ∈ ℚ)
129	70, 128	ax-mp 5	. . . 4 ⊢ 4 ∈ ℚ
130		0le1 8660	. . . 4 ⊢ 0 ≤ 1
131		1lt4 9317	. . . 4 ⊢ 1 < 4
132		modqid 10610	. . . 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 2242	. 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 841 = wceq 1397 ∈ wcel 2202 ≠ wne 2402 ∖ cdif 3197 {csn 3669 class class class wbr 4088 ‘cfv 5326 (class class class)co 6017 ℂcc 8029 0cc0 8031 1c1 8032 + caddc 8034 · cmul 8036 < clt 8213 ≤ cle 8214 − cmin 8349 -cneg 8350 # cap 8760 / cdiv 8851 ℕcn 9142 2c2 9193 4c4 9195 ℕ₀cn0 9401 ℤcz 9478 ℤ_≥cuz 9754 ℚcq 9852 mod cmo 10583 ↑cexp 10799 ∥ cdvds 12347 ℙcprime 12678 /_L clgs 15725

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-xor 1420 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-frec 6556 df-1o 6581 df-2o 6582 df-oadd 6585 df-er 6701 df-en 6909 df-dom 6910 df-fin 6911 df-sup 7182 df-inf 7183 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-5 9204 df-6 9205 df-7 9206 df-8 9207 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-fz 10243 df-fzo 10377 df-fl 10529 df-mod 10584 df-seqfrec 10709 df-exp 10800 df-ihash 11037 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-clim 11839 df-proddc 12111 df-dvds 12348 df-gcd 12524 df-prm 12679 df-phi 12782 df-pc 12857 df-lgs 15726

This theorem is referenced by: (None)

W3C validator