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 34664

Description: Lemma for tgoldbachgtd 34675. (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 12403	. . . . 5 ⊢ 7 ∈ ℕ₀
2		3re 12205	. . . . . . 7 ⊢ 3 ∈ ℝ
3		4re 12209	. . . . . . . . 9 ⊢ 4 ∈ ℝ
4		8re 12221	. . . . . . . . 9 ⊢ 8 ∈ ℝ
5	3, 4	pm3.2i 470	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 8 ∈ ℝ)
6		dp2cl 32860	. . . . . . . 8 ⊢ ((4 ∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ)
7	5, 6	ax-mp 5	. . . . . . 7 ⊢ _48 ∈ ℝ
8	2, 7	pm3.2i 470	. . . . . 6 ⊢ (3 ∈ ℝ ∧ _48 ∈ ℝ)
9		dp2cl 32860	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ _48 ∈ ℝ) → _3_48 ∈ ℝ)
10	8, 9	ax-mp 5	. . . . 5 ⊢ _3_48 ∈ ℝ
11		dpcl 32871	. . . . 5 ⊢ ((7 ∈ ℕ₀ ∧ _3_48 ∈ ℝ) → (7._3_48) ∈ ℝ)
12	1, 10, 11	mp2an 692	. . . 4 ⊢ (7._3_48) ∈ ℝ
13	12	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (7._3_48) ∈ ℝ)
14		nn0re 12390	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	14	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ)
16		0re 11114	. . . . . . . 8 ⊢ 0 ∈ ℝ
17	16	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ∈ ℝ)
18		10re 12607	. . . . . . . . 9 ⊢ ;10 ∈ ℝ
19		2nn0 12398	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
20	19, 1	deccl 12603	. . . . . . . . 9 ⊢ ;27 ∈ ℕ₀
21		reexpcl 13985	. . . . . . . . 9 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀) → (;10↑;27) ∈ ℝ)
22	18, 20, 21	mp2an 692	. . . . . . . 8 ⊢ (;10↑;27) ∈ ℝ
23	22	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ∈ ℝ)
24		0lt1 11639	. . . . . . . . 9 ⊢ 0 < 1
25		1nn 12136	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
26		0nn0 12396	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
27		1nn0 12397	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
28		1re 11112	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
29		9re 12224	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
30		1lt9 12326	. . . . . . . . . . . 12 ⊢ 1 < 9
31	28, 29, 30	ltleii 11236	. . . . . . . . . . 11 ⊢ 1 ≤ 9
32	25, 26, 27, 31	declei 12624	. . . . . . . . . 10 ⊢ 1 ≤ ;10
33		expge1 14006	. . . . . . . . . 10 ⊢ ((;10 ∈ ℝ ∧ ;27 ∈ ℕ₀ ∧ 1 ≤ ;10) → 1 ≤ (;10↑;27))
34	18, 20, 32, 33	mp3an 1463	. . . . . . . . 9 ⊢ 1 ≤ (;10↑;27)
35	16, 28, 22	ltletri 11241	. . . . . . . . 9 ⊢ ((0 < 1 ∧ 1 ≤ (;10↑;27)) → 0 < (;10↑;27))
36	24, 34, 35	mp2an 692	. . . . . . . 8 ⊢ 0 < (;10↑;27)
37	36	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (;10↑;27))
38		simpr 484	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (;10↑;27) ≤ 𝑁)
39	17, 23, 15, 37, 38	ltletrd 11273	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < 𝑁)
40	15, 39	elrpd 12931	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 𝑁 ∈ ℝ⁺)
41	40	relogcld 26559	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (log‘𝑁) ∈ ℝ)
42	40	rpge0d 12938	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 ≤ 𝑁)
43	15, 42	resqrtcld 15325	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ∈ ℝ)
44	40	sqrtgt0d 15320	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → 0 < (√‘𝑁))
45	17, 44	gtned 11248	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (√‘𝑁) ≠ 0)
46	41, 43, 45	redivcld 11949	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
47	13, 46	remulcld 11142	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
48		elrp 12892	. . . . . . 7 ⊢ ((;10↑;27) ∈ ℝ⁺ ↔ ((;10↑;27) ∈ ℝ ∧ 0 < (;10↑;27)))
49	22, 36, 48	mpbir2an 711	. . . . . 6 ⊢ (;10↑;27) ∈ ℝ⁺
50		relogcl 26511	. . . . . 6 ⊢ ((;10↑;27) ∈ ℝ⁺ → (log‘(;10↑;27)) ∈ ℝ)
51	49, 50	ax-mp 5	. . . . 5 ⊢ (log‘(;10↑;27)) ∈ ℝ
52	22, 36	sqrtpclii 15290	. . . . 5 ⊢ (√‘(;10↑;27)) ∈ ℝ
53	22, 36	sqrtgt0ii 15291	. . . . . 6 ⊢ 0 < (√‘(;10↑;27))
54	16, 53	gtneii 11225	. . . . 5 ⊢ (√‘(;10↑;27)) ≠ 0
55	51, 52, 54	redivcli 11888	. . . 4 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ
56	55	a1i 11	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘(;10↑;27)) / (√‘(;10↑;27))) ∈ ℝ)
57	13, 56	remulcld 11142	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ)
58		qssre 12857	. . . . 5 ⊢ ℚ ⊆ ℝ
59		4nn0 12400	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
60		nn0ssq 12855	. . . . . . . . . . . . 13 ⊢ ℕ₀ ⊆ ℚ
61		8nn0 12404	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ₀
62	60, 61	sselii 3926	. . . . . . . . . . . 12 ⊢ 8 ∈ ℚ
63	59, 62	dp2clq 32861	. . . . . . . . . . 11 ⊢ _48 ∈ ℚ
64	19, 63	dp2clq 32861	. . . . . . . . . 10 ⊢ _2_48 ∈ ℚ
65	19, 64	dp2clq 32861	. . . . . . . . 9 ⊢ _2_2_48 ∈ ℚ
66	59, 65	dp2clq 32861	. . . . . . . 8 ⊢ _4_2_2_48 ∈ ℚ
67	26, 66	dp2clq 32861	. . . . . . 7 ⊢ _0_4_2_2_48 ∈ ℚ
68	26, 67	dp2clq 32861	. . . . . 6 ⊢ _0_0_4_2_2_48 ∈ ℚ
69	26, 68	dp2clq 32861	. . . . 5 ⊢ _0_0_0_4_2_2_48 ∈ ℚ
70	58, 69	sselii 3926	. . . 4 ⊢ _0_0_0_4_2_2_48 ∈ ℝ
71		dpcl 32871	. . . 4 ⊢ ((0 ∈ ℕ₀ ∧ _0_0_0_4_2_2_48 ∈ ℝ) → (0._0_0_0_4_2_2_48) ∈ ℝ)
72	26, 70, 71	mp2an 692	. . 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 12399	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
75		8pos 12237	. . . . . . . . . . 11 ⊢ 0 < 8
76		elrp 12892	. . . . . . . . . . 11 ⊢ (8 ∈ ℝ⁺ ↔ (8 ∈ ℝ ∧ 0 < 8))
77	4, 75, 76	mpbir2an 711	. . . . . . . . . 10 ⊢ 8 ∈ ℝ⁺
78	59, 77	rpdp2cl 32862	. . . . . . . . 9 ⊢ _48 ∈ ℝ⁺
79	74, 78	rpdp2cl 32862	. . . . . . . 8 ⊢ _3_48 ∈ ℝ⁺
80	1, 79	rpdpcl 32883	. . . . . . 7 ⊢ (7._3_48) ∈ ℝ⁺
81		elrp 12892	. . . . . . 7 ⊢ ((7._3_48) ∈ ℝ⁺ ↔ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48)))
82	80, 81	mpbi 230	. . . . . 6 ⊢ ((7._3_48) ∈ ℝ ∧ 0 < (7._3_48))
83	82	simpri 485	. . . . 5 ⊢ 0 < (7._3_48)
84	16, 12, 83	ltleii 11236	. . . 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 12200	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
88	87	mullidi 11117	. . . . . . . . 9 ⊢ (1 · 2) = 2
89		2nn 12198	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
90	89, 1, 27, 31	declei 12624	. . . . . . . . . 10 ⊢ 1 ≤ ;27
91		2pos 12228	. . . . . . . . . . 11 ⊢ 0 < 2
92	20	nn0rei 12392	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℝ
93		2re 12199	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
94	28, 92, 93	lemul1i 12044	. . . . . . . . . . 11 ⊢ (0 < 2 → (1 ≤ ;27 ↔ (1 · 2) ≤ (;27 · 2)))
95	91, 94	ax-mp 5	. . . . . . . . . 10 ⊢ (1 ≤ ;27 ↔ (1 · 2) ≤ (;27 · 2))
96	90, 95	mpbi 230	. . . . . . . . 9 ⊢ (1 · 2) ≤ (;27 · 2)
97	88, 96	eqbrtrri 5112	. . . . . . . 8 ⊢ 2 ≤ (;27 · 2)
98		1p1e2 12245	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
99		loge 26522	. . . . . . . . . . . . . 14 ⊢ (log‘e) = 1
100		egt2lt3 16115	. . . . . . . . . . . . . . . 16 ⊢ (2 < e ∧ e < 3)
101	100	simpri 485	. . . . . . . . . . . . . . 15 ⊢ e < 3
102		epr 16117	. . . . . . . . . . . . . . . 16 ⊢ e ∈ ℝ⁺
103		3rp 12896	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ⁺
104		logltb 26536	. . . . . . . . . . . . . . . 16 ⊢ ((e ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → (e < 3 ↔ (log‘e) < (log‘3)))
105	102, 103, 104	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (e < 3 ↔ (log‘e) < (log‘3))
106	101, 105	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (log‘e) < (log‘3)
107	99, 106	eqbrtrri 5112	. . . . . . . . . . . . 13 ⊢ 1 < (log‘3)
108		relogcl 26511	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
109	103, 108	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (log‘3) ∈ ℝ
110	28, 28, 109, 109	lt2addi 11679	. . . . . . . . . . . . 13 ⊢ ((1 < (log‘3) ∧ 1 < (log‘3)) → (1 + 1) < ((log‘3) + (log‘3)))
111	107, 107, 110	mp2an 692	. . . . . . . . . . . 12 ⊢ (1 + 1) < ((log‘3) + (log‘3))
112		3cn 12206	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
113		3ne0 12231	. . . . . . . . . . . . . 14 ⊢ 3 ≠ 0
114		logmul2 26552	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ⁺) → (log‘(3 · 3)) = ((log‘3) + (log‘3)))
115	112, 113, 103, 114	mp3an 1463	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) = ((log‘3) + (log‘3))
116		3t3e9 12287	. . . . . . . . . . . . . . 15 ⊢ (3 · 3) = 9
117	116	fveq2i 6825	. . . . . . . . . . . . . 14 ⊢ (log‘(3 · 3)) = (log‘9)
118		9lt10 12719	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
119	29, 18, 118	ltleii 11236	. . . . . . . . . . . . . . 15 ⊢ 9 ≤ ;10
120		9pos 12238	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 9
121		elrp 12892	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ⁺ ↔ (9 ∈ ℝ ∧ 0 < 9))
122	29, 120, 121	mpbir2an 711	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ⁺
123		10pos 12605	. . . . . . . . . . . . . . . . 17 ⊢ 0 < ;10
124		elrp 12892	. . . . . . . . . . . . . . . . 17 ⊢ (;10 ∈ ℝ⁺ ↔ (;10 ∈ ℝ ∧ 0 < ;10))
125	18, 123, 124	mpbir2an 711	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℝ⁺
126		logleb 26539	. . . . . . . . . . . . . . . 16 ⊢ ((9 ∈ ℝ⁺ ∧ ;10 ∈ ℝ⁺) → (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10)))
127	122, 125, 126	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (9 ≤ ;10 ↔ (log‘9) ≤ (log‘;10))
128	119, 127	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (log‘9) ≤ (log‘;10)
129	117, 128	eqbrtri 5110	. . . . . . . . . . . . 13 ⊢ (log‘(3 · 3)) ≤ (log‘;10)
130	115, 129	eqbrtrri 5112	. . . . . . . . . . . 12 ⊢ ((log‘3) + (log‘3)) ≤ (log‘;10)
131	28, 28	readdcli 11127	. . . . . . . . . . . . 13 ⊢ (1 + 1) ∈ ℝ
132	109, 109	readdcli 11127	. . . . . . . . . . . . 13 ⊢ ((log‘3) + (log‘3)) ∈ ℝ
133		relogcl 26511	. . . . . . . . . . . . . 14 ⊢ (;10 ∈ ℝ⁺ → (log‘;10) ∈ ℝ)
134	125, 133	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (log‘;10) ∈ ℝ
135	131, 132, 134	ltletri 11241	. . . . . . . . . . . 12 ⊢ (((1 + 1) < ((log‘3) + (log‘3)) ∧ ((log‘3) + (log‘3)) ≤ (log‘;10)) → (1 + 1) < (log‘;10))
136	111, 130, 135	mp2an 692	. . . . . . . . . . 11 ⊢ (1 + 1) < (log‘;10)
137	98, 136	eqbrtrri 5112	. . . . . . . . . 10 ⊢ 2 < (log‘;10)
138	93, 134	ltlei 11235	. . . . . . . . . 10 ⊢ (2 < (log‘;10) → 2 ≤ (log‘;10))
139	137, 138	ax-mp 5	. . . . . . . . 9 ⊢ 2 ≤ (log‘;10)
140	16, 29, 120	ltleii 11236	. . . . . . . . . . 11 ⊢ 0 ≤ 9
141	89, 1, 26, 140	decltdi 12627	. . . . . . . . . 10 ⊢ 0 < ;27
142	93, 134, 92	lemul2i 12045	. . . . . . . . . 10 ⊢ (0 < ;27 → (2 ≤ (log‘;10) ↔ (;27 · 2) ≤ (;27 · (log‘;10))))
143	141, 142	ax-mp 5	. . . . . . . . 9 ⊢ (2 ≤ (log‘;10) ↔ (;27 · 2) ≤ (;27 · (log‘;10)))
144	139, 143	mpbi 230	. . . . . . . 8 ⊢ (;27 · 2) ≤ (;27 · (log‘;10))
145	92, 93	remulcli 11128	. . . . . . . . 9 ⊢ (;27 · 2) ∈ ℝ
146	20	nn0zi 12497	. . . . . . . . . . 11 ⊢ ;27 ∈ ℤ
147		relogexp 26532	. . . . . . . . . . 11 ⊢ ((;10 ∈ ℝ⁺ ∧ ;27 ∈ ℤ) → (log‘(;10↑;27)) = (;27 · (log‘;10)))
148	125, 146, 147	mp2an 692	. . . . . . . . . 10 ⊢ (log‘(;10↑;27)) = (;27 · (log‘;10))
149	148, 51	eqeltrri 2828	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) ∈ ℝ
150	93, 145, 149	letri 11242	. . . . . . . 8 ⊢ ((2 ≤ (;27 · 2) ∧ (;27 · 2) ≤ (;27 · (log‘;10))) → 2 ≤ (;27 · (log‘;10)))
151	97, 144, 150	mp2an 692	. . . . . . 7 ⊢ 2 ≤ (;27 · (log‘;10))
152		relogef 26518	. . . . . . . 8 ⊢ (2 ∈ ℝ → (log‘(exp‘2)) = 2)
153	93, 152	ax-mp 5	. . . . . . 7 ⊢ (log‘(exp‘2)) = 2
154	151, 153, 148	3brtr4i 5119	. . . . . 6 ⊢ (log‘(exp‘2)) ≤ (log‘(;10↑;27))
155		rpefcl 16013	. . . . . . . 8 ⊢ (2 ∈ ℝ → (exp‘2) ∈ ℝ⁺)
156	93, 155	ax-mp 5	. . . . . . 7 ⊢ (exp‘2) ∈ ℝ⁺
157		logleb 26539	. . . . . . 7 ⊢ (((exp‘2) ∈ ℝ⁺ ∧ (;10↑;27) ∈ ℝ⁺) → ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27))))
158	156, 49, 157	mp2an 692	. . . . . 6 ⊢ ((exp‘2) ≤ (;10↑;27) ↔ (log‘(exp‘2)) ≤ (log‘(;10↑;27)))
159	154, 158	mpbir 231	. . . . 5 ⊢ (exp‘2) ≤ (;10↑;27)
160	159	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → (exp‘2) ≤ (;10↑;27))
161	86, 40, 160, 38	logdivsqrle 34663	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((log‘𝑁) / (√‘𝑁)) ≤ ((log‘(;10↑;27)) / (√‘(;10↑;27))))
162	46, 56, 13, 85, 161	lemul2ad 12062	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) ≤ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
163		3lt10 12725	. . . . . . . 8 ⊢ 3 < ;10
164		4lt10 12724	. . . . . . . . 9 ⊢ 4 < ;10
165		8lt10 12720	. . . . . . . . 9 ⊢ 8 < ;10
166	59, 77, 164, 165	dp2lt10 32864	. . . . . . . 8 ⊢ _48 < ;10
167	74, 78, 163, 166	dp2lt10 32864	. . . . . . 7 ⊢ _3_48 < ;10
168		7p1e8 12269	. . . . . . 7 ⊢ (7 + 1) = 8
169	1, 79, 61, 167, 168	dplti 32885	. . . . . 6 ⊢ (7._3_48) < 8
170	58, 62	sselii 3926	. . . . . . 7 ⊢ 8 ∈ ℝ
171	12, 170, 18	lttri 11239	. . . . . 6 ⊢ (((7._3_48) < 8 ∧ 8 < ;10) → (7._3_48) < ;10)
172	169, 165, 171	mp2an 692	. . . . 5 ⊢ (7._3_48) < ;10
173	27, 26	deccl 12603	. . . . . . . . . 10 ⊢ ;10 ∈ ℕ₀
174	173	numexp0 16987	. . . . . . . . 9 ⊢ (;10↑0) = 1
175		0z 12479	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
176	18, 175, 146	3pm3.2i 1340	. . . . . . . . . 10 ⊢ (;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ)
177		1lt10 12727	. . . . . . . . . . 11 ⊢ 1 < ;10
178	177, 141	pm3.2i 470	. . . . . . . . . 10 ⊢ (1 < ;10 ∧ 0 < ;27)
179		ltexp2a 14073	. . . . . . . . . 10 ⊢ (((;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < ;27)) → (;10↑0) < (;10↑;27))
180	176, 178, 179	mp2an 692	. . . . . . . . 9 ⊢ (;10↑0) < (;10↑;27)
181	174, 180	eqbrtrri 5112	. . . . . . . 8 ⊢ 1 < (;10↑;27)
182		loggt0b 26568	. . . . . . . . 9 ⊢ ((;10↑;27) ∈ ℝ⁺ → (0 < (log‘(;10↑;27)) ↔ 1 < (;10↑;27)))
183	49, 182	ax-mp 5	. . . . . . . 8 ⊢ (0 < (log‘(;10↑;27)) ↔ 1 < (;10↑;27))
184	181, 183	mpbir 231	. . . . . . 7 ⊢ 0 < (log‘(;10↑;27))
185	51, 52	divgt0i 12030	. . . . . . 7 ⊢ ((0 < (log‘(;10↑;27)) ∧ 0 < (√‘(;10↑;27))) → 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))))
186	184, 53, 185	mp2an 692	. . . . . 6 ⊢ 0 < ((log‘(;10↑;27)) / (√‘(;10↑;27)))
187	12, 18, 55	ltmul1i 12040	. . . . . 6 ⊢ (0 < ((log‘(;10↑;27)) / (√‘(;10↑;27))) → ((7._3_48) < ;10 ↔ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27))))))
188	186, 187	ax-mp 5	. . . . 5 ⊢ ((7._3_48) < ;10 ↔ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))))
189	172, 188	mpbi 230	. . . 4 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27))))
190	18	recni 11126	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℂ
191		expmul 14014	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℂ ∧ 7 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (;10↑(7 · 2)) = ((;10↑7)↑2))
192	190, 1, 19, 191	mp3an 1463	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = ((;10↑7)↑2)
193		7t2e14 12697	. . . . . . . . . . . . 13 ⊢ (7 · 2) = ;14
194	193	oveq2i 7357	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = (;10↑;14)
195	192, 194	eqtr3i 2756	. . . . . . . . . . 11 ⊢ ((;10↑7)↑2) = (;10↑;14)
196	195	fveq2i 6825	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (√‘(;10↑;14))
197		reexpcl 13985	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℕ₀) → (;10↑7) ∈ ℝ)
198	18, 1, 197	mp2an 692	. . . . . . . . . . 11 ⊢ (;10↑7) ∈ ℝ
199	1	nn0zi 12497	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℤ
200		expgt0 14002	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑7))
201	18, 199, 123, 200	mp3an 1463	. . . . . . . . . . . 12 ⊢ 0 < (;10↑7)
202	16, 198, 201	ltleii 11236	. . . . . . . . . . 11 ⊢ 0 ≤ (;10↑7)
203		sqrtsq 15176	. . . . . . . . . . 11 ⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤ (;10↑7)) → (√‘((;10↑7)↑2)) = (;10↑7))
204	198, 202, 203	mp2an 692	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (;10↑7)
205	196, 204	eqtr3i 2756	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) = (;10↑7)
206	27, 59	deccl 12603	. . . . . . . . . . . . 13 ⊢ ;14 ∈ ℕ₀
207	206	nn0zi 12497	. . . . . . . . . . . 12 ⊢ ;14 ∈ ℤ
208	18, 207, 146	3pm3.2i 1340	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ)
209		1lt2 12291	. . . . . . . . . . . . 13 ⊢ 1 < 2
210	27, 19, 59, 1, 164, 209	decltc 12617	. . . . . . . . . . . 12 ⊢ ;14 < ;27
211	177, 210	pm3.2i 470	. . . . . . . . . . 11 ⊢ (1 < ;10 ∧ ;14 < ;27)
212		ltexp2a 14073	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27))
213	208, 211, 212	mp2an 692	. . . . . . . . . 10 ⊢ (;10↑;14) < (;10↑;27)
214		reexpcl 13985	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℕ₀) → (;10↑;14) ∈ ℝ)
215	18, 206, 214	mp2an 692	. . . . . . . . . . . 12 ⊢ (;10↑;14) ∈ ℝ
216		expgt0 14002	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14))
217	18, 207, 123, 216	mp3an 1463	. . . . . . . . . . . . 13 ⊢ 0 < (;10↑;14)
218	16, 215, 217	ltleii 11236	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;14)
219	215, 218	pm3.2i 470	. . . . . . . . . . 11 ⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14))
220	16, 22, 36	ltleii 11236	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;27)
221	22, 220	pm3.2i 470	. . . . . . . . . . 11 ⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))
222		sqrtlt 15168	. . . . . . . . . . 11 ⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))))
223	219, 221, 222	mp2an 692	. . . . . . . . . 10 ⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))
224	213, 223	mpbi 230	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) < (√‘(;10↑;27))
225	205, 224	eqbrtrri 5112	. . . . . . . 8 ⊢ (;10↑7) < (√‘(;10↑;27))
226	198, 201	pm3.2i 470	. . . . . . . . 9 ⊢ ((;10↑7) ∈ ℝ ∧ 0 < (;10↑7))
227	52, 53	pm3.2i 470	. . . . . . . . 9 ⊢ ((√‘(;10↑;27)) ∈ ℝ ∧ 0 < (√‘(;10↑;27)))
228	51, 184	pm3.2i 470	. . . . . . . . 9 ⊢ ((log‘(;10↑;27)) ∈ ℝ ∧ 0 < (log‘(;10↑;27)))
229		ltdiv2 12008	. . . . . . . . 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 1463	. . . . . . . 8 ⊢ ((;10↑7) < (√‘(;10↑;27)) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7)))
231	225, 230	mpbi 230	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((log‘(;10↑;27)) / (;10↑7))
232		6nn 12214	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
233	232	nngt0i 12164	. . . . . . . . . . . . . 14 ⊢ 0 < 6
234	27, 26, 232, 233	declt 12616	. . . . . . . . . . . . 13 ⊢ ;10 < ;16
235		6nn0 12402	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ₀
236	27, 235	deccl 12603	. . . . . . . . . . . . . . . 16 ⊢ ;16 ∈ ℕ₀
237	236	nn0rei 12392	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℝ
238	25, 235, 26, 123	declti 12626	. . . . . . . . . . . . . . 15 ⊢ 0 < ;16
239		elrp 12892	. . . . . . . . . . . . . . 15 ⊢ (;16 ∈ ℝ⁺ ↔ (;16 ∈ ℝ ∧ 0 < ;16))
240	237, 238, 239	mpbir2an 711	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℝ⁺
241		logltb 26536	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ⁺ ∧ ;16 ∈ ℝ⁺) → (;10 < ;16 ↔ (log‘;10) < (log‘;16)))
242	125, 240, 241	mp2an 692	. . . . . . . . . . . . 13 ⊢ (;10 < ;16 ↔ (log‘;10) < (log‘;16))
243	234, 242	mpbi 230	. . . . . . . . . . . 12 ⊢ (log‘;10) < (log‘;16)
244		2exp4 16996	. . . . . . . . . . . . . 14 ⊢ (2↑4) = ;16
245	244	fveq2i 6825	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (log‘;16)
246		2rp 12895	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
247	59	nn0zi 12497	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
248		relogexp 26532	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ 4 ∈ ℤ) → (log‘(2↑4)) = (4 · (log‘2)))
249	246, 247, 248	mp2an 692	. . . . . . . . . . . . 13 ⊢ (log‘(2↑4)) = (4 · (log‘2))
250	245, 249	eqtr3i 2756	. . . . . . . . . . . 12 ⊢ (log‘;16) = (4 · (log‘2))
251	243, 250	breqtri 5114	. . . . . . . . . . 11 ⊢ (log‘;10) < (4 · (log‘2))
252	100	simpli 483	. . . . . . . . . . . . . . 15 ⊢ 2 < e
253		logltb 26536	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ⁺ ∧ e ∈ ℝ⁺) → (2 < e ↔ (log‘2) < (log‘e)))
254	246, 102, 253	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (2 < e ↔ (log‘2) < (log‘e))
255	252, 254	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (log‘2) < (log‘e)
256	255, 99	breqtri 5114	. . . . . . . . . . . . 13 ⊢ (log‘2) < 1
257		4pos 12232	. . . . . . . . . . . . . 14 ⊢ 0 < 4
258		relogcl 26511	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
259	246, 258	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (log‘2) ∈ ℝ
260	259, 28, 3	ltmul2i 12043	. . . . . . . . . . . . . 14 ⊢ (0 < 4 → ((log‘2) < 1 ↔ (4 · (log‘2)) < (4 · 1)))
261	257, 260	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((log‘2) < 1 ↔ (4 · (log‘2)) < (4 · 1))
262	256, 261	mpbi 230	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) < (4 · 1)
263		4cn 12210	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℂ
264	263	mulridi 11116	. . . . . . . . . . . 12 ⊢ (4 · 1) = 4
265	262, 264	breqtri 5114	. . . . . . . . . . 11 ⊢ (4 · (log‘2)) < 4
266	3, 259	remulcli 11128	. . . . . . . . . . . 12 ⊢ (4 · (log‘2)) ∈ ℝ
267	134, 266, 3	lttri 11239	. . . . . . . . . . 11 ⊢ (((log‘;10) < (4 · (log‘2)) ∧ (4 · (log‘2)) < 4) → (log‘;10) < 4)
268	251, 265, 267	mp2an 692	. . . . . . . . . 10 ⊢ (log‘;10) < 4
269	134, 3, 92	ltmul2i 12043	. . . . . . . . . . 11 ⊢ (0 < ;27 → ((log‘;10) < 4 ↔ (;27 · (log‘;10)) < (;27 · 4)))
270	141, 269	ax-mp 5	. . . . . . . . . 10 ⊢ ((log‘;10) < 4 ↔ (;27 · (log‘;10)) < (;27 · 4))
271	268, 270	mpbi 230	. . . . . . . . 9 ⊢ (;27 · (log‘;10)) < (;27 · 4)
272	148, 271	eqbrtri 5110	. . . . . . . 8 ⊢ (log‘(;10↑;27)) < (;27 · 4)
273	92, 3	remulcli 11128	. . . . . . . . . 10 ⊢ (;27 · 4) ∈ ℝ
274	51, 273, 198	ltdiv1i 12041	. . . . . . . . 9 ⊢ (0 < (;10↑7) → ((log‘(;10↑;27)) < (;27 · 4) ↔ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))))
275	201, 274	ax-mp 5	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) < (;27 · 4) ↔ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7)))
276	272, 275	mpbi 230	. . . . . . 7 ⊢ ((log‘(;10↑;27)) / (;10↑7)) < ((;27 · 4) / (;10↑7))
277	16, 201	gtneii 11225	. . . . . . . . 9 ⊢ (;10↑7) ≠ 0
278	51, 198, 277	redivcli 11888	. . . . . . . 8 ⊢ ((log‘(;10↑;27)) / (;10↑7)) ∈ ℝ
279	273, 198, 277	redivcli 11888	. . . . . . . 8 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
280	55, 278, 279	lttri 11239	. . . . . . 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 692	. . . . . 6 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((;27 · 4) / (;10↑7))
282		7lt10 12721	. . . . . . . . . 10 ⊢ 7 < ;10
283		2lt10 12726	. . . . . . . . . 10 ⊢ 2 < ;10
284	19, 173, 1, 26, 282, 283	decltc 12617	. . . . . . . . 9 ⊢ ;27 < ;;100
285		10nn 12604	. . . . . . . . . . . . 13 ⊢ ;10 ∈ ℕ
286	285	decnncl2 12612	. . . . . . . . . . . 12 ⊢ ;;100 ∈ ℕ
287	286	nnrei 12134	. . . . . . . . . . 11 ⊢ ;;100 ∈ ℝ
288	92, 287, 3	ltmul1i 12040	. . . . . . . . . 10 ⊢ (0 < 4 → (;27 < ;;100 ↔ (;27 · 4) < (;;100 · 4)))
289	257, 288	ax-mp 5	. . . . . . . . 9 ⊢ (;27 < ;;100 ↔ (;27 · 4) < (;;100 · 4))
290	284, 289	mpbi 230	. . . . . . . 8 ⊢ (;27 · 4) < (;;100 · 4)
291	287, 3	remulcli 11128	. . . . . . . . . 10 ⊢ (;;100 · 4) ∈ ℝ
292	273, 291, 198	ltdiv1i 12041	. . . . . . . . 9 ⊢ (0 < (;10↑7) → ((;27 · 4) < (;;100 · 4) ↔ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7))))
293	201, 292	ax-mp 5	. . . . . . . 8 ⊢ ((;27 · 4) < (;;100 · 4) ↔ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7)))
294	290, 293	mpbi 230	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) < ((;;100 · 4) / (;10↑7))
295		8nn 12220	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ
296		nnrp 12902	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
297	295, 296	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℝ⁺
298	59, 297	rpdp2cl 32862	. . . . . . . . . . . . 13 ⊢ _48 ∈ ℝ⁺
299	19, 298	rpdp2cl 32862	. . . . . . . . . . . 12 ⊢ _2_48 ∈ ℝ⁺
300	19, 299	rpdp2cl 32862	. . . . . . . . . . 11 ⊢ _2_2_48 ∈ ℝ⁺
301	59, 300	dpgti 32886	. . . . . . . . . 10 ⊢ 4 < (4._2_2_48)
302	72	recni 11126	. . . . . . . . . . . . 13 ⊢ (0._0_0_0_4_2_2_48) ∈ ℂ
303	198	recni 11126	. . . . . . . . . . . . 13 ⊢ (;10↑7) ∈ ℂ
304	302, 303	mulcli 11119	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑7)) ∈ ℂ
305	16, 123	gtneii 11225	. . . . . . . . . . . . 13 ⊢ ;10 ≠ 0
306	190, 305	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (;10 ∈ ℂ ∧ ;10 ≠ 0)
307	287	recni 11126	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℂ
308	286	nnne0i 12165	. . . . . . . . . . . . 13 ⊢ ;;100 ≠ 0
309	307, 308	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (;;100 ∈ ℂ ∧ ;;100 ≠ 0)
310		divdiv1 11832	. . . . . . . . . . . 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 1463	. . . . . . . . . . 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 11879	. . . . . . . . . . . 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 7356	. . . . . . . . . . 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 11119	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ∈ ℂ
315	190, 307, 305, 308	mulne0i 11760	. . . . . . . . . . . . 13 ⊢ (;10 · ;;100) ≠ 0
316	302, 303, 314, 315	divassi 11877	. . . . . . . . . . . 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 13975	. . . . . . . . . . . . . . . . . 18 ⊢ ((;10 ∈ ℂ ∧ 2 ∈ ℕ₀) → (;10↑(2 + 1)) = ((;10↑2) · ;10))
318	190, 19, 317	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (;10↑(2 + 1)) = ((;10↑2) · ;10)
319		sq10 14171	. . . . . . . . . . . . . . . . . 18 ⊢ (;10↑2) = ;;100
320	319	oveq1i 7356	. . . . . . . . . . . . . . . . 17 ⊢ ((;10↑2) · ;10) = (;;100 · ;10)
321	307, 190	mulcomi 11120	. . . . . . . . . . . . . . . . 17 ⊢ (;;100 · ;10) = (;10 · ;;100)
322	318, 320, 321	3eqtrri 2759	. . . . . . . . . . . . . . . 16 ⊢ (;10 · ;;100) = (;10↑(2 + 1))
323		2p1e3 12262	. . . . . . . . . . . . . . . . 17 ⊢ (2 + 1) = 3
324	323	oveq2i 7357	. . . . . . . . . . . . . . . 16 ⊢ (;10↑(2 + 1)) = (;10↑3)
325	322, 324	eqtri 2754	. . . . . . . . . . . . . . 15 ⊢ (;10 · ;;100) = (;10↑3)
326	325	oveq2i 7357	. . . . . . . . . . . . . 14 ⊢ ((;10↑7) / (;10 · ;;100)) = ((;10↑7) / (;10↑3))
327	74	nn0zi 12497	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
328	199, 327	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℤ ∧ 3 ∈ ℤ)
329		expsub 14017	. . . . . . . . . . . . . . 15 ⊢ (((;10 ∈ ℂ ∧ ;10 ≠ 0) ∧ (7 ∈ ℤ ∧ 3 ∈ ℤ)) → (;10↑(7 − 3)) = ((;10↑7) / (;10↑3)))
330	306, 328, 329	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = ((;10↑7) / (;10↑3))
331		7cn 12219	. . . . . . . . . . . . . . . 16 ⊢ 7 ∈ ℂ
332		4p3e7 12274	. . . . . . . . . . . . . . . . 17 ⊢ (4 + 3) = 7
333	263, 112, 332	addcomli 11305	. . . . . . . . . . . . . . . 16 ⊢ (3 + 4) = 7
334	331, 112, 263, 333	subaddrii 11450	. . . . . . . . . . . . . . 15 ⊢ (7 − 3) = 4
335	334	oveq2i 7357	. . . . . . . . . . . . . 14 ⊢ (;10↑(7 − 3)) = (;10↑4)
336	326, 330, 335	3eqtr2i 2760	. . . . . . . . . . . . 13 ⊢ ((;10↑7) / (;10 · ;;100)) = (;10↑4)
337	336	oveq2i 7357	. . . . . . . . . . . 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 16988	. . . . . . . . . . . . . 14 ⊢ (;10↑1) = ;10
339	338	oveq2i 7357	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._4_2_2_48) · ;10)
340	59, 300	rpdp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ _4_2_2_48 ∈ ℝ⁺
341	25	nnzi 12496	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
342	89	nnzi 12496	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
343	26, 340, 98, 341, 342	dpexpp1 32888	. . . . . . . . . . . . . 14 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_4_2_2_48) · (;10↑2))
344	26, 340	rpdp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ _0_4_2_2_48 ∈ ℝ⁺
345	26, 344, 323, 342, 327	dpexpp1 32888	. . . . . . . . . . . . . 14 ⊢ ((0._0_4_2_2_48) · (;10↑2)) = ((0._0_0_4_2_2_48) · (;10↑3))
346	26, 344	rpdp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ _0_0_4_2_2_48 ∈ ℝ⁺
347		3p1e4 12265	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
348	26, 346, 347, 327, 247	dpexpp1 32888	. . . . . . . . . . . . . 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 2758	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · (;10↑1)) = ((0._0_0_0_4_2_2_48) · (;10↑4))
350	59, 300	0dp2dp 32889	. . . . . . . . . . . . 13 ⊢ ((0._4_2_2_48) · ;10) = (4._2_2_48)
351	339, 349, 350	3eqtr3i 2762	. . . . . . . . . . . 12 ⊢ ((0._0_0_0_4_2_2_48) · (;10↑4)) = (4._2_2_48)
352	316, 337, 351	3eqtri 2758	. . . . . . . . . . 11 ⊢ (((0._0_0_0_4_2_2_48) · (;10↑7)) / (;10 · ;;100)) = (4._2_2_48)
353	311, 313, 352	3eqtr3i 2762	. . . . . . . . . 10 ⊢ ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100) = (4._2_2_48)
354	301, 353	breqtrri 5116	. . . . . . . . 9 ⊢ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100)
355	72, 18, 305	redivcli 11888	. . . . . . . . . . 11 ⊢ ((0._0_0_0_4_2_2_48) / ;10) ∈ ℝ
356	355, 198	remulcli 11128	. . . . . . . . . 10 ⊢ (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ∈ ℝ
357	286	nngt0i 12164	. . . . . . . . . . 11 ⊢ 0 < ;;100
358	287, 357	pm3.2i 470	. . . . . . . . . 10 ⊢ (;;100 ∈ ℝ ∧ 0 < ;;100)
359		ltmuldiv2 11996	. . . . . . . . . 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 1463	. . . . . . . . 9 ⊢ ((;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) ↔ 4 < ((((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)) / ;;100))
361	354, 360	mpbir 231	. . . . . . . 8 ⊢ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7))
362		ltdivmul2 11999	. . . . . . . . 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 1463	. . . . . . . 8 ⊢ (((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10) ↔ (;;100 · 4) < (((0._0_0_0_4_2_2_48) / ;10) · (;10↑7)))
364	361, 363	mpbir 231	. . . . . . 7 ⊢ ((;;100 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
365	291, 198, 277	redivcli 11888	. . . . . . . 8 ⊢ ((;;100 · 4) / (;10↑7)) ∈ ℝ
366	279, 365, 355	lttri 11239	. . . . . . 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 692	. . . . . 6 ⊢ ((;27 · 4) / (;10↑7)) < ((0._0_0_0_4_2_2_48) / ;10)
368	226	simpli 483	. . . . . . . 8 ⊢ (;10↑7) ∈ ℝ
369	273, 368, 277	redivcli 11888	. . . . . . 7 ⊢ ((;27 · 4) / (;10↑7)) ∈ ℝ
370	55, 369, 355	lttri 11239	. . . . . 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 692	. . . . 5 ⊢ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10)
372	125, 124	mpbi 230	. . . . . 6 ⊢ (;10 ∈ ℝ ∧ 0 < ;10)
373		ltmuldiv2 11996	. . . . . 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 1463	. . . . 5 ⊢ ((;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48) ↔ ((log‘(;10↑;27)) / (√‘(;10↑;27))) < ((0._0_0_0_4_2_2_48) / ;10))
375	371, 374	mpbir 231	. . . 4 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) < (0._0_0_0_4_2_2_48)
376	12, 55	remulcli 11128	. . . . 5 ⊢ ((7._3_48) · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
377	18, 55	remulcli 11128	. . . . 5 ⊢ (;10 · ((log‘(;10↑;27)) / (√‘(;10↑;27)))) ∈ ℝ
378	376, 377, 72	lttri 11239	. . . 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 692	. . 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 11271	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 class class class wbr 5089 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 < clt 11146 ≤ cle 11147 − cmin 11344 / cdiv 11774 ℕcn 12125 2c2 12180 3c3 12181 4c4 12182 6c6 12184 7c7 12185 8c8 12186 9c9 12187 ℕ₀cn0 12381 ℤcz 12468 cdc 12588 ℚcq 12846 ℝ⁺crp 12890 ↑cexp 13968 √csqrt 15140 expce 15968 eceu 15969 logclog 26490 cdp2 32851 .cdp 32868

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cc 10326 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084 ax-addf 11085

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-symdif 4200 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-iin 4942 df-disj 5057 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-ofr 7611 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-oadd 8389 df-omul 8390 df-er 8622 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-fi 9295 df-sup 9326 df-inf 9327 df-oi 9396 df-dju 9794 df-card 9832 df-acn 9835 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-z 12469 df-dec 12589 df-uz 12733 df-q 12847 df-rp 12891 df-xneg 13011 df-xadd 13012 df-xmul 13013 df-ioo 13249 df-ioc 13250 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-shft 14974 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-sum 15594 df-ef 15974 df-e 15975 df-sin 15976 df-cos 15977 df-tan 15978 df-pi 15979 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-submnd 18692 df-mulg 18981 df-cntz 19229 df-cmn 19694 df-psmet 21283 df-xmet 21284 df-met 21285 df-bl 21286 df-mopn 21287 df-fbas 21288 df-fg 21289 df-cnfld 21292 df-top 22809 df-topon 22826 df-topsp 22848 df-bases 22861 df-cld 22934 df-ntr 22935 df-cls 22936 df-nei 23013 df-lp 23051 df-perf 23052 df-cn 23142 df-cnp 23143 df-haus 23230 df-cmp 23302 df-tx 23477 df-hmeo 23670 df-fil 23761 df-fm 23853 df-flim 23854 df-flf 23855 df-xms 24235 df-ms 24236 df-tms 24237 df-cncf 24798 df-ovol 25392 df-vol 25393 df-mbf 25547 df-itg1 25548 df-itg2 25549 df-ibl 25550 df-itg 25551 df-0p 25598 df-limc 25794 df-dv 25795 df-log 26492 df-cxp 26493 df-dp2 32852 df-dp 32869

This theorem is referenced by: tgoldbachgtde 34673

W3C validator