Metamath Proof Explorer


Theorem aks4d1p1p2

Description: Rewrite A in more suitable form. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p2.1 ( 𝜑𝑁 ∈ ℕ )
aks4d1p1p2.2 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) )
aks4d1p1p2.3 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p1p2.4 ( 𝜑 → 3 ≤ 𝑁 )
Assertion aks4d1p1p2 ( 𝜑𝐴 < ( 𝑁𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p2.1 ( 𝜑𝑁 ∈ ℕ )
2 aks4d1p1p2.2 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) )
3 aks4d1p1p2.3 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p1p2.4 ( 𝜑 → 3 ≤ 𝑁 )
5 1 nnred ( 𝜑𝑁 ∈ ℝ )
6 2re 2 ∈ ℝ
7 6 a1i ( 𝜑 → 2 ∈ ℝ )
8 2pos 0 < 2
9 8 a1i ( 𝜑 → 0 < 2 )
10 1 nngt0d ( 𝜑 → 0 < 𝑁 )
11 1red ( 𝜑 → 1 ∈ ℝ )
12 1lt2 1 < 2
13 12 a1i ( 𝜑 → 1 < 2 )
14 11 13 ltned ( 𝜑 → 1 ≠ 2 )
15 14 necomd ( 𝜑 → 2 ≠ 1 )
16 7 9 5 10 15 relogbcld ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
17 5nn0 5 ∈ ℕ0
18 17 a1i ( 𝜑 → 5 ∈ ℕ0 )
19 16 18 reexpcld ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
20 ceilcl ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
21 19 20 syl ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
22 21 zred ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
23 3 a1i ( 𝜑𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
24 23 eleq1d ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ ) )
25 22 24 mpbird ( 𝜑𝐵 ∈ ℝ )
26 0red ( 𝜑 → 0 ∈ ℝ )
27 18 nn0zd ( 𝜑 → 5 ∈ ℤ )
28 3re 3 ∈ ℝ
29 28 a1i ( 𝜑 → 3 ∈ ℝ )
30 1lt3 1 < 3
31 30 a1i ( 𝜑 → 1 < 3 )
32 11 29 5 31 4 ltletrd ( 𝜑 → 1 < 𝑁 )
33 5 10 elrpd ( 𝜑𝑁 ∈ ℝ+ )
34 2rp 2 ∈ ℝ+
35 34 12 pm3.2i ( 2 ∈ ℝ+ ∧ 1 < 2 )
36 35 a1i ( 𝜑 → ( 2 ∈ ℝ+ ∧ 1 < 2 ) )
37 logbgt0b ( ( 𝑁 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) → ( 0 < ( 2 logb 𝑁 ) ↔ 1 < 𝑁 ) )
38 33 36 37 syl2anc ( 𝜑 → ( 0 < ( 2 logb 𝑁 ) ↔ 1 < 𝑁 ) )
39 32 38 mpbird ( 𝜑 → 0 < ( 2 logb 𝑁 ) )
40 expgt0 ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 𝑁 ) ) → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
41 16 27 39 40 syl3anc ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
42 ceilge ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
43 19 42 syl ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
44 26 19 22 41 43 ltletrd ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
45 23 breq2d ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) )
46 44 45 mpbird ( 𝜑 → 0 < 𝐵 )
47 7 9 25 46 15 relogbcld ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
48 47 flcld ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
49 7re 7 ∈ ℝ
50 49 a1i ( 𝜑 → 7 ∈ ℝ )
51 1lt7 1 < 7
52 51 a1i ( 𝜑 → 1 < 7 )
53 5 4 3lexlogpow5ineq3 ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
54 11 50 19 52 53 lttrd ( 𝜑 → 1 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
55 11 19 22 54 43 ltletrd ( 𝜑 → 1 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
56 23 breq2d ( 𝜑 → ( 1 < 𝐵 ↔ 1 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) )
57 55 56 mpbird ( 𝜑 → 1 < 𝐵 )
58 25 46 elrpd ( 𝜑𝐵 ∈ ℝ+ )
59 logbgt0b ( ( 𝐵 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) → ( 0 < ( 2 logb 𝐵 ) ↔ 1 < 𝐵 ) )
60 58 36 59 syl2anc ( 𝜑 → ( 0 < ( 2 logb 𝐵 ) ↔ 1 < 𝐵 ) )
61 57 60 mpbird ( 𝜑 → 0 < ( 2 logb 𝐵 ) )
62 26 47 61 ltled ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) )
63 0zd ( 𝜑 → 0 ∈ ℤ )
64 flge ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
65 47 63 64 syl2anc ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
66 62 65 mpbid ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
67 48 66 jca ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
68 elnn0z ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
69 67 68 sylibr ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
70 5 69 reexpcld ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ )
71 fzfid ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
72 5 adantr ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℝ )
73 elfznn ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
74 73 adantl ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
75 nnnn0 ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
76 74 75 syl ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
77 72 76 reexpcld ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁𝑘 ) ∈ ℝ )
78 1red ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℝ )
79 77 78 resubcld ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁𝑘 ) − 1 ) ∈ ℝ )
80 71 79 fprodrecl ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ∈ ℝ )
81 70 80 remulcld ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ) ∈ ℝ )
82 2 a1i ( 𝜑𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ) )
83 82 eleq1d ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ) ∈ ℝ ) )
84 81 83 mpbird ( 𝜑𝐴 ∈ ℝ )
85 1 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
86 85 nn0ge0d ( 𝜑 → 0 ≤ 𝑁 )
87 19 11 readdcld ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ∈ ℝ )
88 19 ltp1d ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
89 26 19 87 41 88 lttrd ( 𝜑 → 0 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
90 7 9 87 89 15 relogbcld ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℝ )
91 16 resqcld ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ )
92 91 flcld ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ )
93 92 zred ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ )
94 0lt1 0 < 1
95 94 a1i ( 𝜑 → 0 < 1 )
96 7 9 7 9 15 relogbcld ( 𝜑 → ( 2 logb 2 ) ∈ ℝ )
97 96 resqcld ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ∈ ℝ )
98 2nn0 2 ∈ ℕ0
99 98 a1i ( 𝜑 → 2 ∈ ℕ0 )
100 11 leidd ( 𝜑 → 1 ≤ 1 )
101 7 recnd ( 𝜑 → 2 ∈ ℂ )
102 26 9 gtned ( 𝜑 → 2 ≠ 0 )
103 logbid1 ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
104 101 102 15 103 syl3anc ( 𝜑 → ( 2 logb 2 ) = 1 )
105 104 eqcomd ( 𝜑 → 1 = ( 2 logb 2 ) )
106 100 105 breqtrd ( 𝜑 → 1 ≤ ( 2 logb 2 ) )
107 96 99 106 expge1d ( 𝜑 → 1 ≤ ( ( 2 logb 2 ) ↑ 2 ) )
108 105 eqcomd ( 𝜑 → ( 2 logb 2 ) = 1 )
109 108 oveq1d ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) = ( 1 ↑ 2 ) )
110 99 nn0zd ( 𝜑 → 2 ∈ ℤ )
111 1exp ( 2 ∈ ℤ → ( 1 ↑ 2 ) = 1 )
112 110 111 syl ( 𝜑 → ( 1 ↑ 2 ) = 1 )
113 109 112 eqtrd ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) = 1 )
114 7 leidd ( 𝜑 → 2 ≤ 2 )
115 1nn0 1 ∈ ℕ0
116 6 115 nn0addge1i 2 ≤ ( 2 + 1 )
117 2p1e3 ( 2 + 1 ) = 3
118 116 117 breqtri 2 ≤ 3
119 118 a1i ( 𝜑 → 2 ≤ 3 )
120 7 29 5 119 4 letrd ( 𝜑 → 2 ≤ 𝑁 )
121 110 114 7 9 5 10 120 logblebd ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝑁 ) )
122 11 96 16 106 121 letrd ( 𝜑 → 1 ≤ ( 2 logb 𝑁 ) )
123 16 99 122 expge1d ( 𝜑 → 1 ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
124 113 123 eqbrtrd ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
125 1z 1 ∈ ℤ
126 zsqcl ( 1 ∈ ℤ → ( 1 ↑ 2 ) ∈ ℤ )
127 125 126 ax-mp ( 1 ↑ 2 ) ∈ ℤ
128 127 a1i ( 𝜑 → ( 1 ↑ 2 ) ∈ ℤ )
129 109 eleq1d ( 𝜑 → ( ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ↔ ( 1 ↑ 2 ) ∈ ℤ ) )
130 128 129 mpbird ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ )
131 91 130 jca ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ∧ ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ) )
132 flge ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ∧ ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ) → ( ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ↔ ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
133 131 132 syl ( 𝜑 → ( ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ↔ ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
134 124 133 mpbid ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
135 11 97 93 107 134 letrd ( 𝜑 → 1 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
136 26 11 93 95 135 ltletrd ( 𝜑 → 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
137 92 136 jca ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
138 elnnz ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
139 138 bicomi ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↔ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ )
140 139 a1i ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↔ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ ) )
141 137 140 mpbid ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ )
142 141 nnnn0d ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ0 )
143 arisum ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) )
144 142 143 syl ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) )
145 74 nnred ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℝ )
146 71 145 fsumrecl ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ∈ ℝ )
147 144 146 eqeltrrd ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ∈ ℝ )
148 90 147 readdcld ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ∈ ℝ )
149 5 86 148 recxpcld ( 𝜑 → ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ∈ ℝ )
150 4nn0 4 ∈ ℕ0
151 150 a1i ( 𝜑 → 4 ∈ ℕ0 )
152 16 151 reexpcld ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℝ )
153 152 91 readdcld ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ )
154 153 rehalfcld ( 𝜑 → ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ∈ ℝ )
155 90 154 readdcld ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ∈ ℝ )
156 5 86 155 recxpcld ( 𝜑 → ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) ∈ ℝ )
157 reflcl ( ( 2 logb 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ )
158 47 157 syl ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ )
159 5 86 158 recxpcld ( 𝜑 → ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ )
160 33 146 rpcxpcld ( 𝜑 → ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ∈ ℝ+ )
161 33 141 aks4d1p1p1 ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) = ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) )
162 161 eleq1d ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ∈ ℝ+ ↔ ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ∈ ℝ+ ) )
163 160 162 mpbird ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ∈ ℝ+ )
164 163 rpregt0d ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ∈ ℝ ∧ 0 < ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
165 164 simpld ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ∈ ℝ )
166 159 165 remulcld ( 𝜑 → ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) ∈ ℝ )
167 5 86 90 recxpcld ( 𝜑 → ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ )
168 167 165 remulcld ( 𝜑 → ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) ∈ ℝ )
169 71 77 fprodrecl ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) ∈ ℝ )
170 5 69 86 expge0d ( 𝜑 → 0 ≤ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
171 nfv 𝑘 𝜑
172 0red ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 ∈ ℝ )
173 1 nnge1d ( 𝜑 → 1 ≤ 𝑁 )
174 173 adantr ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ 𝑁 )
175 72 76 174 expge1d ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ ( 𝑁𝑘 ) )
176 77 recnd ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁𝑘 ) ∈ ℂ )
177 176 subid1d ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁𝑘 ) − 0 ) = ( 𝑁𝑘 ) )
178 177 breq2d ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 1 ≤ ( ( 𝑁𝑘 ) − 0 ) ↔ 1 ≤ ( 𝑁𝑘 ) ) )
179 175 178 mpbird ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ ( ( 𝑁𝑘 ) − 0 ) )
180 78 77 172 179 lesubd ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 ≤ ( ( 𝑁𝑘 ) − 1 ) )
181 77 lem1d ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁𝑘 ) − 1 ) ≤ ( 𝑁𝑘 ) )
182 171 71 79 180 77 181 fprodle ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ≤ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) )
183 80 169 70 170 182 lemul2ad ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ) ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) ) )
184 82 breq1d ( 𝜑 → ( 𝐴 ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) ) ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁𝑘 ) − 1 ) ) ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) ) ) )
185 183 184 mpbird ( 𝜑𝐴 ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) ) )
186 72 recnd ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℂ )
187 cxpexp ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁𝑐 𝑘 ) = ( 𝑁𝑘 ) )
188 186 76 187 syl2anc ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁𝑐 𝑘 ) = ( 𝑁𝑘 ) )
189 188 eqcomd ( ( 𝜑𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁𝑘 ) = ( 𝑁𝑐 𝑘 ) )
190 189 prodeq2dv ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) = ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) )
191 190 oveq2d ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑘 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
192 185 191 breqtrd ( 𝜑𝐴 ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
193 5 recnd ( 𝜑𝑁 ∈ ℂ )
194 cxpexp ( ( 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ) → ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) = ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
195 193 69 194 syl2anc ( 𝜑 → ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) = ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
196 195 oveq1d ( 𝜑 → ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
197 196 eqcomd ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) = ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
198 192 197 breqtrd ( 𝜑𝐴 ≤ ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
199 159 167 164 3jca ( 𝜑 → ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ ∧ ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ ∧ ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ∈ ℝ ∧ 0 < ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) ) )
200 1 3 4 aks4d1p1p3 ( 𝜑 → ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )
201 ltmul1a ( ( ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ ∧ ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ ∧ ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ∈ ℝ ∧ 0 < ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) ) ∧ ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ) → ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) < ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
202 199 200 201 syl2anc ( 𝜑 → ( ( 𝑁𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) < ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
203 84 166 168 198 202 lelttrd ( 𝜑𝐴 < ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) )
204 161 oveq2d ( 𝜑 → ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁𝑐 𝑘 ) ) = ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) )
205 203 204 breqtrd ( 𝜑𝐴 < ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) )
206 144 oveq2d ( 𝜑 → ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) = ( 𝑁𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) )
207 206 oveq2d ( 𝜑 → ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) = ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) )
208 205 207 breqtrd ( 𝜑𝐴 < ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) )
209 26 10 gtned ( 𝜑𝑁 ≠ 0 )
210 90 recnd ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℂ )
211 141 nncnd ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℂ )
212 211 sqcld ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ∈ ℂ )
213 212 211 addcld ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ ℂ )
214 213 halfcld ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ∈ ℂ )
215 193 209 210 214 cxpaddd ( 𝜑 → ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) = ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) )
216 215 eqcomd ( 𝜑 → ( ( 𝑁𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) = ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) )
217 208 216 breqtrd ( 𝜑𝐴 < ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) )
218 reflcl ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ )
219 91 218 syl ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ )
220 219 resqcld ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ∈ ℝ )
221 220 219 readdcld ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ ℝ )
222 34 a1i ( 𝜑 → 2 ∈ ℝ+ )
223 91 99 reexpcld ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ∈ ℝ )
224 id ( 𝜑𝜑 )
225 142 nn0ge0d ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
226 flle ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
227 91 226 syl ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
228 219 91 99 225 227 leexp1ad ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) )
229 224 228 syl ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) )
230 16 recnd ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℂ )
231 230 99 99 expmuld ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) = ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) )
232 231 eqcomd ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) = ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) )
233 2t2e4 ( 2 · 2 ) = 4
234 233 oveq2i ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) = ( ( 2 logb 𝑁 ) ↑ 4 )
235 234 a1i ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) = ( ( 2 logb 𝑁 ) ↑ 4 ) )
236 232 235 eqtrd ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) = ( ( 2 logb 𝑁 ) ↑ 4 ) )
237 223 236 eqled ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 4 ) )
238 220 223 152 229 237 letrd ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 4 ) )
239 220 219 152 91 238 227 le2addd ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ≤ ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
240 221 153 222 239 lediv1dd ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ≤ ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) )
241 147 154 90 240 leadd2dd ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ≤ ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) )
242 5 32 148 155 cxpled ( 𝜑 → ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ≤ ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ↔ ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ≤ ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) ) )
243 241 242 mpbid ( 𝜑 → ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ≤ ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) )
244 84 149 156 217 243 ltletrd ( 𝜑𝐴 < ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) )
245 152 recnd ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℂ )
246 91 recnd ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℂ )
247 245 246 101 102 divdird ( 𝜑 → ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) = ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) )
248 247 oveq2d ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) = ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) )
249 248 oveq2d ( 𝜑 → ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) = ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) )
250 244 249 breqtrd ( 𝜑𝐴 < ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) )
251 245 101 102 divcld ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ∈ ℂ )
252 246 101 102 divcld ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ∈ ℂ )
253 251 252 addcomd ( 𝜑 → ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) = ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) )
254 253 oveq2d ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) = ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) )
255 210 252 251 addassd ( 𝜑 → ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) = ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) )
256 255 eqcomd ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) = ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) )
257 254 256 eqtrd ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) = ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) )
258 257 oveq2d ( 𝜑 → ( 𝑁𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) = ( 𝑁𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) )
259 250 258 breqtrd ( 𝜑𝐴 < ( 𝑁𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) )