This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑁 ∈ ℙ )