lgslem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgslem1		Structured version Visualization version GIF version

Theorem lgslem1 27681

Description: When 𝑎 is coprime to the prime 𝑝, 𝑎↑((𝑝 − 1) / 2) is equivalent mod 𝑝 to 1 or -1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.)

**Assertion**
Ref	Expression
lgslem1	⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2})

**Proof of Theorem lgslem1**
Step	Hyp	Ref	Expression
1		eldifi 4070	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
2	1	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℙ)
3		prmnn 16893	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
4	2, 3	syl 18	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ)
5		simp1 1154	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ)
6		prmz 16894	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7	2, 6	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ)
8	5, 7	gcdcomd 16730	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴))
9		simp3 1156	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 𝐴)
10		coprm 16931	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1))
11	2, 5, 10	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1))
12	9, 11	mpbid 235	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1)
13	8, 12	eqtrd 2798	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1)
14		eulerth 17004	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
15	4, 5, 13, 14	syl3anc 1399	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
16		phiprm 16998	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
17	2, 16	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1))
18		nnm1nn0 12687	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
19	4, 18	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈ ℕ₀)
20	17, 19	eqeltrd 2864	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈ ℕ₀)
21		zexpcl 14259	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ (ϕ‘𝑃) ∈ ℕ₀) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ)
22	5, 20, 21	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ)
23		1zzd 12767	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈ ℤ)
24		moddvds 16477	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)))
25	4, 22, 23, 24	syl3anc 1399	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)))
26	15, 25	mpbid 235	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))
27	19	nn0cnd 12709	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈ ℂ)
28		2cnd 12461	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈ ℂ)
29		2ne0 12489	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
30	29	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 ≠ 0)
31	27, 28, 30	divcan1d 12134	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1))
32	17, 31	eqtr4d 2801	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (((𝑃 − 1) / 2) · 2))
33	32	oveq2d 7467	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(((𝑃 − 1) / 2) · 2)))
34	5	zcnd 12844	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ)
35		2nn0 12663	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
36	35	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈ ℕ₀)
37		oddprm 17032	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
38	37	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈ ℕ)
39	38	nnnn0d 12707	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈ ℕ₀)
40	34, 36, 39	expmuld 14332	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(((𝑃 − 1) / 2) · 2)) = ((𝐴↑((𝑃 − 1) / 2))↑2))
41	33, 40	eqtrd 2798	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = ((𝐴↑((𝑃 − 1) / 2))↑2))
42	41	oveq1d 7466	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) − 1))
43		sq1 14378	. . . . . . . 8 ⊢ (1↑2) = 1
44	43	oveq2i 7462	. . . . . . 7 ⊢ (((𝐴↑((𝑃 − 1) / 2))↑2) − (1↑2)) = (((𝐴↑((𝑃 − 1) / 2))↑2) − 1)
45	42, 44	eqtr4di 2816	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) − (1↑2)))
46		zexpcl 14259	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℤ)
47	5, 39, 46	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℤ)
48	47	zcnd 12844	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈ ℂ)
49		ax-1cn 11297	. . . . . . 7 ⊢ 1 ∈ ℂ
50		subsq 14394	. . . . . . 7 ⊢ (((𝐴↑((𝑃 − 1) / 2)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2))↑2) − (1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)))
51	48, 49, 50	sylancl 598	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2))↑2) − (1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)))
52	45, 51	eqtrd 2798	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)))
53	26, 52	breqtrd 5137	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)))
54	47	peano2zd 12846	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
55		peano2zm 12779	. . . . . 6 ⊢ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ → ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈ ℤ)
56	47, 55	syl 18	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈ ℤ)
57		euclemma 16933	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧ ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈ ℤ) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1))))
58	2, 54, 56, 57	syl3anc 1399	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1))))
59	53, 58	mpbid 235	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)))
60		dvdsval3 16470	. . . . 5 ⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0))
61	4, 54, 60	syl2anc 596	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0))
62		2z 12768	. . . . . . 7 ⊢ 2 ∈ ℤ
63	62	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈ ℤ)
64		moddvds 16477	. . . . . 6 ⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧ 2 ∈ ℤ) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2)))
65	4, 54, 63, 64	syl3anc 1399	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2)))
66		2re 12457	. . . . . . . 8 ⊢ 2 ∈ ℝ
67	66	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈ ℝ)
68	4	nnrpd 13202	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ⁺)
69		0le2 12485	. . . . . . . 8 ⊢ 0 ≤ 2
70	69	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 0 ≤ 2)
71	4	nnred 12390	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ)
72		prmuz2 16915	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
73	2, 72	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ (ℤ_≥‘2))
74		eluzle 13018	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℤ_≥‘2) → 2 ≤ 𝑃)
75	73, 74	syl 18	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 ≤ 𝑃)
76		eldifsni 4755	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
77	76	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ≠ 2)
78	67, 71, 75, 77	leneltd 11503	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 2 < 𝑃)
79		modid 14076	. . . . . . 7 ⊢ (((2 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2)
80	67, 68, 70, 78, 79	syl22anc 852	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (2 mod 𝑃) = 2)
81	80	eqeq2d 2774	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))
82		df-2 12445	. . . . . . . 8 ⊢ 2 = (1 + 1)
83	82	oveq2i 7462	. . . . . . 7 ⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 + 1))
84	49	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈ ℂ)
85	48, 84, 84	pnpcan2d 11746	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 + 1)) = ((𝐴↑((𝑃 − 1) / 2)) − 1))
86	83, 85	eqtrid 2810	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = ((𝐴↑((𝑃 − 1) / 2)) − 1))
87	86	breq2d 5120	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) ↔ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)))
88	65, 81, 87	3bitr3rd 313	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))
89	61, 88	orbi12d 932	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)))
90	59, 89	mpbid 235	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))
91		ovex 7484	. . 3 ⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ V
92	91	elpr 4609	. 2 ⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} ↔ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))
93	90, 92	sylibr 237	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2})

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∖ cdif 4048 {csn 4588 {cpr 4590 class class class wbr 5108 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 < clt 11382 ≤ cle 11383 − cmin 11580 / cdiv 12013 ℕcn 12375 2c2 12437 ℕ₀cn0 12646 ℤcz 12733 ℤ_≥cuz 13005 ℝ⁺crp 13160 mod cmo 14049 ↑cexp 14244 ∥ cdvds 16466 gcd cgcd 16708 ℙcprime 16890 ϕcphi 16985

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-oadd 8518 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-sup 9471 df-inf 9472 df-dju 10019 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-n0 12647 df-xnn0 12720 df-z 12734 df-uz 13006 df-rp 13161 df-fz 13680 df-fzo 13829 df-fl 13972 df-mod 14050 df-seq 14185 df-exp 14245 df-hash 14516 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-dvds 16467 df-gcd 16709 df-prm 16891 df-phi 16987

This theorem is used by: lgslem4 27684

W3C validator