Metamath Proof Explorer

Theorem aks4d1p1p4

Description: Technical step for inequality. The hard work is in to prove the final hypothesis. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p4.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks4d1p1p4.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p1p4.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p1p4.4 ⊢ ( 𝜑 → 3 ≤ 𝑁 )
aks4d1p1p4.5 ⊢ 𝐶 = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
aks4d1p1p4.6 ⊢ 𝐷 = ( ( 2 logb 𝑁 ) ↑ 2 )
aks4d1p1p4.7 ⊢ 𝐸 = ( ( 2 logb 𝑁 ) ↑ 4 )
aks4d1p1p4.8 ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) + 𝐷 ) ≤ 𝐸 )
Assertion aks4d1p1p4 ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p4.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 aks4d1p1p4.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p1p4.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p1p4.4 ⊢ ( 𝜑 → 3 ≤ 𝑁 )
5 aks4d1p1p4.5 ⊢ 𝐶 = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
6 aks4d1p1p4.6 ⊢ 𝐷 = ( ( 2 logb 𝑁 ) ↑ 2 )
7 aks4d1p1p4.7 ⊢ 𝐸 = ( ( 2 logb 𝑁 ) ↑ 4 )
8 aks4d1p1p4.8 ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) + 𝐷 ) ≤ 𝐸 )
9 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 2re ⊢ 2 ∈ ℝ
11 10 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
12 2pos ⊢ 0 < 2
13 12 a1i ⊢ ( 𝜑 → 0 < 2 )
14 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
15 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
16 1lt2 ⊢ 1 < 2
17 16 a1i ⊢ ( 𝜑 → 1 < 2 )
18 15 17 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
19 18 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
20 11 13 9 14 19 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
21 5nn0 ⊢ 5 ∈ ℕ0
22 21 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
23 20 22 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
24 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
25 23 24 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
26 25 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
27 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
28 27 eleq1d ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ ) )
29 26 28 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
30 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
31 7re ⊢ 7 ∈ ℝ
32 31 a1i ⊢ ( 𝜑 → 7 ∈ ℝ )
33 7pos ⊢ 0 < 7
34 33 a1i ⊢ ( 𝜑 → 0 < 7 )
35 9 4 3lexlogpow5ineq3 ⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
36 32 23 35 ltled ⊢ ( 𝜑 → 7 ≤ ( ( 2 logb 𝑁 ) ↑ 5 ) )
37 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
38 23 37 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
39 38 27 breqtrrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ 𝐵 )
40 32 23 29 36 39 letrd ⊢ ( 𝜑 → 7 ≤ 𝐵 )
41 30 32 29 34 40 ltletrd ⊢ ( 𝜑 → 0 < 𝐵 )
42 11 13 29 41 19 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
43 42 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
44 30 15 readdcld ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℝ )
45 43 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ )
46 45 15 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) + 1 ) ∈ ℝ )
47 11 13 11 13 19 relogbcld ⊢ ( 𝜑 → ( 2 logb 2 ) ∈ ℝ )
48 15 leidd ⊢ ( 𝜑 → 1 ≤ 1 )
49 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
50 49 addid2d ⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
51 11 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
52 30 13 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
53 logbid1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
54 51 52 19 53 syl3anc ⊢ ( 𝜑 → ( 2 logb 2 ) = 1 )
55 54 eqcomd ⊢ ( 𝜑 → 1 = ( 2 logb 2 ) )
56 55 eqcomd ⊢ ( 𝜑 → ( 2 logb 2 ) = 1 )
57 50 56 breq12d ⊢ ( 𝜑 → ( ( 0 + 1 ) ≤ ( 2 logb 2 ) ↔ 1 ≤ 1 ) )
58 48 57 mpbird ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( 2 logb 2 ) )
59 5re ⊢ 5 ∈ ℝ
60 59 a1i ⊢ ( 𝜑 → 5 ∈ ℝ )
61 11 60 readdcld ⊢ ( 𝜑 → ( 2 + 5 ) ∈ ℝ )
62 10 21 nn0addge1i ⊢ 2 ≤ ( 2 + 5 )
63 62 a1i ⊢ ( 𝜑 → 2 ≤ ( 2 + 5 ) )
64 10 recni ⊢ 2 ∈ ℂ
65 5cn ⊢ 5 ∈ ℂ
66 64 65 addcomi ⊢ ( 2 + 5 ) = ( 5 + 2 )
67 5p2e7 ⊢ ( 5 + 2 ) = 7
68 66 67 eqtri ⊢ ( 2 + 5 ) = 7
69 68 a1i ⊢ ( 𝜑 → ( 2 + 5 ) = 7 )
70 32 leidd ⊢ ( 𝜑 → 7 ≤ 7 )
71 69 70 eqbrtrd ⊢ ( 𝜑 → ( 2 + 5 ) ≤ 7 )
72 11 61 32 63 71 letrd ⊢ ( 𝜑 → 2 ≤ 7 )
73 11 32 29 72 40 letrd ⊢ ( 𝜑 → 2 ≤ 𝐵 )
74 2z ⊢ 2 ∈ ℤ
75 74 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
76 75 uzidd ⊢ ( 𝜑 → 2 ∈ ( ℤ≥ ‘ 2 ) )
77 2rp ⊢ 2 ∈ ℝ+
78 77 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
79 29 41 elrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
80 logbleb ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 2 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 2 ≤ 𝐵 ↔ ( 2 logb 2 ) ≤ ( 2 logb 𝐵 ) ) )
81 76 78 79 80 syl3anc ⊢ ( 𝜑 → ( 2 ≤ 𝐵 ↔ ( 2 logb 2 ) ≤ ( 2 logb 𝐵 ) ) )
82 73 81 mpbid ⊢ ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝐵 ) )
83 44 47 42 58 82 letrd ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( 2 logb 𝐵 ) )
84 fllep1 ⊢ ( ( 2 logb 𝐵 ) ∈ ℝ → ( 2 logb 𝐵 ) ≤ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) + 1 ) )
85 42 84 syl ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ≤ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) + 1 ) )
86 44 42 46 83 85 letrd ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) + 1 ) )
87 30 45 15 leadd1d ⊢ ( 𝜑 → ( 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ↔ ( 0 + 1 ) ≤ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) + 1 ) ) )
88 86 87 mpbird ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
89 43 88 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
90 elnn0z ⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
91 89 90 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
92 9 91 reexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ )
93 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
94 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℝ )
95 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
97 96 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
98 94 97 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℝ )
99 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℝ )
100 98 99 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℝ )
101 93 100 fprodrecl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℝ )
102 92 101 remulcld ⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℝ )
103 2 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
104 103 eleq1d ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℝ ) )
105 102 104 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
106 7 a1i ⊢ ( 𝜑 → 𝐸 = ( ( 2 logb 𝑁 ) ↑ 4 ) )
107 106 oveq2d ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐸 ) = ( 𝑁 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
108 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
109 78 rpne0d ⊢ ( 𝜑 → 2 ≠ 0 )
110 109 19 nelprd ⊢ ( 𝜑 → ¬ 2 ∈ { 0 , 1 } )
111 108 110 eldifd ⊢ ( 𝜑 → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
112 9 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
113 30 14 ltned ⊢ ( 𝜑 → 0 ≠ 𝑁 )
114 necom ⊢ ( 0 ≠ 𝑁 ↔ 𝑁 ≠ 0 )
115 114 imbi2i ⊢ ( ( 𝜑 → 0 ≠ 𝑁 ) ↔ ( 𝜑 → 𝑁 ≠ 0 ) )
116 113 115 mpbi ⊢ ( 𝜑 → 𝑁 ≠ 0 )
117 116 neneqd ⊢ ( 𝜑 → ¬ 𝑁 = 0 )
118 c0ex ⊢ 0 ∈ V
119 118 elsn2 ⊢ ( 𝑁 ∈ { 0 } ↔ 𝑁 = 0 )
120 117 119 sylnibr ⊢ ( 𝜑 → ¬ 𝑁 ∈ { 0 } )
121 112 120 eldifd ⊢ ( 𝜑 → 𝑁 ∈ ( ℂ ∖ { 0 } ) )
122 cxplogb ⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑁 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) = 𝑁 )
123 111 121 122 syl2anc ⊢ ( 𝜑 → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) = 𝑁 )
124 123 eqcomd ⊢ ( 𝜑 → 𝑁 = ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) )
125 124 oveq1d ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
126 eqidd ⊢ ( 𝜑 → ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
127 125 126 eqtrd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
128 107 127 eqtrd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐸 ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
129 106 eqcomd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) = 𝐸 )
130 4nn0 ⊢ 4 ∈ ℕ0
131 130 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
132 20 131 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℝ )
133 106 eleq1d ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ ↔ ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℝ ) )
134 132 133 mpbird ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
135 134 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
136 129 135 eqeltrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℂ )
137 78 20 136 cxpmuld ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
138 137 eqcomd ⊢ ( 𝜑 → ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) ) )
139 128 138 eqtrd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐸 ) = ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) ) )
140 20 recnd ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℂ )
141 140 exp1d ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 1 ) = ( 2 logb 𝑁 ) )
142 141 eqcomd ⊢ ( 𝜑 → ( 2 logb 𝑁 ) = ( ( 2 logb 𝑁 ) ↑ 1 ) )
143 142 oveq1d ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( ( ( 2 logb 𝑁 ) ↑ 1 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
144 1nn0 ⊢ 1 ∈ ℕ0
145 144 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
146 140 131 145 expaddd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) = ( ( ( 2 logb 𝑁 ) ↑ 1 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) )
147 146 eqcomd ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 1 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) )
148 143 147 eqtrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) = ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) )
149 148 oveq2d ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( ( 2 logb 𝑁 ) ↑ 4 ) ) ) = ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) ) )
150 139 149 eqtrd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐸 ) = ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) ) )
151 4cn ⊢ 4 ∈ ℂ
152 ax-1cn ⊢ 1 ∈ ℂ
153 4p1e5 ⊢ ( 4 + 1 ) = 5
154 151 152 153 addcomli ⊢ ( 1 + 4 ) = 5
155 154 a1i ⊢ ( 𝜑 → ( 1 + 4 ) = 5 )
156 155 oveq2d ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) = ( ( 2 logb 𝑁 ) ↑ 5 ) )
157 156 oveq2d ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ ( 1 + 4 ) ) ) = ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
158 150 157 eqtrd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐸 ) = ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
159 3re ⊢ 3 ∈ ℝ
160 159 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
161 0le1 ⊢ 0 ≤ 1
162 161 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
163 1lt3 ⊢ 1 < 3
164 163 a1i ⊢ ( 𝜑 → 1 < 3 )
165 15 160 164 ltled ⊢ ( 𝜑 → 1 ≤ 3 )
166 30 15 160 162 165 letrd ⊢ ( 𝜑 → 0 ≤ 3 )
167 30 160 9 166 4 letrd ⊢ ( 𝜑 → 0 ≤ 𝑁 )
168 9 167 134 recxpcld ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐸 ) ∈ ℝ )
169 158 168 eqeltrrd ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
170 27 eleq1d ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ ) )
171 25 170 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
172 30 29 41 ltled ⊢ ( 𝜑 → 0 ≤ 𝐵 )
173 171 172 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ 0 ≤ 𝐵 ) )
174 elnn0z ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℤ ∧ 0 ≤ 𝐵 ) )
175 173 174 sylibr ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
176 11 175 reexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝐵 ) ∈ ℝ )
177 9 14 elrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
178 23 15 readdcld ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ∈ ℝ )
179 22 nn0zd ⊢ ( 𝜑 → 5 ∈ ℤ )
180 logb1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
181 51 52 19 180 syl3anc ⊢ ( 𝜑 → ( 2 logb 1 ) = 0 )
182 181 30 eqeltrd ⊢ ( 𝜑 → ( 2 logb 1 ) ∈ ℝ )
183 30 leidd ⊢ ( 𝜑 → 0 ≤ 0 )
184 181 eqcomd ⊢ ( 𝜑 → 0 = ( 2 logb 1 ) )
185 183 184 breqtrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 1 ) )
186 15 160 9 164 4 ltletrd ⊢ ( 𝜑 → 1 < 𝑁 )
187 1rp ⊢ 1 ∈ ℝ+
188 187 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
189 logblt ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( 1 < 𝑁 ↔ ( 2 logb 1 ) < ( 2 logb 𝑁 ) ) )
190 76 188 177 189 syl3anc ⊢ ( 𝜑 → ( 1 < 𝑁 ↔ ( 2 logb 1 ) < ( 2 logb 𝑁 ) ) )
191 186 190 mpbid ⊢ ( 𝜑 → ( 2 logb 1 ) < ( 2 logb 𝑁 ) )
192 30 182 20 185 191 lelttrd ⊢ ( 𝜑 → 0 < ( 2 logb 𝑁 ) )
193 20 179 192 3jca ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 𝑁 ) ) )
194 expgt0 ⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 𝑁 ) ) → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
195 193 194 syl ⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
196 ltp1 ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
197 23 196 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
198 30 23 178 195 197 lttrd ⊢ ( 𝜑 → 0 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
199 11 13 178 198 19 relogbcld ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℝ )
200 5 a1i ⊢ ( 𝜑 → 𝐶 = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) )
201 200 eleq1d ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ↔ ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℝ ) )
202 199 201 mpbird ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
203 20 resqcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ )
204 6 a1i ⊢ ( 𝜑 → 𝐷 = ( ( 2 logb 𝑁 ) ↑ 2 ) )
205 204 eleq1d ⊢ ( 𝜑 → ( 𝐷 ∈ ℝ ↔ ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ) )
206 203 205 mpbird ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
207 206 rehalfcld ⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ )
208 202 207 readdcld ⊢ ( 𝜑 → ( 𝐶 + ( 𝐷 / 2 ) ) ∈ ℝ )
209 134 11 109 redivcld ⊢ ( 𝜑 → ( 𝐸 / 2 ) ∈ ℝ )
210 208 209 readdcld ⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ∈ ℝ )
211 177 210 rpcxpcld ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ) ∈ ℝ+ )
212 211 rpred ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ) ∈ ℝ )
213 1 2 3 4 aks4d1p1p2 ⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) )
214 129 oveq1d ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) = ( 𝐸 / 2 ) )
215 214 oveq2d ⊢ ( 𝜑 → ( ( ( 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 ) ) )
216 200 eqcomd ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) = 𝐶 )
217 216 oveq1d ⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) = ( 𝐶 + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) )
218 204 eqcomd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) = 𝐷 )
219 218 oveq1d ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) = ( 𝐷 / 2 ) )
220 219 oveq2d ⊢ ( 𝜑 → ( 𝐶 + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) = ( 𝐶 + ( 𝐷 / 2 ) ) )
221 217 220 eqtrd ⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) = ( 𝐶 + ( 𝐷 / 2 ) ) )
222 221 oveq1d ⊢ ( 𝜑 → ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( 𝐸 / 2 ) ) = ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) )
223 215 222 eqtrd ⊢ ( 𝜑 → ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) = ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) )
224 223 oveq2d ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) = ( 𝑁 ↑𝑐 ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ) )
225 213 224 breqtrd ⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ) )
226 202 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
227 226 108 109 divcan3d ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) / 2 ) = 𝐶 )
228 227 eqcomd ⊢ ( 𝜑 → 𝐶 = ( ( 2 · 𝐶 ) / 2 ) )
229 228 oveq1d ⊢ ( 𝜑 → ( 𝐶 + ( 𝐷 / 2 ) ) = ( ( ( 2 · 𝐶 ) / 2 ) + ( 𝐷 / 2 ) ) )
230 11 202 remulcld ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℝ )
231 230 recnd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℂ )
232 206 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
233 231 232 51 109 divdird ⊢ ( 𝜑 → ( ( ( 2 · 𝐶 ) + 𝐷 ) / 2 ) = ( ( ( 2 · 𝐶 ) / 2 ) + ( 𝐷 / 2 ) ) )
234 233 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝐶 ) / 2 ) + ( 𝐷 / 2 ) ) = ( ( ( 2 · 𝐶 ) + 𝐷 ) / 2 ) )
235 229 234 eqtrd ⊢ ( 𝜑 → ( 𝐶 + ( 𝐷 / 2 ) ) = ( ( ( 2 · 𝐶 ) + 𝐷 ) / 2 ) )
236 230 206 readdcld ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) + 𝐷 ) ∈ ℝ )
237 236 134 78 lediv1d ⊢ ( 𝜑 → ( ( ( 2 · 𝐶 ) + 𝐷 ) ≤ 𝐸 ↔ ( ( ( 2 · 𝐶 ) + 𝐷 ) / 2 ) ≤ ( 𝐸 / 2 ) ) )
238 8 237 mpbid ⊢ ( 𝜑 → ( ( ( 2 · 𝐶 ) + 𝐷 ) / 2 ) ≤ ( 𝐸 / 2 ) )
239 235 238 eqbrtrd ⊢ ( 𝜑 → ( 𝐶 + ( 𝐷 / 2 ) ) ≤ ( 𝐸 / 2 ) )
240 208 209 209 239 leadd1dd ⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ≤ ( ( 𝐸 / 2 ) + ( 𝐸 / 2 ) ) )
241 135 2halvesd ⊢ ( 𝜑 → ( ( 𝐸 / 2 ) + ( 𝐸 / 2 ) ) = 𝐸 )
242 240 241 breqtrd ⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ≤ 𝐸 )
243 9 186 210 134 cxpled ⊢ ( 𝜑 → ( ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ≤ 𝐸 ↔ ( 𝑁 ↑𝑐 ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ) ≤ ( 𝑁 ↑𝑐 𝐸 ) ) )
244 242 243 mpbid ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 𝐶 + ( 𝐷 / 2 ) ) + ( 𝐸 / 2 ) ) ) ≤ ( 𝑁 ↑𝑐 𝐸 ) )
245 105 212 168 225 244 ltletrd ⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 𝐸 ) )
246 245 158 breqtrd ⊢ ( 𝜑 → 𝐴 < ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
247 1le2 ⊢ 1 ≤ 2
248 247 a1i ⊢ ( 𝜑 → 1 ≤ 2 )
249 175 nn0red ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
250 27 eqcomd ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) = 𝐵 )
251 38 250 breqtrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ 𝐵 )
252 11 248 23 249 251 cxplead ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 5 ) ) ≤ ( 2 ↑𝑐 𝐵 ) )
253 cxpexp ⊢ ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℕ0 ) → ( 2 ↑𝑐 𝐵 ) = ( 2 ↑ 𝐵 ) )
254 108 175 253 syl2anc ⊢ ( 𝜑 → ( 2 ↑𝑐 𝐵 ) = ( 2 ↑ 𝐵 ) )
255 252 254 breqtrd ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) ↑ 5 ) ) ≤ ( 2 ↑ 𝐵 ) )
256 105 169 176 246 255 ltletrd ⊢ ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )