bposlem8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bposlem8		Structured version Visualization version GIF version

Theorem bposlem8 27464

Description: Lemma for bpos 27466. Evaluate 𝐹(64) and show it is less than log2. (Contributed by Mario Carneiro, 14-Mar-2014.)

**Hypotheses**
Ref	Expression
bposlem7.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
bposlem7.2	⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) / 𝑥))

**Assertion**
Ref	Expression
bposlem8	⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))

**Proof of Theorem bposlem8**
Step	Hyp	Ref	Expression
1		6nn0 12529	. . . . 5 ⊢ 6 ∈ ℕ₀
2		4nn 12328	. . . . 5 ⊢ 4 ∈ ℕ
3	1, 2	decnncl 12739	. . . 4 ⊢ ;64 ∈ ℕ
4		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ;64 → (√‘𝑛) = (√‘;64))
5		8cn 12342	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℂ
6	5	sqvali 14221	. . . . . . . . . . . . . . . . 17 ⊢ (8↑2) = (8 · 8)
7		8t8e64 12841	. . . . . . . . . . . . . . . . 17 ⊢ (8 · 8) = ;64
8	6, 7	eqtri 2786	. . . . . . . . . . . . . . . 16 ⊢ (8↑2) = ;64
9	8	fveq2i 6884	. . . . . . . . . . . . . . 15 ⊢ (√‘(8↑2)) = (√‘;64)
10		0re 11214	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
11		8re 12341	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℝ
12		8pos 12360	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 8
13	10, 11, 12	ltleii 11337	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 8
14	11	sqrtsqi 15431	. . . . . . . . . . . . . . . 16 ⊢ (0 ≤ 8 → (√‘(8↑2)) = 8)
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (√‘(8↑2)) = 8
16	9, 15	eqtr3i 2788	. . . . . . . . . . . . . 14 ⊢ (√‘;64) = 8
17	4, 16	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝑛 = ;64 → (√‘𝑛) = 8)
18	17	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19		8nn 12340	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
20		nnrp 13032	. . . . . . . . . . . . 13 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
21		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 8 → (log‘𝑥) = (log‘8))
22		cu2 14241	. . . . . . . . . . . . . . . . . . 19 ⊢ (2↑3) = 8
23	22	fveq2i 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (log‘(2↑3)) = (log‘8)
24		2rp 13025	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ⁺
25		3z 12631	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℤ
26		relogexp 26770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℝ⁺ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
27	24, 25, 26	mp2an 704	. . . . . . . . . . . . . . . . . 18 ⊢ (log‘(2↑3)) = (3 · (log‘2))
28	23, 27	eqtr3i 2788	. . . . . . . . . . . . . . . . 17 ⊢ (log‘8) = (3 · (log‘2))
29	21, 28	eqtrdi 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 8 → 𝑥 = 8)
31	29, 30	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32		3cn 12326	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
33		2nn 12318	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ
34		nnrp 13032	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℕ → 2 ∈ ℝ⁺)
35		relogcl 26749	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ (log‘2) ∈ ℝ
37	36	recni 11227	. . . . . . . . . . . . . . . 16 ⊢ (log‘2) ∈ ℂ
38	19	nnne0i 12280	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
39	32, 37, 5, 38	div23i 11977	. . . . . . . . . . . . . . 15 ⊢ ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
40	31, 39	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41		bposlem7.2	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) / 𝑥))
42		ovex 7443	. . . . . . . . . . . . . 14 ⊢ ((3 / 8) · (log‘2)) ∈ V
43	40, 41, 42	fvmpt 6989	. . . . . . . . . . . . 13 ⊢ (8 ∈ ℝ⁺ → (𝐺‘8) = ((3 / 8) · (log‘2)))
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12 ⊢ (𝐺‘8) = ((3 / 8) · (log‘2))
45	18, 44	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
46	45	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47		sqrt2re 16310	. . . . . . . . . . . . 13 ⊢ (√‘2) ∈ ℝ
48	47	recni 11227	. . . . . . . . . . . 12 ⊢ (√‘2) ∈ ℂ
49	32, 5, 38	divcli 11961	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
50	48, 49, 37	mulassi 11224	. . . . . . . . . . 11 ⊢ (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51		4cn 12330	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℂ
52	48, 51, 48	mul12i 11409	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53		2re 12319	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
54		0le2 12347	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 2
55		remsqsqrt 15312	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
56	53, 54, 55	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) · (√‘2)) = 2
57	56	oveq2i 7421	. . . . . . . . . . . . . . 15 ⊢ (4 · ((√‘2) · (√‘2))) = (4 · 2)
58		4t2e8 12413	. . . . . . . . . . . . . . 15 ⊢ (4 · 2) = 8
59	52, 57, 58	3eqtri 2790	. . . . . . . . . . . . . 14 ⊢ ((√‘2) · (4 · (√‘2))) = 8
60	59	oveq2i 7421	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
61	51, 48	mulcli 11220	. . . . . . . . . . . . . . 15 ⊢ (4 · (√‘2)) ∈ ℂ
62		nnrp 13032	. . . . . . . . . . . . . . . . . 18 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℝ⁺
64		rpsqrtcl 15320	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ⁺ → (√‘2) ∈ ℝ⁺)
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ (√‘2) ∈ ℝ⁺
66		rpmulcl 13045	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℝ⁺ ∧ (√‘2) ∈ ℝ⁺) → (4 · (√‘2)) ∈ ℝ⁺)
67	63, 65, 66	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ (4 · (√‘2)) ∈ ℝ⁺
68		rpne0 13037	. . . . . . . . . . . . . . . 16 ⊢ ((4 · (√‘2)) ∈ ℝ⁺ → (4 · (√‘2)) ≠ 0)
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (4 · (√‘2)) ≠ 0
70		rpne0 13037	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ ℝ⁺ → (√‘2) ≠ 0)
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ≠ 0
72		divcan5 11921	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
73	32, 72	mp3an1 1477	. . . . . . . . . . . . . . 15 ⊢ ((((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
74	61, 69, 48, 71, 73	mp4an 705	. . . . . . . . . . . . . 14 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2)))
75		4ne0 12356	. . . . . . . . . . . . . . 15 ⊢ 4 ≠ 0
76		divdiv1 11930	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
77	32, 76	mp3an1 1477	. . . . . . . . . . . . . . 15 ⊢ (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
78	51, 75, 48, 71, 77	mp4an 705	. . . . . . . . . . . . . 14 ⊢ ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2)))
79	74, 78	eqtr4i 2789	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
80	48, 32, 5, 38	divassi 11975	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
81	60, 79, 80	3eqtr3ri 2795	. . . . . . . . . . . 12 ⊢ ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
82	81	oveq1i 7420	. . . . . . . . . . 11 ⊢ (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
83	50, 82	eqtr3i 2788	. . . . . . . . . 10 ⊢ ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
84	46, 83	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ;64 → (𝑛 / 2) = (;64 / 2))
86		df-6 12311	. . . . . . . . . . . . . . . . . 18 ⊢ 6 = (5 + 1)
87	86	oveq2i 7421	. . . . . . . . . . . . . . . . 17 ⊢ (2↑6) = (2↑(5 + 1))
88		2exp6 17150	. . . . . . . . . . . . . . . . 17 ⊢ (2↑6) = ;64
89		2cn 12320	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
90		5nn0 12528	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ₀
91		expp1 14109	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 5 ∈ ℕ₀) → (2↑(5 + 1)) = ((2↑5) · 2))
92	89, 90, 91	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (2↑(5 + 1)) = ((2↑5) · 2)
93	87, 88, 92	3eqtr3i 2794	. . . . . . . . . . . . . . . 16 ⊢ ;64 = ((2↑5) · 2)
94	93	oveq1i 7420	. . . . . . . . . . . . . . 15 ⊢ (;64 / 2) = (((2↑5) · 2) / 2)
95		nnexpcl 14115	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 5 ∈ ℕ₀) → (2↑5) ∈ ℕ)
96	33, 90, 95	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (2↑5) ∈ ℕ
97	96	nncni 12247	. . . . . . . . . . . . . . . 16 ⊢ (2↑5) ∈ ℂ
98		2ne0 12351	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
99	97, 89, 98	divcan4i 11966	. . . . . . . . . . . . . . 15 ⊢ (((2↑5) · 2) / 2) = (2↑5)
100	94, 99	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ (;64 / 2) = (2↑5)
101	85, 100	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝑛 = ;64 → (𝑛 / 2) = (2↑5))
102	101	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103		nnrp 13032	. . . . . . . . . . . . 13 ⊢ ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ⁺)
104		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105		5nn 12331	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℕ
106	105	nnzi 12622	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℤ
107		relogexp 26770	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ⁺ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
108	24, 106, 107	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (log‘(2↑5)) = (5 · (log‘2))
109	104, 108	eqtrdi 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (2↑5) → 𝑥 = (2↑5))
111	109, 110	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112		5cn 12333	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℂ
113	96	nnne0i 12280	. . . . . . . . . . . . . . . 16 ⊢ (2↑5) ≠ 0
114	112, 37, 97, 113	div23i 11977	. . . . . . . . . . . . . . 15 ⊢ ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115	111, 114	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116		ovex 7443	. . . . . . . . . . . . . 14 ⊢ ((5 / (2↑5)) · (log‘2)) ∈ V
117	115, 41, 116	fvmpt 6989	. . . . . . . . . . . . 13 ⊢ ((2↑5) ∈ ℝ⁺ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
118	96, 103, 117	mp2b 10	. . . . . . . . . . . 12 ⊢ (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
119	102, 118	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120	119	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121		9cn 12345	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
122	121, 51, 75	divcli 11961	. . . . . . . . . . 11 ⊢ (9 / 4) ∈ ℂ
123	112, 97, 113	divcli 11961	. . . . . . . . . . 11 ⊢ (5 / (2↑5)) ∈ ℂ
124	122, 123, 37	mulassi 11224	. . . . . . . . . 10 ⊢ (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125	120, 124	eqtr4di 2816	. . . . . . . . 9 ⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
126	84, 125	oveq12d 7428	. . . . . . . 8 ⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
127	32, 51, 75	divcli 11961	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
128	127, 48, 71	divcli 11961	. . . . . . . . 9 ⊢ ((3 / 4) / (√‘2)) ∈ ℂ
129	122, 123	mulcli 11220	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130	128, 129, 37	adddiri 11226	. . . . . . . 8 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2)))
131	126, 130	eqtr4di 2816	. . . . . . 7 ⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (2 · 𝑛) = (2 · ;64))
133	132	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = (√‘(2 · ;64)))
134	3	nnrei 12246	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℝ
135	3	nngt0i 12279	. . . . . . . . . . . . 13 ⊢ 0 < ;64
136	10, 134, 135	ltleii 11337	. . . . . . . . . . . 12 ⊢ 0 ≤ ;64
137	53, 134, 54, 136	sqrtmulii 15443	. . . . . . . . . . 11 ⊢ (√‘(2 · ;64)) = ((√‘2) · (√‘;64))
138	16	oveq2i 7421	. . . . . . . . . . 11 ⊢ ((√‘2) · (√‘;64)) = ((√‘2) · 8)
139	137, 138	eqtri 2786	. . . . . . . . . 10 ⊢ (√‘(2 · ;64)) = ((√‘2) · 8)
140	133, 139	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141	140	oveq2d 7426	. . . . . . . 8 ⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
142	48, 5	mulcli 11220	. . . . . . . . . 10 ⊢ ((√‘2) · 8) ∈ ℂ
143		rpmulcl 13045	. . . . . . . . . . . 12 ⊢ (((√‘2) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((√‘2) · 8) ∈ ℝ⁺)
144	65, 20, 143	sylancr 598	. . . . . . . . . . 11 ⊢ (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ⁺)
145		rpne0 13037	. . . . . . . . . . 11 ⊢ (((√‘2) · 8) ∈ ℝ⁺ → ((√‘2) · 8) ≠ 0)
146	19, 144, 145	mp2b 10	. . . . . . . . . 10 ⊢ ((√‘2) · 8) ≠ 0
147		divrec2 11893	. . . . . . . . . 10 ⊢ (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
148	37, 142, 146, 147	mp3an 1490	. . . . . . . . 9 ⊢ ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
149	48, 5	mulcomi 11221	. . . . . . . . . . . 12 ⊢ ((√‘2) · 8) = (8 · (√‘2))
150	149	oveq2i 7421	. . . . . . . . . . 11 ⊢ (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151		recdiv2 11932	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2))))
152	5, 38, 48, 71, 151	mp4an 705	. . . . . . . . . . 11 ⊢ ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2)))
153	150, 152	eqtr4i 2789	. . . . . . . . . 10 ⊢ (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154	153	oveq1i 7420	. . . . . . . . 9 ⊢ ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155	148, 154	eqtri 2786	. . . . . . . 8 ⊢ ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156	141, 155	eqtrdi 2814	. . . . . . 7 ⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157	131, 156	oveq12d 7428	. . . . . 6 ⊢ (𝑛 = ;64 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) + (((1 / 8) / (√‘2)) · (log‘2))))
158	128, 129	addcli 11219	. . . . . . 7 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
159	5, 38	reccli 11949	. . . . . . . 8 ⊢ (1 / 8) ∈ ℂ
160	159, 48, 71	divcli 11961	. . . . . . 7 ⊢ ((1 / 8) / (√‘2)) ∈ ℂ
161	158, 160, 37	adddiri 11226	. . . . . 6 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) + (((1 / 8) / (√‘2)) · (log‘2)))
162	157, 161	eqtr4di 2816	. . . . 5 ⊢ (𝑛 = ;64 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)))
163		bposlem7.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
164		ovex 7443	. . . . 5 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165	162, 163, 164	fvmpt 6989	. . . 4 ⊢ (;64 ∈ ℕ → (𝐹‘;64) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)))
166	3, 165	ax-mp 5	. . 3 ⊢ (𝐹‘;64) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2))
167		3re 12325	. . . . . . . 8 ⊢ 3 ∈ ℝ
168		4re 12329	. . . . . . . 8 ⊢ 4 ∈ ℝ
169	167, 168, 75	redivcli 11986	. . . . . . 7 ⊢ (3 / 4) ∈ ℝ
170	169, 47, 71	redivcli 11986	. . . . . 6 ⊢ ((3 / 4) / (√‘2)) ∈ ℝ
171		9re 12344	. . . . . . . 8 ⊢ 9 ∈ ℝ
172	171, 168, 75	redivcli 11986	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
173		5re 12332	. . . . . . . 8 ⊢ 5 ∈ ℝ
174	96	nnrei 12246	. . . . . . . 8 ⊢ (2↑5) ∈ ℝ
175	173, 174, 113	redivcli 11986	. . . . . . 7 ⊢ (5 / (2↑5)) ∈ ℝ
176	172, 175	remulcli 11229	. . . . . 6 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177	170, 176	readdcli 11228	. . . . 5 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
178	11, 38	rereccli 11984	. . . . . 6 ⊢ (1 / 8) ∈ ℝ
179	178, 47, 71	redivcli 11986	. . . . 5 ⊢ ((1 / 8) / (√‘2)) ∈ ℝ
180	177, 179	readdcli 11228	. . . 4 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181	180, 36	remulcli 11229	. . 3 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182	166, 181	eqeltri 2859	. 2 ⊢ (𝐹‘;64) ∈ ℝ
183	128, 129, 160	add32i 11438	. . . . . 6 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5))))
184		6cn 12336	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
185		ax-1cn 11162	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
186	184, 185, 5, 38	divdiri 11976	. . . . . . . . . 10 ⊢ ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187		df-7 12312	. . . . . . . . . . 11 ⊢ 7 = (6 + 1)
188	187	oveq1i 7420	. . . . . . . . . 10 ⊢ (7 / 8) = ((6 + 1) / 8)
189		divcan5 11921	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
190	32, 189	mp3an1 1477	. . . . . . . . . . . . 13 ⊢ (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
191	51, 75, 89, 98, 190	mp4an 705	. . . . . . . . . . . 12 ⊢ ((2 · 3) / (2 · 4)) = (3 / 4)
192		2t3e6 12411	. . . . . . . . . . . . 13 ⊢ (2 · 3) = 6
193		2t4e8 12414	. . . . . . . . . . . . 13 ⊢ (2 · 4) = 8
194	192, 193	oveq12i 7422	. . . . . . . . . . . 12 ⊢ ((2 · 3) / (2 · 4)) = (6 / 8)
195	191, 194	eqtr3i 2788	. . . . . . . . . . 11 ⊢ (3 / 4) = (6 / 8)
196	195	oveq1i 7420	. . . . . . . . . 10 ⊢ ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
197	186, 188, 196	3eqtr4ri 2797	. . . . . . . . 9 ⊢ ((3 / 4) + (1 / 8)) = (7 / 8)
198	197	oveq1i 7420	. . . . . . . 8 ⊢ (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
199	127, 159, 48, 71	divdiri 11976	. . . . . . . 8 ⊢ (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
200		7cn 12339	. . . . . . . . 9 ⊢ 7 ∈ ℂ
201	200, 5, 48, 38, 71	divdiv32i 11974	. . . . . . . 8 ⊢ ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
202	198, 199, 201	3eqtr3i 2794	. . . . . . 7 ⊢ (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
203	202	oveq1i 7420	. . . . . 6 ⊢ ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
204	183, 203	eqtri 2786	. . . . 5 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205		4nn0 12527	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
206		9nn0 12532	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
207		0nn0 12523	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
208		9lt10 12852	. . . . . . . . . . . 12 ⊢ 9 < ;10
209		4lt5 12424	. . . . . . . . . . . 12 ⊢ 4 < 5
210	205, 90, 206, 207, 208, 209	decltc 12749	. . . . . . . . . . 11 ⊢ ;49 < ;50
211		7t7e49 12834	. . . . . . . . . . 11 ⊢ (7 · 7) = ;49
212	56	oveq1i 7420	. . . . . . . . . . . 12 ⊢ (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
213	48, 48, 112, 112	mul4i 11411	. . . . . . . . . . . 12 ⊢ (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
214		5t2e10 12820	. . . . . . . . . . . . . . 15 ⊢ (5 · 2) = ;10
215	112, 89, 214	mulcomli 11222	. . . . . . . . . . . . . 14 ⊢ (2 · 5) = ;10
216	215	oveq1i 7420	. . . . . . . . . . . . 13 ⊢ ((2 · 5) · 5) = (;10 · 5)
217	89, 112, 112	mulassi 11224	. . . . . . . . . . . . 13 ⊢ ((2 · 5) · 5) = (2 · (5 · 5))
218	90	dec0u 12741	. . . . . . . . . . . . 13 ⊢ (;10 · 5) = ;50
219	216, 217, 218	3eqtr3i 2794	. . . . . . . . . . . 12 ⊢ (2 · (5 · 5)) = ;50
220	212, 213, 219	3eqtr3i 2794	. . . . . . . . . . 11 ⊢ (((√‘2) · 5) · ((√‘2) · 5)) = ;50
221	210, 211, 220	3brtr4i 5141	. . . . . . . . . 10 ⊢ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
222		7re 12338	. . . . . . . . . . . 12 ⊢ 7 ∈ ℝ
223		7pos 12359	. . . . . . . . . . . 12 ⊢ 0 < 7
224	10, 222, 223	ltleii 11337	. . . . . . . . . . 11 ⊢ 0 ≤ 7
225		nnrp 13032	. . . . . . . . . . . . . 14 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
226	105, 225	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℝ⁺
227		rpmulcl 13045	. . . . . . . . . . . . 13 ⊢ (((√‘2) ∈ ℝ⁺ ∧ 5 ∈ ℝ⁺) → ((√‘2) · 5) ∈ ℝ⁺)
228	65, 226, 227	mp2an 704	. . . . . . . . . . . 12 ⊢ ((√‘2) · 5) ∈ ℝ⁺
229		rpge0 13034	. . . . . . . . . . . 12 ⊢ (((√‘2) · 5) ∈ ℝ⁺ → 0 ≤ ((√‘2) · 5))
230	228, 229	ax-mp 5	. . . . . . . . . . 11 ⊢ 0 ≤ ((√‘2) · 5)
231		rpre 13029	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 5) ∈ ℝ⁺ → ((√‘2) · 5) ∈ ℝ)
232	228, 231	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((√‘2) · 5) ∈ ℝ
233	222, 232	lt2msqi 12131	. . . . . . . . . . 11 ⊢ ((0 ≤ 7 ∧ 0 ≤ ((√‘2) · 5)) → (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))))
234	224, 230, 233	mp2an 704	. . . . . . . . . 10 ⊢ (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5)))
235	221, 234	mpbir 234	. . . . . . . . 9 ⊢ 7 < ((√‘2) · 5)
236		rpgt0 13033	. . . . . . . . . . 11 ⊢ ((√‘2) ∈ ℝ⁺ → 0 < (√‘2))
237	24, 64, 236	mp2b 10	. . . . . . . . . 10 ⊢ 0 < (√‘2)
238		ltdivmul 12094	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
239	222, 173, 238	mp3an12 1480	. . . . . . . . . 10 ⊢ (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240	47, 237, 239	mp2an 704	. . . . . . . . 9 ⊢ ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
241	235, 240	mpbir 234	. . . . . . . 8 ⊢ (7 / (√‘2)) < 5
242	222, 47, 71	redivcli 11986	. . . . . . . . 9 ⊢ (7 / (√‘2)) ∈ ℝ
243	242, 173, 11, 12	ltdiv1ii 12148	. . . . . . . 8 ⊢ ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
244	241, 243	mpbi 233	. . . . . . 7 ⊢ ((7 / (√‘2)) / 8) < (5 / 8)
245		divsubdir 11912	. . . . . . . . . . 11 ⊢ ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
246	5, 32, 245	mp3an12 1480	. . . . . . . . . 10 ⊢ ((8 ∈ ℂ ∧ 8 ≠ 0) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
247	5, 38, 246	mp2an 704	. . . . . . . . 9 ⊢ ((8 − 3) / 8) = ((8 / 8) − (3 / 8))
248		5p3e8 12401	. . . . . . . . . . . 12 ⊢ (5 + 3) = 8
249	248	oveq1i 7420	. . . . . . . . . . 11 ⊢ ((5 + 3) − 3) = (8 − 3)
250	112, 32	pncan3oi 11477	. . . . . . . . . . 11 ⊢ ((5 + 3) − 3) = 5
251	249, 250	eqtr3i 2788	. . . . . . . . . 10 ⊢ (8 − 3) = 5
252	251	oveq1i 7420	. . . . . . . . 9 ⊢ ((8 − 3) / 8) = (5 / 8)
253	5, 38	dividi 11952	. . . . . . . . . 10 ⊢ (8 / 8) = 1
254	253	oveq1i 7420	. . . . . . . . 9 ⊢ ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
255	247, 252, 254	3eqtr3ri 2795	. . . . . . . 8 ⊢ (1 − (3 / 8)) = (5 / 8)
256		5lt8 12441	. . . . . . . . . . . . 13 ⊢ 5 < 8
257	11, 173	remulcli 11229	. . . . . . . . . . . . . 14 ⊢ (8 · 5) ∈ ℝ
258	173, 11, 257	ltadd2i 11345	. . . . . . . . . . . . 13 ⊢ (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
259	256, 258	mpbi 233	. . . . . . . . . . . 12 ⊢ ((8 · 5) + 5) < ((8 · 5) + 8)
260		df-9 12314	. . . . . . . . . . . . . 14 ⊢ 9 = (8 + 1)
261	260	oveq1i 7420	. . . . . . . . . . . . 13 ⊢ (9 · 5) = ((8 + 1) · 5)
262	5, 185, 112	adddiri 11226	. . . . . . . . . . . . 13 ⊢ ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
263	112	mullidi 11218	. . . . . . . . . . . . . 14 ⊢ (1 · 5) = 5
264	263	oveq2i 7421	. . . . . . . . . . . . 13 ⊢ ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
265	261, 262, 264	3eqtri 2790	. . . . . . . . . . . 12 ⊢ (9 · 5) = ((8 · 5) + 5)
266	86	oveq2i 7421	. . . . . . . . . . . . 13 ⊢ (8 · 6) = (8 · (5 + 1))
267	5, 112, 185	adddii 11225	. . . . . . . . . . . . 13 ⊢ (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
268	5	mulridi 11217	. . . . . . . . . . . . . 14 ⊢ (8 · 1) = 8
269	268	oveq2i 7421	. . . . . . . . . . . . 13 ⊢ ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
270	266, 267, 269	3eqtri 2790	. . . . . . . . . . . 12 ⊢ (8 · 6) = ((8 · 5) + 8)
271	259, 265, 270	3brtr4i 5141	. . . . . . . . . . 11 ⊢ (9 · 5) < (8 · 6)
272	171, 173	remulcli 11229	. . . . . . . . . . . 12 ⊢ (9 · 5) ∈ ℝ
273		6re 12335	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℝ
274	11, 273	remulcli 11229	. . . . . . . . . . . 12 ⊢ (8 · 6) ∈ ℝ
275	168, 174	remulcli 11229	. . . . . . . . . . . 12 ⊢ (4 · (2↑5)) ∈ ℝ
276	2, 96	nnmulcli 12262	. . . . . . . . . . . . 13 ⊢ (4 · (2↑5)) ∈ ℕ
277	276	nngt0i 12279	. . . . . . . . . . . 12 ⊢ 0 < (4 · (2↑5))
278	272, 274, 275, 277	ltdiv1ii 12148	. . . . . . . . . . 11 ⊢ ((9 · 5) < (8 · 6) ↔ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5))))
279	271, 278	mpbi 233	. . . . . . . . . 10 ⊢ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5)))
280	121, 51, 112, 97, 75, 113	divmuldivi 11979	. . . . . . . . . 10 ⊢ ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
281		nnexpcl 14115	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 4 ∈ ℕ₀) → (2↑4) ∈ ℕ)
282	33, 205, 281	mp2an 704	. . . . . . . . . . . . 13 ⊢ (2↑4) ∈ ℕ
283	282	nncni 12247	. . . . . . . . . . . 12 ⊢ (2↑4) ∈ ℂ
284	282	nnne0i 12280	. . . . . . . . . . . 12 ⊢ (2↑4) ≠ 0
285		divcan5 11921	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
286	32, 285	mp3an1 1477	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
287	5, 38, 283, 284, 286	mp4an 705	. . . . . . . . . . 11 ⊢ (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8)
288		df-4 12309	. . . . . . . . . . . . . . . 16 ⊢ 4 = (3 + 1)
289	288	oveq2i 7421	. . . . . . . . . . . . . . 15 ⊢ (2↑4) = (2↑(3 + 1))
290		3nn0 12526	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ₀
291		expp1 14109	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ₀) → (2↑(3 + 1)) = ((2↑3) · 2))
292	89, 290, 291	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (2↑(3 + 1)) = ((2↑3) · 2)
293	22	oveq1i 7420	. . . . . . . . . . . . . . 15 ⊢ ((2↑3) · 2) = (8 · 2)
294	289, 292, 293	3eqtri 2790	. . . . . . . . . . . . . 14 ⊢ (2↑4) = (8 · 2)
295	294	oveq1i 7420	. . . . . . . . . . . . 13 ⊢ ((2↑4) · 3) = ((8 · 2) · 3)
296	5, 89, 32	mulassi 11224	. . . . . . . . . . . . 13 ⊢ ((8 · 2) · 3) = (8 · (2 · 3))
297	192	oveq2i 7421	. . . . . . . . . . . . 13 ⊢ (8 · (2 · 3)) = (8 · 6)
298	295, 296, 297	3eqtri 2790	. . . . . . . . . . . 12 ⊢ ((2↑4) · 3) = (8 · 6)
299		4p3e7 12398	. . . . . . . . . . . . . . . 16 ⊢ (4 + 3) = 7
300		5p2e7 12400	. . . . . . . . . . . . . . . 16 ⊢ (5 + 2) = 7
301	112, 89	addcomi 11405	. . . . . . . . . . . . . . . 16 ⊢ (5 + 2) = (2 + 5)
302	299, 300, 301	3eqtr2i 2792	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = (2 + 5)
303	302	oveq2i 7421	. . . . . . . . . . . . . 14 ⊢ (2↑(4 + 3)) = (2↑(2 + 5))
304		expadd 14145	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
305	89, 205, 290, 304	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ (2↑(4 + 3)) = ((2↑4) · (2↑3))
306		2nn0 12525	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ₀
307		expadd 14145	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
308	89, 306, 90, 307	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ (2↑(2 + 5)) = ((2↑2) · (2↑5))
309	303, 305, 308	3eqtr3i 2794	. . . . . . . . . . . . 13 ⊢ ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
310	22	oveq2i 7421	. . . . . . . . . . . . 13 ⊢ ((2↑4) · (2↑3)) = ((2↑4) · 8)
311		sq2 14238	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
312	311	oveq1i 7420	. . . . . . . . . . . . 13 ⊢ ((2↑2) · (2↑5)) = (4 · (2↑5))
313	309, 310, 312	3eqtr3i 2794	. . . . . . . . . . . 12 ⊢ ((2↑4) · 8) = (4 · (2↑5))
314	298, 313	oveq12i 7422	. . . . . . . . . . 11 ⊢ (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
315	287, 314	eqtr3i 2788	. . . . . . . . . 10 ⊢ (3 / 8) = ((8 · 6) / (4 · (2↑5)))
316	279, 280, 315	3brtr4i 5141	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) < (3 / 8)
317	167, 11, 38	redivcli 11986	. . . . . . . . . 10 ⊢ (3 / 8) ∈ ℝ
318		1re 11212	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
319		ltsub2 11715	. . . . . . . . . 10 ⊢ ((((9 / 4) · (5 / (2↑5))) ∈ ℝ ∧ (3 / 8) ∈ ℝ ∧ 1 ∈ ℝ) → (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))))
320	176, 317, 318, 319	mp3an 1490	. . . . . . . . 9 ⊢ (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5)))))
321	316, 320	mpbi 233	. . . . . . . 8 ⊢ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))
322	255, 321	eqbrtrri 5134	. . . . . . 7 ⊢ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
323	242, 11, 38	redivcli 11986	. . . . . . . 8 ⊢ ((7 / (√‘2)) / 8) ∈ ℝ
324	173, 11, 38	redivcli 11986	. . . . . . . 8 ⊢ (5 / 8) ∈ ℝ
325	318, 176	resubcli 11524	. . . . . . . 8 ⊢ (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
326	323, 324, 325	lttri 11340	. . . . . . 7 ⊢ ((((7 / (√‘2)) / 8) < (5 / 8) ∧ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))) → ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
327	244, 322, 326	mp2an 704	. . . . . 6 ⊢ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
328	323, 176, 318	ltaddsubi 11779	. . . . . 6 ⊢ ((((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
329	327, 328	mpbir 234	. . . . 5 ⊢ (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1
330	204, 329	eqbrtri 5132	. . . 4 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
331		1lt2 12417	. . . . . . 7 ⊢ 1 < 2
332		rplogcl 26778	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ⁺)
333	53, 331, 332	mp2an 704	. . . . . 6 ⊢ (log‘2) ∈ ℝ⁺
334		rpgt0 13033	. . . . . 6 ⊢ ((log‘2) ∈ ℝ⁺ → 0 < (log‘2))
335	333, 334	ax-mp 5	. . . . 5 ⊢ 0 < (log‘2)
336	180, 318, 36, 335	ltmul1ii 12147	. . . 4 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1 ↔ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2)))
337	330, 336	mpbi 233	. . 3 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2))
338	37	mullidi 11218	. . . 4 ⊢ (1 · (log‘2)) = (log‘2)
339	338	eqcomi 2772	. . 3 ⊢ (log‘2) = (1 · (log‘2))
340	337, 166, 339	3brtr4i 5141	. 2 ⊢ (𝐹‘;64) < (log‘2)
341	182, 340	pm3.2i 475	1 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 class class class wbr 5109 ↦ cmpt 5192 ‘cfv 6536 (class class class)co 7410 ℂcc 11102 ℝcr 11103 0cc0 11104 1c1 11105 + caddc 11107 · cmul 11109 < clt 11247 ≤ cle 11248 − cmin 11445 / cdiv 11875 ℕcn 12237 2c2 12299 3c3 12300 4c4 12301 5c5 12302 6c6 12303 7c7 12304 8c8 12305 9c9 12306 ℕ₀cn0 12508 ℤcz 12595 cdc 12715 ℝ⁺crp 13020 ↑cexp 14102 √csqrt 15289 logclog 26728

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181 ax-pre-sup 11182 ax-addf 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-er 8690 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-fi 9367 df-sup 9398 df-inf 9399 df-oi 9468 df-card 9930 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-div 11876 df-nn 12238 df-2 12307 df-3 12308 df-4 12309 df-5 12310 df-6 12311 df-7 12312 df-8 12313 df-9 12314 df-n0 12509 df-z 12596 df-dec 12716 df-uz 12867 df-q 12977 df-rp 13021 df-xneg 13141 df-xadd 13142 df-xmul 13143 df-ioo 13380 df-ioc 13381 df-ico 13382 df-icc 13383 df-fz 13540 df-fzo 13688 df-fl 13830 df-mod 13908 df-seq 14043 df-exp 14103 df-fac 14315 df-bc 14344 df-hash 14372 df-shft 15109 df-cj 15155 df-re 15156 df-im 15157 df-sqrt 15291 df-abs 15292 df-limsup 15527 df-clim 15544 df-rlim 15545 df-sum 15743 df-ef 16125 df-sin 16127 df-cos 16128 df-pi 16130 df-struct 17211 df-sets 17228 df-slot 17246 df-ndx 17258 df-base 17274 df-ress 17295 df-plusg 17327 df-mulr 17328 df-starv 17329 df-sca 17330 df-vsca 17331 df-ip 17332 df-tset 17333 df-ple 17334 df-ds 17336 df-unif 17337 df-hom 17338 df-cco 17339 df-rest 17479 df-topn 17480 df-0g 17498 df-gsum 17499 df-topgen 17500 df-pt 17501 df-prds 17504 df-xrs 17560 df-qtop 17565 df-imas 17566 df-xps 17568 df-mre 17642 df-mrc 17643 df-acs 17645 df-mgm 18702 df-sgrp 18781 df-mnd 18797 df-submnd 18846 df-mulg 19138 df-cntz 19391 df-cmn 19856 df-psmet 21523 df-xmet 21524 df-met 21525 df-bl 21526 df-mopn 21527 df-fbas 21528 df-fg 21529 df-cnfld 21532 df-top 23060 df-topon 23077 df-topsp 23099 df-bases 23112 df-cld 23185 df-ntr 23186 df-cls 23187 df-nei 23264 df-lp 23302 df-perf 23303 df-cn 23393 df-cnp 23394 df-haus 23481 df-tx 23728 df-hmeo 23921 df-fil 24012 df-fm 24104 df-flim 24105 df-flf 24106 df-xms 24486 df-ms 24487 df-tms 24488 df-cncf 25046 df-limc 26034 df-dv 26035 df-log 26730

This theorem is used by: bposlem9 27465

W3C validator