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

Theorem bposlem8 27269
Description: Lemma for bpos 27271. 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
StepHypRef Expression
1 6nn0 12526 . . . . 5 6 ∈ ℕ0
2 4nn 12328 . . . . 5 4 ∈ ℕ
31, 2decnncl 12730 . . . 4 64 ∈ ℕ
4 fveq2 6896 . . . . . . . . . . . . . 14 (𝑛 = 64 → (√‘𝑛) = (√‘64))
5 8cn 12342 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
65sqvali 14179 . . . . . . . . . . . . . . . . 17 (8↑2) = (8 · 8)
7 8t8e64 12831 . . . . . . . . . . . . . . . . 17 (8 · 8) = 64
86, 7eqtri 2753 . . . . . . . . . . . . . . . 16 (8↑2) = 64
98fveq2i 6899 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = (√‘64)
10 0re 11248 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
11 8re 12341 . . . . . . . . . . . . . . . . 17 8 ∈ ℝ
12 8pos 12357 . . . . . . . . . . . . . . . . 17 0 < 8
1310, 11, 12ltleii 11369 . . . . . . . . . . . . . . . 16 0 ≤ 8
1411sqrtsqi 15357 . . . . . . . . . . . . . . . 16 (0 ≤ 8 → (√‘(8↑2)) = 8)
1513, 14ax-mp 5 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = 8
169, 15eqtr3i 2755 . . . . . . . . . . . . . 14 (√‘64) = 8
174, 16eqtrdi 2781 . . . . . . . . . . . . 13 (𝑛 = 64 → (√‘𝑛) = 8)
1817fveq2d 6900 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19 8nn 12340 . . . . . . . . . . . . 13 8 ∈ ℕ
20 nnrp 13020 . . . . . . . . . . . . 13 (8 ∈ ℕ → 8 ∈ ℝ+)
21 fveq2 6896 . . . . . . . . . . . . . . . . 17 (𝑥 = 8 → (log‘𝑥) = (log‘8))
22 cu2 14199 . . . . . . . . . . . . . . . . . . 19 (2↑3) = 8
2322fveq2i 6899 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (log‘8)
24 2rp 13014 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
25 3z 12628 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℤ
26 relogexp 26575 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
2724, 25, 26mp2an 690 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (3 · (log‘2))
2823, 27eqtr3i 2755 . . . . . . . . . . . . . . . . 17 (log‘8) = (3 · (log‘2))
2921, 28eqtrdi 2781 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → 𝑥 = 8)
3129, 30oveq12d 7437 . . . . . . . . . . . . . . 15 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32 3cn 12326 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
33 2nn 12318 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
34 nnrp 13020 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℕ → 2 ∈ ℝ+)
35 relogcl 26554 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3633, 34, 35mp2b 10 . . . . . . . . . . . . . . . . 17 (log‘2) ∈ ℝ
3736recni 11260 . . . . . . . . . . . . . . . 16 (log‘2) ∈ ℂ
3819nnne0i 12285 . . . . . . . . . . . . . . . 16 8 ≠ 0
3932, 37, 5, 38div23i 12005 . . . . . . . . . . . . . . 15 ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
4031, 39eqtrdi 2781 . . . . . . . . . . . . . 14 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41 bposlem7.2 . . . . . . . . . . . . . 14 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
42 ovex 7452 . . . . . . . . . . . . . 14 ((3 / 8) · (log‘2)) ∈ V
4340, 41, 42fvmpt 7004 . . . . . . . . . . . . 13 (8 ∈ ℝ+ → (𝐺‘8) = ((3 / 8) · (log‘2)))
4419, 20, 43mp2b 10 . . . . . . . . . . . 12 (𝐺‘8) = ((3 / 8) · (log‘2))
4518, 44eqtrdi 2781 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
4645oveq2d 7435 . . . . . . . . . 10 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47 sqrt2re 16230 . . . . . . . . . . . . 13 (√‘2) ∈ ℝ
4847recni 11260 . . . . . . . . . . . 12 (√‘2) ∈ ℂ
4932, 5, 38divcli 11989 . . . . . . . . . . . 12 (3 / 8) ∈ ℂ
5048, 49, 37mulassi 11257 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51 4cn 12330 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
5248, 51, 48mul12i 11441 . . . . . . . . . . . . . . 15 ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53 2re 12319 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
54 0le2 12347 . . . . . . . . . . . . . . . . 17 0 ≤ 2
55 remsqsqrt 15239 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
5653, 54, 55mp2an 690 . . . . . . . . . . . . . . . 16 ((√‘2) · (√‘2)) = 2
5756oveq2i 7430 . . . . . . . . . . . . . . 15 (4 · ((√‘2) · (√‘2))) = (4 · 2)
58 4t2e8 12413 . . . . . . . . . . . . . . 15 (4 · 2) = 8
5952, 57, 583eqtri 2757 . . . . . . . . . . . . . 14 ((√‘2) · (4 · (√‘2))) = 8
6059oveq2i 7430 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
6151, 48mulcli 11253 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ∈ ℂ
62 nnrp 13020 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
632, 62ax-mp 5 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ+
64 rpsqrtcl 15247 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (√‘2) ∈ ℝ+)
6533, 34, 64mp2b 10 . . . . . . . . . . . . . . . . 17 (√‘2) ∈ ℝ+
66 rpmulcl 13032 . . . . . . . . . . . . . . . . 17 ((4 ∈ ℝ+ ∧ (√‘2) ∈ ℝ+) → (4 · (√‘2)) ∈ ℝ+)
6763, 65, 66mp2an 690 . . . . . . . . . . . . . . . 16 (4 · (√‘2)) ∈ ℝ+
68 rpne0 13025 . . . . . . . . . . . . . . . 16 ((4 · (√‘2)) ∈ ℝ+ → (4 · (√‘2)) ≠ 0)
6967, 68ax-mp 5 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ≠ 0
70 rpne0 13025 . . . . . . . . . . . . . . . 16 ((√‘2) ∈ ℝ+ → (√‘2) ≠ 0)
7124, 64, 70mp2b 10 . . . . . . . . . . . . . . 15 (√‘2) ≠ 0
72 divcan5 11949 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7332, 72mp3an1 1444 . . . . . . . . . . . . . . 15 ((((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7461, 69, 48, 71, 73mp4an 691 . . . . . . . . . . . . . 14 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2)))
75 4ne0 12353 . . . . . . . . . . . . . . 15 4 ≠ 0
76 divdiv1 11958 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7732, 76mp3an1 1444 . . . . . . . . . . . . . . 15 (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7851, 75, 48, 71, 77mp4an 691 . . . . . . . . . . . . . 14 ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2)))
7974, 78eqtr4i 2756 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
8048, 32, 5, 38divassi 12003 . . . . . . . . . . . . 13 (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
8160, 79, 803eqtr3ri 2762 . . . . . . . . . . . 12 ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
8281oveq1i 7429 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
8350, 82eqtr3i 2755 . . . . . . . . . 10 ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
8446, 83eqtrdi 2781 . . . . . . . . 9 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85 oveq1 7426 . . . . . . . . . . . . . 14 (𝑛 = 64 → (𝑛 / 2) = (64 / 2))
86 df-6 12312 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
8786oveq2i 7430 . . . . . . . . . . . . . . . . 17 (2↑6) = (2↑(5 + 1))
88 2exp6 17059 . . . . . . . . . . . . . . . . 17 (2↑6) = 64
89 2cn 12320 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
90 5nn0 12525 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ0
91 expp1 14069 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 5 ∈ ℕ0) → (2↑(5 + 1)) = ((2↑5) · 2))
9289, 90, 91mp2an 690 . . . . . . . . . . . . . . . . 17 (2↑(5 + 1)) = ((2↑5) · 2)
9387, 88, 923eqtr3i 2761 . . . . . . . . . . . . . . . 16 64 = ((2↑5) · 2)
9493oveq1i 7429 . . . . . . . . . . . . . . 15 (64 / 2) = (((2↑5) · 2) / 2)
95 nnexpcl 14075 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ ∧ 5 ∈ ℕ0) → (2↑5) ∈ ℕ)
9633, 90, 95mp2an 690 . . . . . . . . . . . . . . . . 17 (2↑5) ∈ ℕ
9796nncni 12255 . . . . . . . . . . . . . . . 16 (2↑5) ∈ ℂ
98 2ne0 12349 . . . . . . . . . . . . . . . 16 2 ≠ 0
9997, 89, 98divcan4i 11994 . . . . . . . . . . . . . . 15 (((2↑5) · 2) / 2) = (2↑5)
10094, 99eqtri 2753 . . . . . . . . . . . . . 14 (64 / 2) = (2↑5)
10185, 100eqtrdi 2781 . . . . . . . . . . . . 13 (𝑛 = 64 → (𝑛 / 2) = (2↑5))
102101fveq2d 6900 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103 nnrp 13020 . . . . . . . . . . . . 13 ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ+)
104 fveq2 6896 . . . . . . . . . . . . . . . . 17 (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105 5nn 12331 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℕ
106105nnzi 12619 . . . . . . . . . . . . . . . . . 18 5 ∈ ℤ
107 relogexp 26575 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
10824, 106, 107mp2an 690 . . . . . . . . . . . . . . . . 17 (log‘(2↑5)) = (5 · (log‘2))
109104, 108eqtrdi 2781 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → 𝑥 = (2↑5))
111109, 110oveq12d 7437 . . . . . . . . . . . . . . 15 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112 5cn 12333 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
11396nnne0i 12285 . . . . . . . . . . . . . . . 16 (2↑5) ≠ 0
114112, 37, 97, 113div23i 12005 . . . . . . . . . . . . . . 15 ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115111, 114eqtrdi 2781 . . . . . . . . . . . . . 14 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116 ovex 7452 . . . . . . . . . . . . . 14 ((5 / (2↑5)) · (log‘2)) ∈ V
117115, 41, 116fvmpt 7004 . . . . . . . . . . . . 13 ((2↑5) ∈ ℝ+ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
11896, 103, 117mp2b 10 . . . . . . . . . . . 12 (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
119102, 118eqtrdi 2781 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120119oveq2d 7435 . . . . . . . . . 10 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121 9cn 12345 . . . . . . . . . . . 12 9 ∈ ℂ
122121, 51, 75divcli 11989 . . . . . . . . . . 11 (9 / 4) ∈ ℂ
123112, 97, 113divcli 11989 . . . . . . . . . . 11 (5 / (2↑5)) ∈ ℂ
124122, 123, 37mulassi 11257 . . . . . . . . . 10 (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125120, 124eqtr4di 2783 . . . . . . . . 9 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
12684, 125oveq12d 7437 . . . . . . . 8 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
12732, 51, 75divcli 11989 . . . . . . . . . 10 (3 / 4) ∈ ℂ
128127, 48, 71divcli 11989 . . . . . . . . 9 ((3 / 4) / (√‘2)) ∈ ℂ
129122, 123mulcli 11253 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130128, 129, 37adddiri 11259 . . . . . . . 8 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2)))
131126, 130eqtr4di 2783 . . . . . . 7 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132 oveq2 7427 . . . . . . . . . . 11 (𝑛 = 64 → (2 · 𝑛) = (2 · 64))
133132fveq2d 6900 . . . . . . . . . 10 (𝑛 = 64 → (√‘(2 · 𝑛)) = (√‘(2 · 64)))
1343nnrei 12254 . . . . . . . . . . . 12 64 ∈ ℝ
1353nngt0i 12284 . . . . . . . . . . . . 13 0 < 64
13610, 134, 135ltleii 11369 . . . . . . . . . . . 12 0 ≤ 64
13753, 134, 54, 136sqrtmulii 15369 . . . . . . . . . . 11 (√‘(2 · 64)) = ((√‘2) · (√‘64))
13816oveq2i 7430 . . . . . . . . . . 11 ((√‘2) · (√‘64)) = ((√‘2) · 8)
139137, 138eqtri 2753 . . . . . . . . . 10 (√‘(2 · 64)) = ((√‘2) · 8)
140133, 139eqtrdi 2781 . . . . . . . . 9 (𝑛 = 64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141140oveq2d 7435 . . . . . . . 8 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
14248, 5mulcli 11253 . . . . . . . . . 10 ((√‘2) · 8) ∈ ℂ
143 rpmulcl 13032 . . . . . . . . . . . 12 (((√‘2) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((√‘2) · 8) ∈ ℝ+)
14465, 20, 143sylancr 585 . . . . . . . . . . 11 (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ+)
145 rpne0 13025 . . . . . . . . . . 11 (((√‘2) · 8) ∈ ℝ+ → ((√‘2) · 8) ≠ 0)
14619, 144, 145mp2b 10 . . . . . . . . . 10 ((√‘2) · 8) ≠ 0
147 divrec2 11922 . . . . . . . . . 10 (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
14837, 142, 146, 147mp3an 1457 . . . . . . . . 9 ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
14948, 5mulcomi 11254 . . . . . . . . . . . 12 ((√‘2) · 8) = (8 · (√‘2))
150149oveq2i 7430 . . . . . . . . . . 11 (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151 recdiv2 11960 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2))))
1525, 38, 48, 71, 151mp4an 691 . . . . . . . . . . 11 ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2)))
153150, 152eqtr4i 2756 . . . . . . . . . 10 (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154153oveq1i 7429 . . . . . . . . 9 ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155148, 154eqtri 2753 . . . . . . . 8 ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156141, 155eqtrdi 2781 . . . . . . 7 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157131, 156oveq12d 7437 . . . . . 6 (𝑛 = 64 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) + (((1 / 8) / (√‘2)) · (log‘2))))
158128, 129addcli 11252 . . . . . . 7 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
1595, 38reccli 11977 . . . . . . . 8 (1 / 8) ∈ ℂ
160159, 48, 71divcli 11989 . . . . . . 7 ((1 / 8) / (√‘2)) ∈ ℂ
161158, 160, 37adddiri 11259 . . . . . 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)))
162157, 161eqtr4di 2783 . . . . 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 7452 . . . . 5 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165162, 163, 164fvmpt 7004 . . . 4 (64 ∈ ℕ → (𝐹64) = (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)))
1663, 165ax-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 ∈ ℝ
169167, 168, 75redivcli 12014 . . . . . . 7 (3 / 4) ∈ ℝ
170169, 47, 71redivcli 12014 . . . . . 6 ((3 / 4) / (√‘2)) ∈ ℝ
171 9re 12344 . . . . . . . 8 9 ∈ ℝ
172171, 168, 75redivcli 12014 . . . . . . 7 (9 / 4) ∈ ℝ
173 5re 12332 . . . . . . . 8 5 ∈ ℝ
17496nnrei 12254 . . . . . . . 8 (2↑5) ∈ ℝ
175173, 174, 113redivcli 12014 . . . . . . 7 (5 / (2↑5)) ∈ ℝ
176172, 175remulcli 11262 . . . . . 6 ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177170, 176readdcli 11261 . . . . 5 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
17811, 38rereccli 12012 . . . . . 6 (1 / 8) ∈ ℝ
179178, 47, 71redivcli 12014 . . . . 5 ((1 / 8) / (√‘2)) ∈ ℝ
180177, 179readdcli 11261 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181180, 36remulcli 11262 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182166, 181eqeltri 2821 . 2 (𝐹64) ∈ ℝ
183128, 129, 160add32i 11469 . . . . . 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 11198 . . . . . . . . . . 11 1 ∈ ℂ
186184, 185, 5, 38divdiri 12004 . . . . . . . . . 10 ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187 df-7 12313 . . . . . . . . . . 11 7 = (6 + 1)
188187oveq1i 7429 . . . . . . . . . 10 (7 / 8) = ((6 + 1) / 8)
189 divcan5 11949 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19032, 189mp3an1 1444 . . . . . . . . . . . . 13 (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19151, 75, 89, 98, 190mp4an 691 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (3 / 4)
192 3t2e6 12411 . . . . . . . . . . . . . 14 (3 · 2) = 6
19332, 89, 192mulcomli 11255 . . . . . . . . . . . . 13 (2 · 3) = 6
19451, 89, 58mulcomli 11255 . . . . . . . . . . . . 13 (2 · 4) = 8
195193, 194oveq12i 7431 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (6 / 8)
196191, 195eqtr3i 2755 . . . . . . . . . . 11 (3 / 4) = (6 / 8)
197196oveq1i 7429 . . . . . . . . . 10 ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
198186, 188, 1973eqtr4ri 2764 . . . . . . . . 9 ((3 / 4) + (1 / 8)) = (7 / 8)
199198oveq1i 7429 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
200127, 159, 48, 71divdiri 12004 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
201 7cn 12339 . . . . . . . . 9 7 ∈ ℂ
202201, 5, 48, 38, 71divdiv32i 12002 . . . . . . . 8 ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
203199, 200, 2023eqtr3i 2761 . . . . . . 7 (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
204203oveq1i 7429 . . . . . 6 ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205183, 204eqtri 2753 . . . . 5 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
206 4nn0 12524 . . . . . . . . . . . 12 4 ∈ ℕ0
207 9nn0 12529 . . . . . . . . . . . 12 9 ∈ ℕ0
208 0nn0 12520 . . . . . . . . . . . 12 0 ∈ ℕ0
209 9lt10 12841 . . . . . . . . . . . 12 9 < 10
210 4lt5 12422 . . . . . . . . . . . 12 4 < 5
211206, 90, 207, 208, 209, 210decltc 12739 . . . . . . . . . . 11 49 < 50
212 7t7e49 12824 . . . . . . . . . . 11 (7 · 7) = 49
21356oveq1i 7429 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
21448, 48, 112, 112mul4i 11443 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
215 5t2e10 12810 . . . . . . . . . . . . . . 15 (5 · 2) = 10
216112, 89, 215mulcomli 11255 . . . . . . . . . . . . . 14 (2 · 5) = 10
217216oveq1i 7429 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (10 · 5)
21889, 112, 112mulassi 11257 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (2 · (5 · 5))
21990dec0u 12731 . . . . . . . . . . . . 13 (10 · 5) = 50
220217, 218, 2193eqtr3i 2761 . . . . . . . . . . . 12 (2 · (5 · 5)) = 50
221213, 214, 2203eqtr3i 2761 . . . . . . . . . . 11 (((√‘2) · 5) · ((√‘2) · 5)) = 50
222211, 212, 2213brtr4i 5179 . . . . . . . . . 10 (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
223 7re 12338 . . . . . . . . . . . 12 7 ∈ ℝ
224 7pos 12356 . . . . . . . . . . . 12 0 < 7
22510, 223, 224ltleii 11369 . . . . . . . . . . 11 0 ≤ 7
226 nnrp 13020 . . . . . . . . . . . . . 14 (5 ∈ ℕ → 5 ∈ ℝ+)
227105, 226ax-mp 5 . . . . . . . . . . . . 13 5 ∈ ℝ+
228 rpmulcl 13032 . . . . . . . . . . . . 13 (((√‘2) ∈ ℝ+ ∧ 5 ∈ ℝ+) → ((√‘2) · 5) ∈ ℝ+)
22965, 227, 228mp2an 690 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ+
230 rpge0 13022 . . . . . . . . . . . 12 (((√‘2) · 5) ∈ ℝ+ → 0 ≤ ((√‘2) · 5))
231229, 230ax-mp 5 . . . . . . . . . . 11 0 ≤ ((√‘2) · 5)
232 rpre 13017 . . . . . . . . . . . . 13 (((√‘2) · 5) ∈ ℝ+ → ((√‘2) · 5) ∈ ℝ)
233229, 232ax-mp 5 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ
234223, 233lt2msqi 12159 . . . . . . . . . . 11 ((0 ≤ 7 ∧ 0 ≤ ((√‘2) · 5)) → (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))))
235225, 231, 234mp2an 690 . . . . . . . . . 10 (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5)))
236222, 235mpbir 230 . . . . . . . . 9 7 < ((√‘2) · 5)
237 rpgt0 13021 . . . . . . . . . . 11 ((√‘2) ∈ ℝ+ → 0 < (√‘2))
23824, 64, 237mp2b 10 . . . . . . . . . 10 0 < (√‘2)
239 ltdivmul 12122 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240223, 173, 239mp3an12 1447 . . . . . . . . . 10 (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
24147, 238, 240mp2an 690 . . . . . . . . 9 ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
242236, 241mpbir 230 . . . . . . . 8 (7 / (√‘2)) < 5
243223, 47, 71redivcli 12014 . . . . . . . . 9 (7 / (√‘2)) ∈ ℝ
244243, 173, 11, 12ltdiv1ii 12176 . . . . . . . 8 ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
245242, 244mpbi 229 . . . . . . 7 ((7 / (√‘2)) / 8) < (5 / 8)
246 divsubdir 11941 . . . . . . . . . . 11 ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2475, 32, 246mp3an12 1447 . . . . . . . . . 10 ((8 ∈ ℂ ∧ 8 ≠ 0) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2485, 38, 247mp2an 690 . . . . . . . . 9 ((8 − 3) / 8) = ((8 / 8) − (3 / 8))
249 5p3e8 12402 . . . . . . . . . . . 12 (5 + 3) = 8
250249oveq1i 7429 . . . . . . . . . . 11 ((5 + 3) − 3) = (8 − 3)
251112, 32pncan3oi 11508 . . . . . . . . . . 11 ((5 + 3) − 3) = 5
252250, 251eqtr3i 2755 . . . . . . . . . 10 (8 − 3) = 5
253252oveq1i 7429 . . . . . . . . 9 ((8 − 3) / 8) = (5 / 8)
2545, 38dividi 11980 . . . . . . . . . 10 (8 / 8) = 1
255254oveq1i 7429 . . . . . . . . 9 ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
256248, 253, 2553eqtr3ri 2762 . . . . . . . 8 (1 − (3 / 8)) = (5 / 8)
257 5lt8 12439 . . . . . . . . . . . . 13 5 < 8
25811, 173remulcli 11262 . . . . . . . . . . . . . 14 (8 · 5) ∈ ℝ
259173, 11, 258ltadd2i 11377 . . . . . . . . . . . . 13 (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
260257, 259mpbi 229 . . . . . . . . . . . 12 ((8 · 5) + 5) < ((8 · 5) + 8)
261 df-9 12315 . . . . . . . . . . . . . 14 9 = (8 + 1)
262261oveq1i 7429 . . . . . . . . . . . . 13 (9 · 5) = ((8 + 1) · 5)
2635, 185, 112adddiri 11259 . . . . . . . . . . . . 13 ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
264112mullidi 11251 . . . . . . . . . . . . . 14 (1 · 5) = 5
265264oveq2i 7430 . . . . . . . . . . . . 13 ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
266262, 263, 2653eqtri 2757 . . . . . . . . . . . 12 (9 · 5) = ((8 · 5) + 5)
26786oveq2i 7430 . . . . . . . . . . . . 13 (8 · 6) = (8 · (5 + 1))
2685, 112, 185adddii 11258 . . . . . . . . . . . . 13 (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
2695mulridi 11250 . . . . . . . . . . . . . 14 (8 · 1) = 8
270269oveq2i 7430 . . . . . . . . . . . . 13 ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
271267, 268, 2703eqtri 2757 . . . . . . . . . . . 12 (8 · 6) = ((8 · 5) + 8)
272260, 266, 2713brtr4i 5179 . . . . . . . . . . 11 (9 · 5) < (8 · 6)
273171, 173remulcli 11262 . . . . . . . . . . . 12 (9 · 5) ∈ ℝ
274 6re 12335 . . . . . . . . . . . . 13 6 ∈ ℝ
27511, 274remulcli 11262 . . . . . . . . . . . 12 (8 · 6) ∈ ℝ
276168, 174remulcli 11262 . . . . . . . . . . . 12 (4 · (2↑5)) ∈ ℝ
2772, 96nnmulcli 12270 . . . . . . . . . . . . 13 (4 · (2↑5)) ∈ ℕ
278277nngt0i 12284 . . . . . . . . . . . 12 0 < (4 · (2↑5))
279273, 275, 276, 278ltdiv1ii 12176 . . . . . . . . . . 11 ((9 · 5) < (8 · 6) ↔ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5))))
280272, 279mpbi 229 . . . . . . . . . 10 ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5)))
281121, 51, 112, 97, 75, 113divmuldivi 12007 . . . . . . . . . 10 ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
282 nnexpcl 14075 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈ ℕ)
28333, 206, 282mp2an 690 . . . . . . . . . . . . 13 (2↑4) ∈ ℕ
284283nncni 12255 . . . . . . . . . . . 12 (2↑4) ∈ ℂ
285283nnne0i 12285 . . . . . . . . . . . 12 (2↑4) ≠ 0
286 divcan5 11949 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
28732, 286mp3an1 1444 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
2885, 38, 284, 285, 287mp4an 691 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8)
289 df-4 12310 . . . . . . . . . . . . . . . 16 4 = (3 + 1)
290289oveq2i 7430 . . . . . . . . . . . . . . 15 (2↑4) = (2↑(3 + 1))
291 3nn0 12523 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
292 expp1 14069 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 3 ∈ ℕ0) → (2↑(3 + 1)) = ((2↑3) · 2))
29389, 291, 292mp2an 690 . . . . . . . . . . . . . . 15 (2↑(3 + 1)) = ((2↑3) · 2)
29422oveq1i 7429 . . . . . . . . . . . . . . 15 ((2↑3) · 2) = (8 · 2)
295290, 293, 2943eqtri 2757 . . . . . . . . . . . . . 14 (2↑4) = (8 · 2)
296295oveq1i 7429 . . . . . . . . . . . . 13 ((2↑4) · 3) = ((8 · 2) · 3)
2975, 89, 32mulassi 11257 . . . . . . . . . . . . 13 ((8 · 2) · 3) = (8 · (2 · 3))
298193oveq2i 7430 . . . . . . . . . . . . 13 (8 · (2 · 3)) = (8 · 6)
299296, 297, 2983eqtri 2757 . . . . . . . . . . . 12 ((2↑4) · 3) = (8 · 6)
300 4p3e7 12399 . . . . . . . . . . . . . . . 16 (4 + 3) = 7
301 5p2e7 12401 . . . . . . . . . . . . . . . 16 (5 + 2) = 7
302112, 89addcomi 11437 . . . . . . . . . . . . . . . 16 (5 + 2) = (2 + 5)
303300, 301, 3023eqtr2i 2759 . . . . . . . . . . . . . . 15 (4 + 3) = (2 + 5)
304303oveq2i 7430 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = (2↑(2 + 5))
305 expadd 14105 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
30689, 206, 291, 305mp3an 1457 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = ((2↑4) · (2↑3))
307 2nn0 12522 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
308 expadd 14105 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 5 ∈ ℕ0) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
30989, 307, 90, 308mp3an 1457 . . . . . . . . . . . . . 14 (2↑(2 + 5)) = ((2↑2) · (2↑5))
310304, 306, 3093eqtr3i 2761 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
31122oveq2i 7430 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑4) · 8)
312 sq2 14196 . . . . . . . . . . . . . 14 (2↑2) = 4
313312oveq1i 7429 . . . . . . . . . . . . 13 ((2↑2) · (2↑5)) = (4 · (2↑5))
314310, 311, 3133eqtr3i 2761 . . . . . . . . . . . 12 ((2↑4) · 8) = (4 · (2↑5))
315299, 314oveq12i 7431 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
316288, 315eqtr3i 2755 . . . . . . . . . 10 (3 / 8) = ((8 · 6) / (4 · (2↑5)))
317280, 281, 3163brtr4i 5179 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) < (3 / 8)
318167, 11, 38redivcli 12014 . . . . . . . . . 10 (3 / 8) ∈ ℝ
319 1re 11246 . . . . . . . . . 10 1 ∈ ℝ
320 ltsub2 11743 . . . . . . . . . 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))))))
321176, 318, 319, 320mp3an 1457 . . . . . . . . 9 (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5)))))
322317, 321mpbi 229 . . . . . . . 8 (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))
323256, 322eqbrtrri 5172 . . . . . . 7 (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
324243, 11, 38redivcli 12014 . . . . . . . 8 ((7 / (√‘2)) / 8) ∈ ℝ
325173, 11, 38redivcli 12014 . . . . . . . 8 (5 / 8) ∈ ℝ
326319, 176resubcli 11554 . . . . . . . 8 (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
327324, 325, 326lttri 11372 . . . . . . 7 ((((7 / (√‘2)) / 8) < (5 / 8) ∧ (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))) → ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
328245, 323, 327mp2an 690 . . . . . 6 ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
329324, 176, 319ltaddsubi 11807 . . . . . 6 ((((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
330328, 329mpbir 230 . . . . 5 (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1
331205, 330eqbrtri 5170 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
332 1lt2 12416 . . . . . . 7 1 < 2
333 rplogcl 26583 . . . . . . 7 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
33453, 332, 333mp2an 690 . . . . . 6 (log‘2) ∈ ℝ+
335 rpgt0 13021 . . . . . 6 ((log‘2) ∈ ℝ+ → 0 < (log‘2))
336334, 335ax-mp 5 . . . . 5 0 < (log‘2)
337180, 319, 36, 336ltmul1ii 12175 . . . 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)))
338331, 337mpbi 229 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2))
33937mullidi 11251 . . . 4 (1 · (log‘2)) = (log‘2)
340339eqcomi 2734 . . 3 (log‘2) = (1 · (log‘2))
341338, 166, 3403brtr4i 5179 . 2 (𝐹64) < (log‘2)
342182, 341pm3.2i 469 1 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1533  wcel 2098  wne 2929   class class class wbr 5149  cmpt 5232  cfv 6549  (class class class)co 7419  cc 11138  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145   < clt 11280  cle 11281  cmin 11476   / cdiv 11903  cn 12245  2c2 12300  3c3 12301  4c4 12302  5c5 12303  6c6 12304  7c7 12305  8c8 12306  9c9 12307  0cn0 12505  cz 12591  cdc 12710  +crp 13009  cexp 14062  csqrt 15216  logclog 26533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9666  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218  ax-addf 11219
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-fi 9436  df-sup 9467  df-inf 9468  df-oi 9535  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12506  df-z 12592  df-dec 12711  df-uz 12856  df-q 12966  df-rp 13010  df-xneg 13127  df-xadd 13128  df-xmul 13129  df-ioo 13363  df-ioc 13364  df-ico 13365  df-icc 13366  df-fz 13520  df-fzo 13663  df-fl 13793  df-mod 13871  df-seq 14003  df-exp 14063  df-fac 14269  df-bc 14298  df-hash 14326  df-shft 15050  df-cj 15082  df-re 15083  df-im 15084  df-sqrt 15218  df-abs 15219  df-limsup 15451  df-clim 15468  df-rlim 15469  df-sum 15669  df-ef 16047  df-sin 16049  df-cos 16050  df-pi 16052  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-starv 17251  df-sca 17252  df-vsca 17253  df-ip 17254  df-tset 17255  df-ple 17256  df-ds 17258  df-unif 17259  df-hom 17260  df-cco 17261  df-rest 17407  df-topn 17408  df-0g 17426  df-gsum 17427  df-topgen 17428  df-pt 17429  df-prds 17432  df-xrs 17487  df-qtop 17492  df-imas 17493  df-xps 17495  df-mre 17569  df-mrc 17570  df-acs 17572  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18744  df-mulg 19032  df-cntz 19280  df-cmn 19749  df-psmet 21288  df-xmet 21289  df-met 21290  df-bl 21291  df-mopn 21292  df-fbas 21293  df-fg 21294  df-cnfld 21297  df-top 22840  df-topon 22857  df-topsp 22879  df-bases 22893  df-cld 22967  df-ntr 22968  df-cls 22969  df-nei 23046  df-lp 23084  df-perf 23085  df-cn 23175  df-cnp 23176  df-haus 23263  df-tx 23510  df-hmeo 23703  df-fil 23794  df-fm 23886  df-flim 23887  df-flf 23888  df-xms 24270  df-ms 24271  df-tms 24272  df-cncf 24842  df-limc 25839  df-dv 25840  df-log 26535
This theorem is referenced by:  bposlem9  27270
  Copyright terms: Public domain W3C validator