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 33651

Description: Lemma for tgoldbachgtd 33662. (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 12490	. . . . 5 ⊢ 7 ∈ ℕ₀
2		3re 12288	. . . . . . 7 ⊢ 3 ∈ ℝ
3		4re 12292	. . . . . . . . 9 ⊢ 4 ∈ ℝ
4		8re 12304	. . . . . . . . 9 ⊢ 8 ∈ ℝ
5	3, 4	pm3.2i 471	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
6		dp2cl 32033	. . . . . . . 8 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
7	5, 6	ax-mp 5	. . . . . . 7 ⊢ _48 ∈ ℝ
8	2, 7	pm3.2i 471	. . . . . 6 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
9		dp2cl 32033	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
10	8, 9	ax-mp 5	. . . . 5 ⊢ _3_48 ∈ ℝ
11		dpcl 32044	. . . . 5 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
12	1, 10, 11	mp2an 690	. . . 4 ⊢ (7._3_48) ∈ ℝ
13	12	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (7._3_48) ∈ ℝ)
14		nn0re 12477	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	14	adantr 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ)
16		0re 11212	. . . . . . . 8 ⊢ 0 ∈ ℝ
17	16	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ∈ ℝ)
18		10re 12692	. . . . . . . . 9 ⊢ ;10 ∈ ℝ
19		2nn0 12485	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
20	19, 1	deccl 12688	. . . . . . . . 9 ⊢ ;27 ∈ ℕ₀
21		reexpcl 14040	. . . . . . . . 9 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀) → (;10↑;27) ∈ ℝ)
22	18, 20, 21	mp2an 690	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
23	22	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ∈ ℝ)
24		0lt1 11732	. . . . . . . . 9 ⊢ 0 < 1
25		1nn 12219	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
26		0nn0 12483	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
27		1nn0 12484	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
28		1re 11210	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
29		9re 12307	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
30		1lt9 12414	. . . . . . . . . . . 12 ⊢ 1 < 9
31	28, 29, 30	ltleii 11333	. . . . . . . . . . 11 ⊢ 1 ≤ 9
32	25, 26, 27, 31	declei 12709	. . . . . . . . . 10 ⊢ 1 ≤ ;10
33		expge1 14061	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀ ∧ 1 ≤ ;10) → 1 ≤ (;10↑;27))
34	18, 20, 32, 33	mp3an 1461	. . . . . . . . 9 ⊢ 1 ≤ (;10↑;27)
35	16, 28, 22	ltletri 11338	. . . . . . . . 9 ⊢ ((0 < 1 ∧ 1 ≤ (;10↑;27)) → 0 < (;10↑;27))
36	24, 34, 35	mp2an 690	. . . . . . . 8 ⊢ 0 < (;10↑;27)
37	36	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (;10↑;27))
38		simpr 485	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ≤ 𝑁)
39	17, 23, 15, 37, 38	ltletrd 11370	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < 𝑁)
40	15, 39	elrpd 13009	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ⁺)
41	40	relogcld 26122	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (log‘𝑁) ∈ ℝ)
42	40	rpge0d 13016	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ≤ 𝑁)
43	15, 42	resqrtcld 15360	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ∈ ℝ)
44	40	sqrtgt0d 15355	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (√‘𝑁))
45	17, 44	gtned 11345	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ≠ 0)
46	41, 43, 45	redivcld 12038	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
47	13, 46	remulcld 11240	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
48		elrp 12972	. . . . . . 7 ⊢ ((;10↑;27) ∈ ℝ⁺ ↔ ((;10↑;27) ∈ ℝ ∧ 0 < (;10↑;27)))
49	22, 36, 48	mpbir2an 709	. . . . . 6 ⊢ (;10↑;27) ∈ ℝ⁺
50		relogcl 26075	. . . . . 6 ⊢ ((;10↑;27) ∈ ℝ⁺ → (log‘(;10↑;27)) ∈ ℝ)
51	49, 50	ax-mp 5	. . . . 5 ⊢ (log‘(;10↑;27)) ∈ ℝ
52	22, 36	sqrtpclii 15325	. . . . 5 ⊢ (√‘(;10↑;27)) ∈ ℝ
53	22, 36	sqrtgt0ii 15326	. . . . . 6 ⊢ 0 < (√‘(;10↑;27))
54	16, 53	gtneii 11322	. . . . 5 ⊢ (√‘(;10↑;27)) ≠ 0
55	51, 52, 54	redivcli 11977	. . . 4 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ
56	55	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ)
57	13, 56	remulcld 11240	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ)
58		qssre 12939	. . . . 5 ⊢ ℚ ⊆ ℝ
59		4nn0 12487	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
60		nn0ssq 12937	. . . . . . . . . . . . 13 ⊢ ℕ₀ ⊆ ℚ
61		8nn0 12491	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ₀
62	60, 61	sselii 3978	. . . . . . . . . . . 12 ⊢ 8 ∈ ℚ
63	59, 62	dp2clq 32034	. . . . . . . . . . 11 ⊢ _48 ∈ ℚ
64	19, 63	dp2clq 32034	. . . . . . . . . 10 ⊢ _2_48 ∈ ℚ
65	19, 64	dp2clq 32034	. . . . . . . . 9 ⊢ _2_2_48 ∈ ℚ
66	59, 65	dp2clq 32034	. . . . . . . 8 ⊢ _4_2_2_48 ∈ ℚ
67	26, 66	dp2clq 32034	. . . . . . 7 ⊢ _0_4_2_2_48 ∈ ℚ
68	26, 67	dp2clq 32034	. . . . . 6 ⊢ _0_0_4_2_2_48 ∈ ℚ
69	26, 68	dp2clq 32034	. . . . 5 ⊢ _0_0_0_4_2_2_48 ∈ ℚ
70	58, 69	sselii 3978	. . . 4 ⊢ _0_0_0_4_2_2_48 ∈ ℝ
71		dpcl 32044	. . . 4 ⊢ ((0 ∈ ℕ₀ ∧ _0_0_0_4_2_2_48 ∈ ℝ) → (0._0_0_0_4_2_2_48) ∈ ℝ)
72	26, 70, 71	mp2an 690	. . 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 12486	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
75		8pos 12320	. . . . . . . . . . 11 ⊢ 0 < 8
76		elrp 12972	. . . . . . . . . . 11 ⊢ (8 ∈ ℝ⁺ ↔ (8 ∈ ℝ ∧ 0 < 8))
77	4, 75, 76	mpbir2an 709	. . . . . . . . . 10 ⊢ 8 ∈ ℝ⁺
78	59, 77	rpdp2cl 32035	. . . . . . . . 9 ⊢ _48 ∈ ℝ⁺
79	74, 78	rpdp2cl 32035	. . . . . . . 8 ⊢ _3_48 ∈ ℝ⁺
80	1, 79	rpdpcl 32056	. . . . . . 7 ⊢ (7._3_48) ∈ ℝ⁺
81		elrp 12972	. . . . . . 7 ⊢ ((7._3_48) ∈ ℝ⁺ ↔ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48)))
82	80, 81	mpbi 229	. . . . . 6 ⊢ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48))
83	82	simpri 486	. . . . 5 ⊢ 0 < (7._3_48)
84	16, 12, 83	ltleii 11333	. . . 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 12283	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
88	87	mullidi 11215	. . . . . . . . 9 ⊢ (1 · 2) = 2
89		2nn 12281	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
90	89, 1, 27, 31	declei 12709	. . . . . . . . . 10 ⊢ 1 ≤ ;27
91		2pos 12311	. . . . . . . . . . 11 ⊢ 0 < 2
92	20	nn0rei 12479	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℝ
93		2re 12282	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
94	28, 92, 93	lemul1i 12132	. . . . . . . . . . 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 229	. . . . . . . . 9 ⊢ (1 · 2) ≤ (;27 · 2)
97	88, 96	eqbrtrri 5170	. . . . . . . 8 ⊢ 2 ≤ (;27 · 2)
98		1p1e2 12333	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
99		loge 26086	. . . . . . . . . . . . . 14 ⊢ (log‘e) = 1
100		egt2lt3 16145	. . . . . . . . . . . . . . . 16 ⊢ (2 < e ∧ e < 3)
101	100	simpri 486	. . . . . . . . . . . . . . 15 ⊢ e < 3
102		epr 16147	. . . . . . . . . . . . . . . 16 ⊢ e ∈ ℝ⁺
103		3rp 12976	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ⁺
104		logltb 26099	. . . . . . . . . . . . . . . 16 ⊢ ((e ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → (e < 3 ↔ (log‘e) < (log‘3)))
105	102, 103, 104	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (e < 3 ↔ (log‘e) < (log‘3))
106	101, 105	mpbi 229	. . . . . . . . . . . . . 14 ⊢ (log‘e) < (log‘3)
107	99, 106	eqbrtrri 5170	. . . . . . . . . . . . 13 ⊢ 1 < (log‘3)
108		relogcl 26075	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
109	103, 108	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (log‘3) ∈ ℝ
110	28, 28, 109, 109	lt2addi 11772	. . . . . . . . . . . . 13 ⊢ ((1 < (log‘3) ∧ 1 < (log‘3)) → (1 + 1) < ((log‘3) + (log‘3)))
111	107, 107, 110	mp2an 690	. . . . . . . . . . . 12 ⊢ (1 + 1) < ((log‘3) + (log‘3))
112		3cn 12289	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
113		3ne0 12314	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 0
114		logmul2 26115	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ⁺) → (log‘(3 · 3)) = ((log‘3) + (log‘3)))
115	112, 113, 103, 114	mp3an 1461	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) = ((log‘3) + (log‘3))
116		3t3e9 12375	. . . . . . . . . . . . . . 15 ⊢ (3 · 3) = 9
117	116	fveq2i 6891	. . . . . . . . . . . . . 14 ⊢ (log‘(3 · 3)) = (log‘9)
118		9lt10 12804	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
119	29, 18, 118	ltleii 11333	. . . . . . . . . . . . . . 15 ⊢ 9 ≤ ;10
120		9pos 12321	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 9
121		elrp 12972	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ⁺ ↔ (9 ∈ ℝ ∧ 0 < 9))
122	29, 120, 121	mpbir2an 709	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ⁺
123		10pos 12690	. . . . . . . . . . . . . . . . 17 ⊢ 0 < ;10
124		elrp 12972	. . . . . . . . . . . . . . . . 17 ⊢ (;10 ∈ ℝ⁺ ↔ (;10 ∈ ℝ ∧ 0 < ;10))
125	18, 123, 124	mpbir2an 709	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℝ⁺
126		logleb 26102	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ⁺ ∧ ;10 ∈ ℝ⁺) → (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10)))
127	122, 125, 126	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10))
128	119, 127	mpbi 229	. . . . . . . . . . . . . 14 ⊢ (log‘9) ≤ (log‘;10)
129	117, 128	eqbrtri 5168	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) ≤ (log‘;10)
130	115, 129	eqbrtrri 5170	. . . . . . . . . . . 12 ⊢ ((log‘3) + (log‘3)) ≤ (log‘;10)
131	28, 28	readdcli 11225	. . . . . . . . . . . . 13 ⊢ (1 + 1) ∈ ℝ
132	109, 109	readdcli 11225	. . . . . . . . . . . . 13 ⊢ ((log‘3) + (log‘3)) ∈ ℝ
133		relogcl 26075	. . . . . . . . . . . . . 14 ⊢ (;10 ∈ ℝ⁺ → (log‘;10) ∈ ℝ)
134	125, 133	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (log‘;10) ∈ ℝ
135	131, 132, 134	ltletri 11338	. . . . . . . . . . . 12 ⊢ (((1 + 1) < ((log‘3) + (log‘3)) ∧ ((log‘3) + (log‘3)) ≤ (log‘;10)) → (1 + 1) < (log‘;10))
136	111, 130, 135	mp2an 690	. . . . . . . . . . 11 ⊢ (1 + 1) < (log‘;10)
137	98, 136	eqbrtrri 5170	. . . . . . . . . 10 ⊢ 2 < (log‘;10)
138	93, 134	ltlei 11332	. . . . . . . . . 10 ⊢ (2 < (log‘;10) → 2 ≤ (log‘;10))
139	137, 138	ax-mp 5	. . . . . . . . 9 ⊢ 2 ≤ (log‘;10)
140	16, 29, 120	ltleii 11333	. . . . . . . . . . 11 ⊢ 0 ≤ 9
141	89, 1, 26, 140	decltdi 12712	. . . . . . . . . 10 ⊢ 0 < ;27
142	93, 134, 92	lemul2i 12133	. . . . . . . . . 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 229	. . . . . . . 8 ⊢ (;27 · 2) ≤ (;27 · (log‘;10))
145	92, 93	remulcli 11226	. . . . . . . . 9 ⊢ (;27 · 2) ∈ ℝ
146	20	nn0zi 12583	. . . . . . . . . . 11 ⊢ ;27 ∈ ℤ
147		relogexp 26095	. . . . . . . . . . 11 ⊢ ((;10 ∈ ℝ⁺ ∧ ;27 ∈ ℤ) → (log‘(;10↑;27)) = (;27 · (log‘;10)))
148	125, 146, 147	mp2an 690	. . . . . . . . . 10 ⊢ (log‘(;10↑;27)) = (;27 · (log‘;10))
149	148, 51	eqeltrri 2830	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) ∈ ℝ
150	93, 145, 149	letri 11339	. . . . . . . 8 ⊢ ((2 ≤ (;27 · 2) ∧ (;27 · 2) ≤ (;27 · (log‘;10))) → 2 ≤ (;27 · (log‘;10)))
151	97, 144, 150	mp2an 690	. . . . . . 7 ⊢ 2 ≤ (;27 · (log‘;10))
152		relogef 26082	. . . . . . . 8 ⊢ (2 ∈ ℝ → (log‘(exp‘2)) = 2)
153	93, 152	ax-mp 5	. . . . . . 7 ⊢ (log‘(exp‘2)) = 2
154	151, 153, 148	3brtr4i 5177	. . . . . 6 ⊢ (log‘(exp‘2)) ≤ (log‘(;10↑;27))
155		rpefcl 16043	. . . . . . . 8 ⊢ (2 ∈ ℝ → (exp‘2) ∈ ℝ⁺)
156	93, 155	ax-mp 5	. . . . . . 7 ⊢ (exp‘2) ∈ ℝ⁺
157		logleb 26102	. . . . . . 7 ⊢ (((exp‘2) ∈ ℝ⁺ ∧ (;10↑;27) ∈ ℝ⁺) → ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27))))
158	156, 49, 157	mp2an 690	. . . . . 6 ⊢ ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27)))
159	154, 158	mpbir 230	. . . . 5 ⊢ (exp‘2) ≤ (;10↑;27)
160	159	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (exp‘2) ≤ (;10↑;27))
161	86, 40, 160, 38	logdivsqrle 33650	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ≤ ((log‘(;10↑;27)) / (√‘(;10↑;27))))
162	46, 56, 13, 85, 161	lemul2ad 12150	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ≤ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
163		3lt10 12810	. . . . . . . 8 ⊢ 3 < ;10
164		4lt10 12809	. . . . . . . . 9 ⊢ 4 < ;10
165		8lt10 12805	. . . . . . . . 9 ⊢ 8 < ;10
166	59, 77, 164, 165	dp2lt10 32037	. . . . . . . 8 ⊢ _48 < ;10
167	74, 78, 163, 166	dp2lt10 32037	. . . . . . 7 ⊢ _3_48 < ;10
168		7p1e8 12357	. . . . . . 7 ⊢ (7 + 1) = 8
169	1, 79, 61, 167, 168	dplti 32058	. . . . . 6 ⊢ (7._3_48) < 8
170	58, 62	sselii 3978	. . . . . . 7 ⊢ 8 ∈ ℝ
171	12, 170, 18	lttri 11336	. . . . . 6 ⊢ (((7._3_48) < 8 ∧ 8 < ;10) → (7._3_48) < ;10)
172	169, 165, 171	mp2an 690	. . . . 5 ⊢ (7._3_48) < ;10
173	27, 26	deccl 12688	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
174	173	numexp0 17005	. . . . . . . . 9 ⊢ (;10↑0) = 1
175		0z 12565	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
176	18, 175, 146	3pm3.2i 1339	. . . . . . . . . 10 ⊢ (;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ)
177		1lt10 12812	. . . . . . . . . . 11 ⊢ 1 < ;10
178	177, 141	pm3.2i 471	. . . . . . . . . 10 ⊢ (1 < ;10 ∧ 0 < ;27)
179		ltexp2a 14127	. . . . . . . . . 10 ⊢ (((;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < ;27)) → (;10↑0) < (;10↑;27))
180	176, 178, 179	mp2an 690	. . . . . . . . 9 ⊢ (;10↑0) < (;10↑;27)
181	174, 180	eqbrtrri 5170	. . . . . . . 8 ⊢ 1 < (;10↑;27)
182		loggt0b 26131	. . . . . . . . 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 230	. . . . . . 7 ⊢ 0 < (log‘(;10↑;27))
185	51, 52	divgt0i 12118	. . . . . . 7 ⊢ ((0 < (log‘(;10↑;27)) ∧ 0 < (√‘(;10↑;27))) → 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))))
186	184, 53, 185	mp2an 690	. . . . . 6 ⊢ 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27)))
187	12, 18, 55	ltmul1i 12128	. . . . . 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 229	. . . 4 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27))))
190	18	recni 11224	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℂ
191		expmul 14069	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℂ ∧ 7 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (;10↑(7 · 2)) = ((;10↑7)↑2))
192	190, 1, 19, 191	mp3an 1461	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = ((;10↑7)↑2)
193		7t2e14 12782	. . . . . . . . . . . . 13 ⊢ (7 · 2) = ;14
194	193	oveq2i 7416	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = (;10↑;14)
195	192, 194	eqtr3i 2762	. . . . . . . . . . 11 ⊢ ((;10↑7)↑2) = (;10↑;14)
196	195	fveq2i 6891	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (√‘(;10↑;14))
197		reexpcl 14040	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℕ₀) → (;10↑7) ∈ ℝ)
198	18, 1, 197	mp2an 690	. . . . . . . . . . 11 ⊢ (;10↑7) ∈ ℝ
199	1	nn0zi 12583	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℤ
200		expgt0 14057	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑7))
201	18, 199, 123, 200	mp3an 1461	. . . . . . . . . . . 12 ⊢ 0 < (;10↑7)
202	16, 198, 201	ltleii 11333	. . . . . . . . . . 11 ⊢ 0 ≤ (;10↑7)
203		sqrtsq 15212	. . . . . . . . . . 11 ⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤ (;10↑7)) → (√‘((;10↑7)↑2)) = (;10↑7))
204	198, 202, 203	mp2an 690	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (;10↑7)
205	196, 204	eqtr3i 2762	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) = (;10↑7)
206	27, 59	deccl 12688	. . . . . . . . . . . . 13 ⊢ ;14 ∈ ℕ₀
207	206	nn0zi 12583	. . . . . . . . . . . 12 ⊢ ;14 ∈ ℤ
208	18, 207, 146	3pm3.2i 1339	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ)
209		1lt2 12379	. . . . . . . . . . . . 13 ⊢ 1 < 2
210	27, 19, 59, 1, 164, 209	decltc 12702	. . . . . . . . . . . 12 ⊢ ;14 < ;27
211	177, 210	pm3.2i 471	. . . . . . . . . . 11 ⊢ (1 < ;10 ∧ ;14 < ;27)
212		ltexp2a 14127	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27))
213	208, 211, 212	mp2an 690	. . . . . . . . . 10 ⊢ (;10↑;14) < (;10↑;27)
214		reexpcl 14040	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℕ₀) → (;10↑;14) ∈ ℝ)
215	18, 206, 214	mp2an 690	. . . . . . . . . . . 12 ⊢ (;10↑;14) ∈ ℝ
216		expgt0 14057	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14))
217	18, 207, 123, 216	mp3an 1461	. . . . . . . . . . . . 13 ⊢ 0 < (;10↑;14)
218	16, 215, 217	ltleii 11333	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;14)
219	215, 218	pm3.2i 471	. . . . . . . . . . 11 ⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14))
220	16, 22, 36	ltleii 11333	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;27)
221	22, 220	pm3.2i 471	. . . . . . . . . . 11 ⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))
222		sqrtlt 15204	. . . . . . . . . . 11 ⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))))
223	219, 221, 222	mp2an 690	. . . . . . . . . 10 ⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))
224	213, 223	mpbi 229	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) < (√‘(;10↑;27))
225	205, 224	eqbrtrri 5170	. . . . . . . 8 ⊢ (;10↑7) < (√‘(;10↑;27))
226	198, 201	pm3.2i 471	. . . . . . . . 9 ⊢ ((;10↑7) ∈ ℝ ∧ 0 < (;10↑7))
227	52, 53	pm3.2i 471	. . . . . . . . 9 ⊢ ((√‘(;10↑;27)) ∈ ℝ ∧ 0 < (√‘(;10↑;27)))
228	51, 184	pm3.2i 471	. . . . . . . . 9 ⊢ ((log‘(;10↑;27)) ∈ ℝ ∧ 0 < (log‘(;10↑;27)))
229		ltdiv2 12096	. . . . . . . . 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 1461	. . . . . . . 8 ⊢ ((;10↑7) < (√‘(;10↑;27)) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7)))
231	225, 230	mpbi 229	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7))
232		6nn 12297	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
233	232	nngt0i 12247	. . . . . . . . . . . . . 14 ⊢ 0 < 6
234	27, 26, 232, 233	declt 12701	. . . . . . . . . . . . 13 ⊢ ;10 < ;16
235		6nn0 12489	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ₀
236	27, 235	deccl 12688	. . . . . . . . . . . . . . . 16 ⊢ ;16 ∈ ℕ₀
237	236	nn0rei 12479	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℝ
238	25, 235, 26, 123	declti 12711	. . . . . . . . . . . . . . 15 ⊢ 0 < ;16
239		elrp 12972	. . . . . . . . . . . . . . 15 ⊢ (;16 ∈ ℝ⁺ ↔ (;16 ∈ ℝ ∧ 0 < ;16))
240	237, 238, 239	mpbir2an 709	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℝ⁺
241		logltb 26099	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ⁺ ∧ ;16 ∈ ℝ⁺) → (;10 < ;16 ↔ (log‘;10) < (log‘;16)))
242	125, 240, 241	mp2an 690	. . . . . . . . . . . . 13 ⊢ (;10 < ;16 ↔ (log‘;10) < (log‘;16))
243	234, 242	mpbi 229	. . . . . . . . . . . 12 ⊢ (log‘;10) < (log‘;16)
244		2exp4 17014	. . . . . . . . . . . . . 14 ⊢ (2↑4) = ;16
245	244	fveq2i 6891	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (log‘;16)
246		2rp 12975	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
247	59	nn0zi 12583	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
248		relogexp 26095	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ 4 ∈ ℤ) → (log‘(2↑4)) = (4 · (log‘2)))
249	246, 247, 248	mp2an 690	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (4 · (log‘2))
250	245, 249	eqtr3i 2762	. . . . . . . . . . . 12 ⊢ (log‘;16) = (4 · (log‘2))
251	243, 250	breqtri 5172	. . . . . . . . . . 11 ⊢ (log‘;10) < (4 · (log‘2))
252	100	simpli 484	. . . . . . . . . . . . . . 15 ⊢ 2 < e
253		logltb 26099	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ⁺ ∧ e ∈ ℝ⁺) → (2 < e ↔ (log‘2) < (log‘e)))
254	246, 102, 253	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (2 < e ↔ (log‘2) < (log‘e))
255	252, 254	mpbi 229	. . . . . . . . . . . . . 14 ⊢ (log‘2) < (log‘e)
256	255, 99	breqtri 5172	. . . . . . . . . . . . 13 ⊢ (log‘2) < 1
257		4pos 12315	. . . . . . . . . . . . . 14 ⊢ 0 < 4
258		relogcl 26075	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
259	246, 258	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (log‘2) ∈ ℝ
260	259, 28, 3	ltmul2i 12131	. . . . . . . . . . . . . 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 229	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) < (4 · 1)
263		4cn 12293	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℂ
264	263	mulridi 11214	. . . . . . . . . . . 12 ⊢ (4 · 1) = 4
265	262, 264	breqtri 5172	. . . . . . . . . . 11 ⊢ (4 · (log‘2)) < 4
266	3, 259	remulcli 11226	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) ∈ ℝ
267	134, 266, 3	lttri 11336	. . . . . . . . . . 11 ⊢ (((log‘;10) < (4 · (log‘2)) ∧ (4 · (log‘2)) < 4) → (log‘;10) < 4)
268	251, 265, 267	mp2an 690	. . . . . . . . . 10 ⊢ (log‘;10) < 4
269	134, 3, 92	ltmul2i 12131	. . . . . . . . . . 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 229	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) < (;27 · 4)
272	148, 271	eqbrtri 5168	. . . . . . . 8 ⊢ (log‘(;10↑;27)) < (;27 · 4)
273	92, 3	remulcli 11226	. . . . . . . . . 10 ⊢ (;27 · 4) ∈ ℝ
274	51, 273, 198	ltdiv1i 12129	. . . . . . . . 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 229	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))
277	16, 201	gtneii 11322	. . . . . . . . 9 ⊢ (;10↑7) ≠ 0
278	51, 198, 277	redivcli 11977	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) / (;10↑7)) ∈ ℝ
279	273, 198, 277	redivcli 11977	. . . . . . . 8 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
280	55, 278, 279	lttri 11336	. . . . . . 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 690	. . . . . 6 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7))
282		7lt10 12806	. . . . . . . . . 10 ⊢ 7 < ;10
283		2lt10 12811	. . . . . . . . . 10 ⊢ 2 < ;10
284	19, 173, 1, 26, 282, 283	decltc 12702	. . . . . . . . 9 ⊢ ;27 < ;;100
285		10nn 12689	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℕ
286	285	decnncl2 12697	. . . . . . . . . . . 12 ⊢ ;;100 ∈ ℕ
287	286	nnrei 12217	. . . . . . . . . . 11 ⊢ ;;100 ∈ ℝ
288	92, 287, 3	ltmul1i 12128	. . . . . . . . . 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 229	. . . . . . . 8 ⊢ (;27 · 4) < (;;100 · 4)
291	287, 3	remulcli 11226	. . . . . . . . . 10 ⊢ (;;100 · 4) ∈ ℝ
292	273, 291, 198	ltdiv1i 12129	. . . . . . . . 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 229	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7))
295		8nn 12303	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ
296		nnrp 12981	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
297	295, 296	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℝ⁺
298	59, 297	rpdp2cl 32035	. . . . . . . . . . . . 13 ⊢ _48 ∈ ℝ⁺
299	19, 298	rpdp2cl 32035	. . . . . . . . . . . 12 ⊢ _2_48 ∈ ℝ⁺
300	19, 299	rpdp2cl 32035	. . . . . . . . . . 11 ⊢ _2_2_48 ∈ ℝ⁺
301	59, 300	dpgti 32059	. . . . . . . . . 10 ⊢ 4 < (4._2_2_48)
302	72	recni 11224	. . . . . . . . . . . . 13 ⊢ (0._0_0_0_4_2_2_48) ∈ ℂ
303	198	recni 11224	. . . . . . . . . . . . 13 ⊢ (;10↑7) ∈ ℂ
304	302, 303	mulcli 11217	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑7)) ∈ ℂ
305	16, 123	gtneii 11322	. . . . . . . . . . . . 13 ⊢ ;10 ≠ 0
306	190, 305	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (;10 ∈ ℂ ∧ ;10 ≠ 0)
307	287	recni 11224	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℂ
308	286	nnne0i 12248	. . . . . . . . . . . . 13 ⊢ ;;100 ≠ 0
309	307, 308	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (;;100 ∈ ℂ ∧ ;;100 ≠ 0)
310		divdiv1 11921	. . . . . . . . . . . 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 1461	. . . . . . . . . . 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 11968	. . . . . . . . . . . 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 7415	. . . . . . . . . . 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 11217	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ∈ ℂ
315	190, 307, 305, 308	mulne0i 11853	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ≠ 0
316	302, 303, 314, 315	divassi 11966	. . . . . . . . . . . 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 14030	. . . . . . . . . . . . . . . . . 18 ⊢ ((;10 ∈ ℂ ∧ 2 ∈ ℕ₀) → (;10↑(2 + 1)) = ((;10↑2) · ;10))
318	190, 19, 317	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (;10↑(2 + 1)) = ((;10↑2) · ;10)
319		sq10 14220	. . . . . . . . . . . . . . . . . 18 ⊢ (;10↑2) = ;;100
320	319	oveq1i 7415	. . . . . . . . . . . . . . . . 17 ⊢ ((;10↑2) · ;10) = (;;100 · ;10)
321	307, 190	mulcomi 11218	. . . . . . . . . . . . . . . . 17 ⊢ (;;100 · ;10) = (;10 · ;;100)
322	318, 320, 321	3eqtrri 2765	. . . . . . . . . . . . . . . 16 ⊢ (;10 · ;;100) = (;10↑(2 + 1))
323		2p1e3 12350	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 1) = 3
324	323	oveq2i 7416	. . . . . . . . . . . . . . . 16 ⊢ (;10↑(2 + 1)) = (;10↑3)
325	322, 324	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ (;10 · ;;100) = (;10↑3)
326	325	oveq2i 7416	. . . . . . . . . . . . . 14 ⊢ ((;10↑7) / (;10 · ;;100)) = ((;10↑7) / (;10↑3))
327	74	nn0zi 12583	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
328	199, 327	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℤ ∧ 3 ∈ ℤ)
329		expsub 14072	. . . . . . . . . . . . . . 15 ⊢ (((;10 ∈ ℂ ∧ ;10 ≠ 0) ∧ (7 ∈ ℤ ∧ 3 ∈ ℤ)) → (;10↑(7 − 3)) = ((;10↑7) / (;10↑3)))
330	306, 328, 329	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = ((;10↑7) / (;10↑3))
331		7cn 12302	. . . . . . . . . . . . . . . 16 ⊢ 7 ∈ ℂ
332		4p3e7 12362	. . . . . . . . . . . . . . . . 17 ⊢ (4 + 3) = 7
333	263, 112, 332	addcomli 11402	. . . . . . . . . . . . . . . 16 ⊢ (3 + 4) = 7
334	331, 112, 263, 333	subaddrii 11545	. . . . . . . . . . . . . . 15 ⊢ (7 − 3) = 4
335	334	oveq2i 7416	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = (;10↑4)
336	326, 330, 335	3eqtr2i 2766	. . . . . . . . . . . . 13 ⊢ ((;10↑7) / (;10 · ;;100)) = (;10↑4)
337	336	oveq2i 7416	. . . . . . . . . . . 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 17006	. . . . . . . . . . . . . 14 ⊢ (;10↑1) = ;10
339	338	oveq2i 7416	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._4_2_2_48) · ;10)
340	59, 300	rpdp2cl 32035	. . . . . . . . . . . . . . 15 ⊢ _4_2_2_48 ∈ ℝ⁺
341	25	nnzi 12582	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
342	89	nnzi 12582	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
343	26, 340, 98, 341, 342	dpexpp1 32061	. . . . . . . . . . . . . 14 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_4_2_2_48) · (;10↑2))
344	26, 340	rpdp2cl 32035	. . . . . . . . . . . . . . 15 ⊢ _0_4_2_2_48 ∈ ℝ⁺
345	26, 344, 323, 342, 327	dpexpp1 32061	. . . . . . . . . . . . . 14 ⊢ ((0._0_4_2_2_48) · (;10↑2)) = ((0._0_0_4_2_2_48) · (;10↑3))
346	26, 344	rpdp2cl 32035	. . . . . . . . . . . . . . 15 ⊢ _0_0_4_2_2_48 ∈ ℝ⁺
347		3p1e4 12353	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
348	26, 346, 347, 327, 247	dpexpp1 32061	. . . . . . . . . . . . . 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 32062	. . . . . . . . . . . . 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 5174	. . . . . . . . 9 ⊢ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)
355	72, 18, 305	redivcli 11977	. . . . . . . . . . 11 ⊢ ((0._0_0_0_4_2_2_48) / ;10) ∈ ℝ
356	355, 198	remulcli 11226	. . . . . . . . . 10 ⊢ (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ∈ ℝ
357	286	nngt0i 12247	. . . . . . . . . . 11 ⊢ 0 < ;;100
358	287, 357	pm3.2i 471	. . . . . . . . . 10 ⊢ (;;100 ∈ ℝ ∧ 0 < ;;100)
359		ltmuldiv2 12084	. . . . . . . . . 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 1461	. . . . . . . . 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 230	. . . . . . . 8 ⊢ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7))
362		ltdivmul2 12087	. . . . . . . . 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 1461	. . . . . . . 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 230	. . . . . . 7 ⊢ ((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
365	291, 198, 277	redivcli 11977	. . . . . . . 8 ⊢ ((;;100 · 4) / (;10↑7)) ∈ ℝ
366	279, 365, 355	lttri 11336	. . . . . . 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 690	. . . . . 6 ⊢ ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
368	226	simpli 484	. . . . . . . 8 ⊢ (;10↑7) ∈ ℝ
369	273, 368, 277	redivcli 11977	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
370	55, 369, 355	lttri 11336	. . . . . 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 690	. . . . 5 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10)
372	125, 124	mpbi 229	. . . . . 6 ⊢ (;10 ∈ ℝ ∧ 0 < ;10)
373		ltmuldiv2 12084	. . . . . 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 1461	. . . . 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 230	. . . 4 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48)
376	12, 55	remulcli 11226	. . . . 5 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
377	18, 55	remulcli 11226	. . . . 5 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
378	376, 377, 72	lttri 11336	. . . 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 690	. . 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 11368	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 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 class class class wbr 5147 ‘cfv 6540 (class class class)co 7405 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 < clt 11244 ≤ cle 11245 − cmin 11440 / cdiv 11867 ℕcn 12208 2c2 12263 3c3 12264 4c4 12265 6c6 12267 7c7 12268 8c8 12269 9c9 12270 ℕ₀cn0 12468 ℤcz 12554 cdc 12673 ℚcq 12928 ℝ⁺crp 12970 ↑cexp 14023 √csqrt 15176 expce 16001 eceu 16002 logclog 26054 cdp2 32024 .cdp 32041

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cc 10426 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185 ax-mulf 11186

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-symdif 4241 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7666 df-ofr 7667 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-oadd 8466 df-omul 8467 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-fi 9402 df-sup 9433 df-inf 9434 df-oi 9501 df-dju 9892 df-card 9930 df-acn 9933 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-q 12929 df-rp 12971 df-xneg 13088 df-xadd 13089 df-xmul 13090 df-ioo 13324 df-ioc 13325 df-ico 13326 df-icc 13327 df-fz 13481 df-fzo 13624 df-fl 13753 df-mod 13831 df-seq 13963 df-exp 14024 df-fac 14230 df-bc 14259 df-hash 14287 df-shft 15010 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-limsup 15411 df-clim 15428 df-rlim 15429 df-sum 15629 df-ef 16007 df-e 16008 df-sin 16009 df-cos 16010 df-tan 16011 df-pi 16012 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17141 df-ress 17170 df-plusg 17206 df-mulr 17207 df-starv 17208 df-sca 17209 df-vsca 17210 df-ip 17211 df-tset 17212 df-ple 17213 df-ds 17215 df-unif 17216 df-hom 17217 df-cco 17218 df-rest 17364 df-topn 17365 df-0g 17383 df-gsum 17384 df-topgen 17385 df-pt 17386 df-prds 17389 df-xrs 17444 df-qtop 17449 df-imas 17450 df-xps 17452 df-mre 17526 df-mrc 17527 df-acs 17529 df-mgm 18557 df-sgrp 18606 df-mnd 18622 df-submnd 18668 df-mulg 18945 df-cntz 19175 df-cmn 19644 df-psmet 20928 df-xmet 20929 df-met 20930 df-bl 20931 df-mopn 20932 df-fbas 20933 df-fg 20934 df-cnfld 20937 df-top 22387 df-topon 22404 df-topsp 22426 df-bases 22440 df-cld 22514 df-ntr 22515 df-cls 22516 df-nei 22593 df-lp 22631 df-perf 22632 df-cn 22722 df-cnp 22723 df-haus 22810 df-cmp 22882 df-tx 23057 df-hmeo 23250 df-fil 23341 df-fm 23433 df-flim 23434 df-flf 23435 df-xms 23817 df-ms 23818 df-tms 23819 df-cncf 24385 df-ovol 24972 df-vol 24973 df-mbf 25127 df-itg1 25128 df-itg2 25129 df-ibl 25130 df-itg 25131 df-0p 25178 df-limc 25374 df-dv 25375 df-log 26056 df-cxp 26057 df-dp2 32025 df-dp 32042

This theorem is referenced by: tgoldbachgtde 33660

W3C validator