pockthi

Description: Pocklington's theorem, which gives a sufficient criterion for a number N to be prime. This is the preferred method for verifying large primes, being much more efficient to compute than trial division. This form has been optimized for application to specific large primes; see pockthg for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014)

	Ref	Expression
Hypotheses	pockthi.p	$⊢ P \in ℙ$
	pockthi.g	$⊢ G \in ℕ$
	pockthi.m	$⊢ M = G P$
	pockthi.n	$⊢ N = M + 1$
	pockthi.d	$⊢ D \in ℕ$
	pockthi.e	$⊢ E \in ℕ$
	pockthi.a	$⊢ A \in ℕ$
	pockthi.fac	$⊢ M = D P^{E}$
	pockthi.gt	$⊢ D < P^{E}$
	pockthi.mod	$⊢ A^{M} \mod N = 1 \mod N$
	pockthi.gcd	$⊢ (A^{G} - 1) \gcd N = 1$
Assertion	pockthi	$⊢ N \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		pockthi.p	$⊢ P \in ℙ$
2		pockthi.g	$⊢ G \in ℕ$
3		pockthi.m	$⊢ M = G P$
4		pockthi.n	$⊢ N = M + 1$
5		pockthi.d	$⊢ D \in ℕ$
6		pockthi.e	$⊢ E \in ℕ$
7		pockthi.a	$⊢ A \in ℕ$
8		pockthi.fac	$⊢ M = D P^{E}$
9		pockthi.gt	$⊢ D < P^{E}$
10		pockthi.mod	$⊢ A^{M} \mod N = 1 \mod N$
11		pockthi.gcd	$⊢ (A^{G} - 1) \gcd N = 1$
12		prmnn	$⊢ P \in ℙ \to P \in ℕ$
13	1 12	ax-mp	$⊢ P \in ℕ$
14	6	nnnn0i	$⊢ E \in ℕ_{0}$
15		nnexpcl	$⊢ (P \in ℕ \land E \in ℕ_{0}) \to P^{E} \in ℕ$
16	13 14 15	mp2an	$⊢ P^{E} \in ℕ$
17	16	a1i	$⊢ D \in ℕ \to P^{E} \in ℕ$
18		id	$⊢ D \in ℕ \to D \in ℕ$
19	9	a1i	$⊢ D \in ℕ \to D < P^{E}$
20	5	nncni	$⊢ D \in ℂ$
21	16	nncni	$⊢ P^{E} \in ℂ$
22	20 21	mulcomi	$⊢ D P^{E} = P^{E} D$
23	8 22	eqtri	$⊢ M = P^{E} D$
24	23	oveq1i	$⊢ M + 1 = P^{E} D + 1$
25	4 24	eqtri	$⊢ N = P^{E} D + 1$
26	25	a1i	$⊢ D \in ℕ \to N = P^{E} D + 1$
27		prmdvdsexpb	$⊢ (x \in ℙ \land P \in ℙ \land E \in ℕ) \to (x ∥ P^{E} \leftrightarrow x = P)$
28	1 6 27	mp3an23	$⊢ x \in ℙ \to (x ∥ P^{E} \leftrightarrow x = P)$
29	2 13	nnmulcli	$⊢ G P \in ℕ$
30	3 29	eqeltri	$⊢ M \in ℕ$
31	30	nncni	$⊢ M \in ℂ$
32		ax-1cn	$⊢ 1 \in ℂ$
33	31 32 4	mvrraddi	$⊢ N - 1 = M$
34	33	oveq2i	$⊢ A^{N - 1} = A^{M}$
35	34	oveq1i	$⊢ A^{N - 1} \mod N = A^{M} \mod N$
36		peano2nn	$⊢ M \in ℕ \to M + 1 \in ℕ$
37	30 36	ax-mp	$⊢ M + 1 \in ℕ$
38	4 37	eqeltri	$⊢ N \in ℕ$
39	38	nnrei	$⊢ N \in ℝ$
40	30	nngt0i	$⊢ 0 < M$
41	30	nnrei	$⊢ M \in ℝ$
42		1re	$⊢ 1 \in ℝ$
43		ltaddpos2	$⊢ (M \in ℝ \land 1 \in ℝ) \to (0 < M \leftrightarrow 1 < M + 1)$
44	41 42 43	mp2an	$⊢ 0 < M \leftrightarrow 1 < M + 1$
45	40 44	mpbi	$⊢ 1 < M + 1$
46	45 4	breqtrri	$⊢ 1 < N$
47		1mod	$⊢ (N \in ℝ \land 1 < N) \to 1 \mod N = 1$
48	39 46 47	mp2an	$⊢ 1 \mod N = 1$
49	10 48	eqtri	$⊢ A^{M} \mod N = 1$
50	35 49	eqtri	$⊢ A^{N - 1} \mod N = 1$
51		oveq2	$⊢ x = P \to \frac{N - 1}{x} = \frac{N - 1}{P}$
52	2	nncni	$⊢ G \in ℂ$
53	13	nncni	$⊢ P \in ℂ$
54	52 53	mulcomi	$⊢ G P = P G$
55	33 3 54	3eqtrri	$⊢ P G = N - 1$
56	38	nncni	$⊢ N \in ℂ$
57	56 32	subcli	$⊢ N - 1 \in ℂ$
58	13	nnne0i	$⊢ P \neq 0$
59	57 53 52 58	divmuli	$⊢ \frac{N - 1}{P} = G \leftrightarrow P G = N - 1$
60	55 59	mpbir	$⊢ \frac{N - 1}{P} = G$
61	51 60	eqtrdi	$⊢ x = P \to \frac{N - 1}{x} = G$
62	61	oveq2d	$⊢ x = P \to A^{\frac{N - 1}{x}} = A^{G}$
63	62	oveq1d	$⊢ x = P \to A^{\frac{N - 1}{x}} - 1 = A^{G} - 1$
64	63	oveq1d	$⊢ x = P \to (A^{\frac{N - 1}{x}} - 1) \gcd N = (A^{G} - 1) \gcd N$
65	64 11	eqtrdi	$⊢ x = P \to (A^{\frac{N - 1}{x}} - 1) \gcd N = 1$
66	7	nnzi	$⊢ A \in ℤ$
67		oveq1	$⊢ y = A \to y^{N - 1} = A^{N - 1}$
68	67	oveq1d	$⊢ y = A \to y^{N - 1} \mod N = A^{N - 1} \mod N$
69	68	eqeq1d	$⊢ y = A \to (y^{N - 1} \mod N = 1 \leftrightarrow A^{N - 1} \mod N = 1)$
70		oveq1	$⊢ y = A \to y^{\frac{N - 1}{x}} = A^{\frac{N - 1}{x}}$
71	70	oveq1d	$⊢ y = A \to y^{\frac{N - 1}{x}} - 1 = A^{\frac{N - 1}{x}} - 1$
72	71	oveq1d	$⊢ y = A \to (y^{\frac{N - 1}{x}} - 1) \gcd N = (A^{\frac{N - 1}{x}} - 1) \gcd N$
73	72	eqeq1d	$⊢ y = A \to ((y^{\frac{N - 1}{x}} - 1) \gcd N = 1 \leftrightarrow (A^{\frac{N - 1}{x}} - 1) \gcd N = 1)$
74	69 73	anbi12d	$⊢ y = A \to ((y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1) \leftrightarrow (A^{N - 1} \mod N = 1 \land (A^{\frac{N - 1}{x}} - 1) \gcd N = 1))$
75	74	rspcev	$⊢ (A \in ℤ \land (A^{N - 1} \mod N = 1 \land (A^{\frac{N - 1}{x}} - 1) \gcd N = 1)) \to \exists y \in ℤ (y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1)$
76	66 75	mpan	$⊢ (A^{N - 1} \mod N = 1 \land (A^{\frac{N - 1}{x}} - 1) \gcd N = 1) \to \exists y \in ℤ (y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1)$
77	50 65 76	sylancr	$⊢ x = P \to \exists y \in ℤ (y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1)$
78	28 77	biimtrdi	$⊢ x \in ℙ \to (x ∥ P^{E} \to \exists y \in ℤ (y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1))$
79	78	rgen	$⊢ \forall x \in ℙ (x ∥ P^{E} \to \exists y \in ℤ (y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1))$
80	79	a1i	$⊢ D \in ℕ \to \forall x \in ℙ (x ∥ P^{E} \to \exists y \in ℤ (y^{N - 1} \mod N = 1 \land (y^{\frac{N - 1}{x}} - 1) \gcd N = 1))$
81	17 18 19 26 80	pockthg	$⊢ D \in ℕ \to N \in ℙ$
82	5 81	ax-mp	$⊢ N \in ℙ$

Metamath Proof Explorer

Theorem pockthi

Proof