Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	pockthg.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	pockthg.3	⊢ ( 𝜑 → 𝐵 < 𝐴 )
	pockthg.4	⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 · 𝐵 ) + 1 ) )
	pockthg.5	⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑁 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑁 ) = 1 ) ) )
Assertion	pockthg	⊢ ( 𝜑 → 𝑁 ∈ ℙ )

Proof

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