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 47968

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 16846), 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 12230	. . . 4 ⊢ 2 ∈ ℕ
2	1	a1i 11	. . 3 ⊢ (𝜑 → 2 ∈ ℕ)
3		proththd.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4	3	nnnn0d 12474	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
5	2, 4	nnexpcld 14180	. 2 ⊢ (𝜑 → (2↑𝑁) ∈ ℕ)
6		proththd.k	. 2 ⊢ (𝜑 → 𝐾 ∈ ℕ)
7		proththd.l	. 2 ⊢ (𝜑 → 𝐾 < (2↑𝑁))
8		proththd.p	. . 3 ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))
9	6	nncnd 12173	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
10	5	nncnd 12173	. . . . 5 ⊢ (𝜑 → (2↑𝑁) ∈ ℂ)
11	9, 10	mulcomd 11165	. . . 4 ⊢ (𝜑 → (𝐾 · (2↑𝑁)) = ((2↑𝑁) · 𝐾))
12	11	oveq1d 7383	. . 3 ⊢ (𝜑 → ((𝐾 · (2↑𝑁)) + 1) = (((2↑𝑁) · 𝐾) + 1))
13	8, 12	eqtrd 2772	. 2 ⊢ (𝜑 → 𝑃 = (((2↑𝑁) · 𝐾) + 1))
14		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
15		2prm 16631	. . . . . 6 ⊢ 2 ∈ ℙ
16	15	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈ ℙ)
17	3	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
18		prmdvdsexpb 16655	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ (2↑𝑁) ↔ 𝑝 = 2))
19	14, 16, 17, 18	syl3anc 1374	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) ↔ 𝑝 = 2))
20		proththd.x	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃))
21	3, 6, 8	proththdlem 47967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ))
22	21	simp1d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 ∈ ℕ)
23	22	nncnd 12173	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℂ)
24		peano2cnm 11459	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℂ → (𝑃 − 1) ∈ ℂ)
25	23, 24	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
26	25	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) ∈ ℂ)
27		2cnd 12235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈ ℂ)
28		2ne0 12261	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ≠ 0)
30	26, 27, 29	divcan1d 11930	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1))
31	30	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) = (((𝑃 − 1) / 2) · 2))
32	31	oveq2d 7384	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = (𝑥↑(((𝑃 − 1) / 2) · 2)))
33		zcn 12505	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
34	33	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ)
35		2nn0 12430	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ₀
36	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈ ℕ₀)
37	21	simp3d 1145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
38	37	nnnn0d 12474	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
39	38	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑃 − 1) / 2) ∈ ℕ₀)
40	34, 36, 39	expmuld 14084	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(((𝑃 − 1) / 2) · 2)) = ((𝑥↑((𝑃 − 1) / 2))↑2))
41	32, 40	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2))
42	41	ad4ant13 752	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2))
43	42	oveq1d 7383	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃))
44	38	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 2) ∈ ℕ₀)
45	44	anim1i 616	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑥 ∈ ℤ))
46	45	ancomd 461	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀))
47		zexpcl 14011	. . . . . . . . . . . . . 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 12959	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℝ⁺)
51	50	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 𝑃 ∈ ℝ⁺)
52	21	simp2d 1144	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 𝑃)
53	52	ad3antrrr 731	. . . . . . . . . . . 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 47966	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃) = 1)
56	43, 55	eqtrd 2772	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = 1)
57		oveq2 7376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 2 → ((𝑃 − 1) / 𝑝) = ((𝑃 − 1) / 2))
58	57	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 2 → (((𝑃 − 1) / 𝑝) ∈ ℕ₀ ↔ ((𝑃 − 1) / 2) ∈ ℕ₀))
59	58	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑃 − 1) / 𝑝) ∈ ℕ₀ ↔ ((𝑃 − 1) / 2) ∈ ℕ₀))
60	44, 59	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 𝑝) ∈ ℕ₀)
61	60	anim2i 618	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝜑 ∧ 𝑝 = 2)) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ₀))
62	61	ancoms 458	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ₀))
63		zexpcl 14011	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ₀) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ)
64	62, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ)
65	64	zred 12608	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ)
66	65	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ)
67		1red 11145	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 ∈ ℝ)
68	67	renegcld 11576	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → -1 ∈ ℝ)
69		oveq2 7376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 = 𝑝 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝))
70	69	eqcoms 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 2 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝))
71	70	oveq2d 7384	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 2 → (𝑥↑((𝑃 − 1) / 2)) = (𝑥↑((𝑃 − 1) / 𝑝)))
72	71	oveq1d 7383	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 2 → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃))
73	72	eqeq1d 2739	. . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (1 mod 𝑃) = (1 mod 𝑃))
78	66, 68, 67, 67, 51, 76, 77	modsub12d 13863	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) = ((-1 − 1) mod 𝑃))
79	78	oveq1d 7383	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((-1 − 1) mod 𝑃) gcd 𝑃))
80		peano2zm 12546	. . . . . . . . . . . . . 14 ⊢ ((𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ)
81	64, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ)
82	22	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → 𝑃 ∈ ℕ)
83		modgcd 16471	. . . . . . . . . . . . 13 ⊢ ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃))
84	81, 82, 83	syl2anc 585	. . . . . . . . . . . 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 11096	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
87		negdi2 11451	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ) → -(1 + 1) = (-1 − 1))
88	87	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ) → (-1 − 1) = -(1 + 1))
89	86, 86, 88	mp2an 693	. . . . . . . . . . . . . . . . 17 ⊢ (-1 − 1) = -(1 + 1)
90		1p1e2 12277	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
91	90	negeqi 11385	. . . . . . . . . . . . . . . . 17 ⊢ -(1 + 1) = -2
92	89, 91	eqtri 2760	. . . . . . . . . . . . . . . 16 ⊢ (-1 − 1) = -2
93	92	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 − 1) = -2)
94	93	oveq1d 7383	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((-1 − 1) mod 𝑃) = (-2 mod 𝑃))
95	94	oveq1d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = ((-2 mod 𝑃) gcd 𝑃))
96		nnnegz 12503	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → -2 ∈ ℤ)
97	2, 96	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -2 ∈ ℤ)
98		modgcd 16471	. . . . . . . . . . . . . . 15 ⊢ ((-2 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃))
99	97, 22, 98	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃))
100		2z 12535	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
101	22	nnzd 12526	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
102		neggcd 16462	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (-2 gcd 𝑃) = (2 gcd 𝑃))
103	100, 101, 102	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-2 gcd 𝑃) = (2 gcd 𝑃))
104		nnz 12521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℤ)
105		oddm1d2 16299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (¬ 2 ∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈ ℤ))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → (¬ 2 ∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈ ℤ))
107	106	biimprd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℕ → (((𝑃 − 1) / 2) ∈ ℤ → ¬ 2 ∥ 𝑃))
108		nnz 12521	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 − 1) / 2) ∈ ℕ → ((𝑃 − 1) / 2) ∈ ℤ)
109	107, 108	impel 505	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → ¬ 2 ∥ 𝑃)
110		isoddgcd1 16670	. . . . . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (2 gcd 𝑃) = 1)
114	113	3adant2 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (2 gcd 𝑃) = 1)
115	21, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 gcd 𝑃) = 1)
116	103, 115	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-2 gcd 𝑃) = 1)
117	99, 116	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = 1)
118	95, 117	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1)
119	118	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1)
120	79, 85, 119	3eqtr3d 2780	. . . . . . . . . 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 3151	. . . . . . 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 240	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
128	127	ralrimiva 3130	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))
129	5, 6, 7, 13, 128	pockthg 16846	1 ⊢ (𝜑 → 𝑃 ∈ ℙ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 class class class wbr 5100 (class class class)co 7368 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11178 − cmin 11376 -cneg 11377 / cdiv 11806 ℕcn 12157 2c2 12212 ℕ₀cn0 12413 ℤcz 12500 ℝ⁺crp 12917 mod cmo 13801 ↑cexp 13996 ∥ cdvds 16191 gcd cgcd 16433 ℙcprime 16610

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-oadd 8411 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-xnn0 12487 df-z 12501 df-uz 12764 df-q 12874 df-rp 12918 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-dvds 16192 df-gcd 16434 df-prm 16611 df-odz 16704 df-phi 16705 df-pc 16777

This theorem is referenced by: 41prothprm 47973

W3C validator