proththd

Description: Proth's theorem (1878). If P is aProth 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 aProth prime. Like Pocklington's theorem (see pockthg ), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020)

	Ref	Expression
Hypotheses	proththd.n	$⊢ φ \to N \in ℕ$
	proththd.k	$⊢ φ \to K \in ℕ$
	proththd.p	$⊢ φ \to P = K 2^{N} + 1$
	proththd.l	$⊢ φ \to K < 2^{N}$
	proththd.x	$⊢ φ \to \exists x \in ℤ x^{\frac{P - 1}{2}} \mod P = -1 \mod P$
Assertion	proththd	$⊢ φ \to P \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		proththd.n	$⊢ φ \to N \in ℕ$
2		proththd.k	$⊢ φ \to K \in ℕ$
3		proththd.p	$⊢ φ \to P = K 2^{N} + 1$
4		proththd.l	$⊢ φ \to K < 2^{N}$
5		proththd.x	$⊢ φ \to \exists x \in ℤ x^{\frac{P - 1}{2}} \mod P = -1 \mod P$
6		2nn	$⊢ 2 \in ℕ$
7	6	a1i	$⊢ φ \to 2 \in ℕ$
8	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
9	7 8	nnexpcld	$⊢ φ \to 2^{N} \in ℕ$
10	2	nncnd	$⊢ φ \to K \in ℂ$
11	9	nncnd	$⊢ φ \to 2^{N} \in ℂ$
12	10 11	mulcomd	$⊢ φ \to K 2^{N} = 2^{N} K$
13	12	oveq1d	$⊢ φ \to K 2^{N} + 1 = 2^{N} K + 1$
14	3 13	eqtrd	$⊢ φ \to P = 2^{N} K + 1$
15		simpr	$⊢ (φ \land p \in ℙ) \to p \in ℙ$
16		2prm	$⊢ 2 \in ℙ$
17	16	a1i	$⊢ (φ \land p \in ℙ) \to 2 \in ℙ$
18	1	adantr	$⊢ (φ \land p \in ℙ) \to N \in ℕ$
19		prmdvdsexpb	$⊢ (p \in ℙ \land 2 \in ℙ \land N \in ℕ) \to (p ∥ 2^{N} \leftrightarrow p = 2)$
20	15 17 18 19	syl3anc	$⊢ (φ \land p \in ℙ) \to (p ∥ 2^{N} \leftrightarrow p = 2)$
21	1 2 3	proththdlem	$⊢ φ \to (P \in ℕ \land 1 < P \land \frac{P - 1}{2} \in ℕ)$
22	21	simp1d	$⊢ φ \to P \in ℕ$
23	22	nncnd	$⊢ φ \to P \in ℂ$
24		peano2cnm	$⊢ P \in ℂ \to P - 1 \in ℂ$
25	23 24	syl	$⊢ φ \to P - 1 \in ℂ$
26	25	adantr	$⊢ (φ \land x \in ℤ) \to P - 1 \in ℂ$
27		2cnd	$⊢ (φ \land x \in ℤ) \to 2 \in ℂ$
28		2ne0	$⊢ 2 \neq 0$
29	28	a1i	$⊢ (φ \land x \in ℤ) \to 2 \neq 0$
30	26 27 29	divcan1d	$⊢ (φ \land x \in ℤ) \to (\frac{P - 1}{2}) \cdot 2 = P - 1$
31	30	eqcomd	$⊢ (φ \land x \in ℤ) \to P - 1 = (\frac{P - 1}{2}) \cdot 2$
32	31	oveq2d	$⊢ (φ \land x \in ℤ) \to x^{P - 1} = x^{(\frac{P - 1}{2}) \cdot 2}$
33		zcn	$⊢ x \in ℤ \to x \in ℂ$
34	33	adantl	$⊢ (φ \land x \in ℤ) \to x \in ℂ$
35		2nn0	$⊢ 2 \in ℕ_{0}$
36	35	a1i	$⊢ (φ \land x \in ℤ) \to 2 \in ℕ_{0}$
37	21	simp3d	$⊢ φ \to \frac{P - 1}{2} \in ℕ$
38	37	nnnn0d	$⊢ φ \to \frac{P - 1}{2} \in ℕ_{0}$
39	38	adantr	$⊢ (φ \land x \in ℤ) \to \frac{P - 1}{2} \in ℕ_{0}$
40	34 36 39	expmuld	$⊢ (φ \land x \in ℤ) \to x^{(\frac{P - 1}{2}) \cdot 2} = {(x^{\frac{P - 1}{2}})}^{2}$
41	32 40	eqtrd	$⊢ (φ \land x \in ℤ) \to x^{P - 1} = {(x^{\frac{P - 1}{2}})}^{2}$
42	41	ad4ant13	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{P - 1} = {(x^{\frac{P - 1}{2}})}^{2}$
43	42	oveq1d	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{P - 1} \mod P = {(x^{\frac{P - 1}{2}})}^{2} \mod P$
44	38	adantr	$⊢ (φ \land p = 2) \to \frac{P - 1}{2} \in ℕ_{0}$
45	44	anim1i	$⊢ ((φ \land p = 2) \land x \in ℤ) \to (\frac{P - 1}{2} \in ℕ_{0} \land x \in ℤ)$
46	45	ancomd	$⊢ ((φ \land p = 2) \land x \in ℤ) \to (x \in ℤ \land \frac{P - 1}{2} \in ℕ_{0})$
47		zexpcl	$⊢ (x \in ℤ \land \frac{P - 1}{2} \in ℕ_{0}) \to x^{\frac{P - 1}{2}} \in ℤ$
48	46 47	syl	$⊢ ((φ \land p = 2) \land x \in ℤ) \to x^{\frac{P - 1}{2}} \in ℤ$
49	48	adantr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{\frac{P - 1}{2}} \in ℤ$
50	22	nnrpd	$⊢ φ \to P \in ℝ^{+}$
51	50	ad3antrrr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to P \in ℝ^{+}$
52	21	simp2d	$⊢ φ \to 1 < P$
53	52	ad3antrrr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to 1 < P$
54		simpr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{\frac{P - 1}{2}} \mod P = -1 \mod P$
55	49 51 53 54	modexp2m1d	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to {(x^{\frac{P - 1}{2}})}^{2} \mod P = 1$
56	43 55	eqtrd	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{P - 1} \mod P = 1$
57		oveq2	$⊢ p = 2 \to \frac{P - 1}{p} = \frac{P - 1}{2}$
58	57	eleq1d	$⊢ p = 2 \to (\frac{P - 1}{p} \in ℕ_{0} \leftrightarrow \frac{P - 1}{2} \in ℕ_{0})$
59	58	adantl	$⊢ (φ \land p = 2) \to (\frac{P - 1}{p} \in ℕ_{0} \leftrightarrow \frac{P - 1}{2} \in ℕ_{0})$
60	44 59	mpbird	$⊢ (φ \land p = 2) \to \frac{P - 1}{p} \in ℕ_{0}$
61	60	anim2i	$⊢ (x \in ℤ \land (φ \land p = 2)) \to (x \in ℤ \land \frac{P - 1}{p} \in ℕ_{0})$
62	61	ancoms	$⊢ ((φ \land p = 2) \land x \in ℤ) \to (x \in ℤ \land \frac{P - 1}{p} \in ℕ_{0})$
63		zexpcl	$⊢ (x \in ℤ \land \frac{P - 1}{p} \in ℕ_{0}) \to x^{\frac{P - 1}{p}} \in ℤ$
64	62 63	syl	$⊢ ((φ \land p = 2) \land x \in ℤ) \to x^{\frac{P - 1}{p}} \in ℤ$
65	64	zred	$⊢ ((φ \land p = 2) \land x \in ℤ) \to x^{\frac{P - 1}{p}} \in ℝ$
66	65	adantr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{\frac{P - 1}{p}} \in ℝ$
67		1red	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to 1 \in ℝ$
68	67	renegcld	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to - 1 \in ℝ$
69		oveq2	$⊢ 2 = p \to \frac{P - 1}{2} = \frac{P - 1}{p}$
70	69	eqcoms	$⊢ p = 2 \to \frac{P - 1}{2} = \frac{P - 1}{p}$
71	70	oveq2d	$⊢ p = 2 \to x^{\frac{P - 1}{2}} = x^{\frac{P - 1}{p}}$
72	71	oveq1d	$⊢ p = 2 \to x^{\frac{P - 1}{2}} \mod P = x^{\frac{P - 1}{p}} \mod P$
73	72	eqeq1d	$⊢ p = 2 \to (x^{\frac{P - 1}{2}} \mod P = -1 \mod P \leftrightarrow x^{\frac{P - 1}{p}} \mod P = -1 \mod P)$
74	73	adantl	$⊢ (φ \land p = 2) \to (x^{\frac{P - 1}{2}} \mod P = -1 \mod P \leftrightarrow x^{\frac{P - 1}{p}} \mod P = -1 \mod P)$
75	74	adantr	$⊢ ((φ \land p = 2) \land x \in ℤ) \to (x^{\frac{P - 1}{2}} \mod P = -1 \mod P \leftrightarrow x^{\frac{P - 1}{p}} \mod P = -1 \mod P)$
76	75	biimpa	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to x^{\frac{P - 1}{p}} \mod P = -1 \mod P$
77		eqidd	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to 1 \mod P = 1 \mod P$
78	66 68 67 67 51 76 77	modsub12d	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to (x^{\frac{P - 1}{p}} - 1) \mod P = (- 1 - 1) \mod P$
79	78	oveq1d	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to ((x^{\frac{P - 1}{p}} - 1) \mod P) \gcd P = ((- 1 - 1) \mod P) \gcd P$
80		peano2zm	$⊢ x^{\frac{P - 1}{p}} \in ℤ \to x^{\frac{P - 1}{p}} - 1 \in ℤ$
81	64 80	syl	$⊢ ((φ \land p = 2) \land x \in ℤ) \to x^{\frac{P - 1}{p}} - 1 \in ℤ$
82	22	ad2antrr	$⊢ ((φ \land p = 2) \land x \in ℤ) \to P \in ℕ$
83		modgcd	$⊢ (x^{\frac{P - 1}{p}} - 1 \in ℤ \land P \in ℕ) \to ((x^{\frac{P - 1}{p}} - 1) \mod P) \gcd P = (x^{\frac{P - 1}{p}} - 1) \gcd P$
84	81 82 83	syl2anc	$⊢ ((φ \land p = 2) \land x \in ℤ) \to ((x^{\frac{P - 1}{p}} - 1) \mod P) \gcd P = (x^{\frac{P - 1}{p}} - 1) \gcd P$
85	84	adantr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to ((x^{\frac{P - 1}{p}} - 1) \mod P) \gcd P = (x^{\frac{P - 1}{p}} - 1) \gcd P$
86		ax-1cn	$⊢ 1 \in ℂ$
87		negdi2	$⊢ (1 \in ℂ \land 1 \in ℂ) \to - (1 + 1) = - 1 - 1$
88	87	eqcomd	$⊢ (1 \in ℂ \land 1 \in ℂ) \to - 1 - 1 = - (1 + 1)$
89	86 86 88	mp2an	$⊢ - 1 - 1 = - (1 + 1)$
90		1p1e2	$⊢ 1 + 1 = 2$
91	90	negeqi	$⊢ - (1 + 1) = - 2$
92	89 91	eqtri	$⊢ - 1 - 1 = - 2$
93	92	a1i	$⊢ φ \to - 1 - 1 = - 2$
94	93	oveq1d	$⊢ φ \to (- 1 - 1) \mod P = -2 \mod P$
95	94	oveq1d	$⊢ φ \to ((- 1 - 1) \mod P) \gcd P = (-2 \mod P) \gcd P$
96		nnnegz	$⊢ 2 \in ℕ \to - 2 \in ℤ$
97	7 96	syl	$⊢ φ \to - 2 \in ℤ$
98		modgcd	$⊢ (- 2 \in ℤ \land P \in ℕ) \to (-2 \mod P) \gcd P = -2 \gcd P$
99	97 22 98	syl2anc	$⊢ φ \to (-2 \mod P) \gcd P = -2 \gcd P$
100		2z	$⊢ 2 \in ℤ$
101	22	nnzd	$⊢ φ \to P \in ℤ$
102		neggcd	$⊢ (2 \in ℤ \land P \in ℤ) \to -2 \gcd P = 2 \gcd P$
103	100 101 102	sylancr	$⊢ φ \to -2 \gcd P = 2 \gcd P$
104		nnz	$⊢ P \in ℕ \to P \in ℤ$
105		oddm1d2	$⊢ P \in ℤ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
106	104 105	syl	$⊢ P \in ℕ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
107	106	biimprd	$⊢ P \in ℕ \to (\frac{P - 1}{2} \in ℤ \to \neg 2 ∥ P)$
108		nnz	$⊢ \frac{P - 1}{2} \in ℕ \to \frac{P - 1}{2} \in ℤ$
109	107 108	impel	$⊢ (P \in ℕ \land \frac{P - 1}{2} \in ℕ) \to \neg 2 ∥ P$
110		isoddgcd1	$⊢ P \in ℤ \to (\neg 2 ∥ P \leftrightarrow 2 \gcd P = 1)$
111	104 110	syl	$⊢ P \in ℕ \to (\neg 2 ∥ P \leftrightarrow 2 \gcd P = 1)$
112	111	adantr	$⊢ (P \in ℕ \land \frac{P - 1}{2} \in ℕ) \to (\neg 2 ∥ P \leftrightarrow 2 \gcd P = 1)$
113	109 112	mpbid	$⊢ (P \in ℕ \land \frac{P - 1}{2} \in ℕ) \to 2 \gcd P = 1$
114	113	3adant2	$⊢ (P \in ℕ \land 1 < P \land \frac{P - 1}{2} \in ℕ) \to 2 \gcd P = 1$
115	21 114	syl	$⊢ φ \to 2 \gcd P = 1$
116	103 115	eqtrd	$⊢ φ \to -2 \gcd P = 1$
117	99 116	eqtrd	$⊢ φ \to (-2 \mod P) \gcd P = 1$
118	95 117	eqtrd	$⊢ φ \to ((- 1 - 1) \mod P) \gcd P = 1$
119	118	ad3antrrr	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to ((- 1 - 1) \mod P) \gcd P = 1$
120	79 85 119	3eqtr3d	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to (x^{\frac{P - 1}{p}} - 1) \gcd P = 1$
121	56 120	jca	$⊢ (((φ \land p = 2) \land x \in ℤ) \land x^{\frac{P - 1}{2}} \mod P = -1 \mod P) \to (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1)$
122	121	ex	$⊢ ((φ \land p = 2) \land x \in ℤ) \to (x^{\frac{P - 1}{2}} \mod P = -1 \mod P \to (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1))$
123	122	reximdva	$⊢ (φ \land p = 2) \to (\exists x \in ℤ x^{\frac{P - 1}{2}} \mod P = -1 \mod P \to \exists x \in ℤ (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1))$
124	123	ex	$⊢ φ \to (p = 2 \to (\exists x \in ℤ x^{\frac{P - 1}{2}} \mod P = -1 \mod P \to \exists x \in ℤ (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1)))$
125	5 124	mpid	$⊢ φ \to (p = 2 \to \exists x \in ℤ (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1))$
126	125	adantr	$⊢ (φ \land p \in ℙ) \to (p = 2 \to \exists x \in ℤ (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1))$
127	20 126	sylbid	$⊢ (φ \land p \in ℙ) \to (p ∥ 2^{N} \to \exists x \in ℤ (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1))$
128	127	ralrimiva	$⊢ φ \to \forall p \in ℙ (p ∥ 2^{N} \to \exists x \in ℤ (x^{P - 1} \mod P = 1 \land (x^{\frac{P - 1}{p}} - 1) \gcd P = 1))$
129	9 2 4 14 128	pockthg	$⊢ φ \to P \in ℙ$

Metamath Proof Explorer

Theorem proththd

Proof