pockthg

Description: The generalized Pocklington's theorem. If N - 1 = A x. B where B < A , then N is prime if and only if for every prime factor p of A , there is an x such that x ^ ( N - 1 ) = 1 ( mod N ) and gcd ( x ^ ( ( N - 1 ) / p ) - 1 , N ) = 1 . (Contributed by Mario Carneiro, 2-Mar-2014)

	Ref	Expression
Hypotheses	pockthg.1	$⊢ φ \to A \in ℕ$
	pockthg.2	$⊢ φ \to B \in ℕ$
	pockthg.3	$⊢ φ \to B < A$
	pockthg.4	$⊢ φ \to N = A B + 1$
	pockthg.5	$⊢ φ \to \forall p \in ℙ (p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))$
Assertion	pockthg	$⊢ φ \to N \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		pockthg.1	$⊢ φ \to A \in ℕ$
2		pockthg.2	$⊢ φ \to B \in ℕ$
3		pockthg.3	$⊢ φ \to B < A$
4		pockthg.4	$⊢ φ \to N = A B + 1$
5		pockthg.5	$⊢ φ \to \forall p \in ℙ (p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))$
6	1 2	nnmulcld	$⊢ φ \to A B \in ℕ$
7		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
8	6 7	eleqtrdi	$⊢ φ \to A B \in ℤ_{\geq 1}$
9		eluzp1p1	$⊢ A B \in ℤ_{\geq 1} \to A B + 1 \in ℤ_{\geq (1 + 1)}$
10	8 9	syl	$⊢ φ \to A B + 1 \in ℤ_{\geq (1 + 1)}$
11		df-2	$⊢ 2 = 1 + 1$
12	11	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
13	10 12	eleqtrrdi	$⊢ φ \to A B + 1 \in ℤ_{\geq 2}$
14	4 13	eqeltrd	$⊢ φ \to N \in ℤ_{\geq 2}$
15		eluzelre	$⊢ N \in ℤ_{\geq 2} \to N \in ℝ$
16	14 15	syl	$⊢ φ \to N \in ℝ$
17	16	adantr	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to N \in ℝ$
18	1	nnred	$⊢ φ \to A \in ℝ$
19	18	resqcld	$⊢ φ \to A^{2} \in ℝ$
20	19	adantr	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to A^{2} \in ℝ$
21		prmnn	$⊢ q \in ℙ \to q \in ℕ$
22	21	ad2antrl	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to q \in ℕ$
23	22	nnred	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to q \in ℝ$
24	23	resqcld	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to q^{2} \in ℝ$
25	2	nnred	$⊢ φ \to B \in ℝ$
26	1	nngt0d	$⊢ φ \to 0 < A$
27		ltmul2	$⊢ (B \in ℝ \land A \in ℝ \land (A \in ℝ \land 0 < A)) \to (B < A \leftrightarrow A B < A A)$
28	25 18 18 26 27	syl112anc	$⊢ φ \to (B < A \leftrightarrow A B < A A)$
29	3 28	mpbid	$⊢ φ \to A B < A A$
30	1 1	nnmulcld	$⊢ φ \to A A \in ℕ$
31		nnltp1le	$⊢ (A B \in ℕ \land A A \in ℕ) \to (A B < A A \leftrightarrow A B + 1 \leq A A)$
32	6 30 31	syl2anc	$⊢ φ \to (A B < A A \leftrightarrow A B + 1 \leq A A)$
33	29 32	mpbid	$⊢ φ \to A B + 1 \leq A A$
34	1	nncnd	$⊢ φ \to A \in ℂ$
35	34	sqvald	$⊢ φ \to A^{2} = A A$
36	33 4 35	3brtr4d	$⊢ φ \to N \leq A^{2}$
37	36	adantr	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to N \leq A^{2}$
38	5	adantr	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to \forall p \in ℙ (p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))$
39		prmnn	$⊢ p \in ℙ \to p \in ℕ$
40	39	ad2antrl	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to p \in ℕ$
41	40	nncnd	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to p \in ℂ$
42	41	exp1d	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to p^{1} = p$
43		nnge1	$⊢ p pCnt A \in ℕ \to 1 \leq p pCnt A$
44	43	ad2antll	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to 1 \leq p pCnt A$
45		simprl	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to p \in ℙ$
46	1	nnzd	$⊢ φ \to A \in ℤ$
47	46	ad2antrr	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to A \in ℤ$
48		1nn0	$⊢ 1 \in ℕ_{0}$
49	48	a1i	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to 1 \in ℕ_{0}$
50		pcdvdsb	$⊢ (p \in ℙ \land A \in ℤ \land 1 \in ℕ_{0}) \to (1 \leq p pCnt A \leftrightarrow p^{1} ∥ A)$
51	45 47 49 50	syl3anc	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to (1 \leq p pCnt A \leftrightarrow p^{1} ∥ A)$
52	44 51	mpbid	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to p^{1} ∥ A$
53	42 52	eqbrtrrd	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to p ∥ A$
54		simpl1	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to φ$
55	54 1	syl	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to A \in ℕ$
56	54 2	syl	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to B \in ℕ$
57	54 3	syl	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to B < A$
58	54 4	syl	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to N = A B + 1$
59		simpl2l	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to q \in ℙ$
60		simpl2r	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to q ∥ N$
61		simpl3l	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to p \in ℙ$
62		simpl3r	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to p pCnt A \in ℕ$
63		simprl	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to x \in ℤ$
64		simprrl	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to x^{N - 1} \mod N = 1$
65		simprrr	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to (x^{\frac{N - 1}{p}} - 1) \gcd N = 1$
66	55 56 57 58 59 60 61 62 63 64 65	pockthlem	$⊢ ((φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \land (x \in ℤ \land (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1))) \to p pCnt A \leq p pCnt (q - 1)$
67	66	rexlimdvaa	$⊢ (φ \land (q \in ℙ \land q ∥ N) \land (p \in ℙ \land p pCnt A \in ℕ)) \to (\exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1) \to p pCnt A \leq p pCnt (q - 1))$
68	67	3expa	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to (\exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1) \to p pCnt A \leq p pCnt (q - 1))$
69	53 68	embantd	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land (p \in ℙ \land p pCnt A \in ℕ)) \to ((p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1)) \to p pCnt A \leq p pCnt (q - 1))$
70	69	expr	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to (p pCnt A \in ℕ \to ((p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1)) \to p pCnt A \leq p pCnt (q - 1)))$
71		id	$⊢ p \in ℙ \to p \in ℙ$
72		prmuz2	$⊢ q \in ℙ \to q \in ℤ_{\geq 2}$
73		uz2m1nn	$⊢ q \in ℤ_{\geq 2} \to q - 1 \in ℕ$
74	72 73	syl	$⊢ q \in ℙ \to q - 1 \in ℕ$
75	74	ad2antrl	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to q - 1 \in ℕ$
76		pccl	$⊢ (p \in ℙ \land q - 1 \in ℕ) \to p pCnt (q - 1) \in ℕ_{0}$
77	71 75 76	syl2anr	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to p pCnt (q - 1) \in ℕ_{0}$
78	77	nn0ge0d	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to 0 \leq p pCnt (q - 1)$
79		breq1	$⊢ p pCnt A = 0 \to (p pCnt A \leq p pCnt (q - 1) \leftrightarrow 0 \leq p pCnt (q - 1))$
80	78 79	syl5ibrcom	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to (p pCnt A = 0 \to p pCnt A \leq p pCnt (q - 1))$
81	80	a1dd	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to (p pCnt A = 0 \to ((p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1)) \to p pCnt A \leq p pCnt (q - 1)))$
82		simpr	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to p \in ℙ$
83	1	ad2antrr	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to A \in ℕ$
84	82 83	pccld	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to p pCnt A \in ℕ_{0}$
85		elnn0	$⊢ p pCnt A \in ℕ_{0} \leftrightarrow (p pCnt A \in ℕ \lor p pCnt A = 0)$
86	84 85	sylib	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to (p pCnt A \in ℕ \lor p pCnt A = 0)$
87	70 81 86	mpjaod	$⊢ ((φ \land (q \in ℙ \land q ∥ N)) \land p \in ℙ) \to ((p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1)) \to p pCnt A \leq p pCnt (q - 1))$
88	87	ralimdva	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to (\forall p \in ℙ (p ∥ A \to \exists x \in ℤ (x^{N - 1} \mod N = 1 \land (x^{\frac{N - 1}{p}} - 1) \gcd N = 1)) \to \forall p \in ℙ p pCnt A \leq p pCnt (q - 1))$
89	38 88	mpd	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to \forall p \in ℙ p pCnt A \leq p pCnt (q - 1)$
90	75	nnzd	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to q - 1 \in ℤ$
91		pc2dvds	$⊢ (A \in ℤ \land q - 1 \in ℤ) \to (A ∥ (q - 1) \leftrightarrow \forall p \in ℙ p pCnt A \leq p pCnt (q - 1))$
92	46 90 91	syl2an2r	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to (A ∥ (q - 1) \leftrightarrow \forall p \in ℙ p pCnt A \leq p pCnt (q - 1))$
93	89 92	mpbird	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to A ∥ (q - 1)$
94		dvdsle	$⊢ (A \in ℤ \land q - 1 \in ℕ) \to (A ∥ (q - 1) \to A \leq q - 1)$
95	46 75 94	syl2an2r	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to (A ∥ (q - 1) \to A \leq q - 1)$
96	93 95	mpd	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to A \leq q - 1$
97	1	nnnn0d	$⊢ φ \to A \in ℕ_{0}$
98	22	nnnn0d	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to q \in ℕ_{0}$
99		nn0ltlem1	$⊢ (A \in ℕ_{0} \land q \in ℕ_{0}) \to (A < q \leftrightarrow A \leq q - 1)$
100	97 98 99	syl2an2r	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to (A < q \leftrightarrow A \leq q - 1)$
101	96 100	mpbird	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to A < q$
102	18	adantr	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to A \in ℝ$
103	97	nn0ge0d	$⊢ φ \to 0 \leq A$
104	103	adantr	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to 0 \leq A$
105	98	nn0ge0d	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to 0 \leq q$
106	102 23 104 105	lt2sqd	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to (A < q \leftrightarrow A^{2} < q^{2})$
107	101 106	mpbid	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to A^{2} < q^{2}$
108	17 20 24 37 107	lelttrd	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to N < q^{2}$
109	17 24	ltnled	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to (N < q^{2} \leftrightarrow \neg q^{2} \leq N)$
110	108 109	mpbid	$⊢ (φ \land (q \in ℙ \land q ∥ N)) \to \neg q^{2} \leq N$
111	110	expr	$⊢ (φ \land q \in ℙ) \to (q ∥ N \to \neg q^{2} \leq N)$
112	111	con2d	$⊢ (φ \land q \in ℙ) \to (q^{2} \leq N \to \neg q ∥ N)$
113	112	ralrimiva	$⊢ φ \to \forall q \in ℙ (q^{2} \leq N \to \neg q ∥ N)$
114		isprm5	$⊢ N \in ℙ \leftrightarrow (N \in ℤ_{\geq 2} \land \forall q \in ℙ (q^{2} \leq N \to \neg q ∥ N))$
115	14 113 114	sylanbrc	$⊢ φ \to N \in ℙ$

Metamath Proof Explorer

Theorem pockthg

Proof