hgt750lem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hgt750lem		Structured version Visualization version GIF version

Theorem hgt750lem 34815

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

**Assertion**
Ref	Expression
hgt750lem	⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))

**Proof of Theorem hgt750lem**
Step	Hyp	Ref	Expression
1		7nn0 12454	. . . . 5 ⊢ 7 ∈ ℕ₀
2		3re 12256	. . . . . . 7 ⊢ 3 ∈ ℝ
3		4re 12260	. . . . . . . . 9 ⊢ 4 ∈ ℝ
4		8re 12272	. . . . . . . . 9 ⊢ 8 ∈ ℝ
5	3, 4	pm3.2i 470	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
6		dp2cl 32958	. . . . . . . 8 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
7	5, 6	ax-mp 5	. . . . . . 7 ⊢ _48 ∈ ℝ
8	2, 7	pm3.2i 470	. . . . . 6 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
9		dp2cl 32958	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
10	8, 9	ax-mp 5	. . . . 5 ⊢ _3_48 ∈ ℝ
11		dpcl 32969	. . . . 5 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
12	1, 10, 11	mp2an 693	. . . 4 ⊢ (7._3_48) ∈ ℝ
13	12	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (7._3_48) ∈ ℝ)
14		nn0re 12441	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	14	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ)
16		0re 11141	. . . . . . . 8 ⊢ 0 ∈ ℝ
17	16	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ∈ ℝ)
18		10re 12658	. . . . . . . . 9 ⊢ ;10 ∈ ℝ
19		2nn0 12449	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
20	19, 1	deccl 12654	. . . . . . . . 9 ⊢ ;27 ∈ ℕ₀
21		reexpcl 14035	. . . . . . . . 9 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀) → (;10↑;27) ∈ ℝ)
22	18, 20, 21	mp2an 693	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
23	22	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ∈ ℝ)
24		0lt1 11667	. . . . . . . . 9 ⊢ 0 < 1
25		1nn 12180	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
26		0nn0 12447	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
27		1nn0 12448	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
28		1re 11139	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
29		9re 12275	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
30		1lt9 12377	. . . . . . . . . . . 12 ⊢ 1 < 9
31	28, 29, 30	ltleii 11264	. . . . . . . . . . 11 ⊢ 1 ≤ 9
32	25, 26, 27, 31	declei 12675	. . . . . . . . . 10 ⊢ 1 ≤ ;10
33		expge1 14056	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀ ∧ 1 ≤ ;10) → 1 ≤ (;10↑;27))
34	18, 20, 32, 33	mp3an 1464	. . . . . . . . 9 ⊢ 1 ≤ (;10↑;27)
35	16, 28, 22	ltletri 11269	. . . . . . . . 9 ⊢ ((0 < 1 ∧ 1 ≤ (;10↑;27)) → 0 < (;10↑;27))
36	24, 34, 35	mp2an 693	. . . . . . . 8 ⊢ 0 < (;10↑;27)
37	36	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (;10↑;27))
38		simpr 484	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ≤ 𝑁)
39	17, 23, 15, 37, 38	ltletrd 11301	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < 𝑁)
40	15, 39	elrpd 12978	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ⁺)
41	40	relogcld 26604	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (log‘𝑁) ∈ ℝ)
42	40	rpge0d 12985	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ≤ 𝑁)
43	15, 42	resqrtcld 15375	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ∈ ℝ)
44	40	sqrtgt0d 15370	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (√‘𝑁))
45	17, 44	gtned 11276	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ≠ 0)
46	41, 43, 45	redivcld 11978	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
47	13, 46	remulcld 11170	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
48		elrp 12939	. . . . . . 7 ⊢ ((;10↑;27) ∈ ℝ⁺ ↔ ((;10↑;27) ∈ ℝ ∧ 0 < (;10↑;27)))
49	22, 36, 48	mpbir2an 712	. . . . . 6 ⊢ (;10↑;27) ∈ ℝ⁺
50		relogcl 26556	. . . . . 6 ⊢ ((;10↑;27) ∈ ℝ⁺ → (log‘(;10↑;27)) ∈ ℝ)
51	49, 50	ax-mp 5	. . . . 5 ⊢ (log‘(;10↑;27)) ∈ ℝ
52	22, 36	sqrtpclii 15340	. . . . 5 ⊢ (√‘(;10↑;27)) ∈ ℝ
53	22, 36	sqrtgt0ii 15341	. . . . . 6 ⊢ 0 < (√‘(;10↑;27))
54	16, 53	gtneii 11253	. . . . 5 ⊢ (√‘(;10↑;27)) ≠ 0
55	51, 52, 54	redivcli 11917	. . . 4 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ
56	55	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ)
57	13, 56	remulcld 11170	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ)
58		qssre 12904	. . . . 5 ⊢ ℚ ⊆ ℝ
59		4nn0 12451	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
60		nn0ssq 12902	. . . . . . . . . . . . 13 ⊢ ℕ₀ ⊆ ℚ
61		8nn0 12455	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ₀
62	60, 61	sselii 3919	. . . . . . . . . . . 12 ⊢ 8 ∈ ℚ
63	59, 62	dp2clq 32959	. . . . . . . . . . 11 ⊢ _48 ∈ ℚ
64	19, 63	dp2clq 32959	. . . . . . . . . 10 ⊢ _2_48 ∈ ℚ
65	19, 64	dp2clq 32959	. . . . . . . . 9 ⊢ _2_2_48 ∈ ℚ
66	59, 65	dp2clq 32959	. . . . . . . 8 ⊢ _4_2_2_48 ∈ ℚ
67	26, 66	dp2clq 32959	. . . . . . 7 ⊢ _0_4_2_2_48 ∈ ℚ
68	26, 67	dp2clq 32959	. . . . . 6 ⊢ _0_0_4_2_2_48 ∈ ℚ
69	26, 68	dp2clq 32959	. . . . 5 ⊢ _0_0_0_4_2_2_48 ∈ ℚ
70	58, 69	sselii 3919	. . . 4 ⊢ _0_0_0_4_2_2_48 ∈ ℝ
71		dpcl 32969	. . . 4 ⊢ ((0 ∈ ℕ₀ ∧ _0_0_0_4_2_2_48 ∈ ℝ) → (0._0_0_0_4_2_2_48) ∈ ℝ)
72	26, 70, 71	mp2an 693	. . 3 ⊢ (0._0_0_0_4_2_2_48) ∈ ℝ
73	72	a1i 11	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (0._0_0_0_4_2_2_48) ∈ ℝ)
74		3nn0 12450	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
75		8pos 12288	. . . . . . . . . . 11 ⊢ 0 < 8
76		elrp 12939	. . . . . . . . . . 11 ⊢ (8 ∈ ℝ⁺ ↔ (8 ∈ ℝ ∧ 0 < 8))
77	4, 75, 76	mpbir2an 712	. . . . . . . . . 10 ⊢ 8 ∈ ℝ⁺
78	59, 77	rpdp2cl 32960	. . . . . . . . 9 ⊢ _48 ∈ ℝ⁺
79	74, 78	rpdp2cl 32960	. . . . . . . 8 ⊢ _3_48 ∈ ℝ⁺
80	1, 79	rpdpcl 32981	. . . . . . 7 ⊢ (7._3_48) ∈ ℝ⁺
81		elrp 12939	. . . . . . 7 ⊢ ((7._3_48) ∈ ℝ⁺ ↔ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48)))
82	80, 81	mpbi 230	. . . . . 6 ⊢ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48))
83	82	simpri 485	. . . . 5 ⊢ 0 < (7._3_48)
84	16, 12, 83	ltleii 11264	. . . 4 ⊢ 0 ≤ (7._3_48)
85	84	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ≤ (7._3_48))
86	49	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ∈ ℝ⁺)
87		2cn 12251	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
88	87	mullidi 11145	. . . . . . . . 9 ⊢ (1 · 2) = 2
89		2nn 12249	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
90	89, 1, 27, 31	declei 12675	. . . . . . . . . 10 ⊢ 1 ≤ ;27
91		2pos 12279	. . . . . . . . . . 11 ⊢ 0 < 2
92	20	nn0rei 12443	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℝ
93		2re 12250	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
94	28, 92, 93	lemul1i 12073	. . . . . . . . . . 11 ⊢ (0 < 2 → (1 ≤ ;27 ↔ (1 · 2) ≤ (;27 · 2)))
95	91, 94	ax-mp 5	. . . . . . . . . 10 ⊢ (1 ≤ ;27 ↔ (1 · 2) ≤ (;27 · 2))
96	90, 95	mpbi 230	. . . . . . . . 9 ⊢ (1 · 2) ≤ (;27 · 2)
97	88, 96	eqbrtrri 5109	. . . . . . . 8 ⊢ 2 ≤ (;27 · 2)
98		1p1e2 12296	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
99		loge 26567	. . . . . . . . . . . . . 14 ⊢ (log‘e) = 1
100		egt2lt3 16168	. . . . . . . . . . . . . . . 16 ⊢ (2 < e ∧ e < 3)
101	100	simpri 485	. . . . . . . . . . . . . . 15 ⊢ e < 3
102		epr 16170	. . . . . . . . . . . . . . . 16 ⊢ e ∈ ℝ⁺
103		3rp 12943	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ⁺
104		logltb 26581	. . . . . . . . . . . . . . . 16 ⊢ ((e ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → (e < 3 ↔ (log‘e) < (log‘3)))
105	102, 103, 104	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ (e < 3 ↔ (log‘e) < (log‘3))
106	101, 105	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (log‘e) < (log‘3)
107	99, 106	eqbrtrri 5109	. . . . . . . . . . . . 13 ⊢ 1 < (log‘3)
108		relogcl 26556	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
109	103, 108	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (log‘3) ∈ ℝ
110	28, 28, 109, 109	lt2addi 11707	. . . . . . . . . . . . 13 ⊢ ((1 < (log‘3) ∧ 1 < (log‘3)) → (1 + 1) < ((log‘3) + (log‘3)))
111	107, 107, 110	mp2an 693	. . . . . . . . . . . 12 ⊢ (1 + 1) < ((log‘3) + (log‘3))
112		3cn 12257	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
113		3ne0 12282	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 0
114		logmul2 26597	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ⁺) → (log‘(3 · 3)) = ((log‘3) + (log‘3)))
115	112, 113, 103, 114	mp3an 1464	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) = ((log‘3) + (log‘3))
116		3t3e9 12338	. . . . . . . . . . . . . . 15 ⊢ (3 · 3) = 9
117	116	fveq2i 6839	. . . . . . . . . . . . . 14 ⊢ (log‘(3 · 3)) = (log‘9)
118		9lt10 12770	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
119	29, 18, 118	ltleii 11264	. . . . . . . . . . . . . . 15 ⊢ 9 ≤ ;10
120		9pos 12289	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 9
121		elrp 12939	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ⁺ ↔ (9 ∈ ℝ ∧ 0 < 9))
122	29, 120, 121	mpbir2an 712	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ⁺
123		10pos 12656	. . . . . . . . . . . . . . . . 17 ⊢ 0 < ;10
124		elrp 12939	. . . . . . . . . . . . . . . . 17 ⊢ (;10 ∈ ℝ⁺ ↔ (;10 ∈ ℝ ∧ 0 < ;10))
125	18, 123, 124	mpbir2an 712	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℝ⁺
126		logleb 26584	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ⁺ ∧ ;10 ∈ ℝ⁺) → (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10)))
127	122, 125, 126	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10))
128	119, 127	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (log‘9) ≤ (log‘;10)
129	117, 128	eqbrtri 5107	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) ≤ (log‘;10)
130	115, 129	eqbrtrri 5109	. . . . . . . . . . . 12 ⊢ ((log‘3) + (log‘3)) ≤ (log‘;10)
131	28, 28	readdcli 11155	. . . . . . . . . . . . 13 ⊢ (1 + 1) ∈ ℝ
132	109, 109	readdcli 11155	. . . . . . . . . . . . 13 ⊢ ((log‘3) + (log‘3)) ∈ ℝ
133		relogcl 26556	. . . . . . . . . . . . . 14 ⊢ (;10 ∈ ℝ⁺ → (log‘;10) ∈ ℝ)
134	125, 133	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (log‘;10) ∈ ℝ
135	131, 132, 134	ltletri 11269	. . . . . . . . . . . 12 ⊢ (((1 + 1) < ((log‘3) + (log‘3)) ∧ ((log‘3) + (log‘3)) ≤ (log‘;10)) → (1 + 1) < (log‘;10))
136	111, 130, 135	mp2an 693	. . . . . . . . . . 11 ⊢ (1 + 1) < (log‘;10)
137	98, 136	eqbrtrri 5109	. . . . . . . . . 10 ⊢ 2 < (log‘;10)
138	93, 134	ltlei 11263	. . . . . . . . . 10 ⊢ (2 < (log‘;10) → 2 ≤ (log‘;10))
139	137, 138	ax-mp 5	. . . . . . . . 9 ⊢ 2 ≤ (log‘;10)
140	16, 29, 120	ltleii 11264	. . . . . . . . . . 11 ⊢ 0 ≤ 9
141	89, 1, 26, 140	decltdi 12678	. . . . . . . . . 10 ⊢ 0 < ;27
142	93, 134, 92	lemul2i 12074	. . . . . . . . . 10 ⊢ (0 < ;27 → (2 ≤ (log‘;10) ↔ (;27 · 2) ≤ (;27 · (log‘;10))))
143	141, 142	ax-mp 5	. . . . . . . . 9 ⊢ (2 ≤ (log‘;10) ↔ (;27 · 2) ≤ (;27 · (log‘;10)))
144	139, 143	mpbi 230	. . . . . . . 8 ⊢ (;27 · 2) ≤ (;27 · (log‘;10))
145	92, 93	remulcli 11156	. . . . . . . . 9 ⊢ (;27 · 2) ∈ ℝ
146	20	nn0zi 12547	. . . . . . . . . . 11 ⊢ ;27 ∈ ℤ
147		relogexp 26577	. . . . . . . . . . 11 ⊢ ((;10 ∈ ℝ⁺ ∧ ;27 ∈ ℤ) → (log‘(;10↑;27)) = (;27 · (log‘;10)))
148	125, 146, 147	mp2an 693	. . . . . . . . . 10 ⊢ (log‘(;10↑;27)) = (;27 · (log‘;10))
149	148, 51	eqeltrri 2834	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) ∈ ℝ
150	93, 145, 149	letri 11270	. . . . . . . 8 ⊢ ((2 ≤ (;27 · 2) ∧ (;27 · 2) ≤ (;27 · (log‘;10))) → 2 ≤ (;27 · (log‘;10)))
151	97, 144, 150	mp2an 693	. . . . . . 7 ⊢ 2 ≤ (;27 · (log‘;10))
152		relogef 26563	. . . . . . . 8 ⊢ (2 ∈ ℝ → (log‘(exp‘2)) = 2)
153	93, 152	ax-mp 5	. . . . . . 7 ⊢ (log‘(exp‘2)) = 2
154	151, 153, 148	3brtr4i 5116	. . . . . 6 ⊢ (log‘(exp‘2)) ≤ (log‘(;10↑;27))
155		rpefcl 16066	. . . . . . . 8 ⊢ (2 ∈ ℝ → (exp‘2) ∈ ℝ⁺)
156	93, 155	ax-mp 5	. . . . . . 7 ⊢ (exp‘2) ∈ ℝ⁺
157		logleb 26584	. . . . . . 7 ⊢ (((exp‘2) ∈ ℝ⁺ ∧ (;10↑;27) ∈ ℝ⁺) → ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27))))
158	156, 49, 157	mp2an 693	. . . . . 6 ⊢ ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27)))
159	154, 158	mpbir 231	. . . . 5 ⊢ (exp‘2) ≤ (;10↑;27)
160	159	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (exp‘2) ≤ (;10↑;27))
161	86, 40, 160, 38	logdivsqrle 34814	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ≤ ((log‘(;10↑;27)) / (√‘(;10↑;27))))
162	46, 56, 13, 85, 161	lemul2ad 12091	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ≤ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
163		3lt10 12776	. . . . . . . 8 ⊢ 3 < ;10
164		4lt10 12775	. . . . . . . . 9 ⊢ 4 < ;10
165		8lt10 12771	. . . . . . . . 9 ⊢ 8 < ;10
166	59, 77, 164, 165	dp2lt10 32962	. . . . . . . 8 ⊢ _48 < ;10
167	74, 78, 163, 166	dp2lt10 32962	. . . . . . 7 ⊢ _3_48 < ;10
168		7p1e8 12320	. . . . . . 7 ⊢ (7 + 1) = 8
169	1, 79, 61, 167, 168	dplti 32983	. . . . . 6 ⊢ (7._3_48) < 8
170	58, 62	sselii 3919	. . . . . . 7 ⊢ 8 ∈ ℝ
171	12, 170, 18	lttri 11267	. . . . . 6 ⊢ (((7._3_48) < 8 ∧ 8 < ;10) → (7._3_48) < ;10)
172	169, 165, 171	mp2an 693	. . . . 5 ⊢ (7._3_48) < ;10
173	27, 26	deccl 12654	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
174	173	numexp0 17041	. . . . . . . . 9 ⊢ (;10↑0) = 1
175		0z 12530	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
176	18, 175, 146	3pm3.2i 1341	. . . . . . . . . 10 ⊢ (;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ)
177		1lt10 12778	. . . . . . . . . . 11 ⊢ 1 < ;10
178	177, 141	pm3.2i 470	. . . . . . . . . 10 ⊢ (1 < ;10 ∧ 0 < ;27)
179		ltexp2a 14123	. . . . . . . . . 10 ⊢ (((;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < ;27)) → (;10↑0) < (;10↑;27))
180	176, 178, 179	mp2an 693	. . . . . . . . 9 ⊢ (;10↑0) < (;10↑;27)
181	174, 180	eqbrtrri 5109	. . . . . . . 8 ⊢ 1 < (;10↑;27)
182		loggt0b 26613	. . . . . . . . 9 ⊢ ((;10↑;27) ∈ ℝ⁺ → (0 < (log‘(;10↑;27)) ↔ 1 < (;10↑;27)))
183	49, 182	ax-mp 5	. . . . . . . 8 ⊢ (0 < (log‘(;10↑;27)) ↔ 1 < (;10↑;27))
184	181, 183	mpbir 231	. . . . . . 7 ⊢ 0 < (log‘(;10↑;27))
185	51, 52	divgt0i 12059	. . . . . . 7 ⊢ ((0 < (log‘(;10↑;27)) ∧ 0 < (√‘(;10↑;27))) → 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))))
186	184, 53, 185	mp2an 693	. . . . . 6 ⊢ 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27)))
187	12, 18, 55	ltmul1i 12069	. . . . . 6 ⊢ (0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))) → ((7._3_48) < ;10 ↔ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27))))))
188	186, 187	ax-mp 5	. . . . 5 ⊢ ((7._3_48) < ;10 ↔ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
189	172, 188	mpbi 230	. . . 4 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27))))
190	18	recni 11154	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℂ
191		expmul 14064	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℂ ∧ 7 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (;10↑(7 · 2)) = ((;10↑7)↑2))
192	190, 1, 19, 191	mp3an 1464	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = ((;10↑7)↑2)
193		7t2e14 12748	. . . . . . . . . . . . 13 ⊢ (7 · 2) = ;14
194	193	oveq2i 7373	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = (;10↑;14)
195	192, 194	eqtr3i 2762	. . . . . . . . . . 11 ⊢ ((;10↑7)↑2) = (;10↑;14)
196	195	fveq2i 6839	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (√‘(;10↑;14))
197		reexpcl 14035	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℕ₀) → (;10↑7) ∈ ℝ)
198	18, 1, 197	mp2an 693	. . . . . . . . . . 11 ⊢ (;10↑7) ∈ ℝ
199	1	nn0zi 12547	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℤ
200		expgt0 14052	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑7))
201	18, 199, 123, 200	mp3an 1464	. . . . . . . . . . . 12 ⊢ 0 < (;10↑7)
202	16, 198, 201	ltleii 11264	. . . . . . . . . . 11 ⊢ 0 ≤ (;10↑7)
203		sqrtsq 15226	. . . . . . . . . . 11 ⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤ (;10↑7)) → (√‘((;10↑7)↑2)) = (;10↑7))
204	198, 202, 203	mp2an 693	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (;10↑7)
205	196, 204	eqtr3i 2762	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) = (;10↑7)
206	27, 59	deccl 12654	. . . . . . . . . . . . 13 ⊢ ;14 ∈ ℕ₀
207	206	nn0zi 12547	. . . . . . . . . . . 12 ⊢ ;14 ∈ ℤ
208	18, 207, 146	3pm3.2i 1341	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ)
209		1lt2 12342	. . . . . . . . . . . . 13 ⊢ 1 < 2
210	27, 19, 59, 1, 164, 209	decltc 12668	. . . . . . . . . . . 12 ⊢ ;14 < ;27
211	177, 210	pm3.2i 470	. . . . . . . . . . 11 ⊢ (1 < ;10 ∧ ;14 < ;27)
212		ltexp2a 14123	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27))
213	208, 211, 212	mp2an 693	. . . . . . . . . 10 ⊢ (;10↑;14) < (;10↑;27)
214		reexpcl 14035	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℕ₀) → (;10↑;14) ∈ ℝ)
215	18, 206, 214	mp2an 693	. . . . . . . . . . . 12 ⊢ (;10↑;14) ∈ ℝ
216		expgt0 14052	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14))
217	18, 207, 123, 216	mp3an 1464	. . . . . . . . . . . . 13 ⊢ 0 < (;10↑;14)
218	16, 215, 217	ltleii 11264	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;14)
219	215, 218	pm3.2i 470	. . . . . . . . . . 11 ⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14))
220	16, 22, 36	ltleii 11264	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;27)
221	22, 220	pm3.2i 470	. . . . . . . . . . 11 ⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))
222		sqrtlt 15218	. . . . . . . . . . 11 ⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))))
223	219, 221, 222	mp2an 693	. . . . . . . . . 10 ⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))
224	213, 223	mpbi 230	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) < (√‘(;10↑;27))
225	205, 224	eqbrtrri 5109	. . . . . . . 8 ⊢ (;10↑7) < (√‘(;10↑;27))
226	198, 201	pm3.2i 470	. . . . . . . . 9 ⊢ ((;10↑7) ∈ ℝ ∧ 0 < (;10↑7))
227	52, 53	pm3.2i 470	. . . . . . . . 9 ⊢ ((√‘(;10↑;27)) ∈ ℝ ∧ 0 < (√‘(;10↑;27)))
228	51, 184	pm3.2i 470	. . . . . . . . 9 ⊢ ((log‘(;10↑;27)) ∈ ℝ ∧ 0 < (log‘(;10↑;27)))
229		ltdiv2 12037	. . . . . . . . 9 ⊢ ((((;10↑7) ∈ ℝ ∧ 0 < (;10↑7)) ∧ ((√‘(;10↑;27)) ∈ ℝ ∧ 0 < (√‘(;10↑;27))) ∧ ((log‘(;10↑;27)) ∈ ℝ ∧ 0 < (log‘(;10↑;27)))) → ((;10↑7) < (√‘(;10↑;27)) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7))))
230	226, 227, 228, 229	mp3an 1464	. . . . . . . 8 ⊢ ((;10↑7) < (√‘(;10↑;27)) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7)))
231	225, 230	mpbi 230	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7))
232		6nn 12265	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
233	232	nngt0i 12211	. . . . . . . . . . . . . 14 ⊢ 0 < 6
234	27, 26, 232, 233	declt 12667	. . . . . . . . . . . . 13 ⊢ ;10 < ;16
235		6nn0 12453	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ₀
236	27, 235	deccl 12654	. . . . . . . . . . . . . . . 16 ⊢ ;16 ∈ ℕ₀
237	236	nn0rei 12443	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℝ
238	25, 235, 26, 123	declti 12677	. . . . . . . . . . . . . . 15 ⊢ 0 < ;16
239		elrp 12939	. . . . . . . . . . . . . . 15 ⊢ (;16 ∈ ℝ⁺ ↔ (;16 ∈ ℝ ∧ 0 < ;16))
240	237, 238, 239	mpbir2an 712	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℝ⁺
241		logltb 26581	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ⁺ ∧ ;16 ∈ ℝ⁺) → (;10 < ;16 ↔ (log‘;10) < (log‘;16)))
242	125, 240, 241	mp2an 693	. . . . . . . . . . . . 13 ⊢ (;10 < ;16 ↔ (log‘;10) < (log‘;16))
243	234, 242	mpbi 230	. . . . . . . . . . . 12 ⊢ (log‘;10) < (log‘;16)
244		2exp4 17050	. . . . . . . . . . . . . 14 ⊢ (2↑4) = ;16
245	244	fveq2i 6839	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (log‘;16)
246		2rp 12942	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
247	59	nn0zi 12547	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
248		relogexp 26577	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ 4 ∈ ℤ) → (log‘(2↑4)) = (4 · (log‘2)))
249	246, 247, 248	mp2an 693	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (4 · (log‘2))
250	245, 249	eqtr3i 2762	. . . . . . . . . . . 12 ⊢ (log‘;16) = (4 · (log‘2))
251	243, 250	breqtri 5111	. . . . . . . . . . 11 ⊢ (log‘;10) < (4 · (log‘2))
252	100	simpli 483	. . . . . . . . . . . . . . 15 ⊢ 2 < e
253		logltb 26581	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ⁺ ∧ e ∈ ℝ⁺) → (2 < e ↔ (log‘2) < (log‘e)))
254	246, 102, 253	mp2an 693	. . . . . . . . . . . . . . 15 ⊢ (2 < e ↔ (log‘2) < (log‘e))
255	252, 254	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (log‘2) < (log‘e)
256	255, 99	breqtri 5111	. . . . . . . . . . . . 13 ⊢ (log‘2) < 1
257		4pos 12283	. . . . . . . . . . . . . 14 ⊢ 0 < 4
258		relogcl 26556	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
259	246, 258	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (log‘2) ∈ ℝ
260	259, 28, 3	ltmul2i 12072	. . . . . . . . . . . . . 14 ⊢ (0 < 4 → ((log‘2) < 1 ↔ (4 · (log‘2)) < (4 · 1)))
261	257, 260	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((log‘2) < 1 ↔ (4 · (log‘2)) < (4 · 1))
262	256, 261	mpbi 230	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) < (4 · 1)
263		4cn 12261	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℂ
264	263	mulridi 11144	. . . . . . . . . . . 12 ⊢ (4 · 1) = 4
265	262, 264	breqtri 5111	. . . . . . . . . . 11 ⊢ (4 · (log‘2)) < 4
266	3, 259	remulcli 11156	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) ∈ ℝ
267	134, 266, 3	lttri 11267	. . . . . . . . . . 11 ⊢ (((log‘;10) < (4 · (log‘2)) ∧ (4 · (log‘2)) < 4) → (log‘;10) < 4)
268	251, 265, 267	mp2an 693	. . . . . . . . . 10 ⊢ (log‘;10) < 4
269	134, 3, 92	ltmul2i 12072	. . . . . . . . . . 11 ⊢ (0 < ;27 → ((log‘;10) < 4 ↔ (;27 · (log‘;10)) < (;27 · 4)))
270	141, 269	ax-mp 5	. . . . . . . . . 10 ⊢ ((log‘;10) < 4 ↔ (;27 · (log‘;10)) < (;27 · 4))
271	268, 270	mpbi 230	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) < (;27 · 4)
272	148, 271	eqbrtri 5107	. . . . . . . 8 ⊢ (log‘(;10↑;27)) < (;27 · 4)
273	92, 3	remulcli 11156	. . . . . . . . . 10 ⊢ (;27 · 4) ∈ ℝ
274	51, 273, 198	ltdiv1i 12070	. . . . . . . . 9 ⊢ (0 < (;10↑7) → ((log‘(;10↑;27)) < (;27 · 4) ↔ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))))
275	201, 274	ax-mp 5	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) < (;27 · 4) ↔ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7)))
276	272, 275	mpbi 230	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))
277	16, 201	gtneii 11253	. . . . . . . . 9 ⊢ (;10↑7) ≠ 0
278	51, 198, 277	redivcli 11917	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) / (;10↑7)) ∈ ℝ
279	273, 198, 277	redivcli 11917	. . . . . . . 8 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
280	55, 278, 279	lttri 11267	. . . . . . 7 ⊢ ((((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7)) ∧ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7)))
281	231, 276, 280	mp2an 693	. . . . . 6 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7))
282		7lt10 12772	. . . . . . . . . 10 ⊢ 7 < ;10
283		2lt10 12777	. . . . . . . . . 10 ⊢ 2 < ;10
284	19, 173, 1, 26, 282, 283	decltc 12668	. . . . . . . . 9 ⊢ ;27 < ;;100
285		10nn 12655	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℕ
286	285	decnncl2 12663	. . . . . . . . . . . 12 ⊢ ;;100 ∈ ℕ
287	286	nnrei 12178	. . . . . . . . . . 11 ⊢ ;;100 ∈ ℝ
288	92, 287, 3	ltmul1i 12069	. . . . . . . . . 10 ⊢ (0 < 4 → (;27 < ;;100 ↔ (;27 · 4) < (;;100 · 4)))
289	257, 288	ax-mp 5	. . . . . . . . 9 ⊢ (;27 < ;;100 ↔ (;27 · 4) < (;;100 · 4))
290	284, 289	mpbi 230	. . . . . . . 8 ⊢ (;27 · 4) < (;;100 · 4)
291	287, 3	remulcli 11156	. . . . . . . . . 10 ⊢ (;;100 · 4) ∈ ℝ
292	273, 291, 198	ltdiv1i 12070	. . . . . . . . 9 ⊢ (0 < (;10↑7) → ((;27 · 4) < (;;100 · 4) ↔ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7))))
293	201, 292	ax-mp 5	. . . . . . . 8 ⊢ ((;27 · 4) < (;;100 · 4) ↔ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7)))
294	290, 293	mpbi 230	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7))
295		8nn 12271	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ
296		nnrp 12949	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
297	295, 296	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℝ⁺
298	59, 297	rpdp2cl 32960	. . . . . . . . . . . . 13 ⊢ _48 ∈ ℝ⁺
299	19, 298	rpdp2cl 32960	. . . . . . . . . . . 12 ⊢ _2_48 ∈ ℝ⁺
300	19, 299	rpdp2cl 32960	. . . . . . . . . . 11 ⊢ _2_2_48 ∈ ℝ⁺
301	59, 300	dpgti 32984	. . . . . . . . . 10 ⊢ 4 < (4._2_2_48)
302	72	recni 11154	. . . . . . . . . . . . 13 ⊢ (0._0_0_0_4_2_2_48) ∈ ℂ
303	198	recni 11154	. . . . . . . . . . . . 13 ⊢ (;10↑7) ∈ ℂ
304	302, 303	mulcli 11147	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑7)) ∈ ℂ
305	16, 123	gtneii 11253	. . . . . . . . . . . . 13 ⊢ ;10 ≠ 0
306	190, 305	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (;10 ∈ ℂ ∧ ;10 ≠ 0)
307	287	recni 11154	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℂ
308	286	nnne0i 12212	. . . . . . . . . . . . 13 ⊢ ;;100 ≠ 0
309	307, 308	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (;;100 ∈ ℂ ∧ ;;100 ≠ 0)
310		divdiv1 11861	. . . . . . . . . . . 12 ⊢ ((((0._0_0_0_4_2_2_48) · (;10↑7)) ∈ ℂ ∧ (;10 ∈ ℂ ∧ ;10 ≠ 0) ∧ (;;100 ∈ ℂ ∧ ;;100 ≠ 0)) → ((((0._0_0_0_4_2_2_48) · (;10↑7)) / ;10) / ;;100) = (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100)))
311	304, 306, 309, 310	mp3an 1464	. . . . . . . . . . 11 ⊢ ((((0._0_0_0_4_2_2_48) · (;10↑7)) / ;10) / ;;100) = (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100))
312	302, 303, 190, 305	div23i 11908	. . . . . . . . . . . 12 ⊢ (((0._0_0_0_4_2_2_48) · (;10↑7)) / ;10) = (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7))
313	312	oveq1i 7372	. . . . . . . . . . 11 ⊢ ((((0._0_0_0_4_2_2_48) · (;10↑7)) / ;10) / ;;100) = ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)
314	190, 307	mulcli 11147	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ∈ ℂ
315	190, 307, 305, 308	mulne0i 11788	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ≠ 0
316	302, 303, 314, 315	divassi 11906	. . . . . . . . . . . 12 ⊢ (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100)) = ((0._0_0_0_4_2_2_48) · ((;10↑7) / (;10 · ;;100)))
317		expp1 14025	. . . . . . . . . . . . . . . . . 18 ⊢ ((;10 ∈ ℂ ∧ 2 ∈ ℕ₀) → (;10↑(2 + 1)) = ((;10↑2) · ;10))
318	190, 19, 317	mp2an 693	. . . . . . . . . . . . . . . . 17 ⊢ (;10↑(2 + 1)) = ((;10↑2) · ;10)
319		sq10 14221	. . . . . . . . . . . . . . . . . 18 ⊢ (;10↑2) = ;;100
320	319	oveq1i 7372	. . . . . . . . . . . . . . . . 17 ⊢ ((;10↑2) · ;10) = (;;100 · ;10)
321	307, 190	mulcomi 11148	. . . . . . . . . . . . . . . . 17 ⊢ (;;100 · ;10) = (;10 · ;;100)
322	318, 320, 321	3eqtrri 2765	. . . . . . . . . . . . . . . 16 ⊢ (;10 · ;;100) = (;10↑(2 + 1))
323		2p1e3 12313	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 1) = 3
324	323	oveq2i 7373	. . . . . . . . . . . . . . . 16 ⊢ (;10↑(2 + 1)) = (;10↑3)
325	322, 324	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ (;10 · ;;100) = (;10↑3)
326	325	oveq2i 7373	. . . . . . . . . . . . . 14 ⊢ ((;10↑7) / (;10 · ;;100)) = ((;10↑7) / (;10↑3))
327	74	nn0zi 12547	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
328	199, 327	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℤ ∧ 3 ∈ ℤ)
329		expsub 14067	. . . . . . . . . . . . . . 15 ⊢ (((;10 ∈ ℂ ∧ ;10 ≠ 0) ∧ (7 ∈ ℤ ∧ 3 ∈ ℤ)) → (;10↑(7 − 3)) = ((;10↑7) / (;10↑3)))
330	306, 328, 329	mp2an 693	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = ((;10↑7) / (;10↑3))
331		7cn 12270	. . . . . . . . . . . . . . . 16 ⊢ 7 ∈ ℂ
332		4p3e7 12325	. . . . . . . . . . . . . . . . 17 ⊢ (4 + 3) = 7
333	263, 112, 332	addcomli 11333	. . . . . . . . . . . . . . . 16 ⊢ (3 + 4) = 7
334	331, 112, 263, 333	subaddrii 11478	. . . . . . . . . . . . . . 15 ⊢ (7 − 3) = 4
335	334	oveq2i 7373	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = (;10↑4)
336	326, 330, 335	3eqtr2i 2766	. . . . . . . . . . . . 13 ⊢ ((;10↑7) / (;10 · ;;100)) = (;10↑4)
337	336	oveq2i 7373	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · ((;10↑7) / (;10 · ;;100))) = ((0._0_0_0_4_2_2_48) · (;10↑4))
338	173	numexp1 17042	. . . . . . . . . . . . . 14 ⊢ (;10↑1) = ;10
339	338	oveq2i 7373	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._4_2_2_48) · ;10)
340	59, 300	rpdp2cl 32960	. . . . . . . . . . . . . . 15 ⊢ _4_2_2_48 ∈ ℝ⁺
341	25	nnzi 12546	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
342	89	nnzi 12546	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
343	26, 340, 98, 341, 342	dpexpp1 32986	. . . . . . . . . . . . . 14 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_4_2_2_48) · (;10↑2))
344	26, 340	rpdp2cl 32960	. . . . . . . . . . . . . . 15 ⊢ _0_4_2_2_48 ∈ ℝ⁺
345	26, 344, 323, 342, 327	dpexpp1 32986	. . . . . . . . . . . . . 14 ⊢ ((0._0_4_2_2_48) · (;10↑2)) = ((0._0_0_4_2_2_48) · (;10↑3))
346	26, 344	rpdp2cl 32960	. . . . . . . . . . . . . . 15 ⊢ _0_0_4_2_2_48 ∈ ℝ⁺
347		3p1e4 12316	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
348	26, 346, 347, 327, 247	dpexpp1 32986	. . . . . . . . . . . . . 14 ⊢ ((0._0_0_4_2_2_48) · (;10↑3)) = ((0._0_0_0_4_2_2_48) · (;10↑4))
349	343, 345, 348	3eqtri 2764	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_0_0_4_2_2_48) · (;10↑4))
350	59, 300	0dp2dp 32987	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · ;10) = (4._2_2_48)
351	339, 349, 350	3eqtr3i 2768	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑4)) = (4._2_2_48)
352	316, 337, 351	3eqtri 2764	. . . . . . . . . . 11 ⊢ (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100)) = (4._2_2_48)
353	311, 313, 352	3eqtr3i 2768	. . . . . . . . . 10 ⊢ ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100) = (4._2_2_48)
354	301, 353	breqtrri 5113	. . . . . . . . 9 ⊢ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)
355	72, 18, 305	redivcli 11917	. . . . . . . . . . 11 ⊢ ((0._0_0_0_4_2_2_48) / ;10) ∈ ℝ
356	355, 198	remulcli 11156	. . . . . . . . . 10 ⊢ (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ∈ ℝ
357	286	nngt0i 12211	. . . . . . . . . . 11 ⊢ 0 < ;;100
358	287, 357	pm3.2i 470	. . . . . . . . . 10 ⊢ (;;100 ∈ ℝ ∧ 0 < ;;100)
359		ltmuldiv2 12025	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ∈ ℝ ∧ (;;100 ∈ ℝ ∧ 0 < ;;100)) → ((;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ↔ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)))
360	3, 356, 358, 359	mp3an 1464	. . . . . . . . 9 ⊢ ((;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ↔ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100))
361	354, 360	mpbir 231	. . . . . . . 8 ⊢ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7))
362		ltdivmul2 12028	. . . . . . . . 9 ⊢ (((;;100 · 4) ∈ ℝ ∧ ((0._0_0_0_4_2_2_48) / ;10) ∈ ℝ ∧ ((;10↑7) ∈ ℝ ∧ 0 < (;10↑7))) → (((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10) ↔ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7))))
363	291, 355, 226, 362	mp3an 1464	. . . . . . . 8 ⊢ (((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10) ↔ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)))
364	361, 363	mpbir 231	. . . . . . 7 ⊢ ((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
365	291, 198, 277	redivcli 11917	. . . . . . . 8 ⊢ ((;;100 · 4) / (;10↑7)) ∈ ℝ
366	279, 365, 355	lttri 11267	. . . . . . 7 ⊢ ((((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7)) ∧ ((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)) → ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10))
367	294, 364, 366	mp2an 693	. . . . . 6 ⊢ ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
368	226	simpli 483	. . . . . . . 8 ⊢ (;10↑7) ∈ ℝ
369	273, 368, 277	redivcli 11917	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
370	55, 369, 355	lttri 11267	. . . . . 6 ⊢ ((((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7)) ∧ ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10))
371	281, 367, 370	mp2an 693	. . . . 5 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10)
372	125, 124	mpbi 230	. . . . . 6 ⊢ (;10 ∈ ℝ ∧ 0 < ;10)
373		ltmuldiv2 12025	. . . . . 6 ⊢ ((((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ ∧ (0._0_0_0_4_2_2_48) ∈ ℝ ∧ (;10 ∈ ℝ ∧ 0 < ;10)) → ((;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10)))
374	55, 72, 372, 373	mp3an 1464	. . . . 5 ⊢ ((;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10))
375	371, 374	mpbir 231	. . . 4 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48)
376	12, 55	remulcli 11156	. . . . 5 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
377	18, 55	remulcli 11156	. . . . 5 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
378	376, 377, 72	lttri 11267	. . . 4 ⊢ ((((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∧ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48)) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48))
379	189, 375, 378	mp2an 693	. . 3 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48)
380	379	a1i 11	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48))
381	47, 57, 73, 162, 380	lelttrd 11299	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5086 ‘cfv 6494 (class class class)co 7362 ℂcc 11031 ℝcr 11032 0cc0 11033 1c1 11034 + caddc 11036 · cmul 11038 < clt 11174 ≤ cle 11175 − cmin 11372 / cdiv 11802 ℕcn 12169 2c2 12231 3c3 12232 4c4 12233 6c6 12235 7c7 12236 8c8 12237 9c9 12238 ℕ₀cn0 12432 ℤcz 12519 cdc 12639 ℚcq 12893 ℝ⁺crp 12937 ↑cexp 14018 √csqrt 15190 expce 16021 eceu 16022 logclog 26535 cdp2 32949 .cdp 32966

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-inf2 9557 ax-cc 10352 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111 ax-addf 11112

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-symdif 4194 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-se 5580 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-isom 6503 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-of 7626 df-ofr 7627 df-om 7813 df-1st 7937 df-2nd 7938 df-supp 8106 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-oadd 8404 df-omul 8405 df-er 8638 df-map 8770 df-pm 8771 df-ixp 8841 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-fsupp 9270 df-fi 9319 df-sup 9350 df-inf 9351 df-oi 9420 df-dju 9820 df-card 9858 df-acn 9861 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-z 12520 df-dec 12640 df-uz 12784 df-q 12894 df-rp 12938 df-xneg 13058 df-xadd 13059 df-xmul 13060 df-ioo 13297 df-ioc 13298 df-ico 13299 df-icc 13300 df-fz 13457 df-fzo 13604 df-fl 13746 df-mod 13824 df-seq 13959 df-exp 14019 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15024 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-limsup 15428 df-clim 15445 df-rlim 15446 df-sum 15644 df-ef 16027 df-e 16028 df-sin 16029 df-cos 16030 df-tan 16031 df-pi 16032 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-starv 17230 df-sca 17231 df-vsca 17232 df-ip 17233 df-tset 17234 df-ple 17235 df-ds 17237 df-unif 17238 df-hom 17239 df-cco 17240 df-rest 17380 df-topn 17381 df-0g 17399 df-gsum 17400 df-topgen 17401 df-pt 17402 df-prds 17405 df-xrs 17461 df-qtop 17466 df-imas 17467 df-xps 17469 df-mre 17543 df-mrc 17544 df-acs 17546 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-mulg 19039 df-cntz 19287 df-cmn 19752 df-psmet 21340 df-xmet 21341 df-met 21342 df-bl 21343 df-mopn 21344 df-fbas 21345 df-fg 21346 df-cnfld 21349 df-top 22873 df-topon 22890 df-topsp 22912 df-bases 22925 df-cld 22998 df-ntr 22999 df-cls 23000 df-nei 23077 df-lp 23115 df-perf 23116 df-cn 23206 df-cnp 23207 df-haus 23294 df-cmp 23366 df-tx 23541 df-hmeo 23734 df-fil 23825 df-fm 23917 df-flim 23918 df-flf 23919 df-xms 24299 df-ms 24300 df-tms 24301 df-cncf 24859 df-ovol 25445 df-vol 25446 df-mbf 25600 df-itg1 25601 df-itg2 25602 df-ibl 25603 df-itg 25604 df-0p 25651 df-limc 25847 df-dv 25848 df-log 26537 df-cxp 26538 df-dp2 32950 df-dp 32967

This theorem is referenced by: tgoldbachgtde 34824

W3C validator