m1lgs - Intuitionistic Logic Explorer

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

Theorem m1lgs 15533

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 9403	. . . . . . . . 9 ⊢ -1 ∈ ℤ
2		oddprm 12553	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
3	2	nnnn0d 9347	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ₀)
4		zexpcl 10697	. . . . . . . . 9 ⊢ ((-1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
5	1, 3, 4	sylancr 414	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
6	5	peano2zd 9497	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
7		eldifi 3294	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 12403	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	7, 8	syl 14	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
10	6, 9	zmodcld 10488	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℕ₀)
11	10	nn0cnd 9349	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℂ)
12		1cnd 8087	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℂ)
13	11, 12, 12	subaddd 8400	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
14		2z 9399	. . . . . . . . 9 ⊢ 2 ∈ ℤ
15		zq 9746	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
16	14, 15	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ ℚ
17	16	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℚ)
18		prmz 12404	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
19		zq 9746	. . . . . . . 8 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
20	7, 18, 19	3syl 17	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℚ)
21		0le2 9125	. . . . . . . 8 ⊢ 0 ≤ 2
22	21	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 ≤ 2)
23		oddprmgt2 12427	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
24		modqid 10492	. . . . . . 7 ⊢ (((2 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
25	17, 20, 22, 23, 24	syl22anc 1250	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = 2)
26		df-2 9094	. . . . . 6 ⊢ 2 = (1 + 1)
27	25, 26	eqtrdi 2253	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = (1 + 1))
28	27	eqeq1d 2213	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
29		2nn 9197	. . . . . . . 8 ⊢ 2 ∈ ℕ
30	2	nnzd 9493	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℤ)
31		dvdsdc 12080	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℤ) → DECID 2 ∥ ((𝑃 − 1) / 2))
32	29, 30, 31	sylancr 414	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → DECID 2 ∥ ((𝑃 − 1) / 2))
33		eldifsni 3761	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
34	33	neneqd 2396	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 = 2)
35		prmuz2 12424	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ_≥‘2))
37		2prm 12420	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
38		dvdsprm 12430	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
39	36, 37, 38	sylancl 413	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
40	34, 39	mtbird 674	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 ∥ 2)
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ 2)
42		1cnd 8087	. . . . . . . . . . . . . . . 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 12159	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
46	42, 43, 44, 45	syl3anc 1249	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
47	43	nnzd 9493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℤ)
48		1exp 10711	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 − 1) / 2) ∈ ℤ → (1↑((𝑃 − 1) / 2)) = 1)
49	47, 48	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1)
50	49	negeqd 8266	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1)
51	46, 50	eqtrd 2237	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -1)
52	51	oveq1d 5958	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (-1 + 1))
53		ax-1cn 8017	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
54		neg1cn 9140	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
55		1pneg1e0 9146	. . . . . . . . . . . . . 14 ⊢ (1 + -1) = 0
56	53, 54, 55	addcomli 8216	. . . . . . . . . . . . 13 ⊢ (-1 + 1) = 0
57	52, 56	eqtrdi 2253	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = 0)
58	57	oveq2d 5959	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = (2 − 0))
59		2cn 9106	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
60	59	subid1i 8343	. . . . . . . . . . 11 ⊢ (2 − 0) = 2
61	58, 60	eqtrdi 2253	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = 2)
62	61	breq2d 4055	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2))
63	41, 62	mtbird 674	. . . . . . . 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 854	. . . . . . 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 12081	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
69	9, 67, 6, 68	syl3anc 1249	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
70		4z 9401	. . . . . . . . 9 ⊢ 4 ∈ ℤ
71		4ne0 9133	. . . . . . . . 9 ⊢ 4 ≠ 0
72		nnm1nn0 9335	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
73	9, 72	syl 14	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℕ₀)
74	73	nn0zd 9492	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℤ)
75		dvdsval2 12072	. . . . . . . . 9 ⊢ ((4 ∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
76	70, 71, 74, 75	mp3an12i 1353	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
77	73	nn0cnd 9349	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℂ)
78	59	a1i 9	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℂ)
79	29	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℕ)
80	79	nnap0d 9081	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 # 0)
81	77, 78, 78, 80, 80	divdivap1d 8894	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / (2 · 2)))
82		2t2e4 9190	. . . . . . . . . . 11 ⊢ (2 · 2) = 4
83	82	oveq2i 5954	. . . . . . . . . 10 ⊢ ((𝑃 − 1) / (2 · 2)) = ((𝑃 − 1) / 4)
84	81, 83	eqtrdi 2253	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / 4))
85	84	eleq1d 2273	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((𝑃 − 1) / 2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈ ℤ))
86	76, 85	bitr4d 191	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
87		2ne0 9127	. . . . . . . 8 ⊢ 2 ≠ 0
88		dvdsval2 12072	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
89	14, 87, 30, 88	mp3an12i 1353	. . . . . . 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 9144	. . . . . . . . . . . 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 10728	. . . . . . . . . . 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 1250	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
99	2	nncnd 9049	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℂ)
100	99, 78, 80	divcanap2d 8864	. . . . . . . . . . . 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 5959	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = (-1↑((𝑃 − 1) / 2)))
103		neg1sqe1 10777	. . . . . . . . . . . 12 ⊢ (-1↑2) = 1
104	103	oveq1i 5953	. . . . . . . . . . 11 ⊢ ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) / 2))
105		1exp 10711	. . . . . . . . . . . 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 2249	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1)
108	98, 102, 107	3eqtr3d 2245	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑((𝑃 − 1) / 2)) = 1)
109	108	oveq1d 5958	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (1 + 1))
110	26, 109	eqtr4id 2256	. . . . . . 7 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 = ((-1↑((𝑃 − 1) / 2)) + 1))
111	110	oveq1d 5958	. . . . . 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 15466	. . . . 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 2213	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1))
118		4nn 9199	. . . . 5 ⊢ 4 ∈ ℕ
119	118	a1i 9	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 4 ∈ ℕ)
120	7, 18	syl 14	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
121		1zzd 9398	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℤ)
122		moddvds 12081	. . . 4 ⊢ ((4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
123	119, 120, 121, 122	syl3anc 1249	. . 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 9397	. . . . 5 ⊢ 1 ∈ ℤ
126		zq 9746	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
127	125, 126	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
128		zq 9746	. . . . 5 ⊢ (4 ∈ ℤ → 4 ∈ ℚ)
129	70, 128	ax-mp 5	. . . 4 ⊢ 4 ∈ ℚ
130		0le1 8553	. . . 4 ⊢ 0 ≤ 1
131		1lt4 9210	. . . 4 ⊢ 1 < 4
132		modqid 10492	. . . 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 2215	. 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 835 = wceq 1372 ∈ wcel 2175 ≠ wne 2375 ∖ cdif 3162 {csn 3632 class class class wbr 4043 ‘cfv 5270 (class class class)co 5943 ℂcc 7922 0cc0 7924 1c1 7925 + caddc 7927 · cmul 7929 < clt 8106 ≤ cle 8107 − cmin 8242 -cneg 8243 # cap 8653 / cdiv 8744 ℕcn 9035 2c2 9086 4c4 9088 ℕ₀cn0 9294 ℤcz 9371 ℤ_≥cuz 9647 ℚcq 9739 mod cmo 10465 ↑cexp 10681 ∥ cdvds 12069 ℙcprime 12400 /_L clgs 15445

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 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-iinf 4635 ax-cnex 8015 ax-resscn 8016 ax-1cn 8017 ax-1re 8018 ax-icn 8019 ax-addcl 8020 ax-addrcl 8021 ax-mulcl 8022 ax-mulrcl 8023 ax-addcom 8024 ax-mulcom 8025 ax-addass 8026 ax-mulass 8027 ax-distr 8028 ax-i2m1 8029 ax-0lt1 8030 ax-1rid 8031 ax-0id 8032 ax-rnegex 8033 ax-precex 8034 ax-cnre 8035 ax-pre-ltirr 8036 ax-pre-ltwlin 8037 ax-pre-lttrn 8038 ax-pre-apti 8039 ax-pre-ltadd 8040 ax-pre-mulgt0 8041 ax-pre-mulext 8042 ax-arch 8043 ax-caucvg 8044

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-xor 1395 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-reu 2490 df-rmo 2491 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-if 3571 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4339 df-po 4342 df-iso 4343 df-iord 4412 df-on 4414 df-ilim 4415 df-suc 4417 df-iom 4638 df-xp 4680 df-rel 4681 df-cnv 4682 df-co 4683 df-dm 4684 df-rn 4685 df-res 4686 df-ima 4687 df-iota 5231 df-fun 5272 df-fn 5273 df-f 5274 df-f1 5275 df-fo 5276 df-f1o 5277 df-fv 5278 df-isom 5279 df-riota 5898 df-ov 5946 df-oprab 5947 df-mpo 5948 df-1st 6225 df-2nd 6226 df-recs 6390 df-irdg 6455 df-frec 6476 df-1o 6501 df-2o 6502 df-oadd 6505 df-er 6619 df-en 6827 df-dom 6828 df-fin 6829 df-sup 7085 df-inf 7086 df-pnf 8108 df-mnf 8109 df-xr 8110 df-ltxr 8111 df-le 8112 df-sub 8244 df-neg 8245 df-reap 8647 df-ap 8654 df-div 8745 df-inn 9036 df-2 9094 df-3 9095 df-4 9096 df-5 9097 df-6 9098 df-7 9099 df-8 9100 df-n0 9295 df-z 9372 df-uz 9648 df-q 9740 df-rp 9775 df-fz 10130 df-fzo 10264 df-fl 10411 df-mod 10466 df-seqfrec 10591 df-exp 10682 df-ihash 10919 df-cj 11124 df-re 11125 df-im 11126 df-rsqrt 11280 df-abs 11281 df-clim 11561 df-proddc 11833 df-dvds 12070 df-gcd 12246 df-prm 12401 df-phi 12504 df-pc 12579 df-lgs 15446

This theorem is referenced by: (None)

W3C validator