bposlem8 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bposlem8		GIF version

Theorem bposlem8 16247

Description: Lemma for bpos 16249. Show that 𝐹(64) 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 9589	. . . . 5 ⊢ 6 ∈ ℕ₀
2		4nn 9473	. . . . 5 ⊢ 4 ∈ ℕ
3	1, 2	decnncl 9805	. . . 4 ⊢ ;64 ∈ ℕ
4		fveq2 5695	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ;64 → (√‘𝑛) = (√‘;64))
5		8cn 9393	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℂ
6	5	sqvali 11071	. . . . . . . . . . . . . . . . 17 ⊢ (8↑2) = (8 · 8)
7		8t8e64 9907	. . . . . . . . . . . . . . . . 17 ⊢ (8 · 8) = ;64
8	6, 7	eqtri 2259	. . . . . . . . . . . . . . . 16 ⊢ (8↑2) = ;64
9	8	fveq2i 5698	. . . . . . . . . . . . . . 15 ⊢ (√‘(8↑2)) = (√‘;64)
10		0re 8327	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
11		8re 9392	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℝ
12		8pos 9410	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 8
13	10, 11, 12	ltleii 8430	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 8
14	11	sqrtsqi 11906	. . . . . . . . . . . . . . . 16 ⊢ (0 ≤ 8 → (√‘(8↑2)) = 8)
15	13, 14	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (√‘(8↑2)) = 8
16	9, 15	eqtr3i 2261	. . . . . . . . . . . . . 14 ⊢ (√‘;64) = 8
17	4, 16	eqtrdi 2287	. . . . . . . . . . . . 13 ⊢ (𝑛 = ;64 → (√‘𝑛) = 8)
18	17	fveq2d 5699	. . . . . . . . . . . 12 ⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19		8nn 9477	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
20		nnrp 10075	. . . . . . . . . . . . 13 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
21		fveq2 5695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 8 → (log‘𝑥) = (log‘8))
22		cu2 11090	. . . . . . . . . . . . . . . . . . 19 ⊢ (2↑3) = 8
23	22	fveq2i 5698	. . . . . . . . . . . . . . . . . 18 ⊢ (log‘(2↑3)) = (log‘8)
24		2rp 10070	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ⁺
25		3z 9678	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℤ
26		relogexp 16034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℝ⁺ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
27	24, 25, 26	mp2an 430	. . . . . . . . . . . . . . . . . 18 ⊢ (log‘(2↑3)) = (3 · (log‘2))
28	23, 27	eqtr3i 2261	. . . . . . . . . . . . . . . . 17 ⊢ (log‘8) = (3 · (log‘2))
29	21, 28	eqtrdi 2287	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 8 → 𝑥 = 8)
31	29, 30	oveq12d 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32		3cn 9382	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
33		2nn 9471	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ
34		nnrp 10075	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℕ → 2 ∈ ℝ⁺)
35		relogcl 16023	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
36	33, 34, 35	mp2b 8	. . . . . . . . . . . . . . . . 17 ⊢ (log‘2) ∈ ℝ
37	36	recni 8339	. . . . . . . . . . . . . . . 16 ⊢ (log‘2) ∈ ℂ
38	11, 12	gt0ap0ii 8959	. . . . . . . . . . . . . . . 16 ⊢ 8 # 0
39	32, 37, 5, 38	div23api 9103	. . . . . . . . . . . . . . 15 ⊢ ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
40	31, 39	eqtrdi 2287	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41		bposlem7.2	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) / 𝑥))
42		znq 10034	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 ∈ ℤ ∧ 8 ∈ ℕ) → (3 / 8) ∈ ℚ)
43	25, 19, 42	mp2an 430	. . . . . . . . . . . . . . . . 17 ⊢ (3 / 8) ∈ ℚ
44		qre 10035	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 8) ∈ ℚ → (3 / 8) ∈ ℝ)
45	43, 44	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (3 / 8) ∈ ℝ
46	45, 36	remulcli 8341	. . . . . . . . . . . . . . 15 ⊢ ((3 / 8) · (log‘2)) ∈ ℝ
47	46	elexi 2834	. . . . . . . . . . . . . 14 ⊢ ((3 / 8) · (log‘2)) ∈ V
48	40, 41, 47	fvmpt 5782	. . . . . . . . . . . . 13 ⊢ (8 ∈ ℝ⁺ → (𝐺‘8) = ((3 / 8) · (log‘2)))
49	19, 20, 48	mp2b 8	. . . . . . . . . . . 12 ⊢ (𝐺‘8) = ((3 / 8) · (log‘2))
50	18, 49	eqtrdi 2287	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
51	50	oveq2d 6101	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
52		sqrt2re 12961	. . . . . . . . . . . . 13 ⊢ (√‘2) ∈ ℝ
53	52	recni 8339	. . . . . . . . . . . 12 ⊢ (√‘2) ∈ ℂ
54	32, 5, 38	divclapi 9087	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
55	53, 54, 37	mulassi 8336	. . . . . . . . . . 11 ⊢ (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
56		4cn 9385	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℂ
57	53, 56, 53	mul12i 8474	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
58		2re 9377	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
59		0le2 9397	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 2
60		remsqsqrt 11814	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
61	58, 59, 60	mp2an 430	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) · (√‘2)) = 2
62	61	oveq2i 6096	. . . . . . . . . . . . . . 15 ⊢ (4 · ((√‘2) · (√‘2))) = (4 · 2)
63		4t2e8 9467	. . . . . . . . . . . . . . 15 ⊢ (4 · 2) = 8
64	57, 62, 63	3eqtri 2263	. . . . . . . . . . . . . 14 ⊢ ((√‘2) · (4 · (√‘2))) = 8
65	64	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
66	56, 53	mulcli 8332	. . . . . . . . . . . . . . 15 ⊢ (4 · (√‘2)) ∈ ℂ
67		nnrp 10075	. . . . . . . . . . . . . . . . . 18 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
68	2, 67	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℝ⁺
69		rpsqrtcl 11823	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ⁺ → (√‘2) ∈ ℝ⁺)
70	33, 34, 69	mp2b 8	. . . . . . . . . . . . . . . . 17 ⊢ (√‘2) ∈ ℝ⁺
71		rpmulcl 10090	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℝ⁺ ∧ (√‘2) ∈ ℝ⁺) → (4 · (√‘2)) ∈ ℝ⁺)
72	68, 70, 71	mp2an 430	. . . . . . . . . . . . . . . 16 ⊢ (4 · (√‘2)) ∈ ℝ⁺
73		rpap0 10082	. . . . . . . . . . . . . . . 16 ⊢ ((4 · (√‘2)) ∈ ℝ⁺ → (4 · (√‘2)) # 0)
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (4 · (√‘2)) # 0
75		rpap0 10082	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ∈ ℝ⁺ → (√‘2) # 0)
76	24, 69, 75	mp2b 8	. . . . . . . . . . . . . . 15 ⊢ (√‘2) # 0
77		divcanap5 9047	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) # 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) # 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
78	32, 77	mp3an1 1365	. . . . . . . . . . . . . . 15 ⊢ ((((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) # 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) # 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
79	66, 74, 53, 76, 78	mp4an 431	. . . . . . . . . . . . . 14 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2)))
80		4ap0 9406	. . . . . . . . . . . . . . 15 ⊢ 4 # 0
81		divdivap1 9056	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 # 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) # 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
82	32, 81	mp3an1 1365	. . . . . . . . . . . . . . 15 ⊢ (((4 ∈ ℂ ∧ 4 # 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) # 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
83	56, 80, 53, 76, 82	mp4an 431	. . . . . . . . . . . . . 14 ⊢ ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2)))
84	79, 83	eqtr4i 2262	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
85	53, 32, 5, 38	divassapi 9101	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
86	65, 84, 85	3eqtr3ri 2268	. . . . . . . . . . . 12 ⊢ ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
87	86	oveq1i 6095	. . . . . . . . . . 11 ⊢ (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
88	55, 87	eqtr3i 2261	. . . . . . . . . 10 ⊢ ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
89	51, 88	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
90		oveq1 6092	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ;64 → (𝑛 / 2) = (;64 / 2))
91		df-6 9370	. . . . . . . . . . . . . . . . . 18 ⊢ 6 = (5 + 1)
92	91	oveq2i 6096	. . . . . . . . . . . . . . . . 17 ⊢ (2↑6) = (2↑(5 + 1))
93		2exp6 13236	. . . . . . . . . . . . . . . . 17 ⊢ (2↑6) = ;64
94		2cn 9378	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
95		5nn0 9588	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ₀
96		expp1 10998	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 5 ∈ ℕ₀) → (2↑(5 + 1)) = ((2↑5) · 2))
97	94, 95, 96	mp2an 430	. . . . . . . . . . . . . . . . 17 ⊢ (2↑(5 + 1)) = ((2↑5) · 2)
98	92, 93, 97	3eqtr3i 2267	. . . . . . . . . . . . . . . 16 ⊢ ;64 = ((2↑5) · 2)
99	98	oveq1i 6095	. . . . . . . . . . . . . . 15 ⊢ (;64 / 2) = (((2↑5) · 2) / 2)
100		nnexpcl 11004	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 5 ∈ ℕ₀) → (2↑5) ∈ ℕ)
101	33, 95, 100	mp2an 430	. . . . . . . . . . . . . . . . 17 ⊢ (2↑5) ∈ ℕ
102	101	nncni 9317	. . . . . . . . . . . . . . . 16 ⊢ (2↑5) ∈ ℂ
103	33	nnap0i 9338	. . . . . . . . . . . . . . . 16 ⊢ 2 # 0
104	102, 94, 103	divcanap4i 9092	. . . . . . . . . . . . . . 15 ⊢ (((2↑5) · 2) / 2) = (2↑5)
105	99, 104	eqtri 2259	. . . . . . . . . . . . . 14 ⊢ (;64 / 2) = (2↑5)
106	90, 105	eqtrdi 2287	. . . . . . . . . . . . 13 ⊢ (𝑛 = ;64 → (𝑛 / 2) = (2↑5))
107	106	fveq2d 5699	. . . . . . . . . . . 12 ⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
108		nnrp 10075	. . . . . . . . . . . . 13 ⊢ ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ⁺)
109		fveq2 5695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
110		5nn 9474	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℕ
111	110	nnzi 9670	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℤ
112		relogexp 16034	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ⁺ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
113	24, 111, 112	mp2an 430	. . . . . . . . . . . . . . . . 17 ⊢ (log‘(2↑5)) = (5 · (log‘2))
114	109, 113	eqtrdi 2287	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
115		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (2↑5) → 𝑥 = (2↑5))
116	114, 115	oveq12d 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
117		5cn 9387	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℂ
118	101	nnap0i 9338	. . . . . . . . . . . . . . . 16 ⊢ (2↑5) # 0
119	117, 37, 102, 118	div23api 9103	. . . . . . . . . . . . . . 15 ⊢ ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
120	116, 119	eqtrdi 2287	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
121		znq 10034	. . . . . . . . . . . . . . . . . 18 ⊢ ((5 ∈ ℤ ∧ (2↑5) ∈ ℕ) → (5 / (2↑5)) ∈ ℚ)
122	111, 101, 121	mp2an 430	. . . . . . . . . . . . . . . . 17 ⊢ (5 / (2↑5)) ∈ ℚ
123		qre 10035	. . . . . . . . . . . . . . . . 17 ⊢ ((5 / (2↑5)) ∈ ℚ → (5 / (2↑5)) ∈ ℝ)
124	122, 123	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (5 / (2↑5)) ∈ ℝ
125	124, 36	remulcli 8341	. . . . . . . . . . . . . . 15 ⊢ ((5 / (2↑5)) · (log‘2)) ∈ ℝ
126	125	elexi 2834	. . . . . . . . . . . . . 14 ⊢ ((5 / (2↑5)) · (log‘2)) ∈ V
127	120, 41, 126	fvmpt 5782	. . . . . . . . . . . . 13 ⊢ ((2↑5) ∈ ℝ⁺ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
128	101, 108, 127	mp2b 8	. . . . . . . . . . . 12 ⊢ (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
129	107, 128	eqtrdi 2287	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
130	129	oveq2d 6101	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
131		9cn 9395	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
132	131, 56, 80	divclapi 9087	. . . . . . . . . . 11 ⊢ (9 / 4) ∈ ℂ
133	117, 102, 118	divclapi 9087	. . . . . . . . . . 11 ⊢ (5 / (2↑5)) ∈ ℂ
134	132, 133, 37	mulassi 8336	. . . . . . . . . 10 ⊢ (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
135	130, 134	eqtr4di 2289	. . . . . . . . 9 ⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
136	89, 135	oveq12d 6103	. . . . . . . 8 ⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
137	32, 56, 80	divclapi 9087	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
138	137, 53, 76	divclapi 9087	. . . . . . . . 9 ⊢ ((3 / 4) / (√‘2)) ∈ ℂ
139	132, 133	mulcli 8332	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℂ
140	138, 139, 37	adddiri 8338	. . . . . . . 8 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2)))
141	136, 140	eqtr4di 2289	. . . . . . 7 ⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
142		oveq2 6093	. . . . . . . . . . 11 ⊢ (𝑛 = ;64 → (2 · 𝑛) = (2 · ;64))
143	142	fveq2d 5699	. . . . . . . . . 10 ⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = (√‘(2 · ;64)))
144	3	nnrei 9316	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℝ
145	3	nngt0i 9337	. . . . . . . . . . . . 13 ⊢ 0 < ;64
146	10, 144, 145	ltleii 8430	. . . . . . . . . . . 12 ⊢ 0 ≤ ;64
147	58, 144, 59, 146	sqrtmulii 11917	. . . . . . . . . . 11 ⊢ (√‘(2 · ;64)) = ((√‘2) · (√‘;64))
148	16	oveq2i 6096	. . . . . . . . . . 11 ⊢ ((√‘2) · (√‘;64)) = ((√‘2) · 8)
149	147, 148	eqtri 2259	. . . . . . . . . 10 ⊢ (√‘(2 · ;64)) = ((√‘2) · 8)
150	143, 149	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
151	150	oveq2d 6101	. . . . . . . 8 ⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
152	53, 5	mulcli 8332	. . . . . . . . . 10 ⊢ ((√‘2) · 8) ∈ ℂ
153		rpmulcl 10090	. . . . . . . . . . . 12 ⊢ (((√‘2) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((√‘2) · 8) ∈ ℝ⁺)
154	70, 20, 153	sylancr 418	. . . . . . . . . . 11 ⊢ (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ⁺)
155		rpap0 10082	. . . . . . . . . . 11 ⊢ (((√‘2) · 8) ∈ ℝ⁺ → ((√‘2) · 8) # 0)
156	19, 154, 155	mp2b 8	. . . . . . . . . 10 ⊢ ((√‘2) · 8) # 0
157		divrecap2 9022	. . . . . . . . . 10 ⊢ (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) # 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
158	37, 152, 156, 157	mp3an 1378	. . . . . . . . 9 ⊢ ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
159	53, 5	mulcomi 8333	. . . . . . . . . . . 12 ⊢ ((√‘2) · 8) = (8 · (√‘2))
160	159	oveq2i 6096	. . . . . . . . . . 11 ⊢ (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
161		recdivap2 9058	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 # 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) # 0)) → ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2))))
162	5, 38, 53, 76, 161	mp4an 431	. . . . . . . . . . 11 ⊢ ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2)))
163	160, 162	eqtr4i 2262	. . . . . . . . . 10 ⊢ (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
164	163	oveq1i 6095	. . . . . . . . 9 ⊢ ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
165	158, 164	eqtri 2259	. . . . . . . 8 ⊢ ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
166	151, 165	eqtrdi 2287	. . . . . . 7 ⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
167	141, 166	oveq12d 6103	. . . . . 6 ⊢ (𝑛 = ;64 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) + (((1 / 8) / (√‘2)) · (log‘2))))
168	138, 139	addcli 8331	. . . . . . 7 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
169	5, 38	recclapi 9075	. . . . . . . 8 ⊢ (1 / 8) ∈ ℂ
170	169, 53, 76	divclapi 9087	. . . . . . 7 ⊢ ((1 / 8) / (√‘2)) ∈ ℂ
171	168, 170, 37	adddiri 8338	. . . . . 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)))
172	167, 171	eqtr4di 2289	. . . . 5 ⊢ (𝑛 = ;64 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)))
173		bposlem7.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
174		3re 9381	. . . . . . . . . . 11 ⊢ 3 ∈ ℝ
175		4re 9384	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
176	174, 175, 80	redivclapi 9112	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℝ
177	176, 52, 76	redivclapi 9112	. . . . . . . . 9 ⊢ ((3 / 4) / (√‘2)) ∈ ℝ
178		9nn 9478	. . . . . . . . . . . . 13 ⊢ 9 ∈ ℕ
179	178	nnzi 9670	. . . . . . . . . . . 12 ⊢ 9 ∈ ℤ
180		znq 10034	. . . . . . . . . . . 12 ⊢ ((9 ∈ ℤ ∧ 4 ∈ ℕ) → (9 / 4) ∈ ℚ)
181	179, 2, 180	mp2an 430	. . . . . . . . . . 11 ⊢ (9 / 4) ∈ ℚ
182		qre 10035	. . . . . . . . . . 11 ⊢ ((9 / 4) ∈ ℚ → (9 / 4) ∈ ℝ)
183	181, 182	ax-mp 5	. . . . . . . . . 10 ⊢ (9 / 4) ∈ ℝ
184	183, 124	remulcli 8341	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℝ
185	177, 184	readdcli 8340	. . . . . . . 8 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
186	11, 38	rerecclapi 9110	. . . . . . . . 9 ⊢ (1 / 8) ∈ ℝ
187	186, 52, 76	redivclapi 9112	. . . . . . . 8 ⊢ ((1 / 8) / (√‘2)) ∈ ℝ
188	185, 187	readdcli 8340	. . . . . . 7 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
189	188, 36	remulcli 8341	. . . . . 6 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
190	189	elexi 2834	. . . . 5 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
191	172, 173, 190	fvmpt 5782	. . . 4 ⊢ (;64 ∈ ℕ → (𝐹‘;64) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)))
192	3, 191	ax-mp 5	. . 3 ⊢ (𝐹‘;64) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2))
193		9re 9394	. . . . . . . 8 ⊢ 9 ∈ ℝ
194	193, 175, 80	redivclapi 9112	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
195		5re 9386	. . . . . . . 8 ⊢ 5 ∈ ℝ
196	101	nnrei 9316	. . . . . . . 8 ⊢ (2↑5) ∈ ℝ
197	195, 196, 118	redivclapi 9112	. . . . . . 7 ⊢ (5 / (2↑5)) ∈ ℝ
198	194, 197	remulcli 8341	. . . . . 6 ⊢ ((9 / 4) · (5 / (2↑5))) ∈ ℝ
199	177, 198	readdcli 8340	. . . . 5 ⊢ (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
200	199, 187	readdcli 8340	. . . 4 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
201	200, 36	remulcli 8341	. . 3 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
202	192, 201	eqeltri 2311	. 2 ⊢ (𝐹‘;64) ∈ ℝ
203	138, 139, 170	add32i 8492	. . . . . 6 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5))))
204		6cn 9389	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
205		ax-1cn 8273	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
206	204, 205, 5, 38	divdirapi 9102	. . . . . . . . . 10 ⊢ ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
207		df-7 9371	. . . . . . . . . . 11 ⊢ 7 = (6 + 1)
208	207	oveq1i 6095	. . . . . . . . . 10 ⊢ (7 / 8) = ((6 + 1) / 8)
209		divcanap5 9047	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 # 0) ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
210	32, 209	mp3an1 1365	. . . . . . . . . . . . 13 ⊢ (((4 ∈ ℂ ∧ 4 # 0) ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
211	56, 80, 94, 103, 210	mp4an 431	. . . . . . . . . . . 12 ⊢ ((2 · 3) / (2 · 4)) = (3 / 4)
212		2t3e6 9465	. . . . . . . . . . . . 13 ⊢ (2 · 3) = 6
213		2t4e8 9468	. . . . . . . . . . . . 13 ⊢ (2 · 4) = 8
214	212, 213	oveq12i 6097	. . . . . . . . . . . 12 ⊢ ((2 · 3) / (2 · 4)) = (6 / 8)
215	211, 214	eqtr3i 2261	. . . . . . . . . . 11 ⊢ (3 / 4) = (6 / 8)
216	215	oveq1i 6095	. . . . . . . . . 10 ⊢ ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
217	206, 208, 216	3eqtr4ri 2270	. . . . . . . . 9 ⊢ ((3 / 4) + (1 / 8)) = (7 / 8)
218	217	oveq1i 6095	. . . . . . . 8 ⊢ (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
219	137, 169, 53, 76	divdirapi 9102	. . . . . . . 8 ⊢ (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
220		7cn 9391	. . . . . . . . 9 ⊢ 7 ∈ ℂ
221	220, 5, 53, 38, 76	divdiv32api 9100	. . . . . . . 8 ⊢ ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
222	218, 219, 221	3eqtr3i 2267	. . . . . . 7 ⊢ (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
223	222	oveq1i 6095	. . . . . 6 ⊢ ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
224	203, 223	eqtri 2259	. . . . 5 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
225		4nn0 9587	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
226		9nn0 9592	. . . . . . . . . . . 12 ⊢ 9 ∈ ℕ₀
227		0nn0 9583	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ₀
228		9lt10 9917	. . . . . . . . . . . 12 ⊢ 9 < ;10
229		4lt5 9485	. . . . . . . . . . . 12 ⊢ 4 < 5
230	225, 95, 226, 227, 228, 229	decltc 9815	. . . . . . . . . . 11 ⊢ ;49 < ;50
231		7t7e49 9900	. . . . . . . . . . 11 ⊢ (7 · 7) = ;49
232	61	oveq1i 6095	. . . . . . . . . . . 12 ⊢ (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
233	53, 53, 117, 117	mul4i 8476	. . . . . . . . . . . 12 ⊢ (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
234		5t2e10 9886	. . . . . . . . . . . . . . 15 ⊢ (5 · 2) = ;10
235	117, 94, 234	mulcomli 8334	. . . . . . . . . . . . . 14 ⊢ (2 · 5) = ;10
236	235	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ ((2 · 5) · 5) = (;10 · 5)
237	94, 117, 117	mulassi 8336	. . . . . . . . . . . . 13 ⊢ ((2 · 5) · 5) = (2 · (5 · 5))
238	95	dec0u 9807	. . . . . . . . . . . . 13 ⊢ (;10 · 5) = ;50
239	236, 237, 238	3eqtr3i 2267	. . . . . . . . . . . 12 ⊢ (2 · (5 · 5)) = ;50
240	232, 233, 239	3eqtr3i 2267	. . . . . . . . . . 11 ⊢ (((√‘2) · 5) · ((√‘2) · 5)) = ;50
241	230, 231, 240	3brtr4i 4160	. . . . . . . . . 10 ⊢ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
242		7re 9390	. . . . . . . . . . . 12 ⊢ 7 ∈ ℝ
243		7pos 9409	. . . . . . . . . . . 12 ⊢ 0 < 7
244	10, 242, 243	ltleii 8430	. . . . . . . . . . 11 ⊢ 0 ≤ 7
245		nnrp 10075	. . . . . . . . . . . . . 14 ⊢ (5 ∈ ℕ → 5 ∈ ℝ⁺)
246	110, 245	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℝ⁺
247		rpmulcl 10090	. . . . . . . . . . . . 13 ⊢ (((√‘2) ∈ ℝ⁺ ∧ 5 ∈ ℝ⁺) → ((√‘2) · 5) ∈ ℝ⁺)
248	70, 246, 247	mp2an 430	. . . . . . . . . . . 12 ⊢ ((√‘2) · 5) ∈ ℝ⁺
249		rpge0 10078	. . . . . . . . . . . 12 ⊢ (((√‘2) · 5) ∈ ℝ⁺ → 0 ≤ ((√‘2) · 5))
250	248, 249	ax-mp 5	. . . . . . . . . . 11 ⊢ 0 ≤ ((√‘2) · 5)
251		rpre 10072	. . . . . . . . . . . . 13 ⊢ (((√‘2) · 5) ∈ ℝ⁺ → ((√‘2) · 5) ∈ ℝ)
252	248, 251	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((√‘2) · 5) ∈ ℝ
253	242, 252	lt2msqi 9247	. . . . . . . . . . 11 ⊢ ((0 ≤ 7 ∧ 0 ≤ ((√‘2) · 5)) → (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))))
254	244, 250, 253	mp2an 430	. . . . . . . . . 10 ⊢ (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5)))
255	241, 254	mpbir 146	. . . . . . . . 9 ⊢ 7 < ((√‘2) · 5)
256		rpgt0 10077	. . . . . . . . . . 11 ⊢ ((√‘2) ∈ ℝ⁺ → 0 < (√‘2))
257	24, 69, 256	mp2b 8	. . . . . . . . . 10 ⊢ 0 < (√‘2)
258		ltdivmul 9209	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
259	242, 195, 258	mp3an12 1368	. . . . . . . . . 10 ⊢ (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
260	52, 257, 259	mp2an 430	. . . . . . . . 9 ⊢ ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
261	255, 260	mpbir 146	. . . . . . . 8 ⊢ (7 / (√‘2)) < 5
262	242, 52, 76	redivclapi 9112	. . . . . . . . 9 ⊢ (7 / (√‘2)) ∈ ℝ
263	262, 195, 11, 12	ltdiv1ii 9262	. . . . . . . 8 ⊢ ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
264	261, 263	mpbi 145	. . . . . . 7 ⊢ ((7 / (√‘2)) / 8) < (5 / 8)
265		divsubdirap 9041	. . . . . . . . . . 11 ⊢ ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 # 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
266	5, 32, 265	mp3an12 1368	. . . . . . . . . 10 ⊢ ((8 ∈ ℂ ∧ 8 # 0) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
267	5, 38, 266	mp2an 430	. . . . . . . . 9 ⊢ ((8 − 3) / 8) = ((8 / 8) − (3 / 8))
268		5p3e8 9455	. . . . . . . . . . . 12 ⊢ (5 + 3) = 8
269	268	oveq1i 6095	. . . . . . . . . . 11 ⊢ ((5 + 3) − 3) = (8 − 3)
270	117, 32	pncan3oi 8544	. . . . . . . . . . 11 ⊢ ((5 + 3) − 3) = 5
271	269, 270	eqtr3i 2261	. . . . . . . . . 10 ⊢ (8 − 3) = 5
272	271	oveq1i 6095	. . . . . . . . 9 ⊢ ((8 − 3) / 8) = (5 / 8)
273	5, 38	dividapi 9078	. . . . . . . . . 10 ⊢ (8 / 8) = 1
274	273	oveq1i 6095	. . . . . . . . 9 ⊢ ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
275	267, 272, 274	3eqtr3ri 2268	. . . . . . . 8 ⊢ (1 − (3 / 8)) = (5 / 8)
276		5lt8 9502	. . . . . . . . . . . . 13 ⊢ 5 < 8
277	11, 195	remulcli 8341	. . . . . . . . . . . . . 14 ⊢ (8 · 5) ∈ ℝ
278	195, 11, 277	ltadd2i 8750	. . . . . . . . . . . . 13 ⊢ (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
279	276, 278	mpbi 145	. . . . . . . . . . . 12 ⊢ ((8 · 5) + 5) < ((8 · 5) + 8)
280		df-9 9373	. . . . . . . . . . . . . 14 ⊢ 9 = (8 + 1)
281	280	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ (9 · 5) = ((8 + 1) · 5)
282	5, 205, 117	adddiri 8338	. . . . . . . . . . . . 13 ⊢ ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
283	117	mullidi 8330	. . . . . . . . . . . . . 14 ⊢ (1 · 5) = 5
284	283	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
285	281, 282, 284	3eqtri 2263	. . . . . . . . . . . 12 ⊢ (9 · 5) = ((8 · 5) + 5)
286	91	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ (8 · 6) = (8 · (5 + 1))
287	5, 117, 205	adddii 8337	. . . . . . . . . . . . 13 ⊢ (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
288	5	mulridi 8329	. . . . . . . . . . . . . 14 ⊢ (8 · 1) = 8
289	288	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
290	286, 287, 289	3eqtri 2263	. . . . . . . . . . . 12 ⊢ (8 · 6) = ((8 · 5) + 8)
291	279, 285, 290	3brtr4i 4160	. . . . . . . . . . 11 ⊢ (9 · 5) < (8 · 6)
292	193, 195	remulcli 8341	. . . . . . . . . . . 12 ⊢ (9 · 5) ∈ ℝ
293		6re 9388	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℝ
294	11, 293	remulcli 8341	. . . . . . . . . . . 12 ⊢ (8 · 6) ∈ ℝ
295	175, 196	remulcli 8341	. . . . . . . . . . . 12 ⊢ (4 · (2↑5)) ∈ ℝ
296	2, 101	nnmulcli 9329	. . . . . . . . . . . . 13 ⊢ (4 · (2↑5)) ∈ ℕ
297	296	nngt0i 9337	. . . . . . . . . . . 12 ⊢ 0 < (4 · (2↑5))
298	292, 294, 295, 297	ltdiv1ii 9262	. . . . . . . . . . 11 ⊢ ((9 · 5) < (8 · 6) ↔ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5))))
299	291, 298	mpbi 145	. . . . . . . . . 10 ⊢ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5)))
300	131, 56, 117, 102, 80, 118	divmuldivapi 9105	. . . . . . . . . 10 ⊢ ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
301		nnexpcl 11004	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 4 ∈ ℕ₀) → (2↑4) ∈ ℕ)
302	33, 225, 301	mp2an 430	. . . . . . . . . . . . 13 ⊢ (2↑4) ∈ ℕ
303	302	nncni 9317	. . . . . . . . . . . 12 ⊢ (2↑4) ∈ ℂ
304	302	nnap0i 9338	. . . . . . . . . . . 12 ⊢ (2↑4) # 0
305		divcanap5 9047	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 # 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) # 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
306	32, 305	mp3an1 1365	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 # 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) # 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
307	5, 38, 303, 304, 306	mp4an 431	. . . . . . . . . . 11 ⊢ (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8)
308		df-4 9368	. . . . . . . . . . . . . . . 16 ⊢ 4 = (3 + 1)
309	308	oveq2i 6096	. . . . . . . . . . . . . . 15 ⊢ (2↑4) = (2↑(3 + 1))
310		3nn0 9586	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ₀
311		expp1 10998	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ₀) → (2↑(3 + 1)) = ((2↑3) · 2))
312	94, 310, 311	mp2an 430	. . . . . . . . . . . . . . 15 ⊢ (2↑(3 + 1)) = ((2↑3) · 2)
313	22	oveq1i 6095	. . . . . . . . . . . . . . 15 ⊢ ((2↑3) · 2) = (8 · 2)
314	309, 312, 313	3eqtri 2263	. . . . . . . . . . . . . 14 ⊢ (2↑4) = (8 · 2)
315	314	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ ((2↑4) · 3) = ((8 · 2) · 3)
316	5, 94, 32	mulassi 8336	. . . . . . . . . . . . 13 ⊢ ((8 · 2) · 3) = (8 · (2 · 3))
317	212	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ (8 · (2 · 3)) = (8 · 6)
318	315, 316, 317	3eqtri 2263	. . . . . . . . . . . 12 ⊢ ((2↑4) · 3) = (8 · 6)
319		4p3e7 9452	. . . . . . . . . . . . . . . 16 ⊢ (4 + 3) = 7
320		5p2e7 9454	. . . . . . . . . . . . . . . 16 ⊢ (5 + 2) = 7
321	117, 94	addcomi 8472	. . . . . . . . . . . . . . . 16 ⊢ (5 + 2) = (2 + 5)
322	319, 320, 321	3eqtr2i 2265	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = (2 + 5)
323	322	oveq2i 6096	. . . . . . . . . . . . . 14 ⊢ (2↑(4 + 3)) = (2↑(2 + 5))
324		expadd 11033	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 4 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
325	94, 225, 310, 324	mp3an 1378	. . . . . . . . . . . . . 14 ⊢ (2↑(4 + 3)) = ((2↑4) · (2↑3))
326		2nn0 9585	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ₀
327		expadd 11033	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
328	94, 326, 95, 327	mp3an 1378	. . . . . . . . . . . . . 14 ⊢ (2↑(2 + 5)) = ((2↑2) · (2↑5))
329	323, 325, 328	3eqtr3i 2267	. . . . . . . . . . . . 13 ⊢ ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
330	22	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ ((2↑4) · (2↑3)) = ((2↑4) · 8)
331		sq2 11087	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
332	331	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ ((2↑2) · (2↑5)) = (4 · (2↑5))
333	329, 330, 332	3eqtr3i 2267	. . . . . . . . . . . 12 ⊢ ((2↑4) · 8) = (4 · (2↑5))
334	318, 333	oveq12i 6097	. . . . . . . . . . 11 ⊢ (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
335	307, 334	eqtr3i 2261	. . . . . . . . . 10 ⊢ (3 / 8) = ((8 · 6) / (4 · (2↑5)))
336	299, 300, 335	3brtr4i 4160	. . . . . . . . 9 ⊢ ((9 / 4) · (5 / (2↑5))) < (3 / 8)
337	174, 11, 38	redivclapi 9112	. . . . . . . . . 10 ⊢ (3 / 8) ∈ ℝ
338		1re 8326	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
339		ltsub2 8789	. . . . . . . . . 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))))))
340	198, 337, 338, 339	mp3an 1378	. . . . . . . . 9 ⊢ (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5)))))
341	336, 340	mpbi 145	. . . . . . . 8 ⊢ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))
342	275, 341	eqbrtrri 4153	. . . . . . 7 ⊢ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
343	262, 11, 38	redivclapi 9112	. . . . . . . 8 ⊢ ((7 / (√‘2)) / 8) ∈ ℝ
344	195, 11, 38	redivclapi 9112	. . . . . . . 8 ⊢ (5 / 8) ∈ ℝ
345	338, 198	resubcli 8591	. . . . . . . 8 ⊢ (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
346	343, 344, 345	lttri 8432	. . . . . . 7 ⊢ ((((7 / (√‘2)) / 8) < (5 / 8) ∧ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))) → ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
347	264, 342, 346	mp2an 430	. . . . . 6 ⊢ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
348	343, 198, 338	ltaddsubi 8839	. . . . . 6 ⊢ ((((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
349	347, 348	mpbir 146	. . . . 5 ⊢ (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1
350	224, 349	eqbrtri 4151	. . . 4 ⊢ ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
351		1lt2 9479	. . . . . . 7 ⊢ 1 < 2
352		rplogcl 16041	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ⁺)
353	58, 351, 352	mp2an 430	. . . . . 6 ⊢ (log‘2) ∈ ℝ⁺
354		rpgt0 10077	. . . . . 6 ⊢ ((log‘2) ∈ ℝ⁺ → 0 < (log‘2))
355	353, 354	ax-mp 5	. . . . 5 ⊢ 0 < (log‘2)
356	200, 338, 36, 355	ltmul1ii 9261	. . . 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)))
357	350, 356	mpbi 145	. . 3 ⊢ (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2))
358	37	mullidi 8330	. . . 4 ⊢ (1 · (log‘2)) = (log‘2)
359	358	eqcomi 2242	. . 3 ⊢ (log‘2) = (1 · (log‘2))
360	357, 192, 359	3brtr4i 4160	. 2 ⊢ (𝐹‘;64) < (log‘2)
361	202, 360	pm3.2i 272	1 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))

Colors of variables: wff set class

This proof depends on syntax axioms: ∧ wa 104 ↔ wb 105 = wceq 1402 ∈ wcel 2209 class class class wbr 4130 ↦ cmpt 4192 ‘cfv 5377 (class class class)co 6085 ℂcc 8178 ℝcr 8179 0cc0 8180 1c1 8181 + caddc 8183 · cmul 8185 < clt 8361 ≤ cle 8362 − cmin 8499 # cap 8912 / cdiv 9005 ℕcn 9307 2c2 9358 3c3 9359 4c4 9360 5c5 9361 6c6 9362 7c7 9363 8c8 9364 9c9 9365 ℕ₀cn0 9568 ℤcz 9649 cdc 9782 ℚcq 10029 ℝ⁺crp 10065 ↑cexp 10990 √csqrt 11778 logclog 16017

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8271 ax-resscn 8272 ax-1cn 8273 ax-1re 8274 ax-icn 8275 ax-addcl 8276 ax-addrcl 8277 ax-mulcl 8278 ax-mulrcl 8279 ax-addcom 8280 ax-mulcom 8281 ax-addass 8282 ax-mulass 8283 ax-distr 8284 ax-i2m1 8285 ax-0lt1 8286 ax-1rid 8287 ax-0id 8288 ax-rnegex 8289 ax-precex 8290 ax-cnre 8291 ax-pre-ltirr 8292 ax-pre-ltwlin 8293 ax-pre-lttrn 8294 ax-pre-apti 8295 ax-pre-ltadd 8296 ax-pre-mulgt0 8297 ax-pre-mulext 8298 ax-arch 8299 ax-caucvg 8300 ax-pre-suploc 8301 ax-addf 8302 ax-mulf 8303

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-of 6302 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-oadd 6691 df-er 6807 df-map 6924 df-pm 6925 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7325 df-inf 7326 df-pnf 8363 df-mnf 8364 df-xr 8365 df-ltxr 8366 df-le 8367 df-sub 8501 df-neg 8502 df-reap 8906 df-ap 8913 df-div 9006 df-inn 9308 df-2 9366 df-3 9367 df-4 9368 df-5 9369 df-6 9370 df-7 9371 df-8 9372 df-9 9373 df-n0 9569 df-z 9650 df-dec 9783 df-uz 9932 df-q 10030 df-rp 10066 df-xneg 10185 df-xadd 10186 df-ioo 10305 df-ico 10307 df-icc 10308 df-fz 10423 df-fzo 10561 df-seqfrec 10900 df-exp 10991 df-fac 11180 df-bc 11202 df-ihash 11231 df-shft 11596 df-cj 11623 df-re 11624 df-im 11625 df-rsqrt 11780 df-abs 11781 df-clim 12064 df-sumdc 12139 df-ef 12434 df-e 12435 df-rest 13647 df-topgen 13666 df-psmet 14932 df-xmet 14933 df-met 14934 df-bl 14935 df-mopn 14936 df-top 15158 df-topon 15171 df-bases 15203 df-ntr 15256 df-cn 15348 df-cnp 15349 df-tx 15413 df-cncf 15731 df-limced 15816 df-dvap 15817 df-relog 16019

This theorem is used by: bposlem9 16248

W3C validator