Metamath Proof Explorer

Theorem hgt750lem

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 17-Dec-2021)

Ref Expression
Assertion hgt750lem ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) )

Proof

Step Hyp Ref Expression
1 7nn0 ⊢ 7 ∈ ℕ0
2 3re ⊢ 3 ∈ ℝ
3 4re ⊢ 4 ∈ ℝ
4 8re ⊢ 8 ∈ ℝ
5 3 4 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 8 ∈ ℝ )
6 dp2cl ⊢ ( ( 4 ∈ ℝ ∧ 8 ∈ ℝ ) → 4 8 ∈ ℝ )
7 5 6 ax-mp ⊢ 4 8 ∈ ℝ
8 2 7 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 4 8 ∈ ℝ )
9 dp2cl ⊢ ( ( 3 ∈ ℝ ∧ 4 8 ∈ ℝ ) → 3 4 8 ∈ ℝ )
10 8 9 ax-mp ⊢ 3 4 8 ∈ ℝ
11 dpcl ⊢ ( ( 7 ∈ ℕ0 ∧ 3 4 8 ∈ ℝ ) → ( 7 . 3 4 8 ) ∈ ℝ )
12 1 10 11 mp2an ⊢ ( 7 . 3 4 8 ) ∈ ℝ
13 12 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( 7 . 3 4 8 ) ∈ ℝ )
14 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 𝑁 ∈ ℝ )
16 0re ⊢ 0 ∈ ℝ
17 16 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 0 ∈ ℝ )
18 10re ⊢ 1 0 ∈ ℝ
19 2nn0 ⊢ 2 ∈ ℕ0
20 19 1 deccl ⊢ 2 7 ∈ ℕ0
21 reexpcl ⊢ ( ( 1 0 ∈ ℝ ∧ 2 7 ∈ ℕ0 ) → ( 1 0 ↑ 2 7 ) ∈ ℝ )
22 18 20 21 mp2an ⊢ ( 1 0 ↑ 2 7 ) ∈ ℝ
23 22 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( 1 0 ↑ 2 7 ) ∈ ℝ )
24 0lt1 ⊢ 0 < 1
25 1nn ⊢ 1 ∈ ℕ
26 0nn0 ⊢ 0 ∈ ℕ0
27 1nn0 ⊢ 1 ∈ ℕ0
28 1re ⊢ 1 ∈ ℝ
29 9re ⊢ 9 ∈ ℝ
30 1lt9 ⊢ 1 < 9
31 28 29 30 ltleii ⊢ 1 ≤ 9
32 25 26 27 31 declei ⊢ 1 ≤ 1 0
33 expge1 ⊢ ( ( 1 0 ∈ ℝ ∧ 2 7 ∈ ℕ0 ∧ 1 ≤ 1 0 ) → 1 ≤ ( 1 0 ↑ 2 7 ) )
34 18 20 32 33 mp3an ⊢ 1 ≤ ( 1 0 ↑ 2 7 )
35 16 28 22 ltletri ⊢ ( ( 0 < 1 ∧ 1 ≤ ( 1 0 ↑ 2 7 ) ) → 0 < ( 1 0 ↑ 2 7 ) )
36 24 34 35 mp2an ⊢ 0 < ( 1 0 ↑ 2 7 )
37 36 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 0 < ( 1 0 ↑ 2 7 ) )
38 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
39 17 23 15 37 38 ltletrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 0 < 𝑁 )
40 15 39 elrpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 𝑁 ∈ ℝ+ )
41 40 relogcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( log ‘ 𝑁 ) ∈ ℝ )
42 40 rpge0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 0 ≤ 𝑁 )
43 15 42 resqrtcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( √ ‘ 𝑁 ) ∈ ℝ )
44 40 sqrtgt0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 0 < ( √ ‘ 𝑁 ) )
45 17 44 gtned ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( √ ‘ 𝑁 ) ≠ 0 )
46 41 43 45 redivcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ∈ ℝ )
47 13 46 remulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
48 elrp ⊢ ( ( 1 0 ↑ 2 7 ) ∈ ℝ+ ↔ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 2 7 ) ) )
49 22 36 48 mpbir2an ⊢ ( 1 0 ↑ 2 7 ) ∈ ℝ+
50 relogcl ⊢ ( ( 1 0 ↑ 2 7 ) ∈ ℝ+ → ( log ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ )
51 49 50 ax-mp ⊢ ( log ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ
52 22 36 sqrtpclii ⊢ ( √ ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ
53 22 36 sqrtgt0ii ⊢ 0 < ( √ ‘ ( 1 0 ↑ 2 7 ) )
54 16 53 gtneii ⊢ ( √ ‘ ( 1 0 ↑ 2 7 ) ) ≠ 0
55 51 52 54 redivcli ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ∈ ℝ
56 55 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ∈ ℝ )
57 13 56 remulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) ∈ ℝ )
58 qssre ⊢ ℚ ⊆ ℝ
59 4nn0 ⊢ 4 ∈ ℕ0
60 nn0ssq ⊢ ℕ0 ⊆ ℚ
61 8nn0 ⊢ 8 ∈ ℕ0
62 60 61 sselii ⊢ 8 ∈ ℚ
63 59 62 dp2clq ⊢ 4 8 ∈ ℚ
64 19 63 dp2clq ⊢ 2 4 8 ∈ ℚ
65 19 64 dp2clq ⊢ 2 2 4 8 ∈ ℚ
66 59 65 dp2clq ⊢ 4 2 2 4 8 ∈ ℚ
67 26 66 dp2clq ⊢ 0 4 2 2 4 8 ∈ ℚ
68 26 67 dp2clq ⊢ 0 0 4 2 2 4 8 ∈ ℚ
69 26 68 dp2clq ⊢ 0 0 0 4 2 2 4 8 ∈ ℚ
70 58 69 sselii ⊢ 0 0 0 4 2 2 4 8 ∈ ℝ
71 dpcl ⊢ ( ( 0 ∈ ℕ0 ∧ 0 0 0 4 2 2 4 8 ∈ ℝ ) → ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ )
72 26 70 71 mp2an ⊢ ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ
73 72 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ )
74 3nn0 ⊢ 3 ∈ ℕ0
75 8pos ⊢ 0 < 8
76 elrp ⊢ ( 8 ∈ ℝ+ ↔ ( 8 ∈ ℝ ∧ 0 < 8 ) )
77 4 75 76 mpbir2an ⊢ 8 ∈ ℝ+
78 59 77 rpdp2cl ⊢ 4 8 ∈ ℝ+
79 74 78 rpdp2cl ⊢ 3 4 8 ∈ ℝ+
80 1 79 rpdpcl ⊢ ( 7 . 3 4 8 ) ∈ ℝ+
81 elrp ⊢ ( ( 7 . 3 4 8 ) ∈ ℝ+ ↔ ( ( 7 . 3 4 8 ) ∈ ℝ ∧ 0 < ( 7 . 3 4 8 ) ) )
82 80 81 mpbi ⊢ ( ( 7 . 3 4 8 ) ∈ ℝ ∧ 0 < ( 7 . 3 4 8 ) )
83 82 simpri ⊢ 0 < ( 7 . 3 4 8 )
84 16 12 83 ltleii ⊢ 0 ≤ ( 7 . 3 4 8 )
85 84 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → 0 ≤ ( 7 . 3 4 8 ) )
86 49 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( 1 0 ↑ 2 7 ) ∈ ℝ+ )
87 2cn ⊢ 2 ∈ ℂ
88 87 mulid2i ⊢ ( 1 · 2 ) = 2
89 2nn ⊢ 2 ∈ ℕ
90 89 1 27 31 declei ⊢ 1 ≤ 2 7
91 2pos ⊢ 0 < 2
92 20 nn0rei ⊢ 2 7 ∈ ℝ
93 2re ⊢ 2 ∈ ℝ
94 28 92 93 lemul1i ⊢ ( 0 < 2 → ( 1 ≤ 2 7 ↔ ( 1 · 2 ) ≤ ( 2 7 · 2 ) ) )
95 91 94 ax-mp ⊢ ( 1 ≤ 2 7 ↔ ( 1 · 2 ) ≤ ( 2 7 · 2 ) )
96 90 95 mpbi ⊢ ( 1 · 2 ) ≤ ( 2 7 · 2 )
97 88 96 eqbrtrri ⊢ 2 ≤ ( 2 7 · 2 )
98 1p1e2 ⊢ ( 1 + 1 ) = 2
99 loge ⊢ ( log ‘ e ) = 1
100 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
101 100 simpri ⊢ e < 3
102 epr ⊢ e ∈ ℝ+
103 3rp ⊢ 3 ∈ ℝ+
104 logltb ⊢ ( ( e ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( e < 3 ↔ ( log ‘ e ) < ( log ‘ 3 ) ) )
105 102 103 104 mp2an ⊢ ( e < 3 ↔ ( log ‘ e ) < ( log ‘ 3 ) )
106 101 105 mpbi ⊢ ( log ‘ e ) < ( log ‘ 3 )
107 99 106 eqbrtrri ⊢ 1 < ( log ‘ 3 )
108 relogcl ⊢ ( 3 ∈ ℝ+ → ( log ‘ 3 ) ∈ ℝ )
109 103 108 ax-mp ⊢ ( log ‘ 3 ) ∈ ℝ
110 28 28 109 109 lt2addi ⊢ ( ( 1 < ( log ‘ 3 ) ∧ 1 < ( log ‘ 3 ) ) → ( 1 + 1 ) < ( ( log ‘ 3 ) + ( log ‘ 3 ) ) )
111 107 107 110 mp2an ⊢ ( 1 + 1 ) < ( ( log ‘ 3 ) + ( log ‘ 3 ) )
112 3cn ⊢ 3 ∈ ℂ
113 3ne0 ⊢ 3 ≠ 0
114 logmul2 ⊢ ( ( 3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ+ ) → ( log ‘ ( 3 · 3 ) ) = ( ( log ‘ 3 ) + ( log ‘ 3 ) ) )
115 112 113 103 114 mp3an ⊢ ( log ‘ ( 3 · 3 ) ) = ( ( log ‘ 3 ) + ( log ‘ 3 ) )
116 3t3e9 ⊢ ( 3 · 3 ) = 9
117 116 fveq2i ⊢ ( log ‘ ( 3 · 3 ) ) = ( log ‘ 9 )
118 9lt10 ⊢ 9 < 1 0
119 29 18 118 ltleii ⊢ 9 ≤ 1 0
120 9pos ⊢ 0 < 9
121 elrp ⊢ ( 9 ∈ ℝ+ ↔ ( 9 ∈ ℝ ∧ 0 < 9 ) )
122 29 120 121 mpbir2an ⊢ 9 ∈ ℝ+
123 10pos ⊢ 0 < 1 0
124 elrp ⊢ ( 1 0 ∈ ℝ+ ↔ ( 1 0 ∈ ℝ ∧ 0 < 1 0 ) )
125 18 123 124 mpbir2an ⊢ 1 0 ∈ ℝ+
126 logleb ⊢ ( ( 9 ∈ ℝ+ ∧ 1 0 ∈ ℝ+ ) → ( 9 ≤ 1 0 ↔ ( log ‘ 9 ) ≤ ( log ‘ 1 0 ) ) )
127 122 125 126 mp2an ⊢ ( 9 ≤ 1 0 ↔ ( log ‘ 9 ) ≤ ( log ‘ 1 0 ) )
128 119 127 mpbi ⊢ ( log ‘ 9 ) ≤ ( log ‘ 1 0 )
129 117 128 eqbrtri ⊢ ( log ‘ ( 3 · 3 ) ) ≤ ( log ‘ 1 0 )
130 115 129 eqbrtrri ⊢ ( ( log ‘ 3 ) + ( log ‘ 3 ) ) ≤ ( log ‘ 1 0 )
131 28 28 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
132 109 109 readdcli ⊢ ( ( log ‘ 3 ) + ( log ‘ 3 ) ) ∈ ℝ
133 relogcl ⊢ ( 1 0 ∈ ℝ+ → ( log ‘ 1 0 ) ∈ ℝ )
134 125 133 ax-mp ⊢ ( log ‘ 1 0 ) ∈ ℝ
135 131 132 134 ltletri ⊢ ( ( ( 1 + 1 ) < ( ( log ‘ 3 ) + ( log ‘ 3 ) ) ∧ ( ( log ‘ 3 ) + ( log ‘ 3 ) ) ≤ ( log ‘ 1 0 ) ) → ( 1 + 1 ) < ( log ‘ 1 0 ) )
136 111 130 135 mp2an ⊢ ( 1 + 1 ) < ( log ‘ 1 0 )
137 98 136 eqbrtrri ⊢ 2 < ( log ‘ 1 0 )
138 93 134 ltlei ⊢ ( 2 < ( log ‘ 1 0 ) → 2 ≤ ( log ‘ 1 0 ) )
139 137 138 ax-mp ⊢ 2 ≤ ( log ‘ 1 0 )
140 16 29 120 ltleii ⊢ 0 ≤ 9
141 89 1 26 140 decltdi ⊢ 0 < 2 7
142 93 134 92 lemul2i ⊢ ( 0 < 2 7 → ( 2 ≤ ( log ‘ 1 0 ) ↔ ( 2 7 · 2 ) ≤ ( 2 7 · ( log ‘ 1 0 ) ) ) )
143 141 142 ax-mp ⊢ ( 2 ≤ ( log ‘ 1 0 ) ↔ ( 2 7 · 2 ) ≤ ( 2 7 · ( log ‘ 1 0 ) ) )
144 139 143 mpbi ⊢ ( 2 7 · 2 ) ≤ ( 2 7 · ( log ‘ 1 0 ) )
145 92 93 remulcli ⊢ ( 2 7 · 2 ) ∈ ℝ
146 20 nn0zi ⊢ 2 7 ∈ ℤ
147 relogexp ⊢ ( ( 1 0 ∈ ℝ+ ∧ 2 7 ∈ ℤ ) → ( log ‘ ( 1 0 ↑ 2 7 ) ) = ( 2 7 · ( log ‘ 1 0 ) ) )
148 125 146 147 mp2an ⊢ ( log ‘ ( 1 0 ↑ 2 7 ) ) = ( 2 7 · ( log ‘ 1 0 ) )
149 148 51 eqeltrri ⊢ ( 2 7 · ( log ‘ 1 0 ) ) ∈ ℝ
150 93 145 149 letri ⊢ ( ( 2 ≤ ( 2 7 · 2 ) ∧ ( 2 7 · 2 ) ≤ ( 2 7 · ( log ‘ 1 0 ) ) ) → 2 ≤ ( 2 7 · ( log ‘ 1 0 ) ) )
151 97 144 150 mp2an ⊢ 2 ≤ ( 2 7 · ( log ‘ 1 0 ) )
152 relogef ⊢ ( 2 ∈ ℝ → ( log ‘ ( exp ‘ 2 ) ) = 2 )
153 93 152 ax-mp ⊢ ( log ‘ ( exp ‘ 2 ) ) = 2
154 151 153 148 3brtr4i ⊢ ( log ‘ ( exp ‘ 2 ) ) ≤ ( log ‘ ( 1 0 ↑ 2 7 ) )
155 rpefcl ⊢ ( 2 ∈ ℝ → ( exp ‘ 2 ) ∈ ℝ+ )
156 93 155 ax-mp ⊢ ( exp ‘ 2 ) ∈ ℝ+
157 logleb ⊢ ( ( ( exp ‘ 2 ) ∈ ℝ+ ∧ ( 1 0 ↑ 2 7 ) ∈ ℝ+ ) → ( ( exp ‘ 2 ) ≤ ( 1 0 ↑ 2 7 ) ↔ ( log ‘ ( exp ‘ 2 ) ) ≤ ( log ‘ ( 1 0 ↑ 2 7 ) ) ) )
158 156 49 157 mp2an ⊢ ( ( exp ‘ 2 ) ≤ ( 1 0 ↑ 2 7 ) ↔ ( log ‘ ( exp ‘ 2 ) ) ≤ ( log ‘ ( 1 0 ↑ 2 7 ) ) )
159 154 158 mpbir ⊢ ( exp ‘ 2 ) ≤ ( 1 0 ↑ 2 7 )
160 159 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( exp ‘ 2 ) ≤ ( 1 0 ↑ 2 7 ) )
161 86 40 160 38 logdivsqrle ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ≤ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) )
162 46 56 13 85 161 lemul2ad ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) ≤ ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) )
163 3lt10 ⊢ 3 < 1 0
164 4lt10 ⊢ 4 < 1 0
165 8lt10 ⊢ 8 < 1 0
166 59 77 164 165 dp2lt10 ⊢ 4 8 < 1 0
167 74 78 163 166 dp2lt10 ⊢ 3 4 8 < 1 0
168 7p1e8 ⊢ ( 7 + 1 ) = 8
169 1 79 61 167 168 dplti ⊢ ( 7 . 3 4 8 ) < 8
170 58 62 sselii ⊢ 8 ∈ ℝ
171 12 170 18 lttri ⊢ ( ( ( 7 . 3 4 8 ) < 8 ∧ 8 < 1 0 ) → ( 7 . 3 4 8 ) < 1 0 )
172 169 165 171 mp2an ⊢ ( 7 . 3 4 8 ) < 1 0
173 27 26 deccl ⊢ 1 0 ∈ ℕ0
174 173 numexp0 ⊢ ( 1 0 ↑ 0 ) = 1
175 0z ⊢ 0 ∈ ℤ
176 18 175 146 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 2 7 ∈ ℤ )
177 1lt10 ⊢ 1 < 1 0
178 177 141 pm3.2i ⊢ ( 1 < 1 0 ∧ 0 < 2 7 )
179 ltexp2a ⊢ ( ( ( 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 0 < 2 7 ) ) → ( 1 0 ↑ 0 ) < ( 1 0 ↑ 2 7 ) )
180 176 178 179 mp2an ⊢ ( 1 0 ↑ 0 ) < ( 1 0 ↑ 2 7 )
181 174 180 eqbrtrri ⊢ 1 < ( 1 0 ↑ 2 7 )
182 loggt0b ⊢ ( ( 1 0 ↑ 2 7 ) ∈ ℝ+ → ( 0 < ( log ‘ ( 1 0 ↑ 2 7 ) ) ↔ 1 < ( 1 0 ↑ 2 7 ) ) )
183 49 182 ax-mp ⊢ ( 0 < ( log ‘ ( 1 0 ↑ 2 7 ) ) ↔ 1 < ( 1 0 ↑ 2 7 ) )
184 181 183 mpbir ⊢ 0 < ( log ‘ ( 1 0 ↑ 2 7 ) )
185 51 52 divgt0i ⊢ ( ( 0 < ( log ‘ ( 1 0 ↑ 2 7 ) ) ∧ 0 < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) → 0 < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) )
186 184 53 185 mp2an ⊢ 0 < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
187 12 18 55 ltmul1i ⊢ ( 0 < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) → ( ( 7 . 3 4 8 ) < 1 0 ↔ ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) ) )
188 186 187 ax-mp ⊢ ( ( 7 . 3 4 8 ) < 1 0 ↔ ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) )
189 172 188 mpbi ⊢ ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) )
190 18 recni ⊢ 1 0 ∈ ℂ
191 expmul ⊢ ( ( 1 0 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 1 0 ↑ ( 7 · 2 ) ) = ( ( 1 0 ↑ 7 ) ↑ 2 ) )
192 190 1 19 191 mp3an ⊢ ( 1 0 ↑ ( 7 · 2 ) ) = ( ( 1 0 ↑ 7 ) ↑ 2 )
193 7t2e14 ⊢ ( 7 · 2 ) = 1 4
194 193 oveq2i ⊢ ( 1 0 ↑ ( 7 · 2 ) ) = ( 1 0 ↑ 1 4 )
195 192 194 eqtr3i ⊢ ( ( 1 0 ↑ 7 ) ↑ 2 ) = ( 1 0 ↑ 1 4 )
196 195 fveq2i ⊢ ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( √ ‘ ( 1 0 ↑ 1 4 ) )
197 reexpcl ⊢ ( ( 1 0 ∈ ℝ ∧ 7 ∈ ℕ0 ) → ( 1 0 ↑ 7 ) ∈ ℝ )
198 18 1 197 mp2an ⊢ ( 1 0 ↑ 7 ) ∈ ℝ
199 1 nn0zi ⊢ 7 ∈ ℤ
200 expgt0 ⊢ ( ( 1 0 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < 1 0 ) → 0 < ( 1 0 ↑ 7 ) )
201 18 199 123 200 mp3an ⊢ 0 < ( 1 0 ↑ 7 )
202 16 198 201 ltleii ⊢ 0 ≤ ( 1 0 ↑ 7 )
203 sqrtsq ⊢ ( ( ( 1 0 ↑ 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 7 ) ) → ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( 1 0 ↑ 7 ) )
204 198 202 203 mp2an ⊢ ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( 1 0 ↑ 7 )
205 196 204 eqtr3i ⊢ ( √ ‘ ( 1 0 ↑ 1 4 ) ) = ( 1 0 ↑ 7 )
206 27 59 deccl ⊢ 1 4 ∈ ℕ0
207 206 nn0zi ⊢ 1 4 ∈ ℤ
208 18 207 146 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 2 7 ∈ ℤ )
209 1lt2 ⊢ 1 < 2
210 27 19 59 1 164 209 decltc ⊢ 1 4 < 2 7
211 177 210 pm3.2i ⊢ ( 1 < 1 0 ∧ 1 4 < 2 7 )
212 ltexp2a ⊢ ( ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 1 4 < 2 7 ) ) → ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) )
213 208 211 212 mp2an ⊢ ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 )
214 reexpcl ⊢ ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℕ0 ) → ( 1 0 ↑ 1 4 ) ∈ ℝ )
215 18 206 214 mp2an ⊢ ( 1 0 ↑ 1 4 ) ∈ ℝ
216 expgt0 ⊢ ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 0 < 1 0 ) → 0 < ( 1 0 ↑ 1 4 ) )
217 18 207 123 216 mp3an ⊢ 0 < ( 1 0 ↑ 1 4 )
218 16 215 217 ltleii ⊢ 0 ≤ ( 1 0 ↑ 1 4 )
219 215 218 pm3.2i ⊢ ( ( 1 0 ↑ 1 4 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 1 4 ) )
220 16 22 36 ltleii ⊢ 0 ≤ ( 1 0 ↑ 2 7 )
221 22 220 pm3.2i ⊢ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 2 7 ) )
222 sqrtlt ⊢ ( ( ( ( 1 0 ↑ 1 4 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 1 4 ) ) ∧ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 2 7 ) ) ) → ( ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) ↔ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) )
223 219 221 222 mp2an ⊢ ( ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) ↔ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
224 213 223 mpbi ⊢ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) )
225 205 224 eqbrtrri ⊢ ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) )
226 198 201 pm3.2i ⊢ ( ( 1 0 ↑ 7 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 7 ) )
227 52 53 pm3.2i ⊢ ( ( √ ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
228 51 184 pm3.2i ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ ∧ 0 < ( log ‘ ( 1 0 ↑ 2 7 ) ) )
229 ltdiv2 ⊢ ( ( ( ( 1 0 ↑ 7 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 7 ) ) ∧ ( ( √ ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ∧ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ ∧ 0 < ( log ‘ ( 1 0 ↑ 2 7 ) ) ) ) → ( ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ↔ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) ) )
230 226 227 228 229 mp3an ⊢ ( ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ↔ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) )
231 225 230 mpbi ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) )
232 6nn ⊢ 6 ∈ ℕ
233 232 nngt0i ⊢ 0 < 6
234 27 26 232 233 declt ⊢ 1 0 < 1 6
235 6nn0 ⊢ 6 ∈ ℕ0
236 27 235 deccl ⊢ 1 6 ∈ ℕ0
237 236 nn0rei ⊢ 1 6 ∈ ℝ
238 25 235 26 123 declti ⊢ 0 < 1 6
239 elrp ⊢ ( 1 6 ∈ ℝ+ ↔ ( 1 6 ∈ ℝ ∧ 0 < 1 6 ) )
240 237 238 239 mpbir2an ⊢ 1 6 ∈ ℝ+
241 logltb ⊢ ( ( 1 0 ∈ ℝ+ ∧ 1 6 ∈ ℝ+ ) → ( 1 0 < 1 6 ↔ ( log ‘ 1 0 ) < ( log ‘ 1 6 ) ) )
242 125 240 241 mp2an ⊢ ( 1 0 < 1 6 ↔ ( log ‘ 1 0 ) < ( log ‘ 1 6 ) )
243 234 242 mpbi ⊢ ( log ‘ 1 0 ) < ( log ‘ 1 6 )
244 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
245 244 fveq2i ⊢ ( log ‘ ( 2 ↑ 4 ) ) = ( log ‘ 1 6 )
246 2rp ⊢ 2 ∈ ℝ+
247 59 nn0zi ⊢ 4 ∈ ℤ
248 relogexp ⊢ ( ( 2 ∈ ℝ+ ∧ 4 ∈ ℤ ) → ( log ‘ ( 2 ↑ 4 ) ) = ( 4 · ( log ‘ 2 ) ) )
249 246 247 248 mp2an ⊢ ( log ‘ ( 2 ↑ 4 ) ) = ( 4 · ( log ‘ 2 ) )
250 245 249 eqtr3i ⊢ ( log ‘ 1 6 ) = ( 4 · ( log ‘ 2 ) )
251 243 250 breqtri ⊢ ( log ‘ 1 0 ) < ( 4 · ( log ‘ 2 ) )
252 100 simpli ⊢ 2 < e
253 logltb ⊢ ( ( 2 ∈ ℝ+ ∧ e ∈ ℝ+ ) → ( 2 < e ↔ ( log ‘ 2 ) < ( log ‘ e ) ) )
254 246 102 253 mp2an ⊢ ( 2 < e ↔ ( log ‘ 2 ) < ( log ‘ e ) )
255 252 254 mpbi ⊢ ( log ‘ 2 ) < ( log ‘ e )
256 255 99 breqtri ⊢ ( log ‘ 2 ) < 1
257 4pos ⊢ 0 < 4
258 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
259 246 258 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
260 259 28 3 ltmul2i ⊢ ( 0 < 4 → ( ( log ‘ 2 ) < 1 ↔ ( 4 · ( log ‘ 2 ) ) < ( 4 · 1 ) ) )
261 257 260 ax-mp ⊢ ( ( log ‘ 2 ) < 1 ↔ ( 4 · ( log ‘ 2 ) ) < ( 4 · 1 ) )
262 256 261 mpbi ⊢ ( 4 · ( log ‘ 2 ) ) < ( 4 · 1 )
263 4cn ⊢ 4 ∈ ℂ
264 263 mulid1i ⊢ ( 4 · 1 ) = 4
265 262 264 breqtri ⊢ ( 4 · ( log ‘ 2 ) ) < 4
266 3 259 remulcli ⊢ ( 4 · ( log ‘ 2 ) ) ∈ ℝ
267 134 266 3 lttri ⊢ ( ( ( log ‘ 1 0 ) < ( 4 · ( log ‘ 2 ) ) ∧ ( 4 · ( log ‘ 2 ) ) < 4 ) → ( log ‘ 1 0 ) < 4 )
268 251 265 267 mp2an ⊢ ( log ‘ 1 0 ) < 4
269 134 3 92 ltmul2i ⊢ ( 0 < 2 7 → ( ( log ‘ 1 0 ) < 4 ↔ ( 2 7 · ( log ‘ 1 0 ) ) < ( 2 7 · 4 ) ) )
270 141 269 ax-mp ⊢ ( ( log ‘ 1 0 ) < 4 ↔ ( 2 7 · ( log ‘ 1 0 ) ) < ( 2 7 · 4 ) )
271 268 270 mpbi ⊢ ( 2 7 · ( log ‘ 1 0 ) ) < ( 2 7 · 4 )
272 148 271 eqbrtri ⊢ ( log ‘ ( 1 0 ↑ 2 7 ) ) < ( 2 7 · 4 )
273 92 3 remulcli ⊢ ( 2 7 · 4 ) ∈ ℝ
274 51 273 198 ltdiv1i ⊢ ( 0 < ( 1 0 ↑ 7 ) → ( ( log ‘ ( 1 0 ↑ 2 7 ) ) < ( 2 7 · 4 ) ↔ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) ) )
275 201 274 ax-mp ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) < ( 2 7 · 4 ) ↔ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) )
276 272 275 mpbi ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) )
277 16 201 gtneii ⊢ ( 1 0 ↑ 7 ) ≠ 0
278 51 198 277 redivcli ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) ∈ ℝ
279 273 198 277 redivcli ⊢ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) ∈ ℝ
280 55 278 279 lttri ⊢ ( ( ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) ∧ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( 1 0 ↑ 7 ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) ) → ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) )
281 231 276 280 mp2an ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) )
282 7lt10 ⊢ 7 < 1 0
283 2lt10 ⊢ 2 < 1 0
284 19 173 1 26 282 283 decltc ⊢ 2 7 < 1 0 0
285 10nn ⊢ 1 0 ∈ ℕ
286 285 decnncl2 ⊢ 1 0 0 ∈ ℕ
287 286 nnrei ⊢ 1 0 0 ∈ ℝ
288 92 287 3 ltmul1i ⊢ ( 0 < 4 → ( 2 7 < 1 0 0 ↔ ( 2 7 · 4 ) < ( 1 0 0 · 4 ) ) )
289 257 288 ax-mp ⊢ ( 2 7 < 1 0 0 ↔ ( 2 7 · 4 ) < ( 1 0 0 · 4 ) )
290 284 289 mpbi ⊢ ( 2 7 · 4 ) < ( 1 0 0 · 4 )
291 287 3 remulcli ⊢ ( 1 0 0 · 4 ) ∈ ℝ
292 273 291 198 ltdiv1i ⊢ ( 0 < ( 1 0 ↑ 7 ) → ( ( 2 7 · 4 ) < ( 1 0 0 · 4 ) ↔ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) ) )
293 201 292 ax-mp ⊢ ( ( 2 7 · 4 ) < ( 1 0 0 · 4 ) ↔ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) )
294 290 293 mpbi ⊢ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) )
295 8nn ⊢ 8 ∈ ℕ
296 nnrp ⊢ ( 8 ∈ ℕ → 8 ∈ ℝ+ )
297 295 296 ax-mp ⊢ 8 ∈ ℝ+
298 59 297 rpdp2cl ⊢ 4 8 ∈ ℝ+
299 19 298 rpdp2cl ⊢ 2 4 8 ∈ ℝ+
300 19 299 rpdp2cl ⊢ 2 2 4 8 ∈ ℝ+
301 59 300 dpgti ⊢ 4 < ( 4 . 2 2 4 8 )
302 72 recni ⊢ ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℂ
303 198 recni ⊢ ( 1 0 ↑ 7 ) ∈ ℂ
304 302 303 mulcli ⊢ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) ∈ ℂ
305 16 123 gtneii ⊢ 1 0 ≠ 0
306 190 305 pm3.2i ⊢ ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 )
307 287 recni ⊢ 1 0 0 ∈ ℂ
308 286 nnne0i ⊢ 1 0 0 ≠ 0
309 307 308 pm3.2i ⊢ ( 1 0 0 ∈ ℂ ∧ 1 0 0 ≠ 0 )
310 divdiv1 ⊢ ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) ∈ ℂ ∧ ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) ∧ ( 1 0 0 ∈ ℂ ∧ 1 0 0 ≠ 0 ) ) → ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / 1 0 ) / 1 0 0 ) = ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / ( 1 0 · 1 0 0 ) ) )
311 304 306 309 310 mp3an ⊢ ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / 1 0 ) / 1 0 0 ) = ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / ( 1 0 · 1 0 0 ) )
312 302 303 190 305 div23i ⊢ ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / 1 0 ) = ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) )
313 312 oveq1i ⊢ ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / 1 0 ) / 1 0 0 ) = ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) / 1 0 0 )
314 190 307 mulcli ⊢ ( 1 0 · 1 0 0 ) ∈ ℂ
315 190 307 305 308 mulne0i ⊢ ( 1 0 · 1 0 0 ) ≠ 0
316 302 303 314 315 divassi ⊢ ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / ( 1 0 · 1 0 0 ) ) = ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( ( 1 0 ↑ 7 ) / ( 1 0 · 1 0 0 ) ) )
317 expp1 ⊢ ( ( 1 0 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 1 0 ↑ ( 2 + 1 ) ) = ( ( 1 0 ↑ 2 ) · 1 0 ) )
318 190 19 317 mp2an ⊢ ( 1 0 ↑ ( 2 + 1 ) ) = ( ( 1 0 ↑ 2 ) · 1 0 )
319 sq10 ⊢ ( 1 0 ↑ 2 ) = 1 0 0
320 319 oveq1i ⊢ ( ( 1 0 ↑ 2 ) · 1 0 ) = ( 1 0 0 · 1 0 )
321 307 190 mulcomi ⊢ ( 1 0 0 · 1 0 ) = ( 1 0 · 1 0 0 )
322 318 320 321 3eqtrri ⊢ ( 1 0 · 1 0 0 ) = ( 1 0 ↑ ( 2 + 1 ) )
323 2p1e3 ⊢ ( 2 + 1 ) = 3
324 323 oveq2i ⊢ ( 1 0 ↑ ( 2 + 1 ) ) = ( 1 0 ↑ 3 )
325 322 324 eqtri ⊢ ( 1 0 · 1 0 0 ) = ( 1 0 ↑ 3 )
326 325 oveq2i ⊢ ( ( 1 0 ↑ 7 ) / ( 1 0 · 1 0 0 ) ) = ( ( 1 0 ↑ 7 ) / ( 1 0 ↑ 3 ) )
327 74 nn0zi ⊢ 3 ∈ ℤ
328 199 327 pm3.2i ⊢ ( 7 ∈ ℤ ∧ 3 ∈ ℤ )
329 expsub ⊢ ( ( ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) ∧ ( 7 ∈ ℤ ∧ 3 ∈ ℤ ) ) → ( 1 0 ↑ ( 7 − 3 ) ) = ( ( 1 0 ↑ 7 ) / ( 1 0 ↑ 3 ) ) )
330 306 328 329 mp2an ⊢ ( 1 0 ↑ ( 7 − 3 ) ) = ( ( 1 0 ↑ 7 ) / ( 1 0 ↑ 3 ) )
331 7cn ⊢ 7 ∈ ℂ
332 4p3e7 ⊢ ( 4 + 3 ) = 7
333 263 112 332 addcomli ⊢ ( 3 + 4 ) = 7
334 331 112 263 333 subaddrii ⊢ ( 7 − 3 ) = 4
335 334 oveq2i ⊢ ( 1 0 ↑ ( 7 − 3 ) ) = ( 1 0 ↑ 4 )
336 326 330 335 3eqtr2i ⊢ ( ( 1 0 ↑ 7 ) / ( 1 0 · 1 0 0 ) ) = ( 1 0 ↑ 4 )
337 336 oveq2i ⊢ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( ( 1 0 ↑ 7 ) / ( 1 0 · 1 0 0 ) ) ) = ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 4 ) )
338 173 numexp1 ⊢ ( 1 0 ↑ 1 ) = 1 0
339 338 oveq2i ⊢ ( ( 0 . 4 2 2 4 8 ) · ( 1 0 ↑ 1 ) ) = ( ( 0 . 4 2 2 4 8 ) · 1 0 )
340 59 300 rpdp2cl ⊢ 4 2 2 4 8 ∈ ℝ+
341 25 nnzi ⊢ 1 ∈ ℤ
342 89 nnzi ⊢ 2 ∈ ℤ
343 26 340 98 341 342 dpexpp1 ⊢ ( ( 0 . 4 2 2 4 8 ) · ( 1 0 ↑ 1 ) ) = ( ( 0 . 0 4 2 2 4 8 ) · ( 1 0 ↑ 2 ) )
344 26 340 rpdp2cl ⊢ 0 4 2 2 4 8 ∈ ℝ+
345 26 344 323 342 327 dpexpp1 ⊢ ( ( 0 . 0 4 2 2 4 8 ) · ( 1 0 ↑ 2 ) ) = ( ( 0 . 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 3 ) )
346 26 344 rpdp2cl ⊢ 0 0 4 2 2 4 8 ∈ ℝ+
347 3p1e4 ⊢ ( 3 + 1 ) = 4
348 26 346 347 327 247 dpexpp1 ⊢ ( ( 0 . 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 3 ) ) = ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 4 ) )
349 343 345 348 3eqtri ⊢ ( ( 0 . 4 2 2 4 8 ) · ( 1 0 ↑ 1 ) ) = ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 4 ) )
350 59 300 0dp2dp ⊢ ( ( 0 . 4 2 2 4 8 ) · 1 0 ) = ( 4 . 2 2 4 8 )
351 339 349 350 3eqtr3i ⊢ ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 4 ) ) = ( 4 . 2 2 4 8 )
352 316 337 351 3eqtri ⊢ ( ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 1 0 ↑ 7 ) ) / ( 1 0 · 1 0 0 ) ) = ( 4 . 2 2 4 8 )
353 311 313 352 3eqtr3i ⊢ ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) / 1 0 0 ) = ( 4 . 2 2 4 8 )
354 301 353 breqtrri ⊢ 4 < ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) / 1 0 0 )
355 72 18 305 redivcli ⊢ ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ∈ ℝ
356 355 198 remulcli ⊢ ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) ∈ ℝ
357 286 nngt0i ⊢ 0 < 1 0 0
358 287 357 pm3.2i ⊢ ( 1 0 0 ∈ ℝ ∧ 0 < 1 0 0 )
359 ltmuldiv2 ⊢ ( ( 4 ∈ ℝ ∧ ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) ∈ ℝ ∧ ( 1 0 0 ∈ ℝ ∧ 0 < 1 0 0 ) ) → ( ( 1 0 0 · 4 ) < ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) ↔ 4 < ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) / 1 0 0 ) ) )
360 3 356 358 359 mp3an ⊢ ( ( 1 0 0 · 4 ) < ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) ↔ 4 < ( ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) / 1 0 0 ) )
361 354 360 mpbir ⊢ ( 1 0 0 · 4 ) < ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) )
362 ltdivmul2 ⊢ ( ( ( 1 0 0 · 4 ) ∈ ℝ ∧ ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ∈ ℝ ∧ ( ( 1 0 ↑ 7 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 7 ) ) ) → ( ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ↔ ( 1 0 0 · 4 ) < ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) ) )
363 291 355 226 362 mp3an ⊢ ( ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ↔ ( 1 0 0 · 4 ) < ( ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) · ( 1 0 ↑ 7 ) ) )
364 361 363 mpbir ⊢ ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 )
365 291 198 277 redivcli ⊢ ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) ∈ ℝ
366 279 365 355 lttri ⊢ ( ( ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) ∧ ( ( 1 0 0 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ) → ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) )
367 294 364 366 mp2an ⊢ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 )
368 226 simpli ⊢ ( 1 0 ↑ 7 ) ∈ ℝ
369 273 368 277 redivcli ⊢ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) ∈ ℝ
370 55 369 355 lttri ⊢ ( ( ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) ∧ ( ( 2 7 · 4 ) / ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ) → ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) )
371 281 367 370 mp2an ⊢ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 )
372 125 124 mpbi ⊢ ( 1 0 ∈ ℝ ∧ 0 < 1 0 )
373 ltmuldiv2 ⊢ ( ( ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ∈ ℝ ∧ ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ ∧ ( 1 0 ∈ ℝ ∧ 0 < 1 0 ) ) → ( ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) ↔ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) ) )
374 55 72 372 373 mp3an ⊢ ( ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) ↔ ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) / 1 0 ) )
375 371 374 mpbir ⊢ ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 )
376 12 55 remulcli ⊢ ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) ∈ ℝ
377 18 55 remulcli ⊢ ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) ∈ ℝ
378 376 377 72 lttri ⊢ ( ( ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) ∧ ( 1 0 · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) )
379 189 375 378 mp2an ⊢ ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 )
380 379 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ ( 1 0 ↑ 2 7 ) ) / ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) )
381 47 57 73 162 380 lelttrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) )