Theorem 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 \mathbb{P}$$
	pockthi.g	$$⊢G\in \mathbb{N}$$
	pockthi.m	$$⊢M=GP$$
	pockthi.n	$$⊢N=M+1$$
	pockthi.d	$$⊢D\in \mathbb{N}$$
	pockthi.e	$$⊢E\in \mathbb{N}$$
	pockthi.a	$$⊢A\in \mathbb{N}$$
	pockthi.fac	$$⊢M=D{P}^E$$
	pockthi.gt	$$⊢D<P^E$$
	pockthi.mod	$$⊢A^M\mathrm{mod}N=1\mathrm{mod}N$$
	pockthi.gcd	$$⊢\left(A^G-1\right)\gcd N=1$$
Assertion	pockthi	$$⊢N\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		pockthi.p	$$⊢P\in \mathbb{P}$$
2		pockthi.g	$$⊢G\in \mathbb{N}$$
3		pockthi.m	$$⊢M=GP$$
4		pockthi.n	$$⊢N=M+1$$
5		pockthi.d	$$⊢D\in \mathbb{N}$$
6		pockthi.e	$$⊢E\in \mathbb{N}$$
7		pockthi.a	$$⊢A\in \mathbb{N}$$
8		pockthi.fac	$$⊢M=D{P}^E$$
9		pockthi.gt	$$⊢D<P^E$$
10		pockthi.mod	$$⊢A^M\mathrm{mod}N=1\mathrm{mod}N$$
11		pockthi.gcd	$$⊢\left(A^G-1\right)\gcd N=1$$
12		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
13	1 12	ax-mp	$$⊢P\in \mathbb{N}$$
14	6	nnnn0i	$$⊢E\in {\mathbb{N}}_0$$
15		nnexpcl	$$⊢\left(P\in \mathbb{N}\wedge E\in {\mathbb{N}}_0\right)\to P^E\in \mathbb{N}$$
16	13 14 15	mp2an	$$⊢P^E\in \mathbb{N}$$
17	16	a1i	$$⊢D\in \mathbb{N}\to P^E\in \mathbb{N}$$
18		id	$$⊢D\in \mathbb{N}\to D\in \mathbb{N}$$
19	9	a1i	$$⊢D\in \mathbb{N}\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 \mathbb{N}\to N=P^{E}D+1$$
27		prmdvdsexpb	$$⊢\left(x\in \mathbb{P}\wedge P\in \mathbb{P}\wedge E\in \mathbb{N}\right)\to \left(x\parallel P^E\leftrightarrow x=P\right)$$
28	1 6 27	mp3an23	$$⊢x\in \mathbb{P}\to \left(x\parallel P^E\leftrightarrow x=P\right)$$
29	2 13	nnmulcli	$$⊢GP\in \mathbb{N}$$
30	3 29	eqeltri	$$⊢M\in \mathbb{N}$$
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}\mathrm{mod}N=A^M\mathrm{mod}N$$
36		peano2nn	$$⊢M\in \mathbb{N}\to M+1\in \mathbb{N}$$
37	30 36	ax-mp	$$⊢M+1\in \mathbb{N}$$
38	4 37	eqeltri	$$⊢N\in \mathbb{N}$$
39	38	nnrei	$$⊢N\in ℝ$$
40	30	nngt0i	$$⊢0<M$$
41	30	nnrei	$$⊢M\in ℝ$$
42		1re	$$⊢1\in ℝ$$
43		ltaddpos2	$$⊢\left(M\in ℝ\wedge 1\in ℝ\right)\to \left(0<M\leftrightarrow 1<M+1\right)$$
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	$$⊢\left(N\in ℝ\wedge 1<N\right)\to 1\mathrm{mod}N=1$$
48	39 46 47	mp2an	$$⊢1\mathrm{mod}N=1$$
49	10 48	eqtri	$$⊢A^M\mathrm{mod}N=1$$
50	35 49	eqtri	$$⊢A^{N-1}\mathrm{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	$$⊢GP=PG$$
55	33 3 54	3eqtrri	$$⊢PG=N-1$$
56	38	nncni	$$⊢N\in ℂ$$
57	56 32	subcli	$$⊢N-1\in ℂ$$
58	13	nnne0i	$$⊢P\ne 0$$
59	57 53 52 58	divmuli	$$⊢\frac{N-1}{P}=G\leftrightarrow PG=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 \left(A^{\frac{N-1}{x}}-1\right)\gcd N=\left(A^G-1\right)\gcd N$$
65	64 11	eqtrdi	$$⊢x=P\to \left(A^{\frac{N-1}{x}}-1\right)\gcd N=1$$
66	7	nnzi	$$⊢A\in \mathbb{Z}$$
67		oveq1	$$⊢y=A\to y^{N-1}=A^{N-1}$$
68	67	oveq1d	$$⊢y=A\to y^{N-1}\mathrm{mod}N=A^{N-1}\mathrm{mod}N$$
69	68	eqeq1d	$$⊢y=A\to \left(y^{N-1}\mathrm{mod}N=1\leftrightarrow A^{N-1}\mathrm{mod}N=1\right)$$
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 \left(y^{\frac{N-1}{x}}-1\right)\gcd N=\left(A^{\frac{N-1}{x}}-1\right)\gcd N$$
73	72	eqeq1d	$$⊢y=A\to \left(\left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\leftrightarrow \left(A^{\frac{N-1}{x}}-1\right)\gcd N=1\right)$$
74	69 73	anbi12d	$$⊢y=A\to \left(\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\leftrightarrow \left(A^{N-1}\mathrm{mod}N=1\wedge \left(A^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\right)$$
75	74	rspcev	$$⊢\left(A\in \mathbb{Z}\wedge \left(A^{N-1}\mathrm{mod}N=1\wedge \left(A^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\right)\to \exists y\in \mathbb{Z}\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)$$
76	66 75	mpan	$$⊢\left(A^{N-1}\mathrm{mod}N=1\wedge \left(A^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\to \exists y\in \mathbb{Z}\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)$$
77	50 65 76	sylancr	$$⊢x=P\to \exists y\in \mathbb{Z}\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)$$
78	28 77	syl6bi	$$⊢x\in \mathbb{P}\to \left(x\parallel P^E\to \exists y\in \mathbb{Z}\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\right)$$
79	78	rgen	$$⊢\forall x\in \mathbb{P}\left(x\parallel P^E\to \exists y\in \mathbb{Z}\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\right)$$
80	79	a1i	$$⊢D\in \mathbb{N}\to \forall x\in \mathbb{P}\left(x\parallel P^E\to \exists y\in \mathbb{Z}\left(y^{N-1}\mathrm{mod}N=1\wedge \left(y^{\frac{N-1}{x}}-1\right)\gcd N=1\right)\right)$$
81	17 18 19 26 80	pockthg	$$⊢D\in \mathbb{N}\to N\in \mathbb{P}$$
82	5 81	ax-mp	$$⊢N\in \mathbb{P}$$