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 25869

Description: Lemma for bpos 25871. 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 11921	. . . . 5 ⊢ 6 ∈ ℕ₀
2		4nn 11723	. . . . 5 ⊢ 4 ∈ ℕ
3	1, 2	decnncl 12121	. . . 4 ⊢ ;64 ∈ ℕ
4		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ;64 → (√‘𝑛) = (√‘;64))
5		8cn 11737	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℂ
6	5	sqvali 13546	. . . . . . . . . . . . . . . . 17 ⊢ (8↑2) = (8 · 8)
7		8t8e64 12222	. . . . . . . . . . . . . . . . 17 ⊢ (8 · 8) = ;64
8	6, 7	eqtri 2846	. . . . . . . . . . . . . . . 16 ⊢ (8↑2) = ;64
9	8	fveq2i 6675	. . . . . . . . . . . . . . 15 ⊢ (√‘(8↑2)) = (√‘;64)
10		0re 10645	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
11		8re 11736	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℝ
12		8pos 11752	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 8
13	10, 11, 12	ltleii 10765	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 8
14	11	sqrtsqi 14736	. . . . . . . . . . . . . . . 16 ⊢ (0 ≤ 8 → (√‘(8↑2)) = 8)
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (√‘(8↑2)) = 8
16	9, 15	eqtr3i 2848	. . . . . . . . . . . . . 14 ⊢ (√‘;64) = 8
17	4, 16	syl6eq 2874	. . . . . . . . . . . . 13 ⊢ (𝑛 = ;64 → (√‘𝑛) = 8)
18	17	fveq2d 6676	. . . . . . . . . . . 12 ⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19		8nn 11735	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
20		nnrp 12403	. . . . . . . . . . . . 13 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
21		fveq2 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 8 → (log‘𝑥) = (log‘8))
22		cu2 13566	. . . . . . . . . . . . . . . . . . 19 ⊢ (2↑3) = 8
23	22	fveq2i 6675	. . . . . . . . . . . . . . . . . 18 ⊢ (log‘(2↑3)) = (log‘8)
24		2rp 12397	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ⁺
25		3z 12018	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℤ
26		relogexp 25181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℝ⁺ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
27	24, 25, 26	mp2an 690	. . . . . . . . . . . . . . . . . 18 ⊢ (log‘(2↑3)) = (3 · (log‘2))
28	23, 27	eqtr3i 2848	. . . . . . . . . . . . . . . . 17 ⊢ (log‘8) = (3 · (log‘2))
29	21, 28	syl6eq 2874	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 8 → 𝑥 = 8)
31	29, 30	oveq12d 7176	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32		3cn 11721	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
33		2nn 11713	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ
34		nnrp 12403	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℕ → 2 ∈ ℝ⁺)
35		relogcl 25161	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
36	33, 34, 35	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ (log‘2) ∈ ℝ
37	36	recni 10657	. . . . . . . . . . . . . . . 16 ⊢ (log‘2) ∈ ℂ
38	19	nnne0i 11680	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
39	32, 37, 5, 38	div23i 11400	. . . . . . . . . . . . . . 15 ⊢ ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
40	31, 39	syl6eq 2874	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41		bposlem7.2	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) / 𝑥))
42		ovex 7191	. . . . . . . . . . . . . 14 ⊢ ((3 / 8) · (log‘2)) ∈ V
43	40, 41, 42	fvmpt 6770	. . . . . . . . . . . . 13 ⊢ (8 ∈ ℝ⁺ → (𝐺‘8) = ((3 / 8) · (log‘2)))
44	19, 20, 43	mp2b 10	. . . . . . . . . . . 12 ⊢ (𝐺‘8) = ((3 / 8) · (log‘2))
45	18, 44	syl6eq 2874	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
46	45	oveq2d 7174	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47		sqrt2re 15605	. . . . . . . . . . . . 13 ⊢ (√‘2) ∈ ℝ
48	47	recni 10657	. . . . . . . . . . . 12 ⊢ (√‘2) ∈ ℂ
49	32, 5, 38	divcli 11384	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
50	48, 49, 37	mulassi 10654	. . . . . . . . . . 11 ⊢ (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51		4cn 11725	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℂ
52	48, 51, 48	mul12i 10837	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53		2re 11714	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
54		0le2 11742	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 2
55		remsqsqrt 14618	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
56	53, 54, 55	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) · (√‘2)) = 2
57	56	oveq2i 7169	. . . . . . . . . . . . . . 15 ⊢ (4 · ((√‘2) · (√‘2))) = (4 · 2)
58		4t2e8 11808	. . . . . . . . . . . . . . 15 ⊢ (4 · 2) = 8
59	52, 57, 58	3eqtri 2850	. . . . . . . . . . . . . 14 ⊢ ((√‘2) · (4 · (√‘2))) = 8
60	59	oveq2i 7169	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
61	51, 48	mulcli 10650	. . . . . . . . . . . . . . 15 ⊢ (4 · (√‘2)) ∈ ℂ
62		nnrp 12403	. . . . . . . . . . . . . . . . . 18 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
63	2, 62	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℝ⁺
64		rpsqrtcl 14626	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ⁺ → (√‘2) ∈ ℝ⁺)
65	33, 34, 64	mp2b 10	. . . . . . . . . . . . . . . . 17 ⊢ (√‘2) ∈ ℝ⁺
66		rpmulcl 12415	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℝ⁺ ∧ (√‘2) ∈ ℝ⁺) → (4 · (√‘2)) ∈ ℝ⁺)
67	63, 65, 66	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ (4 · (√‘2)) ∈ ℝ⁺
68		rpne0 12408	. . . . . . . . . . . . . . . 16 ⊢ ((4 · (√‘2)) ∈ ℝ⁺ → (4 · (√‘2)) ≠ 0)
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (4 · (√‘2)) ≠ 0
70		rpne0 12408	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ ℝ⁺ → (√‘2) ≠ 0)
71	24, 64, 70	mp2b 10	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ≠ 0
72		divcan5 11344	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
73	32, 72	mp3an1 1444	. . . . . . . . . . . . . . 15 ⊢ ((((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
74	61, 69, 48, 71, 73	mp4an 691	. . . . . . . . . . . . . 14 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2)))
75		4ne0 11748	. . . . . . . . . . . . . . 15 ⊢ 4 ≠ 0
76		divdiv1 11353	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
77	32, 76	mp3an1 1444	. . . . . . . . . . . . . . 15 ⊢ (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
78	51, 75, 48, 71, 77	mp4an 691	. . . . . . . . . . . . . 14 ⊢ ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2)))
79	74, 78	eqtr4i 2849	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
80	48, 32, 5, 38	divassi 11398	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
81	60, 79, 80	3eqtr3ri 2855	. . . . . . . . . . . 12 ⊢ ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
82	81	oveq1i 7168	. . . . . . . . . . 11 ⊢ (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
83	50, 82	eqtr3i 2848	. . . . . . . . . 10 ⊢ ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
84	46, 83	syl6eq 2874	. . . . . . . . 9 ⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85		oveq1 7165	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ;64 → (𝑛 / 2) = (;64 / 2))
86		df-6 11707	. . . . . . . . . . . . . . . . . 18 ⊢ 6 = (5 + 1)
87	86	oveq2i 7169	. . . . . . . . . . . . . . . . 17 ⊢ (2↑6) = (2↑(5 + 1))
88		2exp6 16424	. . . . . . . . . . . . . . . . 17 ⊢ (2↑6) = ;64
89		2cn 11715	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
90		5nn0 11920	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ₀
91		expp1 13439	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 5 ∈ ℕ₀) → (2↑(5 + 1)) = ((2↑5) · 2))
92	89, 90, 91	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (2↑(5 + 1)) = ((2↑5) · 2)
93	87, 88, 92	3eqtr3i 2854	. . . . . . . . . . . . . . . 16 ⊢ ;64 = ((2↑5) · 2)
94	93	oveq1i 7168	. . . . . . . . . . . . . . 15 ⊢ (;64 / 2) = (((2↑5) · 2) / 2)
95		nnexpcl 13445	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 5 ∈ ℕ₀) → (2↑5) ∈ ℕ)
96	33, 90, 95	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (2↑5) ∈ ℕ
97	96	nncni 11650	. . . . . . . . . . . . . . . 16 ⊢ (2↑5) ∈ ℂ
98		2ne0 11744	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
99	97, 89, 98	divcan4i 11389	. . . . . . . . . . . . . . 15 ⊢ (((2↑5) · 2) / 2) = (2↑5)
100	94, 99	eqtri 2846	. . . . . . . . . . . . . 14 ⊢ (;64 / 2) = (2↑5)
101	85, 100	syl6eq 2874	. . . . . . . . . . . . 13 ⊢ (𝑛 = ;64 → (𝑛 / 2) = (2↑5))
102	101	fveq2d 6676	. . . . . . . . . . . 12 ⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103		nnrp 12403	. . . . . . . . . . . . 13 ⊢ ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ⁺)
104		fveq2 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105		5nn 11726	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℕ
106	105	nnzi 12009	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℤ
107		relogexp 25181	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ⁺ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
108	24, 106, 107	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (log‘(2↑5)) = (5 · (log‘2))
109	104, 108	syl6eq 2874	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (2↑5) → 𝑥 = (2↑5))
111	109, 110	oveq12d 7176	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112		5cn 11728	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℂ
113	96	nnne0i 11680	. . . . . . . . . . . . . . . 16 ⊢ (2↑5) ≠ 0
114	112, 37, 97, 113	div23i 11400	. . . . . . . . . . . . . . 15 ⊢ ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115	111, 114	syl6eq 2874	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116		ovex 7191	. . . . . . . . . . . . . 14 ⊢ ((5 / (2↑5)) · (log‘2)) ∈ V
117	115, 41, 116	fvmpt 6770	. . . . . . . . . . . . 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	syl6eq 2874	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120	119	oveq2d 7174	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121		9cn 11740	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
122	121, 51, 75	divcli 11384	. . . . . . . . . . 11 ⊢ (9 / 4) ∈ ℂ
123	112, 97, 113	divcli 11384	. . . . . . . . . . 11 ⊢ (5 / (2↑5)) ∈ ℂ
124	122, 123, 37	mulassi 10654	. . . . . . . . . 10 ⊢ (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125	120, 124	syl6eqr 2876	. . . . . . . . 9 ⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
126	84, 125	oveq12d 7176	. . . . . . . 8 ⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
127	32, 51, 75	divcli 11384	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
128	127, 48, 71	divcli 11384	. . . . . . . . 9 ⊢ ((3 / 4) / (√‘2)) ∈ ℂ
129	122, 123	mulcli 10650	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130	128, 129, 37	adddiri 10656	. . . . . . . 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	syl6eqr 2876	. . . . . . 7 ⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132		oveq2 7166	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (2 · 𝑛) = (2 · ;64))
133	132	fveq2d 6676	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = (√‘(2 · ;64)))
134	3	nnrei 11649	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℝ
135	3	nngt0i 11679	. . . . . . . . . . . . 13 ⊢ 0 < ;64
136	10, 134, 135	ltleii 10765	. . . . . . . . . . . 12 ⊢ 0 ≤ ;64
137	53, 134, 54, 136	sqrtmulii 14748	. . . . . . . . . . 11 ⊢ (√‘(2 · ;64)) = ((√‘2) · (√‘;64))
138	16	oveq2i 7169	. . . . . . . . . . 11 ⊢ ((√‘2) · (√‘;64)) = ((√‘2) · 8)
139	137, 138	eqtri 2846	. . . . . . . . . 10 ⊢ (√‘(2 · ;64)) = ((√‘2) · 8)
140	133, 139	syl6eq 2874	. . . . . . . . 9 ⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141	140	oveq2d 7174	. . . . . . . 8 ⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
142	48, 5	mulcli 10650	. . . . . . . . . 10 ⊢ ((√‘2) · 8) ∈ ℂ
143		rpmulcl 12415	. . . . . . . . . . . 12 ⊢ (((√‘2) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((√‘2) · 8) ∈ ℝ⁺)
144	65, 20, 143	sylancr 589	. . . . . . . . . . 11 ⊢ (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ⁺)
145		rpne0 12408	. . . . . . . . . . 11 ⊢ (((√‘2) · 8) ∈ ℝ⁺ → ((√‘2) · 8) ≠ 0)
146	19, 144, 145	mp2b 10	. . . . . . . . . 10 ⊢ ((√‘2) · 8) ≠ 0
147		divrec2 11317	. . . . . . . . . 10 ⊢ (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
148	37, 142, 146, 147	mp3an 1457	. . . . . . . . 9 ⊢ ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
149	48, 5	mulcomi 10651	. . . . . . . . . . . 12 ⊢ ((√‘2) · 8) = (8 · (√‘2))
150	149	oveq2i 7169	. . . . . . . . . . 11 ⊢ (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151		recdiv2 11355	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2))))
152	5, 38, 48, 71, 151	mp4an 691	. . . . . . . . . . 11 ⊢ ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2)))
153	150, 152	eqtr4i 2849	. . . . . . . . . 10 ⊢ (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154	153	oveq1i 7168	. . . . . . . . 9 ⊢ ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155	148, 154	eqtri 2846	. . . . . . . 8 ⊢ ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156	141, 155	syl6eq 2874	. . . . . . 7 ⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157	131, 156	oveq12d 7176	. . . . . 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 10649	. . . . . . 7 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
159	5, 38	reccli 11372	. . . . . . . 8 ⊢ (1 / 8) ∈ ℂ
160	159, 48, 71	divcli 11384	. . . . . . 7 ⊢ ((1 / 8) / (√‘2)) ∈ ℂ
161	158, 160, 37	adddiri 10656	. . . . . 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	syl6eqr 2876	. . . . 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 7191	. . . . 5 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165	162, 163, 164	fvmpt 6770	. . . 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 11720	. . . . . . . 8 ⊢ 3 ∈ ℝ
168		4re 11724	. . . . . . . 8 ⊢ 4 ∈ ℝ
169	167, 168, 75	redivcli 11409	. . . . . . 7 ⊢ (3 / 4) ∈ ℝ
170	169, 47, 71	redivcli 11409	. . . . . 6 ⊢ ((3 / 4) / (√‘2)) ∈ ℝ
171		9re 11739	. . . . . . . 8 ⊢ 9 ∈ ℝ
172	171, 168, 75	redivcli 11409	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
173		5re 11727	. . . . . . . 8 ⊢ 5 ∈ ℝ
174	96	nnrei 11649	. . . . . . . 8 ⊢ (2↑5) ∈ ℝ
175	173, 174, 113	redivcli 11409	. . . . . . 7 ⊢ (5 / (2↑5)) ∈ ℝ
176	172, 175	remulcli 10659	. . . . . 6 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177	170, 176	readdcli 10658	. . . . 5 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
178	11, 38	rereccli 11407	. . . . . 6 ⊢ (1 / 8) ∈ ℝ
179	178, 47, 71	redivcli 11409	. . . . 5 ⊢ ((1 / 8) / (√‘2)) ∈ ℝ
180	177, 179	readdcli 10658	. . . 4 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181	180, 36	remulcli 10659	. . 3 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182	166, 181	eqeltri 2911	. 2 ⊢ (𝐹‘;64) ∈ ℝ
183	128, 129, 160	add32i 10865	. . . . . 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 11731	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
185		ax-1cn 10597	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
186	184, 185, 5, 38	divdiri 11399	. . . . . . . . . 10 ⊢ ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187		df-7 11708	. . . . . . . . . . 11 ⊢ 7 = (6 + 1)
188	187	oveq1i 7168	. . . . . . . . . 10 ⊢ (7 / 8) = ((6 + 1) / 8)
189		divcan5 11344	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
190	32, 189	mp3an1 1444	. . . . . . . . . . . . 13 ⊢ (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
191	51, 75, 89, 98, 190	mp4an 691	. . . . . . . . . . . 12 ⊢ ((2 · 3) / (2 · 4)) = (3 / 4)
192		3t2e6 11806	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = 6
193	32, 89, 192	mulcomli 10652	. . . . . . . . . . . . 13 ⊢ (2 · 3) = 6
194	51, 89, 58	mulcomli 10652	. . . . . . . . . . . . 13 ⊢ (2 · 4) = 8
195	193, 194	oveq12i 7170	. . . . . . . . . . . 12 ⊢ ((2 · 3) / (2 · 4)) = (6 / 8)
196	191, 195	eqtr3i 2848	. . . . . . . . . . 11 ⊢ (3 / 4) = (6 / 8)
197	196	oveq1i 7168	. . . . . . . . . 10 ⊢ ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
198	186, 188, 197	3eqtr4ri 2857	. . . . . . . . 9 ⊢ ((3 / 4) + (1 / 8)) = (7 / 8)
199	198	oveq1i 7168	. . . . . . . 8 ⊢ (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
200	127, 159, 48, 71	divdiri 11399	. . . . . . . 8 ⊢ (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
201		7cn 11734	. . . . . . . . 9 ⊢ 7 ∈ ℂ
202	201, 5, 48, 38, 71	divdiv32i 11397	. . . . . . . 8 ⊢ ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
203	199, 200, 202	3eqtr3i 2854	. . . . . . 7 ⊢ (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
204	203	oveq1i 7168	. . . . . 6 ⊢ ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205	183, 204	eqtri 2846	. . . . 5 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
206		4nn0 11919	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
207		9nn0 11924	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
208		0nn0 11915	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
209		9lt10 12232	. . . . . . . . . . . 12 ⊢ 9 < ;10
210		4lt5 11817	. . . . . . . . . . . 12 ⊢ 4 < 5
211	206, 90, 207, 208, 209, 210	decltc 12130	. . . . . . . . . . 11 ⊢ ;49 < ;50
212		7t7e49 12215	. . . . . . . . . . 11 ⊢ (7 · 7) = ;49
213	56	oveq1i 7168	. . . . . . . . . . . 12 ⊢ (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
214	48, 48, 112, 112	mul4i 10839	. . . . . . . . . . . 12 ⊢ (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
215		5t2e10 12201	. . . . . . . . . . . . . . 15 ⊢ (5 · 2) = ;10
216	112, 89, 215	mulcomli 10652	. . . . . . . . . . . . . 14 ⊢ (2 · 5) = ;10
217	216	oveq1i 7168	. . . . . . . . . . . . 13 ⊢ ((2 · 5) · 5) = (;10 · 5)
218	89, 112, 112	mulassi 10654	. . . . . . . . . . . . 13 ⊢ ((2 · 5) · 5) = (2 · (5 · 5))
219	90	dec0u 12122	. . . . . . . . . . . . 13 ⊢ (;10 · 5) = ;50
220	217, 218, 219	3eqtr3i 2854	. . . . . . . . . . . 12 ⊢ (2 · (5 · 5)) = ;50
221	213, 214, 220	3eqtr3i 2854	. . . . . . . . . . 11 ⊢ (((√‘2) · 5) · ((√‘2) · 5)) = ;50
222	211, 212, 221	3brtr4i 5098	. . . . . . . . . 10 ⊢ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
223		7re 11733	. . . . . . . . . . . 12 ⊢ 7 ∈ ℝ
224		7pos 11751	. . . . . . . . . . . 12 ⊢ 0 < 7
225	10, 223, 224	ltleii 10765	. . . . . . . . . . 11 ⊢ 0 ≤ 7
226		nnrp 12403	. . . . . . . . . . . . . 14 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
227	105, 226	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℝ⁺
228		rpmulcl 12415	. . . . . . . . . . . . 13 ⊢ (((√‘2) ∈ ℝ⁺ ∧ 5 ∈ ℝ⁺) → ((√‘2) · 5) ∈ ℝ⁺)
229	65, 227, 228	mp2an 690	. . . . . . . . . . . 12 ⊢ ((√‘2) · 5) ∈ ℝ⁺
230		rpge0 12405	. . . . . . . . . . . 12 ⊢ (((√‘2) · 5) ∈ ℝ⁺ → 0 ≤ ((√‘2) · 5))
231	229, 230	ax-mp 5	. . . . . . . . . . 11 ⊢ 0 ≤ ((√‘2) · 5)
232		rpre 12400	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 5) ∈ ℝ⁺ → ((√‘2) · 5) ∈ ℝ)
233	229, 232	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((√‘2) · 5) ∈ ℝ
234	223, 233	lt2msqi 11554	. . . . . . . . . . 11 ⊢ ((0 ≤ 7 ∧ 0 ≤ ((√‘2) · 5)) → (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))))
235	225, 231, 234	mp2an 690	. . . . . . . . . 10 ⊢ (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5)))
236	222, 235	mpbir 233	. . . . . . . . 9 ⊢ 7 < ((√‘2) · 5)
237		rpgt0 12404	. . . . . . . . . . 11 ⊢ ((√‘2) ∈ ℝ⁺ → 0 < (√‘2))
238	24, 64, 237	mp2b 10	. . . . . . . . . 10 ⊢ 0 < (√‘2)
239		ltdivmul 11517	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240	223, 173, 239	mp3an12 1447	. . . . . . . . . 10 ⊢ (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
241	47, 238, 240	mp2an 690	. . . . . . . . 9 ⊢ ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
242	236, 241	mpbir 233	. . . . . . . 8 ⊢ (7 / (√‘2)) < 5
243	223, 47, 71	redivcli 11409	. . . . . . . . 9 ⊢ (7 / (√‘2)) ∈ ℝ
244	243, 173, 11, 12	ltdiv1ii 11571	. . . . . . . 8 ⊢ ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
245	242, 244	mpbi 232	. . . . . . 7 ⊢ ((7 / (√‘2)) / 8) < (5 / 8)
246		divsubdir 11336	. . . . . . . . . . 11 ⊢ ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
247	5, 32, 246	mp3an12 1447	. . . . . . . . . 10 ⊢ ((8 ∈ ℂ ∧ 8 ≠ 0) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
248	5, 38, 247	mp2an 690	. . . . . . . . 9 ⊢ ((8 − 3) / 8) = ((8 / 8) − (3 / 8))
249		5p3e8 11797	. . . . . . . . . . . 12 ⊢ (5 + 3) = 8
250	249	oveq1i 7168	. . . . . . . . . . 11 ⊢ ((5 + 3) − 3) = (8 − 3)
251	112, 32	pncan3oi 10904	. . . . . . . . . . 11 ⊢ ((5 + 3) − 3) = 5
252	250, 251	eqtr3i 2848	. . . . . . . . . 10 ⊢ (8 − 3) = 5
253	252	oveq1i 7168	. . . . . . . . 9 ⊢ ((8 − 3) / 8) = (5 / 8)
254	5, 38	dividi 11375	. . . . . . . . . 10 ⊢ (8 / 8) = 1
255	254	oveq1i 7168	. . . . . . . . 9 ⊢ ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
256	248, 253, 255	3eqtr3ri 2855	. . . . . . . 8 ⊢ (1 − (3 / 8)) = (5 / 8)
257		5lt8 11834	. . . . . . . . . . . . 13 ⊢ 5 < 8
258	11, 173	remulcli 10659	. . . . . . . . . . . . . 14 ⊢ (8 · 5) ∈ ℝ
259	173, 11, 258	ltadd2i 10773	. . . . . . . . . . . . 13 ⊢ (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
260	257, 259	mpbi 232	. . . . . . . . . . . 12 ⊢ ((8 · 5) + 5) < ((8 · 5) + 8)
261		df-9 11710	. . . . . . . . . . . . . 14 ⊢ 9 = (8 + 1)
262	261	oveq1i 7168	. . . . . . . . . . . . 13 ⊢ (9 · 5) = ((8 + 1) · 5)
263	5, 185, 112	adddiri 10656	. . . . . . . . . . . . 13 ⊢ ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
264	112	mulid2i 10648	. . . . . . . . . . . . . 14 ⊢ (1 · 5) = 5
265	264	oveq2i 7169	. . . . . . . . . . . . 13 ⊢ ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
266	262, 263, 265	3eqtri 2850	. . . . . . . . . . . 12 ⊢ (9 · 5) = ((8 · 5) + 5)
267	86	oveq2i 7169	. . . . . . . . . . . . 13 ⊢ (8 · 6) = (8 · (5 + 1))
268	5, 112, 185	adddii 10655	. . . . . . . . . . . . 13 ⊢ (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
269	5	mulid1i 10647	. . . . . . . . . . . . . 14 ⊢ (8 · 1) = 8
270	269	oveq2i 7169	. . . . . . . . . . . . 13 ⊢ ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
271	267, 268, 270	3eqtri 2850	. . . . . . . . . . . 12 ⊢ (8 · 6) = ((8 · 5) + 8)
272	260, 266, 271	3brtr4i 5098	. . . . . . . . . . 11 ⊢ (9 · 5) < (8 · 6)
273	171, 173	remulcli 10659	. . . . . . . . . . . 12 ⊢ (9 · 5) ∈ ℝ
274		6re 11730	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℝ
275	11, 274	remulcli 10659	. . . . . . . . . . . 12 ⊢ (8 · 6) ∈ ℝ
276	168, 174	remulcli 10659	. . . . . . . . . . . 12 ⊢ (4 · (2↑5)) ∈ ℝ
277	2, 96	nnmulcli 11665	. . . . . . . . . . . . 13 ⊢ (4 · (2↑5)) ∈ ℕ
278	277	nngt0i 11679	. . . . . . . . . . . 12 ⊢ 0 < (4 · (2↑5))
279	273, 275, 276, 278	ltdiv1ii 11571	. . . . . . . . . . 11 ⊢ ((9 · 5) < (8 · 6) ↔ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5))))
280	272, 279	mpbi 232	. . . . . . . . . 10 ⊢ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5)))
281	121, 51, 112, 97, 75, 113	divmuldivi 11402	. . . . . . . . . 10 ⊢ ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
282		nnexpcl 13445	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 4 ∈ ℕ₀) → (2↑4) ∈ ℕ)
283	33, 206, 282	mp2an 690	. . . . . . . . . . . . 13 ⊢ (2↑4) ∈ ℕ
284	283	nncni 11650	. . . . . . . . . . . 12 ⊢ (2↑4) ∈ ℂ
285	283	nnne0i 11680	. . . . . . . . . . . 12 ⊢ (2↑4) ≠ 0
286		divcan5 11344	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
287	32, 286	mp3an1 1444	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
288	5, 38, 284, 285, 287	mp4an 691	. . . . . . . . . . 11 ⊢ (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8)
289		df-4 11705	. . . . . . . . . . . . . . . 16 ⊢ 4 = (3 + 1)
290	289	oveq2i 7169	. . . . . . . . . . . . . . 15 ⊢ (2↑4) = (2↑(3 + 1))
291		3nn0 11918	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ₀
292		expp1 13439	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ₀) → (2↑(3 + 1)) = ((2↑3) · 2))
293	89, 291, 292	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (2↑(3 + 1)) = ((2↑3) · 2)
294	22	oveq1i 7168	. . . . . . . . . . . . . . 15 ⊢ ((2↑3) · 2) = (8 · 2)
295	290, 293, 294	3eqtri 2850	. . . . . . . . . . . . . 14 ⊢ (2↑4) = (8 · 2)
296	295	oveq1i 7168	. . . . . . . . . . . . 13 ⊢ ((2↑4) · 3) = ((8 · 2) · 3)
297	5, 89, 32	mulassi 10654	. . . . . . . . . . . . 13 ⊢ ((8 · 2) · 3) = (8 · (2 · 3))
298	193	oveq2i 7169	. . . . . . . . . . . . 13 ⊢ (8 · (2 · 3)) = (8 · 6)
299	296, 297, 298	3eqtri 2850	. . . . . . . . . . . 12 ⊢ ((2↑4) · 3) = (8 · 6)
300		4p3e7 11794	. . . . . . . . . . . . . . . 16 ⊢ (4 + 3) = 7
301		5p2e7 11796	. . . . . . . . . . . . . . . 16 ⊢ (5 + 2) = 7
302	112, 89	addcomi 10833	. . . . . . . . . . . . . . . 16 ⊢ (5 + 2) = (2 + 5)
303	300, 301, 302	3eqtr2i 2852	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = (2 + 5)
304	303	oveq2i 7169	. . . . . . . . . . . . . 14 ⊢ (2↑(4 + 3)) = (2↑(2 + 5))
305		expadd 13474	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
306	89, 206, 291, 305	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (2↑(4 + 3)) = ((2↑4) · (2↑3))
307		2nn0 11917	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ₀
308		expadd 13474	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
309	89, 307, 90, 308	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (2↑(2 + 5)) = ((2↑2) · (2↑5))
310	304, 306, 309	3eqtr3i 2854	. . . . . . . . . . . . 13 ⊢ ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
311	22	oveq2i 7169	. . . . . . . . . . . . 13 ⊢ ((2↑4) · (2↑3)) = ((2↑4) · 8)
312		sq2 13563	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
313	312	oveq1i 7168	. . . . . . . . . . . . 13 ⊢ ((2↑2) · (2↑5)) = (4 · (2↑5))
314	310, 311, 313	3eqtr3i 2854	. . . . . . . . . . . 12 ⊢ ((2↑4) · 8) = (4 · (2↑5))
315	299, 314	oveq12i 7170	. . . . . . . . . . 11 ⊢ (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
316	288, 315	eqtr3i 2848	. . . . . . . . . 10 ⊢ (3 / 8) = ((8 · 6) / (4 · (2↑5)))
317	280, 281, 316	3brtr4i 5098	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) < (3 / 8)
318	167, 11, 38	redivcli 11409	. . . . . . . . . 10 ⊢ (3 / 8) ∈ ℝ
319		1re 10643	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
320		ltsub2 11139	. . . . . . . . . 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))))))
321	176, 318, 319, 320	mp3an 1457	. . . . . . . . 9 ⊢ (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5)))))
322	317, 321	mpbi 232	. . . . . . . 8 ⊢ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))
323	256, 322	eqbrtrri 5091	. . . . . . 7 ⊢ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
324	243, 11, 38	redivcli 11409	. . . . . . . 8 ⊢ ((7 / (√‘2)) / 8) ∈ ℝ
325	173, 11, 38	redivcli 11409	. . . . . . . 8 ⊢ (5 / 8) ∈ ℝ
326	319, 176	resubcli 10950	. . . . . . . 8 ⊢ (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
327	324, 325, 326	lttri 10768	. . . . . . 7 ⊢ ((((7 / (√‘2)) / 8) < (5 / 8) ∧ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))) → ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
328	245, 323, 327	mp2an 690	. . . . . 6 ⊢ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
329	324, 176, 319	ltaddsubi 11203	. . . . . 6 ⊢ ((((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
330	328, 329	mpbir 233	. . . . 5 ⊢ (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1
331	205, 330	eqbrtri 5089	. . . 4 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
332		1lt2 11811	. . . . . . 7 ⊢ 1 < 2
333		rplogcl 25189	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ⁺)
334	53, 332, 333	mp2an 690	. . . . . 6 ⊢ (log‘2) ∈ ℝ⁺
335		rpgt0 12404	. . . . . 6 ⊢ ((log‘2) ∈ ℝ⁺ → 0 < (log‘2))
336	334, 335	ax-mp 5	. . . . 5 ⊢ 0 < (log‘2)
337	180, 319, 36, 336	ltmul1ii 11570	. . . 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)))
338	331, 337	mpbi 232	. . 3 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2))
339	37	mulid2i 10648	. . . 4 ⊢ (1 · (log‘2)) = (log‘2)
340	339	eqcomi 2832	. . 3 ⊢ (log‘2) = (1 · (log‘2))
341	338, 166, 340	3brtr4i 5098	. 2 ⊢ (𝐹‘;64) < (log‘2)
342	182, 341	pm3.2i 473	1 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 class class class wbr 5068 ↦ cmpt 5148 ‘cfv 6357 (class class class)co 7158 ℂcc 10537 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 · cmul 10544 < clt 10677 ≤ cle 10678 − cmin 10872 / cdiv 11299 ℕcn 11640 2c2 11695 3c3 11696 4c4 11697 5c5 11698 6c6 11699 7c7 11700 8c8 11701 9c9 11702 ℕ₀cn0 11900 ℤcz 11984 cdc 12101 ℝ⁺crp 12392 ↑cexp 13432 √csqrt 14594 logclog 25140

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-inf2 9106 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617 ax-addf 10618 ax-mulf 10619

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-iin 4924 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-se 5517 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-of 7411 df-om 7583 df-1st 7691 df-2nd 7692 df-supp 7833 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-pm 8411 df-ixp 8464 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fsupp 8836 df-fi 8877 df-sup 8908 df-inf 8909 df-oi 8976 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ioc 12746 df-ico 12747 df-icc 12748 df-fz 12896 df-fzo 13037 df-fl 13165 df-mod 13241 df-seq 13373 df-exp 13433 df-fac 13637 df-bc 13666 df-hash 13694 df-shft 14428 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-limsup 14830 df-clim 14847 df-rlim 14848 df-sum 15045 df-ef 15423 df-sin 15425 df-cos 15426 df-pi 15428 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-sets 16492 df-ress 16493 df-plusg 16580 df-mulr 16581 df-starv 16582 df-sca 16583 df-vsca 16584 df-ip 16585 df-tset 16586 df-ple 16587 df-ds 16589 df-unif 16590 df-hom 16591 df-cco 16592 df-rest 16698 df-topn 16699 df-0g 16717 df-gsum 16718 df-topgen 16719 df-pt 16720 df-prds 16723 df-xrs 16777 df-qtop 16782 df-imas 16783 df-xps 16785 df-mre 16859 df-mrc 16860 df-acs 16862 df-mgm 17854 df-sgrp 17903 df-mnd 17914 df-submnd 17959 df-mulg 18227 df-cntz 18449 df-cmn 18910 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-fbas 20544 df-fg 20545 df-cnfld 20548 df-top 21504 df-topon 21521 df-topsp 21543 df-bases 21556 df-cld 21629 df-ntr 21630 df-cls 21631 df-nei 21708 df-lp 21746 df-perf 21747 df-cn 21837 df-cnp 21838 df-haus 21925 df-tx 22172 df-hmeo 22365 df-fil 22456 df-fm 22548 df-flim 22549 df-flf 22550 df-xms 22932 df-ms 22933 df-tms 22934 df-cncf 23488 df-limc 24466 df-dv 24467 df-log 25142

This theorem is referenced by: bposlem9 25870

W3C validator