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 34983

Description: Lemma for tgoldbachgtd 34994. (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 12526	. . . . 5 ⊢ 7 ∈ ℕ₀
2		3re 12321	. . . . . . 7 ⊢ 3 ∈ ℝ
3		4re 12325	. . . . . . . . 9 ⊢ 4 ∈ ℝ
4		8re 12337	. . . . . . . . 9 ⊢ 8 ∈ ℝ
5	3, 4	pm3.2i 475	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
6		dp2cl 33140	. . . . . . . 8 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
7	5, 6	ax-mp 5	. . . . . . 7 ⊢ _48 ∈ ℝ
8	2, 7	pm3.2i 475	. . . . . 6 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
9		dp2cl 33140	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
10	8, 9	ax-mp 5	. . . . 5 ⊢ _3_48 ∈ ℝ
11		dpcl 33151	. . . . 5 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
12	1, 10, 11	mp2an 704	. . . 4 ⊢ (7._3_48) ∈ ℝ
13	12	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (7._3_48) ∈ ℝ)
14		nn0re 12513	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	14	adantr 485	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ)
16		0re 11210	. . . . . . . 8 ⊢ 0 ∈ ℝ
17	16	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ∈ ℝ)
18		10re 12734	. . . . . . . . 9 ⊢ ;10 ∈ ℝ
19		2nn0 12521	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
20	19, 1	deccl 12726	. . . . . . . . 9 ⊢ ;27 ∈ ℕ₀
21		reexpcl 14114	. . . . . . . . 9 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀) → (;10↑;27) ∈ ℝ)
22	18, 20, 21	mp2an 704	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
23	22	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ∈ ℝ)
24		0lt1 11736	. . . . . . . . 9 ⊢ 0 < 1
25		1nn 12244	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
26		0nn0 12519	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
27		1nn0 12520	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
28		1re 11208	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
29		9re 12340	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
30		1lt9 12449	. . . . . . . . . . . 12 ⊢ 1 < 9
31	28, 29, 30	ltleii 11333	. . . . . . . . . . 11 ⊢ 1 ≤ 9
32	25, 26, 27, 31	declei 12752	. . . . . . . . . 10 ⊢ 1 ≤ ;10
33		expge1 14135	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀ ∧ 1 ≤ ;10) → 1 ≤ (;10↑;27))
34	18, 20, 32, 33	mp3an 1487	. . . . . . . . 9 ⊢ 1 ≤ (;10↑;27)
35	16, 28, 22	ltletri 11338	. . . . . . . . 9 ⊢ ((0 < 1 ∧ 1 ≤ (;10↑;27)) → 0 < (;10↑;27))
36	24, 34, 35	mp2an 704	. . . . . . . 8 ⊢ 0 < (;10↑;27)
37	36	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (;10↑;27))
38		simpr 489	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ≤ 𝑁)
39	17, 23, 15, 37, 38	ltletrd 11370	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < 𝑁)
40	15, 39	elrpd 13057	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ⁺)
41	40	relogcld 26754	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (log‘𝑁) ∈ ℝ)
42	40	rpge0d 13064	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ≤ 𝑁)
43	15, 42	resqrtcld 15469	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ∈ ℝ)
44	40	sqrtgt0d 15464	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (√‘𝑁))
45	17, 44	gtned 11345	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ≠ 0)
46	41, 43, 45	redivcld 12043	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
47	13, 46	remulcld 11239	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
48		elrp 13018	. . . . . . 7 ⊢ ((;10↑;27) ∈ ℝ⁺ ↔ ((;10↑;27) ∈ ℝ ∧ 0 < (;10↑;27)))
49	22, 36, 48	mpbir2an 723	. . . . . 6 ⊢ (;10↑;27) ∈ ℝ⁺
50		relogcl 26706	. . . . . 6 ⊢ ((;10↑;27) ∈ ℝ⁺ → (log‘(;10↑;27)) ∈ ℝ)
51	49, 50	ax-mp 5	. . . . 5 ⊢ (log‘(;10↑;27)) ∈ ℝ
52	22, 36	sqrtpclii 15434	. . . . 5 ⊢ (√‘(;10↑;27)) ∈ ℝ
53	22, 36	sqrtgt0ii 15435	. . . . . 6 ⊢ 0 < (√‘(;10↑;27))
54	16, 53	gtneii 11322	. . . . 5 ⊢ (√‘(;10↑;27)) ≠ 0
55	51, 52, 54	redivcli 11982	. . . 4 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ
56	55	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ)
57	13, 56	remulcld 11239	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ)
58		qssre 12983	. . . . 5 ⊢ ℚ ⊆ ℝ
59		4nn0 12523	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
60		nn0ssq 12981	. . . . . . . . . . . . 13 ⊢ ℕ₀ ⊆ ℚ
61		8nn0 12527	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ₀
62	60, 61	sselii 3940	. . . . . . . . . . . 12 ⊢ 8 ∈ ℚ
63	59, 62	dp2clq 33141	. . . . . . . . . . 11 ⊢ _48 ∈ ℚ
64	19, 63	dp2clq 33141	. . . . . . . . . 10 ⊢ _2_48 ∈ ℚ
65	19, 64	dp2clq 33141	. . . . . . . . 9 ⊢ _2_2_48 ∈ ℚ
66	59, 65	dp2clq 33141	. . . . . . . 8 ⊢ _4_2_2_48 ∈ ℚ
67	26, 66	dp2clq 33141	. . . . . . 7 ⊢ _0_4_2_2_48 ∈ ℚ
68	26, 67	dp2clq 33141	. . . . . 6 ⊢ _0_0_4_2_2_48 ∈ ℚ
69	26, 68	dp2clq 33141	. . . . 5 ⊢ _0_0_0_4_2_2_48 ∈ ℚ
70	58, 69	sselii 3940	. . . 4 ⊢ _0_0_0_4_2_2_48 ∈ ℝ
71		dpcl 33151	. . . 4 ⊢ ((0 ∈ ℕ₀ ∧ _0_0_0_4_2_2_48 ∈ ℝ) → (0._0_0_0_4_2_2_48) ∈ ℝ)
72	26, 70, 71	mp2an 704	. . 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 12522	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
75		8pos 12356	. . . . . . . . . . 11 ⊢ 0 < 8
76		elrp 13018	. . . . . . . . . . 11 ⊢ (8 ∈ ℝ⁺ ↔ (8 ∈ ℝ ∧ 0 < 8))
77	4, 75, 76	mpbir2an 723	. . . . . . . . . 10 ⊢ 8 ∈ ℝ⁺
78	59, 77	rpdp2cl 33142	. . . . . . . . 9 ⊢ _48 ∈ ℝ⁺
79	74, 78	rpdp2cl 33142	. . . . . . . 8 ⊢ _3_48 ∈ ℝ⁺
80	1, 79	rpdpcl 33163	. . . . . . 7 ⊢ (7._3_48) ∈ ℝ⁺
81		elrp 13018	. . . . . . 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 490	. . . . 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 12316	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
88	87	mullidi 11214	. . . . . . . . 9 ⊢ (1 · 2) = 2
89		2nn 12314	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
90	89, 1, 27, 31	declei 12752	. . . . . . . . . 10 ⊢ 1 ≤ ;27
91		2pos 12345	. . . . . . . . . . 11 ⊢ 0 < 2
92	20	nn0rei 12515	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℝ
93		2re 12315	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
94	28, 92, 93	lemul1i 12137	. . . . . . . . . . 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 5136	. . . . . . . 8 ⊢ 2 ≤ (;27 · 2)
98		1p1e2 12364	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
99		loge 26717	. . . . . . . . . . . . . 14 ⊢ (log‘e) = 1
100		egt2lt3 16262	. . . . . . . . . . . . . . . 16 ⊢ (2 < e ∧ e < 3)
101	100	simpri 490	. . . . . . . . . . . . . . 15 ⊢ e < 3
102		epr 16264	. . . . . . . . . . . . . . . 16 ⊢ e ∈ ℝ⁺
103		3rp 13022	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ⁺
104		logltb 26731	. . . . . . . . . . . . . . . 16 ⊢ ((e ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → (e < 3 ↔ (log‘e) < (log‘3)))
105	102, 103, 104	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (e < 3 ↔ (log‘e) < (log‘3))
106	101, 105	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (log‘e) < (log‘3)
107	99, 106	eqbrtrri 5136	. . . . . . . . . . . . 13 ⊢ 1 < (log‘3)
108		relogcl 26706	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
109	103, 108	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (log‘3) ∈ ℝ
110	28, 28, 109, 109	lt2addi 11776	. . . . . . . . . . . . 13 ⊢ ((1 < (log‘3) ∧ 1 < (log‘3)) → (1 + 1) < ((log‘3) + (log‘3)))
111	107, 107, 110	mp2an 704	. . . . . . . . . . . 12 ⊢ (1 + 1) < ((log‘3) + (log‘3))
112		3cn 12322	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
113		3ne0 12350	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 0
114		logmul2 26747	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ⁺) → (log‘(3 · 3)) = ((log‘3) + (log‘3)))
115	112, 113, 103, 114	mp3an 1487	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) = ((log‘3) + (log‘3))
116		3t3e9 12408	. . . . . . . . . . . . . . 15 ⊢ (3 · 3) = 9
117	116	fveq2i 6885	. . . . . . . . . . . . . 14 ⊢ (log‘(3 · 3)) = (log‘9)
118		9lt10 12848	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
119	29, 18, 118	ltleii 11333	. . . . . . . . . . . . . . 15 ⊢ 9 ≤ ;10
120		9pos 12357	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 9
121		elrp 13018	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ⁺ ↔ (9 ∈ ℝ ∧ 0 < 9))
122	29, 120, 121	mpbir2an 723	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ⁺
123		10pos 12732	. . . . . . . . . . . . . . . . 17 ⊢ 0 < ;10
124		elrp 13018	. . . . . . . . . . . . . . . . 17 ⊢ (;10 ∈ ℝ⁺ ↔ (;10 ∈ ℝ ∧ 0 < ;10))
125	18, 123, 124	mpbir2an 723	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℝ⁺
126		logleb 26734	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ⁺ ∧ ;10 ∈ ℝ⁺) → (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10)))
127	122, 125, 126	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10))
128	119, 127	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (log‘9) ≤ (log‘;10)
129	117, 128	eqbrtri 5134	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) ≤ (log‘;10)
130	115, 129	eqbrtrri 5136	. . . . . . . . . . . 12 ⊢ ((log‘3) + (log‘3)) ≤ (log‘;10)
131	28, 28	readdcli 11224	. . . . . . . . . . . . 13 ⊢ (1 + 1) ∈ ℝ
132	109, 109	readdcli 11224	. . . . . . . . . . . . 13 ⊢ ((log‘3) + (log‘3)) ∈ ℝ
133		relogcl 26706	. . . . . . . . . . . . . 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 704	. . . . . . . . . . 11 ⊢ (1 + 1) < (log‘;10)
137	98, 136	eqbrtrri 5136	. . . . . . . . . 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 12755	. . . . . . . . . 10 ⊢ 0 < ;27
142	93, 134, 92	lemul2i 12138	. . . . . . . . . 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 11225	. . . . . . . . 9 ⊢ (;27 · 2) ∈ ℝ
146	20	nn0zi 12619	. . . . . . . . . . 11 ⊢ ;27 ∈ ℤ
147		relogexp 26727	. . . . . . . . . . 11 ⊢ ((;10 ∈ ℝ⁺ ∧ ;27 ∈ ℤ) → (log‘(;10↑;27)) = (;27 · (log‘;10)))
148	125, 146, 147	mp2an 704	. . . . . . . . . 10 ⊢ (log‘(;10↑;27)) = (;27 · (log‘;10))
149	148, 51	eqeltrri 2866	. . . . . . . . 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 704	. . . . . . 7 ⊢ 2 ≤ (;27 · (log‘;10))
152		relogef 26713	. . . . . . . 8 ⊢ (2 ∈ ℝ → (log‘(exp‘2)) = 2)
153	93, 152	ax-mp 5	. . . . . . 7 ⊢ (log‘(exp‘2)) = 2
154	151, 153, 148	3brtr4i 5143	. . . . . 6 ⊢ (log‘(exp‘2)) ≤ (log‘(;10↑;27))
155		rpefcl 16160	. . . . . . . 8 ⊢ (2 ∈ ℝ → (exp‘2) ∈ ℝ⁺)
156	93, 155	ax-mp 5	. . . . . . 7 ⊢ (exp‘2) ∈ ℝ⁺
157		logleb 26734	. . . . . . 7 ⊢ (((exp‘2) ∈ ℝ⁺ ∧ (;10↑;27) ∈ ℝ⁺) → ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27))))
158	156, 49, 157	mp2an 704	. . . . . 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 34982	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ≤ ((log‘(;10↑;27)) / (√‘(;10↑;27))))
162	46, 56, 13, 85, 161	lemul2ad 12155	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ≤ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
163		3lt10 12854	. . . . . . . 8 ⊢ 3 < ;10
164		4lt10 12853	. . . . . . . . 9 ⊢ 4 < ;10
165		8lt10 12849	. . . . . . . . 9 ⊢ 8 < ;10
166	59, 77, 164, 165	dp2lt10 33144	. . . . . . . 8 ⊢ _48 < ;10
167	74, 78, 163, 166	dp2lt10 33144	. . . . . . 7 ⊢ _3_48 < ;10
168		7p1e8 12389	. . . . . . 7 ⊢ (7 + 1) = 8
169	1, 79, 61, 167, 168	dplti 33165	. . . . . 6 ⊢ (7._3_48) < 8
170	58, 62	sselii 3940	. . . . . . 7 ⊢ 8 ∈ ℝ
171	12, 170, 18	lttri 11336	. . . . . 6 ⊢ (((7._3_48) < 8 ∧ 8 < ;10) → (7._3_48) < ;10)
172	169, 165, 171	mp2an 704	. . . . 5 ⊢ (7._3_48) < ;10
173	27, 26	deccl 12726	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
174	173	numexp0 17135	. . . . . . . . 9 ⊢ (;10↑0) = 1
175		0z 12602	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
176	18, 175, 146	3pm3.2i 1356	. . . . . . . . . 10 ⊢ (;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ)
177		1lt10 12856	. . . . . . . . . . 11 ⊢ 1 < ;10
178	177, 141	pm3.2i 475	. . . . . . . . . 10 ⊢ (1 < ;10 ∧ 0 < ;27)
179		ltexp2a 14202	. . . . . . . . . 10 ⊢ (((;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < ;27)) → (;10↑0) < (;10↑;27))
180	176, 178, 179	mp2an 704	. . . . . . . . 9 ⊢ (;10↑0) < (;10↑;27)
181	174, 180	eqbrtrri 5136	. . . . . . . 8 ⊢ 1 < (;10↑;27)
182		loggt0b 26763	. . . . . . . . 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 12123	. . . . . . 7 ⊢ ((0 < (log‘(;10↑;27)) ∧ 0 < (√‘(;10↑;27))) → 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))))
186	184, 53, 185	mp2an 704	. . . . . 6 ⊢ 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27)))
187	12, 18, 55	ltmul1i 12133	. . . . . 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 11223	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℂ
191		expmul 14143	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℂ ∧ 7 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (;10↑(7 · 2)) = ((;10↑7)↑2))
192	190, 1, 19, 191	mp3an 1487	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = ((;10↑7)↑2)
193		7t2e14 12825	. . . . . . . . . . . . 13 ⊢ (7 · 2) = ;14
194	193	oveq2i 7422	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = (;10↑;14)
195	192, 194	eqtr3i 2794	. . . . . . . . . . 11 ⊢ ((;10↑7)↑2) = (;10↑;14)
196	195	fveq2i 6885	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (√‘(;10↑;14))
197		reexpcl 14114	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℕ₀) → (;10↑7) ∈ ℝ)
198	18, 1, 197	mp2an 704	. . . . . . . . . . 11 ⊢ (;10↑7) ∈ ℝ
199	1	nn0zi 12619	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℤ
200		expgt0 14131	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑7))
201	18, 199, 123, 200	mp3an 1487	. . . . . . . . . . . 12 ⊢ 0 < (;10↑7)
202	16, 198, 201	ltleii 11333	. . . . . . . . . . 11 ⊢ 0 ≤ (;10↑7)
203		sqrtsq 15320	. . . . . . . . . . 11 ⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤ (;10↑7)) → (√‘((;10↑7)↑2)) = (;10↑7))
204	198, 202, 203	mp2an 704	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (;10↑7)
205	196, 204	eqtr3i 2794	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) = (;10↑7)
206	27, 59	deccl 12726	. . . . . . . . . . . . 13 ⊢ ;14 ∈ ℕ₀
207	206	nn0zi 12619	. . . . . . . . . . . 12 ⊢ ;14 ∈ ℤ
208	18, 207, 146	3pm3.2i 1356	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ)
209		1lt2 12413	. . . . . . . . . . . . 13 ⊢ 1 < 2
210	27, 19, 59, 1, 164, 209	decltc 12745	. . . . . . . . . . . 12 ⊢ ;14 < ;27
211	177, 210	pm3.2i 475	. . . . . . . . . . 11 ⊢ (1 < ;10 ∧ ;14 < ;27)
212		ltexp2a 14202	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27))
213	208, 211, 212	mp2an 704	. . . . . . . . . 10 ⊢ (;10↑;14) < (;10↑;27)
214		reexpcl 14114	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℕ₀) → (;10↑;14) ∈ ℝ)
215	18, 206, 214	mp2an 704	. . . . . . . . . . . 12 ⊢ (;10↑;14) ∈ ℝ
216		expgt0 14131	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14))
217	18, 207, 123, 216	mp3an 1487	. . . . . . . . . . . . 13 ⊢ 0 < (;10↑;14)
218	16, 215, 217	ltleii 11333	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;14)
219	215, 218	pm3.2i 475	. . . . . . . . . . 11 ⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14))
220	16, 22, 36	ltleii 11333	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;27)
221	22, 220	pm3.2i 475	. . . . . . . . . . 11 ⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))
222		sqrtlt 15312	. . . . . . . . . . 11 ⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))))
223	219, 221, 222	mp2an 704	. . . . . . . . . 10 ⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))
224	213, 223	mpbi 233	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) < (√‘(;10↑;27))
225	205, 224	eqbrtrri 5136	. . . . . . . 8 ⊢ (;10↑7) < (√‘(;10↑;27))
226	198, 201	pm3.2i 475	. . . . . . . . 9 ⊢ ((;10↑7) ∈ ℝ ∧ 0 < (;10↑7))
227	52, 53	pm3.2i 475	. . . . . . . . 9 ⊢ ((√‘(;10↑;27)) ∈ ℝ ∧ 0 < (√‘(;10↑;27)))
228	51, 184	pm3.2i 475	. . . . . . . . 9 ⊢ ((log‘(;10↑;27)) ∈ ℝ ∧ 0 < (log‘(;10↑;27)))
229		ltdiv2 12101	. . . . . . . . 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 1487	. . . . . . . 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 12330	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
233	232	nngt0i 12275	. . . . . . . . . . . . . 14 ⊢ 0 < 6
234	27, 26, 232, 233	declt 12744	. . . . . . . . . . . . 13 ⊢ ;10 < ;16
235		6nn0 12525	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ₀
236	27, 235	deccl 12726	. . . . . . . . . . . . . . . 16 ⊢ ;16 ∈ ℕ₀
237	236	nn0rei 12515	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℝ
238	25, 235, 26, 123	declti 12754	. . . . . . . . . . . . . . 15 ⊢ 0 < ;16
239		elrp 13018	. . . . . . . . . . . . . . 15 ⊢ (;16 ∈ ℝ⁺ ↔ (;16 ∈ ℝ ∧ 0 < ;16))
240	237, 238, 239	mpbir2an 723	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℝ⁺
241		logltb 26731	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ⁺ ∧ ;16 ∈ ℝ⁺) → (;10 < ;16 ↔ (log‘;10) < (log‘;16)))
242	125, 240, 241	mp2an 704	. . . . . . . . . . . . 13 ⊢ (;10 < ;16 ↔ (log‘;10) < (log‘;16))
243	234, 242	mpbi 233	. . . . . . . . . . . 12 ⊢ (log‘;10) < (log‘;16)
244		2exp4 17144	. . . . . . . . . . . . . 14 ⊢ (2↑4) = ;16
245	244	fveq2i 6885	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (log‘;16)
246		2rp 13021	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
247	59	nn0zi 12619	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
248		relogexp 26727	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ 4 ∈ ℤ) → (log‘(2↑4)) = (4 · (log‘2)))
249	246, 247, 248	mp2an 704	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (4 · (log‘2))
250	245, 249	eqtr3i 2794	. . . . . . . . . . . 12 ⊢ (log‘;16) = (4 · (log‘2))
251	243, 250	breqtri 5138	. . . . . . . . . . 11 ⊢ (log‘;10) < (4 · (log‘2))
252	100	simpli 488	. . . . . . . . . . . . . . 15 ⊢ 2 < e
253		logltb 26731	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ⁺ ∧ e ∈ ℝ⁺) → (2 < e ↔ (log‘2) < (log‘e)))
254	246, 102, 253	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (2 < e ↔ (log‘2) < (log‘e))
255	252, 254	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (log‘2) < (log‘e)
256	255, 99	breqtri 5138	. . . . . . . . . . . . 13 ⊢ (log‘2) < 1
257		4pos 12351	. . . . . . . . . . . . . 14 ⊢ 0 < 4
258		relogcl 26706	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
259	246, 258	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (log‘2) ∈ ℝ
260	259, 28, 3	ltmul2i 12136	. . . . . . . . . . . . . 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 12326	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℂ
264	263	mulridi 11213	. . . . . . . . . . . 12 ⊢ (4 · 1) = 4
265	262, 264	breqtri 5138	. . . . . . . . . . 11 ⊢ (4 · (log‘2)) < 4
266	3, 259	remulcli 11225	. . . . . . . . . . . 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 704	. . . . . . . . . 10 ⊢ (log‘;10) < 4
269	134, 3, 92	ltmul2i 12136	. . . . . . . . . . 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 5134	. . . . . . . 8 ⊢ (log‘(;10↑;27)) < (;27 · 4)
273	92, 3	remulcli 11225	. . . . . . . . . 10 ⊢ (;27 · 4) ∈ ℝ
274	51, 273, 198	ltdiv1i 12134	. . . . . . . . 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 11322	. . . . . . . . 9 ⊢ (;10↑7) ≠ 0
278	51, 198, 277	redivcli 11982	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) / (;10↑7)) ∈ ℝ
279	273, 198, 277	redivcli 11982	. . . . . . . 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 704	. . . . . 6 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7))
282		7lt10 12850	. . . . . . . . . 10 ⊢ 7 < ;10
283		2lt10 12855	. . . . . . . . . 10 ⊢ 2 < ;10
284	19, 173, 1, 26, 282, 283	decltc 12745	. . . . . . . . 9 ⊢ ;27 < ;;100
285		10nn 12731	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℕ
286	285	decnncl2 12740	. . . . . . . . . . . 12 ⊢ ;;100 ∈ ℕ
287	286	nnrei 12242	. . . . . . . . . . 11 ⊢ ;;100 ∈ ℝ
288	92, 287, 3	ltmul1i 12133	. . . . . . . . . 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 11225	. . . . . . . . . 10 ⊢ (;;100 · 4) ∈ ℝ
292	273, 291, 198	ltdiv1i 12134	. . . . . . . . 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 12336	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ
296		nnrp 13028	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
297	295, 296	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℝ⁺
298	59, 297	rpdp2cl 33142	. . . . . . . . . . . . 13 ⊢ _48 ∈ ℝ⁺
299	19, 298	rpdp2cl 33142	. . . . . . . . . . . 12 ⊢ _2_48 ∈ ℝ⁺
300	19, 299	rpdp2cl 33142	. . . . . . . . . . 11 ⊢ _2_2_48 ∈ ℝ⁺
301	59, 300	dpgti 33166	. . . . . . . . . 10 ⊢ 4 < (4._2_2_48)
302	72	recni 11223	. . . . . . . . . . . . 13 ⊢ (0._0_0_0_4_2_2_48) ∈ ℂ
303	198	recni 11223	. . . . . . . . . . . . 13 ⊢ (;10↑7) ∈ ℂ
304	302, 303	mulcli 11216	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑7)) ∈ ℂ
305	16, 123	gtneii 11322	. . . . . . . . . . . . 13 ⊢ ;10 ≠ 0
306	190, 305	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (;10 ∈ ℂ ∧ ;10 ≠ 0)
307	287	recni 11223	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℂ
308	286	nnne0i 12276	. . . . . . . . . . . . 13 ⊢ ;;100 ≠ 0
309	307, 308	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (;;100 ∈ ℂ ∧ ;;100 ≠ 0)
310		divdiv1 11926	. . . . . . . . . . . 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 1487	. . . . . . . . . . 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 11973	. . . . . . . . . . . 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 7421	. . . . . . . . . . 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 11216	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ∈ ℂ
315	190, 307, 305, 308	mulne0i 11857	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ≠ 0
316	302, 303, 314, 315	divassi 11971	. . . . . . . . . . . 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 14104	. . . . . . . . . . . . . . . . . 18 ⊢ ((;10 ∈ ℂ ∧ 2 ∈ ℕ₀) → (;10↑(2 + 1)) = ((;10↑2) · ;10))
318	190, 19, 317	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (;10↑(2 + 1)) = ((;10↑2) · ;10)
319		sq10 14300	. . . . . . . . . . . . . . . . . 18 ⊢ (;10↑2) = ;;100
320	319	oveq1i 7421	. . . . . . . . . . . . . . . . 17 ⊢ ((;10↑2) · ;10) = (;;100 · ;10)
321	307, 190	mulcomi 11217	. . . . . . . . . . . . . . . . 17 ⊢ (;;100 · ;10) = (;10 · ;;100)
322	318, 320, 321	3eqtrri 2797	. . . . . . . . . . . . . . . 16 ⊢ (;10 · ;;100) = (;10↑(2 + 1))
323		2p1e3 12382	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 1) = 3
324	323	oveq2i 7422	. . . . . . . . . . . . . . . 16 ⊢ (;10↑(2 + 1)) = (;10↑3)
325	322, 324	eqtri 2792	. . . . . . . . . . . . . . 15 ⊢ (;10 · ;;100) = (;10↑3)
326	325	oveq2i 7422	. . . . . . . . . . . . . 14 ⊢ ((;10↑7) / (;10 · ;;100)) = ((;10↑7) / (;10↑3))
327	74	nn0zi 12619	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
328	199, 327	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℤ ∧ 3 ∈ ℤ)
329		expsub 14146	. . . . . . . . . . . . . . 15 ⊢ (((;10 ∈ ℂ ∧ ;10 ≠ 0) ∧ (7 ∈ ℤ ∧ 3 ∈ ℤ)) → (;10↑(7 − 3)) = ((;10↑7) / (;10↑3)))
330	306, 328, 329	mp2an 704	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = ((;10↑7) / (;10↑3))
331		7cn 12335	. . . . . . . . . . . . . . . 16 ⊢ 7 ∈ ℂ
332		4p3e7 12394	. . . . . . . . . . . . . . . . 17 ⊢ (4 + 3) = 7
333	263, 112, 332	addcomli 11402	. . . . . . . . . . . . . . . 16 ⊢ (3 + 4) = 7
334	331, 112, 263, 333	subaddrii 11547	. . . . . . . . . . . . . . 15 ⊢ (7 − 3) = 4
335	334	oveq2i 7422	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = (;10↑4)
336	326, 330, 335	3eqtr2i 2798	. . . . . . . . . . . . 13 ⊢ ((;10↑7) / (;10 · ;;100)) = (;10↑4)
337	336	oveq2i 7422	. . . . . . . . . . . 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 17136	. . . . . . . . . . . . . 14 ⊢ (;10↑1) = ;10
339	338	oveq2i 7422	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._4_2_2_48) · ;10)
340	59, 300	rpdp2cl 33142	. . . . . . . . . . . . . . 15 ⊢ _4_2_2_48 ∈ ℝ⁺
341	25	nnzi 12618	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
342	89	nnzi 12618	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
343	26, 340, 98, 341, 342	dpexpp1 33168	. . . . . . . . . . . . . 14 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_4_2_2_48) · (;10↑2))
344	26, 340	rpdp2cl 33142	. . . . . . . . . . . . . . 15 ⊢ _0_4_2_2_48 ∈ ℝ⁺
345	26, 344, 323, 342, 327	dpexpp1 33168	. . . . . . . . . . . . . 14 ⊢ ((0._0_4_2_2_48) · (;10↑2)) = ((0._0_0_4_2_2_48) · (;10↑3))
346	26, 344	rpdp2cl 33142	. . . . . . . . . . . . . . 15 ⊢ _0_0_4_2_2_48 ∈ ℝ⁺
347		3p1e4 12385	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
348	26, 346, 347, 327, 247	dpexpp1 33168	. . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_0_0_4_2_2_48) · (;10↑4))
350	59, 300	0dp2dp 33169	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · ;10) = (4._2_2_48)
351	339, 349, 350	3eqtr3i 2800	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑4)) = (4._2_2_48)
352	316, 337, 351	3eqtri 2796	. . . . . . . . . . 11 ⊢ (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100)) = (4._2_2_48)
353	311, 313, 352	3eqtr3i 2800	. . . . . . . . . 10 ⊢ ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100) = (4._2_2_48)
354	301, 353	breqtrri 5140	. . . . . . . . 9 ⊢ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)
355	72, 18, 305	redivcli 11982	. . . . . . . . . . 11 ⊢ ((0._0_0_0_4_2_2_48) / ;10) ∈ ℝ
356	355, 198	remulcli 11225	. . . . . . . . . 10 ⊢ (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ∈ ℝ
357	286	nngt0i 12275	. . . . . . . . . . 11 ⊢ 0 < ;;100
358	287, 357	pm3.2i 475	. . . . . . . . . 10 ⊢ (;;100 ∈ ℝ ∧ 0 < ;;100)
359		ltmuldiv2 12089	. . . . . . . . . 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 1487	. . . . . . . . 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 12092	. . . . . . . . 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 1487	. . . . . . . 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 11982	. . . . . . . 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 704	. . . . . 6 ⊢ ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
368	226	simpli 488	. . . . . . . 8 ⊢ (;10↑7) ∈ ℝ
369	273, 368, 277	redivcli 11982	. . . . . . 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 704	. . . . 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 12089	. . . . . 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 1487	. . . . 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 11225	. . . . 5 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
377	18, 55	remulcli 11225	. . . . 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 704	. . 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 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 class class class wbr 5111 ‘cfv 6537 (class class class)co 7411 ℂcc 11098 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 < clt 11243 ≤ cle 11244 − cmin 11441 / cdiv 11871 ℕcn 12233 2c2 12295 3c3 12296 4c4 12297 6c6 12299 7c7 12300 8c8 12301 9c9 12302 ℕ₀cn0 12504 ℤcz 12591 cdc 12711 ℚcq 12972 ℝ⁺crp 13016 ↑cexp 14097 √csqrt 15284 expce 16115 eceu 16116 logclog 26685 cdp2 33131 .cdp 33148

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610 ax-cc 10419 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178 ax-addf 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-symdif 4212 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-disj 5079 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-ofr 7676 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8157 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-oadd 8457 df-omul 8458 df-er 8694 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9322 df-fi 9371 df-sup 9402 df-inf 9403 df-oi 9472 df-dju 9887 df-card 9925 df-acn 9928 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-z 12592 df-dec 12712 df-uz 12863 df-q 12973 df-rp 13017 df-xneg 13137 df-xadd 13138 df-xmul 13139 df-ioo 13376 df-ioc 13377 df-ico 13378 df-icc 13379 df-fz 13536 df-fzo 13683 df-fl 13825 df-mod 13903 df-seq 14038 df-exp 14098 df-fac 14310 df-bc 14339 df-hash 14367 df-shft 15104 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-limsup 15522 df-clim 15539 df-rlim 15540 df-sum 15738 df-ef 16121 df-e 16122 df-sin 16123 df-cos 16124 df-tan 16125 df-pi 16126 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-starv 17325 df-sca 17326 df-vsca 17327 df-ip 17328 df-tset 17329 df-ple 17330 df-ds 17332 df-unif 17333 df-hom 17334 df-cco 17335 df-rest 17475 df-topn 17476 df-0g 17494 df-gsum 17495 df-topgen 17496 df-pt 17497 df-prds 17500 df-xrs 17556 df-qtop 17561 df-imas 17562 df-xps 17564 df-mre 17638 df-mrc 17639 df-acs 17641 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-submnd 18842 df-mulg 19134 df-cntz 19387 df-cmn 19852 df-psmet 21483 df-xmet 21484 df-met 21485 df-bl 21486 df-mopn 21487 df-fbas 21488 df-fg 21489 df-cnfld 21492 df-top 23020 df-topon 23037 df-topsp 23059 df-bases 23072 df-cld 23145 df-ntr 23146 df-cls 23147 df-nei 23224 df-lp 23262 df-perf 23263 df-cn 23353 df-cnp 23354 df-haus 23441 df-cmp 23513 df-tx 23688 df-hmeo 23881 df-fil 23972 df-fm 24064 df-flim 24065 df-flf 24066 df-xms 24446 df-ms 24447 df-tms 24448 df-cncf 25006 df-ovol 25592 df-vol 25593 df-mbf 25747 df-itg1 25748 df-itg2 25749 df-ibl 25750 df-itg 25751 df-0p 25798 df-limc 25994 df-dv 25995 df-log 26687 df-cxp 26688 df-dp2 33132 df-dp 33149

This theorem is referenced by: tgoldbachgtde 34992

W3C validator