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 35347

Description: Lemma for tgoldbachgtd 35358. (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 12652	. . . . 5 ⊢ 7 ∈ ℕ₀
2		3re 12447	. . . . . . 7 ⊢ 3 ∈ ℝ
3		4re 12451	. . . . . . . . 9 ⊢ 4 ∈ ℝ
4		8re 12463	. . . . . . . . 9 ⊢ 8 ∈ ℝ
5	3, 4	pm3.2i 476	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
6		dp2cl 33513	. . . . . . . 8 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
7	5, 6	ax-mp 5	. . . . . . 7 ⊢ _48 ∈ ℝ
8	2, 7	pm3.2i 476	. . . . . 6 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
9		dp2cl 33513	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
10	8, 9	ax-mp 5	. . . . 5 ⊢ _3_48 ∈ ℝ
11		dpcl 33524	. . . . 5 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
12	1, 10, 11	mp2an 705	. . . 4 ⊢ (7._3_48) ∈ ℝ
13	12	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (7._3_48) ∈ ℝ)
14		nn0re 12639	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	14	adantr 486	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ)
16		0re 11334	. . . . . . . 8 ⊢ 0 ∈ ℝ
17	16	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ∈ ℝ)
18		10re 12861	. . . . . . . . 9 ⊢ ;10 ∈ ℝ
19		2nn0 12647	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
20	19, 1	deccl 12853	. . . . . . . . 9 ⊢ ;27 ∈ ℕ₀
21		reexpcl 14245	. . . . . . . . 9 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀) → (;10↑;27) ∈ ℝ)
22	18, 20, 21	mp2an 705	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
23	22	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ∈ ℝ)
24		0lt1 11862	. . . . . . . . 9 ⊢ 0 < 1
25		1nn 12370	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
26		0nn0 12645	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
27		1nn0 12646	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
28		1re 11332	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
29		9re 12466	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
30		1lt9 12575	. . . . . . . . . . . 12 ⊢ 1 < 9
31	28, 29, 30	ltleii 11457	. . . . . . . . . . 11 ⊢ 1 ≤ 9
32	25, 26, 27, 31	declei 12879	. . . . . . . . . 10 ⊢ 1 ≤ ;10
33		expge1 14266	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀ ∧ 1 ≤ ;10) → 1 ≤ (;10↑;27))
34	18, 20, 32, 33	mp3an 1491	. . . . . . . . 9 ⊢ 1 ≤ (;10↑;27)
35	16, 28, 22	ltletri 11462	. . . . . . . . 9 ⊢ ((0 < 1 ∧ 1 ≤ (;10↑;27)) → 0 < (;10↑;27))
36	24, 34, 35	mp2an 705	. . . . . . . 8 ⊢ 0 < (;10↑;27)
37	36	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (;10↑;27))
38		simpr 490	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ≤ 𝑁)
39	17, 23, 15, 37, 38	ltletrd 11494	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < 𝑁)
40	15, 39	elrpd 13185	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ⁺)
41	40	relogcld 26978	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (log‘𝑁) ∈ ℝ)
42	40	rpge0d 13192	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ≤ 𝑁)
43	15, 42	resqrtcld 15611	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ∈ ℝ)
44	40	sqrtgt0d 15606	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (√‘𝑁))
45	17, 44	gtned 11469	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ≠ 0)
46	41, 43, 45	redivcld 12169	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
47	13, 46	remulcld 11363	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
48		elrp 13146	. . . . . . 7 ⊢ ((;10↑;27) ∈ ℝ⁺ ↔ ((;10↑;27) ∈ ℝ ∧ 0 < (;10↑;27)))
49	22, 36, 48	mpbir2an 724	. . . . . 6 ⊢ (;10↑;27) ∈ ℝ⁺
50		relogcl 26930	. . . . . 6 ⊢ ((;10↑;27) ∈ ℝ⁺ → (log‘(;10↑;27)) ∈ ℝ)
51	49, 50	ax-mp 5	. . . . 5 ⊢ (log‘(;10↑;27)) ∈ ℝ
52	22, 36	sqrtpclii 15576	. . . . 5 ⊢ (√‘(;10↑;27)) ∈ ℝ
53	22, 36	sqrtgt0ii 15577	. . . . . 6 ⊢ 0 < (√‘(;10↑;27))
54	16, 53	gtneii 11446	. . . . 5 ⊢ (√‘(;10↑;27)) ≠ 0
55	51, 52, 54	redivcli 12108	. . . 4 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ
56	55	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ)
57	13, 56	remulcld 11363	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ)
58		qssre 13110	. . . . 5 ⊢ ℚ ⊆ ℝ
59		4nn0 12649	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
60		nn0ssq 13108	. . . . . . . . . . . . 13 ⊢ ℕ₀ ⊆ ℚ
61		8nn0 12653	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ₀
62	60, 61	sselii 3910	. . . . . . . . . . . 12 ⊢ 8 ∈ ℚ
63	59, 62	dp2clq 33514	. . . . . . . . . . 11 ⊢ _48 ∈ ℚ
64	19, 63	dp2clq 33514	. . . . . . . . . 10 ⊢ _2_48 ∈ ℚ
65	19, 64	dp2clq 33514	. . . . . . . . 9 ⊢ _2_2_48 ∈ ℚ
66	59, 65	dp2clq 33514	. . . . . . . 8 ⊢ _4_2_2_48 ∈ ℚ
67	26, 66	dp2clq 33514	. . . . . . 7 ⊢ _0_4_2_2_48 ∈ ℚ
68	26, 67	dp2clq 33514	. . . . . 6 ⊢ _0_0_4_2_2_48 ∈ ℚ
69	26, 68	dp2clq 33514	. . . . 5 ⊢ _0_0_0_4_2_2_48 ∈ ℚ
70	58, 69	sselii 3910	. . . 4 ⊢ _0_0_0_4_2_2_48 ∈ ℝ
71		dpcl 33524	. . . 4 ⊢ ((0 ∈ ℕ₀ ∧ _0_0_0_4_2_2_48 ∈ ℝ) → (0._0_0_0_4_2_2_48) ∈ ℝ)
72	26, 70, 71	mp2an 705	. . 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 12648	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
75		8pos 12482	. . . . . . . . . . 11 ⊢ 0 < 8
76		elrp 13146	. . . . . . . . . . 11 ⊢ (8 ∈ ℝ⁺ ↔ (8 ∈ ℝ ∧ 0 < 8))
77	4, 75, 76	mpbir2an 724	. . . . . . . . . 10 ⊢ 8 ∈ ℝ⁺
78	59, 77	rpdp2cl 33515	. . . . . . . . 9 ⊢ _48 ∈ ℝ⁺
79	74, 78	rpdp2cl 33515	. . . . . . . 8 ⊢ _3_48 ∈ ℝ⁺
80	1, 79	rpdpcl 33536	. . . . . . 7 ⊢ (7._3_48) ∈ ℝ⁺
81		elrp 13146	. . . . . . 7 ⊢ ((7._3_48) ∈ ℝ⁺ ↔ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48)))
82	80, 81	mpbi 233	. . . . . 6 ⊢ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48))
83	82	simpri 491	. . . . 5 ⊢ 0 < (7._3_48)
84	16, 12, 83	ltleii 11457	. . . 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 12442	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
88	87	mullidi 11338	. . . . . . . . 9 ⊢ (1 · 2) = 2
89		2nn 12440	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
90	89, 1, 27, 31	declei 12879	. . . . . . . . . 10 ⊢ 1 ≤ ;27
91		2pos 12471	. . . . . . . . . . 11 ⊢ 0 < 2
92	20	nn0rei 12641	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℝ
93		2re 12441	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
94	28, 92, 93	lemul1i 12263	. . . . . . . . . . 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 233	. . . . . . . . 9 ⊢ (1 · 2) ≤ (;27 · 2)
97	88, 96	eqbrtrri 5131	. . . . . . . 8 ⊢ 2 ≤ (;27 · 2)
98		1p1e2 12490	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
99		loge 26941	. . . . . . . . . . . . . 14 ⊢ (log‘e) = 1
100		egt2lt3 16400	. . . . . . . . . . . . . . . 16 ⊢ (2 < e ∧ e < 3)
101	100	simpri 491	. . . . . . . . . . . . . . 15 ⊢ e < 3
102		epr 16402	. . . . . . . . . . . . . . . 16 ⊢ e ∈ ℝ⁺
103		3rp 13150	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ⁺
104		logltb 26955	. . . . . . . . . . . . . . . 16 ⊢ ((e ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → (e < 3 ↔ (log‘e) < (log‘3)))
105	102, 103, 104	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (e < 3 ↔ (log‘e) < (log‘3))
106	101, 105	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (log‘e) < (log‘3)
107	99, 106	eqbrtrri 5131	. . . . . . . . . . . . 13 ⊢ 1 < (log‘3)
108		relogcl 26930	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
109	103, 108	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (log‘3) ∈ ℝ
110	28, 28, 109, 109	lt2addi 11902	. . . . . . . . . . . . 13 ⊢ ((1 < (log‘3) ∧ 1 < (log‘3)) → (1 + 1) < ((log‘3) + (log‘3)))
111	107, 107, 110	mp2an 705	. . . . . . . . . . . 12 ⊢ (1 + 1) < ((log‘3) + (log‘3))
112		3cn 12448	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
113		3ne0 12476	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 0
114		logmul2 26971	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ⁺) → (log‘(3 · 3)) = ((log‘3) + (log‘3)))
115	112, 113, 103, 114	mp3an 1491	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) = ((log‘3) + (log‘3))
116		3t3e9 12534	. . . . . . . . . . . . . . 15 ⊢ (3 · 3) = 9
117	116	fveq2i 6908	. . . . . . . . . . . . . 14 ⊢ (log‘(3 · 3)) = (log‘9)
118		9lt10 12975	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
119	29, 18, 118	ltleii 11457	. . . . . . . . . . . . . . 15 ⊢ 9 ≤ ;10
120		9pos 12483	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 9
121		elrp 13146	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ⁺ ↔ (9 ∈ ℝ ∧ 0 < 9))
122	29, 120, 121	mpbir2an 724	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ⁺
123		10pos 12859	. . . . . . . . . . . . . . . . 17 ⊢ 0 < ;10
124		elrp 13146	. . . . . . . . . . . . . . . . 17 ⊢ (;10 ∈ ℝ⁺ ↔ (;10 ∈ ℝ ∧ 0 < ;10))
125	18, 123, 124	mpbir2an 724	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℝ⁺
126		logleb 26958	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ⁺ ∧ ;10 ∈ ℝ⁺) → (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10)))
127	122, 125, 126	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10))
128	119, 127	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (log‘9) ≤ (log‘;10)
129	117, 128	eqbrtri 5129	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) ≤ (log‘;10)
130	115, 129	eqbrtrri 5131	. . . . . . . . . . . 12 ⊢ ((log‘3) + (log‘3)) ≤ (log‘;10)
131	28, 28	readdcli 11348	. . . . . . . . . . . . 13 ⊢ (1 + 1) ∈ ℝ
132	109, 109	readdcli 11348	. . . . . . . . . . . . 13 ⊢ ((log‘3) + (log‘3)) ∈ ℝ
133		relogcl 26930	. . . . . . . . . . . . . 14 ⊢ (;10 ∈ ℝ⁺ → (log‘;10) ∈ ℝ)
134	125, 133	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (log‘;10) ∈ ℝ
135	131, 132, 134	ltletri 11462	. . . . . . . . . . . 12 ⊢ (((1 + 1) < ((log‘3) + (log‘3)) ∧ ((log‘3) + (log‘3)) ≤ (log‘;10)) → (1 + 1) < (log‘;10))
136	111, 130, 135	mp2an 705	. . . . . . . . . . 11 ⊢ (1 + 1) < (log‘;10)
137	98, 136	eqbrtrri 5131	. . . . . . . . . 10 ⊢ 2 < (log‘;10)
138	93, 134	ltlei 11456	. . . . . . . . . 10 ⊢ (2 < (log‘;10) → 2 ≤ (log‘;10))
139	137, 138	ax-mp 5	. . . . . . . . 9 ⊢ 2 ≤ (log‘;10)
140	16, 29, 120	ltleii 11457	. . . . . . . . . . 11 ⊢ 0 ≤ 9
141	89, 1, 26, 140	decltdi 12882	. . . . . . . . . 10 ⊢ 0 < ;27
142	93, 134, 92	lemul2i 12264	. . . . . . . . . 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 233	. . . . . . . 8 ⊢ (;27 · 2) ≤ (;27 · (log‘;10))
145	92, 93	remulcli 11349	. . . . . . . . 9 ⊢ (;27 · 2) ∈ ℝ
146	20	nn0zi 12745	. . . . . . . . . . 11 ⊢ ;27 ∈ ℤ
147		relogexp 26951	. . . . . . . . . . 11 ⊢ ((;10 ∈ ℝ⁺ ∧ ;27 ∈ ℤ) → (log‘(;10↑;27)) = (;27 · (log‘;10)))
148	125, 146, 147	mp2an 705	. . . . . . . . . 10 ⊢ (log‘(;10↑;27)) = (;27 · (log‘;10))
149	148, 51	eqeltrri 2861	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) ∈ ℝ
150	93, 145, 149	letri 11463	. . . . . . . 8 ⊢ ((2 ≤ (;27 · 2) ∧ (;27 · 2) ≤ (;27 · (log‘;10))) → 2 ≤ (;27 · (log‘;10)))
151	97, 144, 150	mp2an 705	. . . . . . 7 ⊢ 2 ≤ (;27 · (log‘;10))
152		relogef 26937	. . . . . . . 8 ⊢ (2 ∈ ℝ → (log‘(exp‘2)) = 2)
153	93, 152	ax-mp 5	. . . . . . 7 ⊢ (log‘(exp‘2)) = 2
154	151, 153, 148	3brtr4i 5138	. . . . . 6 ⊢ (log‘(exp‘2)) ≤ (log‘(;10↑;27))
155		rpefcl 16298	. . . . . . . 8 ⊢ (2 ∈ ℝ → (exp‘2) ∈ ℝ⁺)
156	93, 155	ax-mp 5	. . . . . . 7 ⊢ (exp‘2) ∈ ℝ⁺
157		logleb 26958	. . . . . . 7 ⊢ (((exp‘2) ∈ ℝ⁺ ∧ (;10↑;27) ∈ ℝ⁺) → ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27))))
158	156, 49, 157	mp2an 705	. . . . . 6 ⊢ ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27)))
159	154, 158	mpbir 234	. . . . 5 ⊢ (exp‘2) ≤ (;10↑;27)
160	159	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (exp‘2) ≤ (;10↑;27))
161	86, 40, 160, 38	logdivsqrle 35346	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ≤ ((log‘(;10↑;27)) / (√‘(;10↑;27))))
162	46, 56, 13, 85, 161	lemul2ad 12281	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ≤ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
163		3lt10 12981	. . . . . . . 8 ⊢ 3 < ;10
164		4lt10 12980	. . . . . . . . 9 ⊢ 4 < ;10
165		8lt10 12976	. . . . . . . . 9 ⊢ 8 < ;10
166	59, 77, 164, 165	dp2lt10 33517	. . . . . . . 8 ⊢ _48 < ;10
167	74, 78, 163, 166	dp2lt10 33517	. . . . . . 7 ⊢ _3_48 < ;10
168		7p1e8 12515	. . . . . . 7 ⊢ (7 + 1) = 8
169	1, 79, 61, 167, 168	dplti 33538	. . . . . 6 ⊢ (7._3_48) < 8
170	58, 62	sselii 3910	. . . . . . 7 ⊢ 8 ∈ ℝ
171	12, 170, 18	lttri 11460	. . . . . 6 ⊢ (((7._3_48) < 8 ∧ 8 < ;10) → (7._3_48) < ;10)
172	169, 165, 171	mp2an 705	. . . . 5 ⊢ (7._3_48) < ;10
173	27, 26	deccl 12853	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
174	173	numexp0 17279	. . . . . . . . 9 ⊢ (;10↑0) = 1
175		0z 12728	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
176	18, 175, 146	3pm3.2i 1358	. . . . . . . . . 10 ⊢ (;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ)
177		1lt10 12983	. . . . . . . . . . 11 ⊢ 1 < ;10
178	177, 141	pm3.2i 476	. . . . . . . . . 10 ⊢ (1 < ;10 ∧ 0 < ;27)
179		ltexp2a 14333	. . . . . . . . . 10 ⊢ (((;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < ;27)) → (;10↑0) < (;10↑;27))
180	176, 178, 179	mp2an 705	. . . . . . . . 9 ⊢ (;10↑0) < (;10↑;27)
181	174, 180	eqbrtrri 5131	. . . . . . . 8 ⊢ 1 < (;10↑;27)
182		loggt0b 26987	. . . . . . . . 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 234	. . . . . . 7 ⊢ 0 < (log‘(;10↑;27))
185	51, 52	divgt0i 12249	. . . . . . 7 ⊢ ((0 < (log‘(;10↑;27)) ∧ 0 < (√‘(;10↑;27))) → 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))))
186	184, 53, 185	mp2an 705	. . . . . 6 ⊢ 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27)))
187	12, 18, 55	ltmul1i 12259	. . . . . 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 233	. . . 4 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27))))
190	18	recni 11347	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℂ
191		expmul 14274	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℂ ∧ 7 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (;10↑(7 · 2)) = ((;10↑7)↑2))
192	190, 1, 19, 191	mp3an 1491	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = ((;10↑7)↑2)
193		7t2e14 12952	. . . . . . . . . . . . 13 ⊢ (7 · 2) = ;14
194	193	oveq2i 7451	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = (;10↑;14)
195	192, 194	eqtr3i 2788	. . . . . . . . . . 11 ⊢ ((;10↑7)↑2) = (;10↑;14)
196	195	fveq2i 6908	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (√‘(;10↑;14))
197		reexpcl 14245	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℕ₀) → (;10↑7) ∈ ℝ)
198	18, 1, 197	mp2an 705	. . . . . . . . . . 11 ⊢ (;10↑7) ∈ ℝ
199	1	nn0zi 12745	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℤ
200		expgt0 14262	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑7))
201	18, 199, 123, 200	mp3an 1491	. . . . . . . . . . . 12 ⊢ 0 < (;10↑7)
202	16, 198, 201	ltleii 11457	. . . . . . . . . . 11 ⊢ 0 ≤ (;10↑7)
203		sqrtsq 15462	. . . . . . . . . . 11 ⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤ (;10↑7)) → (√‘((;10↑7)↑2)) = (;10↑7))
204	198, 202, 203	mp2an 705	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (;10↑7)
205	196, 204	eqtr3i 2788	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) = (;10↑7)
206	27, 59	deccl 12853	. . . . . . . . . . . . 13 ⊢ ;14 ∈ ℕ₀
207	206	nn0zi 12745	. . . . . . . . . . . 12 ⊢ ;14 ∈ ℤ
208	18, 207, 146	3pm3.2i 1358	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ)
209		1lt2 12539	. . . . . . . . . . . . 13 ⊢ 1 < 2
210	27, 19, 59, 1, 164, 209	decltc 12872	. . . . . . . . . . . 12 ⊢ ;14 < ;27
211	177, 210	pm3.2i 476	. . . . . . . . . . 11 ⊢ (1 < ;10 ∧ ;14 < ;27)
212		ltexp2a 14333	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27))
213	208, 211, 212	mp2an 705	. . . . . . . . . 10 ⊢ (;10↑;14) < (;10↑;27)
214		reexpcl 14245	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℕ₀) → (;10↑;14) ∈ ℝ)
215	18, 206, 214	mp2an 705	. . . . . . . . . . . 12 ⊢ (;10↑;14) ∈ ℝ
216		expgt0 14262	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14))
217	18, 207, 123, 216	mp3an 1491	. . . . . . . . . . . . 13 ⊢ 0 < (;10↑;14)
218	16, 215, 217	ltleii 11457	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;14)
219	215, 218	pm3.2i 476	. . . . . . . . . . 11 ⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14))
220	16, 22, 36	ltleii 11457	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;27)
221	22, 220	pm3.2i 476	. . . . . . . . . . 11 ⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))
222		sqrtlt 15454	. . . . . . . . . . 11 ⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))))
223	219, 221, 222	mp2an 705	. . . . . . . . . 10 ⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))
224	213, 223	mpbi 233	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) < (√‘(;10↑;27))
225	205, 224	eqbrtrri 5131	. . . . . . . 8 ⊢ (;10↑7) < (√‘(;10↑;27))
226	198, 201	pm3.2i 476	. . . . . . . . 9 ⊢ ((;10↑7) ∈ ℝ ∧ 0 < (;10↑7))
227	52, 53	pm3.2i 476	. . . . . . . . 9 ⊢ ((√‘(;10↑;27)) ∈ ℝ ∧ 0 < (√‘(;10↑;27)))
228	51, 184	pm3.2i 476	. . . . . . . . 9 ⊢ ((log‘(;10↑;27)) ∈ ℝ ∧ 0 < (log‘(;10↑;27)))
229		ltdiv2 12227	. . . . . . . . 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 1491	. . . . . . . 8 ⊢ ((;10↑7) < (√‘(;10↑;27)) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7)))
231	225, 230	mpbi 233	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7))
232		6nn 12456	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
233	232	nngt0i 12401	. . . . . . . . . . . . . 14 ⊢ 0 < 6
234	27, 26, 232, 233	declt 12871	. . . . . . . . . . . . 13 ⊢ ;10 < ;16
235		6nn0 12651	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ₀
236	27, 235	deccl 12853	. . . . . . . . . . . . . . . 16 ⊢ ;16 ∈ ℕ₀
237	236	nn0rei 12641	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℝ
238	25, 235, 26, 123	declti 12881	. . . . . . . . . . . . . . 15 ⊢ 0 < ;16
239		elrp 13146	. . . . . . . . . . . . . . 15 ⊢ (;16 ∈ ℝ⁺ ↔ (;16 ∈ ℝ ∧ 0 < ;16))
240	237, 238, 239	mpbir2an 724	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℝ⁺
241		logltb 26955	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ⁺ ∧ ;16 ∈ ℝ⁺) → (;10 < ;16 ↔ (log‘;10) < (log‘;16)))
242	125, 240, 241	mp2an 705	. . . . . . . . . . . . 13 ⊢ (;10 < ;16 ↔ (log‘;10) < (log‘;16))
243	234, 242	mpbi 233	. . . . . . . . . . . 12 ⊢ (log‘;10) < (log‘;16)
244		2exp4 17288	. . . . . . . . . . . . . 14 ⊢ (2↑4) = ;16
245	244	fveq2i 6908	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (log‘;16)
246		2rp 13149	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
247	59	nn0zi 12745	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
248		relogexp 26951	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ 4 ∈ ℤ) → (log‘(2↑4)) = (4 · (log‘2)))
249	246, 247, 248	mp2an 705	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (4 · (log‘2))
250	245, 249	eqtr3i 2788	. . . . . . . . . . . 12 ⊢ (log‘;16) = (4 · (log‘2))
251	243, 250	breqtri 5133	. . . . . . . . . . 11 ⊢ (log‘;10) < (4 · (log‘2))
252	100	simpli 489	. . . . . . . . . . . . . . 15 ⊢ 2 < e
253		logltb 26955	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ⁺ ∧ e ∈ ℝ⁺) → (2 < e ↔ (log‘2) < (log‘e)))
254	246, 102, 253	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (2 < e ↔ (log‘2) < (log‘e))
255	252, 254	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (log‘2) < (log‘e)
256	255, 99	breqtri 5133	. . . . . . . . . . . . 13 ⊢ (log‘2) < 1
257		4pos 12477	. . . . . . . . . . . . . 14 ⊢ 0 < 4
258		relogcl 26930	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
259	246, 258	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (log‘2) ∈ ℝ
260	259, 28, 3	ltmul2i 12262	. . . . . . . . . . . . . 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 233	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) < (4 · 1)
263		4cn 12452	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℂ
264	263	mulridi 11337	. . . . . . . . . . . 12 ⊢ (4 · 1) = 4
265	262, 264	breqtri 5133	. . . . . . . . . . 11 ⊢ (4 · (log‘2)) < 4
266	3, 259	remulcli 11349	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) ∈ ℝ
267	134, 266, 3	lttri 11460	. . . . . . . . . . 11 ⊢ (((log‘;10) < (4 · (log‘2)) ∧ (4 · (log‘2)) < 4) → (log‘;10) < 4)
268	251, 265, 267	mp2an 705	. . . . . . . . . 10 ⊢ (log‘;10) < 4
269	134, 3, 92	ltmul2i 12262	. . . . . . . . . . 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 233	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) < (;27 · 4)
272	148, 271	eqbrtri 5129	. . . . . . . 8 ⊢ (log‘(;10↑;27)) < (;27 · 4)
273	92, 3	remulcli 11349	. . . . . . . . . 10 ⊢ (;27 · 4) ∈ ℝ
274	51, 273, 198	ltdiv1i 12260	. . . . . . . . 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 233	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))
277	16, 201	gtneii 11446	. . . . . . . . 9 ⊢ (;10↑7) ≠ 0
278	51, 198, 277	redivcli 12108	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) / (;10↑7)) ∈ ℝ
279	273, 198, 277	redivcli 12108	. . . . . . . 8 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
280	55, 278, 279	lttri 11460	. . . . . . 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 705	. . . . . 6 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7))
282		7lt10 12977	. . . . . . . . . 10 ⊢ 7 < ;10
283		2lt10 12982	. . . . . . . . . 10 ⊢ 2 < ;10
284	19, 173, 1, 26, 282, 283	decltc 12872	. . . . . . . . 9 ⊢ ;27 < ;;100
285		10nn 12858	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℕ
286	285	decnncl2 12867	. . . . . . . . . . . 12 ⊢ ;;100 ∈ ℕ
287	286	nnrei 12368	. . . . . . . . . . 11 ⊢ ;;100 ∈ ℝ
288	92, 287, 3	ltmul1i 12259	. . . . . . . . . 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 233	. . . . . . . 8 ⊢ (;27 · 4) < (;;100 · 4)
291	287, 3	remulcli 11349	. . . . . . . . . 10 ⊢ (;;100 · 4) ∈ ℝ
292	273, 291, 198	ltdiv1i 12260	. . . . . . . . 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 233	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7))
295		8nn 12462	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ
296		nnrp 13156	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
297	295, 296	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℝ⁺
298	59, 297	rpdp2cl 33515	. . . . . . . . . . . . 13 ⊢ _48 ∈ ℝ⁺
299	19, 298	rpdp2cl 33515	. . . . . . . . . . . 12 ⊢ _2_48 ∈ ℝ⁺
300	19, 299	rpdp2cl 33515	. . . . . . . . . . 11 ⊢ _2_2_48 ∈ ℝ⁺
301	59, 300	dpgti 33539	. . . . . . . . . 10 ⊢ 4 < (4._2_2_48)
302	72	recni 11347	. . . . . . . . . . . . 13 ⊢ (0._0_0_0_4_2_2_48) ∈ ℂ
303	198	recni 11347	. . . . . . . . . . . . 13 ⊢ (;10↑7) ∈ ℂ
304	302, 303	mulcli 11340	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑7)) ∈ ℂ
305	16, 123	gtneii 11446	. . . . . . . . . . . . 13 ⊢ ;10 ≠ 0
306	190, 305	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (;10 ∈ ℂ ∧ ;10 ≠ 0)
307	287	recni 11347	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℂ
308	286	nnne0i 12402	. . . . . . . . . . . . 13 ⊢ ;;100 ≠ 0
309	307, 308	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (;;100 ∈ ℂ ∧ ;;100 ≠ 0)
310		divdiv1 12052	. . . . . . . . . . . 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 1491	. . . . . . . . . . 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 12099	. . . . . . . . . . . 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 7450	. . . . . . . . . . 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 11340	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ∈ ℂ
315	190, 307, 305, 308	mulne0i 11983	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ≠ 0
316	302, 303, 314, 315	divassi 12097	. . . . . . . . . . . 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 14235	. . . . . . . . . . . . . . . . . 18 ⊢ ((;10 ∈ ℂ ∧ 2 ∈ ℕ₀) → (;10↑(2 + 1)) = ((;10↑2) · ;10))
318	190, 19, 317	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (;10↑(2 + 1)) = ((;10↑2) · ;10)
319		sq10 14432	. . . . . . . . . . . . . . . . . 18 ⊢ (;10↑2) = ;;100
320	319	oveq1i 7450	. . . . . . . . . . . . . . . . 17 ⊢ ((;10↑2) · ;10) = (;;100 · ;10)
321	307, 190	mulcomi 11341	. . . . . . . . . . . . . . . . 17 ⊢ (;;100 · ;10) = (;10 · ;;100)
322	318, 320, 321	3eqtrri 2791	. . . . . . . . . . . . . . . 16 ⊢ (;10 · ;;100) = (;10↑(2 + 1))
323		2p1e3 12508	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 1) = 3
324	323	oveq2i 7451	. . . . . . . . . . . . . . . 16 ⊢ (;10↑(2 + 1)) = (;10↑3)
325	322, 324	eqtri 2786	. . . . . . . . . . . . . . 15 ⊢ (;10 · ;;100) = (;10↑3)
326	325	oveq2i 7451	. . . . . . . . . . . . . 14 ⊢ ((;10↑7) / (;10 · ;;100)) = ((;10↑7) / (;10↑3))
327	74	nn0zi 12745	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
328	199, 327	pm3.2i 476	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℤ ∧ 3 ∈ ℤ)
329		expsub 14277	. . . . . . . . . . . . . . 15 ⊢ (((;10 ∈ ℂ ∧ ;10 ≠ 0) ∧ (7 ∈ ℤ ∧ 3 ∈ ℤ)) → (;10↑(7 − 3)) = ((;10↑7) / (;10↑3)))
330	306, 328, 329	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = ((;10↑7) / (;10↑3))
331		7cn 12461	. . . . . . . . . . . . . . . 16 ⊢ 7 ∈ ℂ
332		4p3e7 12520	. . . . . . . . . . . . . . . . 17 ⊢ (4 + 3) = 7
333	263, 112, 332	addcomli 11526	. . . . . . . . . . . . . . . 16 ⊢ (3 + 4) = 7
334	331, 112, 263, 333	subaddrii 11671	. . . . . . . . . . . . . . 15 ⊢ (7 − 3) = 4
335	334	oveq2i 7451	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = (;10↑4)
336	326, 330, 335	3eqtr2i 2792	. . . . . . . . . . . . 13 ⊢ ((;10↑7) / (;10 · ;;100)) = (;10↑4)
337	336	oveq2i 7451	. . . . . . . . . . . 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 17280	. . . . . . . . . . . . . 14 ⊢ (;10↑1) = ;10
339	338	oveq2i 7451	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._4_2_2_48) · ;10)
340	59, 300	rpdp2cl 33515	. . . . . . . . . . . . . . 15 ⊢ _4_2_2_48 ∈ ℝ⁺
341	25	nnzi 12744	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
342	89	nnzi 12744	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
343	26, 340, 98, 341, 342	dpexpp1 33541	. . . . . . . . . . . . . 14 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_4_2_2_48) · (;10↑2))
344	26, 340	rpdp2cl 33515	. . . . . . . . . . . . . . 15 ⊢ _0_4_2_2_48 ∈ ℝ⁺
345	26, 344, 323, 342, 327	dpexpp1 33541	. . . . . . . . . . . . . 14 ⊢ ((0._0_4_2_2_48) · (;10↑2)) = ((0._0_0_4_2_2_48) · (;10↑3))
346	26, 344	rpdp2cl 33515	. . . . . . . . . . . . . . 15 ⊢ _0_0_4_2_2_48 ∈ ℝ⁺
347		3p1e4 12511	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
348	26, 346, 347, 327, 247	dpexpp1 33541	. . . . . . . . . . . . . 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 2790	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_0_0_4_2_2_48) · (;10↑4))
350	59, 300	0dp2dp 33542	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · ;10) = (4._2_2_48)
351	339, 349, 350	3eqtr3i 2794	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑4)) = (4._2_2_48)
352	316, 337, 351	3eqtri 2790	. . . . . . . . . . 11 ⊢ (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100)) = (4._2_2_48)
353	311, 313, 352	3eqtr3i 2794	. . . . . . . . . 10 ⊢ ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100) = (4._2_2_48)
354	301, 353	breqtrri 5135	. . . . . . . . 9 ⊢ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)
355	72, 18, 305	redivcli 12108	. . . . . . . . . . 11 ⊢ ((0._0_0_0_4_2_2_48) / ;10) ∈ ℝ
356	355, 198	remulcli 11349	. . . . . . . . . 10 ⊢ (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ∈ ℝ
357	286	nngt0i 12401	. . . . . . . . . . 11 ⊢ 0 < ;;100
358	287, 357	pm3.2i 476	. . . . . . . . . 10 ⊢ (;;100 ∈ ℝ ∧ 0 < ;;100)
359		ltmuldiv2 12215	. . . . . . . . . 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 1491	. . . . . . . . 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 234	. . . . . . . 8 ⊢ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7))
362		ltdivmul2 12218	. . . . . . . . 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 1491	. . . . . . . 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 234	. . . . . . 7 ⊢ ((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
365	291, 198, 277	redivcli 12108	. . . . . . . 8 ⊢ ((;;100 · 4) / (;10↑7)) ∈ ℝ
366	279, 365, 355	lttri 11460	. . . . . . 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 705	. . . . . 6 ⊢ ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
368	226	simpli 489	. . . . . . . 8 ⊢ (;10↑7) ∈ ℝ
369	273, 368, 277	redivcli 12108	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
370	55, 369, 355	lttri 11460	. . . . . 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 705	. . . . 5 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10)
372	125, 124	mpbi 233	. . . . . 6 ⊢ (;10 ∈ ℝ ∧ 0 < ;10)
373		ltmuldiv2 12215	. . . . . 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 1491	. . . . 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 234	. . . 4 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48)
376	12, 55	remulcli 11349	. . . . 5 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
377	18, 55	remulcli 11349	. . . . 5 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
378	376, 377, 72	lttri 11460	. . . 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 705	. . 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 11492	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 class class class wbr 5106 ‘cfv 6555 (class class class)co 7440 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 · cmul 11229 < clt 11367 ≤ cle 11368 − cmin 11565 / cdiv 11997 ℕcn 12359 2c2 12421 3c3 12422 4c4 12423 6c6 12425 7c7 12426 8c8 12427 9c9 12428 ℕ₀cn0 12630 ℤcz 12717 cdc 12838 ℚcq 13099 ℝ⁺crp 13144 ↑cexp 14228 √csqrt 15426 expce 16253 eceu 16254 logclog 26909 cdp2 33504 .cdp 33521

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-cc 10537 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302 ax-addf 11303

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-symdif 4201 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-disj 5074 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-ofr 7715 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-oadd 8505 df-omul 8506 df-er 8742 df-map 8874 df-pm 8875 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-fi 9427 df-sup 9458 df-inf 9459 df-oi 9528 df-dju 10006 df-card 10044 df-acn 10047 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-z 12718 df-dec 12839 df-uz 12990 df-q 13100 df-rp 13145 df-xneg 13265 df-xadd 13266 df-xmul 13267 df-ioo 13504 df-ioc 13505 df-ico 13506 df-icc 13507 df-fz 13664 df-fzo 13813 df-fl 13956 df-mod 14034 df-seq 14169 df-exp 14229 df-fac 14442 df-bc 14471 df-hash 14499 df-shft 15246 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-limsup 15664 df-clim 15681 df-rlim 15682 df-sum 15880 df-ef 16259 df-e 16260 df-sin 16261 df-cos 16262 df-tan 16263 df-pi 16264 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-starv 17469 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-unif 17477 df-hom 17478 df-cco 17479 df-rest 17619 df-topn 17620 df-0g 17638 df-gsum 17639 df-topgen 17640 df-pt 17641 df-prds 17644 df-xrs 17700 df-qtop 17705 df-imas 17706 df-xps 17708 df-mre 17782 df-mrc 17783 df-acs 17785 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-submnd 19005 df-mulg 19304 df-cntz 19558 df-cmn 20023 df-psmet 21697 df-xmet 21698 df-met 21699 df-bl 21700 df-mopn 21701 df-fbas 21702 df-fg 21703 df-cnfld 21706 df-top 23239 df-topon 23256 df-topsp 23278 df-bases 23291 df-cld 23364 df-ntr 23365 df-cls 23366 df-nei 23443 df-lp 23481 df-perf 23482 df-cn 23572 df-cnp 23573 df-haus 23660 df-cmp 23732 df-tx 23908 df-hmeo 24101 df-fil 24192 df-fm 24284 df-flim 24285 df-flf 24286 df-xms 24666 df-ms 24667 df-tms 24668 df-cncf 25226 df-ovol 25812 df-vol 25813 df-mbf 25967 df-itg1 25968 df-itg2 25969 df-ibl 25970 df-itg 25971 df-0p 26018 df-limc 26213 df-dv 26214 df-log 26911 df-cxp 26912 df-dp2 33505 df-dp 33522

This theorem is used by: tgoldbachgtde 35356

W3C validator