proththd - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > proththd		Structured version Visualization version GIF version

Theorem proththd 44954

Description: Proth's theorem (1878). If P is a Proth number, i.e. a number of the form k2^n+1 with k less than 2^n, and if there exists an integer x for which x^((P-1)/2) is -1 modulo P, then P is prime. Such a prime is called a Proth prime. Like Pocklington's theorem (see pockthg 16535), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020.)

**Hypotheses**
Ref	Expression
proththd.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
proththd.k	⊢ (𝜑 → 𝐾 ∈ ℕ)
proththd.p	⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))
proththd.l	⊢ (𝜑 → 𝐾 < (2↑𝑁))
proththd.x	⊢ (𝜑 → ∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃))

**Assertion**
Ref	Expression
proththd	⊢ (𝜑 → 𝑃 ∈ ℙ)

Distinct variable groups: 𝑥,𝑁 𝑥,𝑃 𝜑,𝑥 Allowed substitution hint: 𝐾(𝑥)

Proof of Theorem proththd Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn 11976	. . . 4 ⊢ 2 ∈ ℕ
2	1	a1i 11	. . 3 ⊢ (𝜑 → 2 ∈ ℕ)
3		proththd.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4	3	nnnn0d 12223	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
5	2, 4	nnexpcld 13888	. 2 ⊢ (𝜑 → (2↑𝑁) ∈ ℕ)
6		proththd.k	. 2 ⊢ (𝜑 → 𝐾 ∈ ℕ)
7		proththd.l	. 2 ⊢ (𝜑 → 𝐾 < (2↑𝑁))
8		proththd.p	. . 3 ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))
9	6	nncnd 11919	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
10	5	nncnd 11919	. . . . 5 ⊢ (𝜑 → (2↑𝑁) ∈ ℂ)
11	9, 10	mulcomd 10927	. . . 4 ⊢ (𝜑 → (𝐾 · (2↑𝑁)) = ((2↑𝑁) · 𝐾))
12	11	oveq1d 7270	. . 3 ⊢ (𝜑 → ((𝐾 · (2↑𝑁)) + 1) = (((2↑𝑁) · 𝐾) + 1))
13	8, 12	eqtrd 2778	. 2 ⊢ (𝜑 → 𝑃 = (((2↑𝑁) · 𝐾) + 1))
14		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
15		2prm 16325	. . . . . 6 ⊢ 2 ∈ ℙ
16	15	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈ ℙ)
17	3	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
18		prmdvdsexpb 16349	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ (2↑𝑁) ↔ 𝑝 = 2))
19	14, 16, 17, 18	syl3anc 1369	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) ↔ 𝑝 = 2))
20		proththd.x	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃))
21	3, 6, 8	proththdlem 44953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ))
22	21	simp1d 1140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℕ)
23	22	nncnd 11919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℂ)
24		peano2cnm 11217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℂ → (𝑃 − 1) ∈ ℂ)
25	23, 24	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
26	25	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) ∈ ℂ)
27		2cnd 11981	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈ ℂ)
28		2ne0 12007	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ≠ 0)
30	26, 27, 29	divcan1d 11682	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1))
31	30	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) = (((𝑃 − 1) / 2) · 2))
32	31	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = (𝑥↑(((𝑃 − 1) / 2) · 2)))
33		zcn 12254	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
34	33	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ)
35		2nn0 12180	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ₀
36	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈ ℕ₀)
37	21	simp3d 1142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
38	37	nnnn0d 12223	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
39	38	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑃 − 1) / 2) ∈ ℕ₀)
40	34, 36, 39	expmuld 13795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(((𝑃 − 1) / 2) · 2)) = ((𝑥↑((𝑃 − 1) / 2))↑2))
41	32, 40	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2))
42	41	ad4ant13 747	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2))
43	42	oveq1d 7270	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃))
44	38	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 2) ∈ ℕ₀)
45	44	anim1i 614	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑥 ∈ ℤ))
46	45	ancomd 461	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀))
47		zexpcl 13725	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (𝑥↑((𝑃 − 1) / 2)) ∈ ℤ)
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 2)) ∈ ℤ)
49	48	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 2)) ∈ ℤ)
50	22	nnrpd 12699	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℝ⁺)
51	50	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 𝑃 ∈ ℝ⁺)
52	21	simp2d 1141	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 𝑃)
53	52	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 < 𝑃)
54		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃))
55	49, 51, 53, 54	modexp2m1d 44952	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃) = 1)
56	43, 55	eqtrd 2778	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = 1)
57		oveq2 7263	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 2 → ((𝑃 − 1) / 𝑝) = ((𝑃 − 1) / 2))
58	57	eleq1d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 2 → (((𝑃 − 1) / 𝑝) ∈ ℕ₀ ↔ ((𝑃 − 1) / 2) ∈ ℕ₀))
59	58	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑃 − 1) / 𝑝) ∈ ℕ₀ ↔ ((𝑃 − 1) / 2) ∈ ℕ₀))
60	44, 59	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 𝑝) ∈ ℕ₀)
61	60	anim2i 616	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝜑 ∧ 𝑝 = 2)) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ₀))
62	61	ancoms 458	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ₀))
63		zexpcl 13725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ₀) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ)
64	62, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ)
65	64	zred 12355	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ)
66	65	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ)
67		1red 10907	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 ∈ ℝ)
68	67	renegcld 11332	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → -1 ∈ ℝ)
69		oveq2 7263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 = 𝑝 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝))
70	69	eqcoms 2746	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 2 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝))
71	70	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 2 → (𝑥↑((𝑃 − 1) / 2)) = (𝑥↑((𝑃 − 1) / 𝑝)))
72	71	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 2 → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃))
73	72	eqeq1d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 2 → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃)))
74	73	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃)))
75	74	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃)))
76	75	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))
77		eqidd 2739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (1 mod 𝑃) = (1 mod 𝑃))
78	66, 68, 67, 67, 51, 76, 77	modsub12d 13576	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) = ((-1 − 1) mod 𝑃))
79	78	oveq1d 7270	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((-1 − 1) mod 𝑃) gcd 𝑃))
80		peano2zm 12293	. . . . . . . . . . . . . 14 ⊢ ((𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ)
81	64, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ)
82	22	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → 𝑃 ∈ ℕ)
83		modgcd 16168	. . . . . . . . . . . . 13 ⊢ ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃))
84	81, 82, 83	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃))
85	84	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃))
86		ax-1cn 10860	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
87		negdi2 11209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ) → -(1 + 1) = (-1 − 1))
88	87	eqcomd 2744	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ) → (-1 − 1) = -(1 + 1))
89	86, 86, 88	mp2an 688	. . . . . . . . . . . . . . . . 17 ⊢ (-1 − 1) = -(1 + 1)
90		1p1e2 12028	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
91	90	negeqi 11144	. . . . . . . . . . . . . . . . 17 ⊢ -(1 + 1) = -2
92	89, 91	eqtri 2766	. . . . . . . . . . . . . . . 16 ⊢ (-1 − 1) = -2
93	92	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 − 1) = -2)
94	93	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((-1 − 1) mod 𝑃) = (-2 mod 𝑃))
95	94	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = ((-2 mod 𝑃) gcd 𝑃))
96		nnnegz 12252	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → -2 ∈ ℤ)
97	2, 96	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -2 ∈ ℤ)
98		modgcd 16168	. . . . . . . . . . . . . . 15 ⊢ ((-2 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃))
99	97, 22, 98	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃))
100		2z 12282	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
101	22	nnzd 12354	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
102		neggcd 16158	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (-2 gcd 𝑃) = (2 gcd 𝑃))
103	100, 101, 102	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-2 gcd 𝑃) = (2 gcd 𝑃))
104		nnz 12272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℤ)
105		oddm1d2 15997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (¬ 2 ∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈ ℤ))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → (¬ 2 ∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈ ℤ))
107	106	biimprd 247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℕ → (((𝑃 − 1) / 2) ∈ ℤ → ¬ 2 ∥ 𝑃))
108		nnz 12272	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 − 1) / 2) ∈ ℕ → ((𝑃 − 1) / 2) ∈ ℤ)
109	107, 108	impel 505	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → ¬ 2 ∥ 𝑃)
110		isoddgcd1 16363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℤ → (¬ 2 ∥ 𝑃 ↔ (2 gcd 𝑃) = 1))
111	104, 110	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℕ → (¬ 2 ∥ 𝑃 ↔ (2 gcd 𝑃) = 1))
112	111	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (¬ 2 ∥ 𝑃 ↔ (2 gcd 𝑃) = 1))
113	109, 112	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (2 gcd 𝑃) = 1)
114	113	3adant2 1129	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (2 gcd 𝑃) = 1)
115	21, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 gcd 𝑃) = 1)
116	103, 115	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-2 gcd 𝑃) = 1)
117	99, 116	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = 1)
118	95, 117	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1)
119	118	ad3antrrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1)
120	79, 85, 119	3eqtr3d 2786	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)
121	56, 120	jca 511	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))
122	121	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
123	122	reximdva 3202	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 = 2) → (∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
124	123	ex 412	. . . . . 6 ⊢ (𝜑 → (𝑝 = 2 → (∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))))
125	20, 124	mpid 44	. . . . 5 ⊢ (𝜑 → (𝑝 = 2 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
126	125	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 = 2 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
127	19, 126	sylbid 239	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
128	127	ralrimiva 3107	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
129	5, 6, 7, 13, 128	pockthg 16535	1 ⊢ (𝜑 → 𝑃 ∈ ℙ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 class class class wbr 5070 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤcz 12249 ℝ⁺crp 12659 mod cmo 13517 ↑cexp 13710 ∥ cdvds 15891 gcd cgcd 16129 ℙcprime 16304

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892 df-gcd 16130 df-prm 16305 df-odz 16394 df-phi 16395 df-pc 16466

This theorem is referenced by: 41prothprm 44959

W3C validator