Metamath Proof Explorer

Theorem aks4d1p7d1

Description: Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024)

Ref Expression
Hypotheses aks4d1p7d1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p7d1.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p7d1.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p7d1.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
aks4d1p7d1.5 ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
Assertion aks4d1p7d1 ( 𝜑 → 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p7d1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p7d1.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p7d1.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p7d1.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 aks4d1p7d1.5 ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
6 simp2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑅 ) → 𝑝 ∈ ℙ )
7 1 2 3 4 aks4d1p4 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
8 7 simpld ⊢ ( 𝜑 → 𝑅 ∈ ( 1 ... 𝐵 ) )
9 elfznn ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ∈ ℕ )
10 8 9 syl ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
11 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑅 ) → 𝑅 ∈ ℕ )
12 6 11 pccld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ∈ ℕ0 )
13 12 3expa ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ∈ ℕ0 )
14 13 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ∈ ℝ )
15 2re ⊢ 2 ∈ ℝ
16 15 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
17 2pos ⊢ 0 < 2
18 17 a1i ⊢ ( 𝜑 → 0 < 2 )
19 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
20 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
21 1 20 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 21 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
23 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
24 3re ⊢ 3 ∈ ℝ
25 24 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
26 3pos ⊢ 0 < 3
27 26 a1i ⊢ ( 𝜑 → 0 < 3 )
28 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
29 1 28 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
30 23 25 22 27 29 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
31 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
32 1lt2 ⊢ 1 < 2
33 32 a1i ⊢ ( 𝜑 → 1 < 2 )
34 31 33 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
35 34 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
36 16 18 22 30 35 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
37 5nn0 ⊢ 5 ∈ ℕ0
38 37 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
39 36 38 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
40 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
41 39 40 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
42 41 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
43 19 42 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
44 9re ⊢ 9 ∈ ℝ
45 44 a1i ⊢ ( 𝜑 → 9 ∈ ℝ )
46 9pos ⊢ 0 < 9
47 46 a1i ⊢ ( 𝜑 → 0 < 9 )
48 22 29 3lexlogpow5ineq4 ⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
49 23 45 39 47 48 lttrd ⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
50 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
51 39 50 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
52 23 39 42 49 51 ltletrd ⊢ ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
53 52 19 breqtrrd ⊢ ( 𝜑 → 0 < 𝐵 )
54 16 18 43 53 35 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
55 54 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
56 55 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ )
58 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 𝑝 ∈ ℙ )
59 21 30 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
60 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
61 59 60 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 𝑁 ∈ ℕ )
63 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
64 63 addlidd ⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
65 16 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
66 23 18 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
67 logbid1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
68 65 66 35 67 syl3anc ⊢ ( 𝜑 → ( 2 logb 2 ) = 1 )
69 68 eqcomd ⊢ ( 𝜑 → 1 = ( 2 logb 2 ) )
70 64 69 eqtrd ⊢ ( 𝜑 → ( 0 + 1 ) = ( 2 logb 2 ) )
71 2z ⊢ 2 ∈ ℤ
72 71 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
73 16 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
74 2lt9 ⊢ 2 < 9
75 74 a1i ⊢ ( 𝜑 → 2 < 9 )
76 16 45 75 ltled ⊢ ( 𝜑 → 2 ≤ 9 )
77 45 39 42 48 51 ltletrd ⊢ ( 𝜑 → 9 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
78 77 19 breqtrrd ⊢ ( 𝜑 → 9 < 𝐵 )
79 45 43 78 ltled ⊢ ( 𝜑 → 9 ≤ 𝐵 )
80 16 45 43 76 79 letrd ⊢ ( 𝜑 → 2 ≤ 𝐵 )
81 72 73 16 18 43 53 80 logblebd ⊢ ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝐵 ) )
82 70 81 eqbrtrd ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( 2 logb 𝐵 ) )
83 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
84 83 peano2zd ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℤ )
85 flge ⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ ( 0 + 1 ) ∈ ℤ ) → ( ( 0 + 1 ) ≤ ( 2 logb 𝐵 ) ↔ ( 0 + 1 ) ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
86 54 84 85 syl2anc ⊢ ( 𝜑 → ( ( 0 + 1 ) ≤ ( 2 logb 𝐵 ) ↔ ( 0 + 1 ) ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
87 82 86 mpbid ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
88 83 55 zltp1led ⊢ ( 𝜑 → ( 0 < ( ⌊ ‘ ( 2 logb 𝐵 ) ) ↔ ( 0 + 1 ) ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
89 87 88 mpbird ⊢ ( 𝜑 → 0 < ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
90 55 89 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
91 elnnz ⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
92 90 91 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ )
93 92 nnnn0d ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
94 93 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
95 62 94 nnexpcld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℕ )
96 58 95 pccld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) ∈ ℕ0 )
97 96 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) ∈ ℝ )
98 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑅 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
99 simp3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑅 ) → 𝑝 ∥ 𝑅 )
100 eqid ⊢ ( 𝑝 pCnt 𝑅 ) = ( 𝑝 pCnt 𝑅 )
101 98 2 3 4 6 99 100 aks4d1p6 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
102 101 3expa ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
103 58 62 pccld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑁 ) ∈ ℕ0 )
104 103 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑁 ) ∈ ℝ )
105 23 56 89 ltled ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
108 rsp ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) → ( 𝑝 ∈ ℙ → ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ) )
109 5 108 syl ⊢ ( 𝜑 → ( 𝑝 ∈ ℙ → ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ) )
110 109 imp ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
111 110 imp ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 𝑝 ∥ 𝑁 )
112 61 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ )
113 112 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 𝑁 ∈ ℕ )
114 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑁 ) ∈ ℕ ↔ 𝑝 ∥ 𝑁 ) )
115 58 113 114 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( ( 𝑝 pCnt 𝑁 ) ∈ ℕ ↔ 𝑝 ∥ 𝑁 ) )
116 111 115 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑁 ) ∈ ℕ )
117 nnge1 ⊢ ( ( 𝑝 pCnt 𝑁 ) ∈ ℕ → 1 ≤ ( 𝑝 pCnt 𝑁 ) )
118 116 117 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 1 ≤ ( 𝑝 pCnt 𝑁 ) )
119 57 104 107 118 lemulge11d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ≤ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) · ( 𝑝 pCnt 𝑁 ) ) )
120 zq ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℚ )
121 21 120 syl ⊢ ( 𝜑 → 𝑁 ∈ ℚ )
122 61 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
123 121 122 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) )
125 124 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) )
126 55 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
127 126 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
128 pcexp ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) ∧ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ) → ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) = ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) · ( 𝑝 pCnt 𝑁 ) ) )
129 58 125 127 128 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) = ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) · ( 𝑝 pCnt 𝑁 ) ) )
130 119 129 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
131 14 57 97 102 130 letrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
132 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ¬ 𝑝 ∥ 𝑅 )
133 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → 𝑝 ∈ ℙ )
134 10 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑅 ∈ ℕ )
135 134 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → 𝑅 ∈ ℕ )
136 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑅 ) = 0 ↔ ¬ 𝑝 ∥ 𝑅 ) )
137 133 135 136 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ( ( 𝑝 pCnt 𝑅 ) = 0 ↔ ¬ 𝑝 ∥ 𝑅 ) )
138 132 137 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) = 0 )
139 112 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → 𝑁 ∈ ℕ )
140 93 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
142 139 141 nnexpcld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℕ )
143 133 142 pccld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) ∈ ℕ0 )
144 143 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → 0 ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
145 138 144 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ∥ 𝑅 ) → ( 𝑝 pCnt 𝑅 ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
146 131 145 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑅 ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
147 146 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑅 ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
148 8 elfzelzd ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
149 21 93 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ )
150 pc2dvds ⊢ ( ( 𝑅 ∈ ℤ ∧ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ ) → ( 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑅 ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) ) )
151 148 149 150 syl2anc ⊢ ( 𝜑 → ( 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑅 ) ≤ ( 𝑝 pCnt ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) ) )
152 147 151 mpbird ⊢ ( 𝜑 → 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )