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 ) ) ) )