m1lgs - Intuitionistic Logic Explorer

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

Theorem m1lgs 15785

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 9494	. . . . . . . . 9 ⊢ -1 ∈ ℤ
2		oddprm 12803	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
3	2	nnnn0d 9438	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ₀)
4		zexpcl 10793	. . . . . . . . 9 ⊢ ((-1 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
5	1, 3, 4	sylancr 414	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (-1↑((𝑃 − 1) / 2)) ∈ ℤ)
6	5	peano2zd 9588	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
7		eldifi 3326	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 12653	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	7, 8	syl 14	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
10	6, 9	zmodcld 10584	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℕ₀)
11	10	nn0cnd 9440	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ ℂ)
12		1cnd 8178	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℂ)
13	11, 12, 12	subaddd 8491	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1 ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
14		2z 9490	. . . . . . . . 9 ⊢ 2 ∈ ℤ
15		zq 9838	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
16	14, 15	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ ℚ
17	16	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℚ)
18		prmz 12654	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
19		zq 9838	. . . . . . . 8 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
20	7, 18, 19	3syl 17	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℚ)
21		0le2 9216	. . . . . . . 8 ⊢ 0 ≤ 2
22	21	a1i 9	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 ≤ 2)
23		oddprmgt2 12677	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
24		modqid 10588	. . . . . . 7 ⊢ (((2 ∈ ℚ ∧ 𝑃 ∈ ℚ) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
25	17, 20, 22, 23, 24	syl22anc 1272	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = 2)
26		df-2 9185	. . . . . 6 ⊢ 2 = (1 + 1)
27	25, 26	eqtrdi 2278	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 mod 𝑃) = (1 + 1))
28	27	eqeq1d 2238	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ (1 + 1) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃)))
29		2nn 9288	. . . . . . . 8 ⊢ 2 ∈ ℕ
30	2	nnzd 9584	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℤ)
31		dvdsdc 12330	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℤ) → DECID 2 ∥ ((𝑃 − 1) / 2))
32	29, 30, 31	sylancr 414	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → DECID 2 ∥ ((𝑃 − 1) / 2))
33		eldifsni 3797	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
34	33	neneqd 2421	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 = 2)
35		prmuz2 12674	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ_≥‘2))
37		2prm 12670	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
38		dvdsprm 12680	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
39	36, 37, 38	sylancl 413	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∥ 2 ↔ 𝑃 = 2))
40	34, 39	mtbird 677	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 𝑃 ∥ 2)
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ¬ 𝑃 ∥ 2)
42		1cnd 8178	. . . . . . . . . . . . . . . 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 12409	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
46	42, 43, 44, 45	syl3anc 1271	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -(1↑((𝑃 − 1) / 2)))
47	43	nnzd 9584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((𝑃 − 1) / 2) ∈ ℤ)
48		1exp 10807	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 − 1) / 2) ∈ ℤ → (1↑((𝑃 − 1) / 2)) = 1)
49	47, 48	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (1↑((𝑃 − 1) / 2)) = 1)
50	49	negeqd 8357	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → -(1↑((𝑃 − 1) / 2)) = -1)
51	46, 50	eqtrd 2262	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (-1↑((𝑃 − 1) / 2)) = -1)
52	51	oveq1d 6025	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (-1 + 1))
53		ax-1cn 8108	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
54		neg1cn 9231	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
55		1pneg1e0 9237	. . . . . . . . . . . . . 14 ⊢ (1 + -1) = 0
56	53, 54, 55	addcomli 8307	. . . . . . . . . . . . 13 ⊢ (-1 + 1) = 0
57	52, 56	eqtrdi 2278	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → ((-1↑((𝑃 − 1) / 2)) + 1) = 0)
58	57	oveq2d 6026	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = (2 − 0))
59		2cn 9197	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
60	59	subid1i 8434	. . . . . . . . . . 11 ⊢ (2 − 0) = 2
61	58, 60	eqtrdi 2278	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) = 2)
62	61	breq2d 4095	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ ((𝑃 − 1) / 2)) → (𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1)) ↔ 𝑃 ∥ 2))
63	41, 62	mtbird 677	. . . . . . . 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 858	. . . . . . 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 12331	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ((-1↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
69	9, 67, 6, 68	syl3anc 1271	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 mod 𝑃) = (((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ↔ 𝑃 ∥ (2 − ((-1↑((𝑃 − 1) / 2)) + 1))))
70		4z 9492	. . . . . . . . 9 ⊢ 4 ∈ ℤ
71		4ne0 9224	. . . . . . . . 9 ⊢ 4 ≠ 0
72		nnm1nn0 9426	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
73	9, 72	syl 14	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℕ₀)
74	73	nn0zd 9583	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℤ)
75		dvdsval2 12322	. . . . . . . . 9 ⊢ ((4 ∈ ℤ ∧ 4 ≠ 0 ∧ (𝑃 − 1) ∈ ℤ) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
76	70, 71, 74, 75	mp3an12i 1375	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ ((𝑃 − 1) / 4) ∈ ℤ))
77	73	nn0cnd 9440	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℂ)
78	59	a1i 9	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℂ)
79	29	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 ∈ ℕ)
80	79	nnap0d 9172	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 # 0)
81	77, 78, 78, 80, 80	divdivap1d 8985	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / (2 · 2)))
82		2t2e4 9281	. . . . . . . . . . 11 ⊢ (2 · 2) = 4
83	82	oveq2i 6021	. . . . . . . . . 10 ⊢ ((𝑃 − 1) / (2 · 2)) = ((𝑃 − 1) / 4)
84	81, 83	eqtrdi 2278	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (((𝑃 − 1) / 2) / 2) = ((𝑃 − 1) / 4))
85	84	eleq1d 2298	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((((𝑃 − 1) / 2) / 2) ∈ ℤ ↔ ((𝑃 − 1) / 4) ∈ ℤ))
86	76, 85	bitr4d 191	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (4 ∥ (𝑃 − 1) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
87		2ne0 9218	. . . . . . . 8 ⊢ 2 ≠ 0
88		dvdsval2 12322	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ ((𝑃 − 1) / 2) ∈ ℤ) → (2 ∥ ((𝑃 − 1) / 2) ↔ (((𝑃 − 1) / 2) / 2) ∈ ℤ))
89	14, 87, 30, 88	mp3an12i 1375	. . . . . . 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 9235	. . . . . . . . . . . 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 10824	. . . . . . . . . . 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 1272	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = ((-1↑2)↑(((𝑃 − 1) / 2) / 2)))
99	2	nncnd 9140	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℂ)
100	99, 78, 80	divcanap2d 8955	. . . . . . . . . . . 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 6026	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑(2 · (((𝑃 − 1) / 2) / 2))) = (-1↑((𝑃 − 1) / 2)))
103		neg1sqe1 10873	. . . . . . . . . . . 12 ⊢ (-1↑2) = 1
104	103	oveq1i 6020	. . . . . . . . . . 11 ⊢ ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = (1↑(((𝑃 − 1) / 2) / 2))
105		1exp 10807	. . . . . . . . . . . 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 2274	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑2)↑(((𝑃 − 1) / 2) / 2)) = 1)
108	98, 102, 107	3eqtr3d 2270	. . . . . . . . 9 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → (-1↑((𝑃 − 1) / 2)) = 1)
109	108	oveq1d 6025	. . . . . . . 8 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → ((-1↑((𝑃 − 1) / 2)) + 1) = (1 + 1))
110	26, 109	eqtr4id 2281	. . . . . . 7 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 4 ∥ (𝑃 − 1)) → 2 = ((-1↑((𝑃 − 1) / 2)) + 1))
111	110	oveq1d 6025	. . . . . 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 15718	. . . . 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 2238	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /_L 𝑃) = 1 ↔ ((((-1↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = 1))
118		4nn 9290	. . . . 5 ⊢ 4 ∈ ℕ
119	118	a1i 9	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 4 ∈ ℕ)
120	7, 18	syl 14	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
121		1zzd 9489	. . . 4 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 ∈ ℤ)
122		moddvds 12331	. . . 4 ⊢ ((4 ∈ ℕ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 mod 4) = (1 mod 4) ↔ 4 ∥ (𝑃 − 1)))
123	119, 120, 121, 122	syl3anc 1271	. . 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 9488	. . . . 5 ⊢ 1 ∈ ℤ
126		zq 9838	. . . . 5 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
127	125, 126	ax-mp 5	. . . 4 ⊢ 1 ∈ ℚ
128		zq 9838	. . . . 5 ⊢ (4 ∈ ℤ → 4 ∈ ℚ)
129	70, 128	ax-mp 5	. . . 4 ⊢ 4 ∈ ℚ
130		0le1 8644	. . . 4 ⊢ 0 ≤ 1
131		1lt4 9301	. . . 4 ⊢ 1 < 4
132		modqid 10588	. . . 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 2240	. 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 839 = wceq 1395 ∈ wcel 2200 ≠ wne 2400 ∖ cdif 3194 {csn 3666 class class class wbr 4083 ‘cfv 5321 (class class class)co 6010 ℂcc 8013 0cc0 8015 1c1 8016 + caddc 8018 · cmul 8020 < clt 8197 ≤ cle 8198 − cmin 8333 -cneg 8334 # cap 8744 / cdiv 8835 ℕcn 9126 2c2 9177 4c4 9179 ℕ₀cn0 9385 ℤcz 9462 ℤ_≥cuz 9738 ℚcq 9831 mod cmo 10561 ↑cexp 10777 ∥ cdvds 12319 ℙcprime 12650 /_L clgs 15697

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-nul 4210 ax-pow 4259 ax-pr 4294 ax-un 4525 ax-setind 4630 ax-iinf 4681 ax-cnex 8106 ax-resscn 8107 ax-1cn 8108 ax-1re 8109 ax-icn 8110 ax-addcl 8111 ax-addrcl 8112 ax-mulcl 8113 ax-mulrcl 8114 ax-addcom 8115 ax-mulcom 8116 ax-addass 8117 ax-mulass 8118 ax-distr 8119 ax-i2m1 8120 ax-0lt1 8121 ax-1rid 8122 ax-0id 8123 ax-rnegex 8124 ax-precex 8125 ax-cnre 8126 ax-pre-ltirr 8127 ax-pre-ltwlin 8128 ax-pre-lttrn 8129 ax-pre-apti 8130 ax-pre-ltadd 8131 ax-pre-mulgt0 8132 ax-pre-mulext 8133 ax-arch 8134 ax-caucvg 8135

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-xor 1418 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4385 df-po 4388 df-iso 4389 df-iord 4458 df-on 4460 df-ilim 4461 df-suc 4463 df-iom 4684 df-xp 4726 df-rel 4727 df-cnv 4728 df-co 4729 df-dm 4730 df-rn 4731 df-res 4732 df-ima 4733 df-iota 5281 df-fun 5323 df-fn 5324 df-f 5325 df-f1 5326 df-fo 5327 df-f1o 5328 df-fv 5329 df-isom 5330 df-riota 5963 df-ov 6013 df-oprab 6014 df-mpo 6015 df-1st 6295 df-2nd 6296 df-recs 6462 df-irdg 6527 df-frec 6548 df-1o 6573 df-2o 6574 df-oadd 6577 df-er 6693 df-en 6901 df-dom 6902 df-fin 6903 df-sup 7167 df-inf 7168 df-pnf 8199 df-mnf 8200 df-xr 8201 df-ltxr 8202 df-le 8203 df-sub 8335 df-neg 8336 df-reap 8738 df-ap 8745 df-div 8836 df-inn 9127 df-2 9185 df-3 9186 df-4 9187 df-5 9188 df-6 9189 df-7 9190 df-8 9191 df-n0 9386 df-z 9463 df-uz 9739 df-q 9832 df-rp 9867 df-fz 10222 df-fzo 10356 df-fl 10507 df-mod 10562 df-seqfrec 10687 df-exp 10778 df-ihash 11015 df-cj 11374 df-re 11375 df-im 11376 df-rsqrt 11530 df-abs 11531 df-clim 11811 df-proddc 12083 df-dvds 12320 df-gcd 12496 df-prm 12651 df-phi 12754 df-pc 12829 df-lgs 15698

This theorem is referenced by: (None)

W3C validator