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

Theorem bposlem8 26639
Description: Lemma for bpos 26641. 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 12434 . . . . 5 6 ∈ ℕ0
2 4nn 12236 . . . . 5 4 ∈ ℕ
31, 2decnncl 12638 . . . 4 64 ∈ ℕ
4 fveq2 6842 . . . . . . . . . . . . . 14 (𝑛 = 64 → (√‘𝑛) = (√‘64))
5 8cn 12250 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
65sqvali 14084 . . . . . . . . . . . . . . . . 17 (8↑2) = (8 · 8)
7 8t8e64 12739 . . . . . . . . . . . . . . . . 17 (8 · 8) = 64
86, 7eqtri 2764 . . . . . . . . . . . . . . . 16 (8↑2) = 64
98fveq2i 6845 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = (√‘64)
10 0re 11157 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
11 8re 12249 . . . . . . . . . . . . . . . . 17 8 ∈ ℝ
12 8pos 12265 . . . . . . . . . . . . . . . . 17 0 < 8
1310, 11, 12ltleii 11278 . . . . . . . . . . . . . . . 16 0 ≤ 8
1411sqrtsqi 15259 . . . . . . . . . . . . . . . 16 (0 ≤ 8 → (√‘(8↑2)) = 8)
1513, 14ax-mp 5 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = 8
169, 15eqtr3i 2766 . . . . . . . . . . . . . 14 (√‘64) = 8
174, 16eqtrdi 2792 . . . . . . . . . . . . 13 (𝑛 = 64 → (√‘𝑛) = 8)
1817fveq2d 6846 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19 8nn 12248 . . . . . . . . . . . . 13 8 ∈ ℕ
20 nnrp 12926 . . . . . . . . . . . . 13 (8 ∈ ℕ → 8 ∈ ℝ+)
21 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑥 = 8 → (log‘𝑥) = (log‘8))
22 cu2 14104 . . . . . . . . . . . . . . . . . . 19 (2↑3) = 8
2322fveq2i 6845 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (log‘8)
24 2rp 12920 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
25 3z 12536 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℤ
26 relogexp 25951 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
2724, 25, 26mp2an 690 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (3 · (log‘2))
2823, 27eqtr3i 2766 . . . . . . . . . . . . . . . . 17 (log‘8) = (3 · (log‘2))
2921, 28eqtrdi 2792 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → 𝑥 = 8)
3129, 30oveq12d 7375 . . . . . . . . . . . . . . 15 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32 3cn 12234 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
33 2nn 12226 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
34 nnrp 12926 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℕ → 2 ∈ ℝ+)
35 relogcl 25931 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3633, 34, 35mp2b 10 . . . . . . . . . . . . . . . . 17 (log‘2) ∈ ℝ
3736recni 11169 . . . . . . . . . . . . . . . 16 (log‘2) ∈ ℂ
3819nnne0i 12193 . . . . . . . . . . . . . . . 16 8 ≠ 0
3932, 37, 5, 38div23i 11913 . . . . . . . . . . . . . . 15 ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
4031, 39eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41 bposlem7.2 . . . . . . . . . . . . . 14 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
42 ovex 7390 . . . . . . . . . . . . . 14 ((3 / 8) · (log‘2)) ∈ V
4340, 41, 42fvmpt 6948 . . . . . . . . . . . . 13 (8 ∈ ℝ+ → (𝐺‘8) = ((3 / 8) · (log‘2)))
4419, 20, 43mp2b 10 . . . . . . . . . . . 12 (𝐺‘8) = ((3 / 8) · (log‘2))
4518, 44eqtrdi 2792 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
4645oveq2d 7373 . . . . . . . . . 10 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47 sqrt2re 16132 . . . . . . . . . . . . 13 (√‘2) ∈ ℝ
4847recni 11169 . . . . . . . . . . . 12 (√‘2) ∈ ℂ
4932, 5, 38divcli 11897 . . . . . . . . . . . 12 (3 / 8) ∈ ℂ
5048, 49, 37mulassi 11166 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51 4cn 12238 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
5248, 51, 48mul12i 11350 . . . . . . . . . . . . . . 15 ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53 2re 12227 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
54 0le2 12255 . . . . . . . . . . . . . . . . 17 0 ≤ 2
55 remsqsqrt 15141 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
5653, 54, 55mp2an 690 . . . . . . . . . . . . . . . 16 ((√‘2) · (√‘2)) = 2
5756oveq2i 7368 . . . . . . . . . . . . . . 15 (4 · ((√‘2) · (√‘2))) = (4 · 2)
58 4t2e8 12321 . . . . . . . . . . . . . . 15 (4 · 2) = 8
5952, 57, 583eqtri 2768 . . . . . . . . . . . . . 14 ((√‘2) · (4 · (√‘2))) = 8
6059oveq2i 7368 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
6151, 48mulcli 11162 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ∈ ℂ
62 nnrp 12926 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
632, 62ax-mp 5 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ+
64 rpsqrtcl 15149 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (√‘2) ∈ ℝ+)
6533, 34, 64mp2b 10 . . . . . . . . . . . . . . . . 17 (√‘2) ∈ ℝ+
66 rpmulcl 12938 . . . . . . . . . . . . . . . . 17 ((4 ∈ ℝ+ ∧ (√‘2) ∈ ℝ+) → (4 · (√‘2)) ∈ ℝ+)
6763, 65, 66mp2an 690 . . . . . . . . . . . . . . . 16 (4 · (√‘2)) ∈ ℝ+
68 rpne0 12931 . . . . . . . . . . . . . . . 16 ((4 · (√‘2)) ∈ ℝ+ → (4 · (√‘2)) ≠ 0)
6967, 68ax-mp 5 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ≠ 0
70 rpne0 12931 . . . . . . . . . . . . . . . 16 ((√‘2) ∈ ℝ+ → (√‘2) ≠ 0)
7124, 64, 70mp2b 10 . . . . . . . . . . . . . . 15 (√‘2) ≠ 0
72 divcan5 11857 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7332, 72mp3an1 1448 . . . . . . . . . . . . . . 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 12261 . . . . . . . . . . . . . . 15 4 ≠ 0
76 divdiv1 11866 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7732, 76mp3an1 1448 . . . . . . . . . . . . . . 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 2767 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
8048, 32, 5, 38divassi 11911 . . . . . . . . . . . . 13 (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
8160, 79, 803eqtr3ri 2773 . . . . . . . . . . . 12 ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
8281oveq1i 7367 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
8350, 82eqtr3i 2766 . . . . . . . . . 10 ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
8446, 83eqtrdi 2792 . . . . . . . . 9 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85 oveq1 7364 . . . . . . . . . . . . . 14 (𝑛 = 64 → (𝑛 / 2) = (64 / 2))
86 df-6 12220 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
8786oveq2i 7368 . . . . . . . . . . . . . . . . 17 (2↑6) = (2↑(5 + 1))
88 2exp6 16959 . . . . . . . . . . . . . . . . 17 (2↑6) = 64
89 2cn 12228 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
90 5nn0 12433 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ0
91 expp1 13974 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 5 ∈ ℕ0) → (2↑(5 + 1)) = ((2↑5) · 2))
9289, 90, 91mp2an 690 . . . . . . . . . . . . . . . . 17 (2↑(5 + 1)) = ((2↑5) · 2)
9387, 88, 923eqtr3i 2772 . . . . . . . . . . . . . . . 16 64 = ((2↑5) · 2)
9493oveq1i 7367 . . . . . . . . . . . . . . 15 (64 / 2) = (((2↑5) · 2) / 2)
95 nnexpcl 13980 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ ∧ 5 ∈ ℕ0) → (2↑5) ∈ ℕ)
9633, 90, 95mp2an 690 . . . . . . . . . . . . . . . . 17 (2↑5) ∈ ℕ
9796nncni 12163 . . . . . . . . . . . . . . . 16 (2↑5) ∈ ℂ
98 2ne0 12257 . . . . . . . . . . . . . . . 16 2 ≠ 0
9997, 89, 98divcan4i 11902 . . . . . . . . . . . . . . 15 (((2↑5) · 2) / 2) = (2↑5)
10094, 99eqtri 2764 . . . . . . . . . . . . . 14 (64 / 2) = (2↑5)
10185, 100eqtrdi 2792 . . . . . . . . . . . . 13 (𝑛 = 64 → (𝑛 / 2) = (2↑5))
102101fveq2d 6846 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103 nnrp 12926 . . . . . . . . . . . . 13 ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ+)
104 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105 5nn 12239 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℕ
106105nnzi 12527 . . . . . . . . . . . . . . . . . 18 5 ∈ ℤ
107 relogexp 25951 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
10824, 106, 107mp2an 690 . . . . . . . . . . . . . . . . 17 (log‘(2↑5)) = (5 · (log‘2))
109104, 108eqtrdi 2792 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → 𝑥 = (2↑5))
111109, 110oveq12d 7375 . . . . . . . . . . . . . . 15 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112 5cn 12241 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
11396nnne0i 12193 . . . . . . . . . . . . . . . 16 (2↑5) ≠ 0
114112, 37, 97, 113div23i 11913 . . . . . . . . . . . . . . 15 ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115111, 114eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116 ovex 7390 . . . . . . . . . . . . . 14 ((5 / (2↑5)) · (log‘2)) ∈ V
117115, 41, 116fvmpt 6948 . . . . . . . . . . . . 13 ((2↑5) ∈ ℝ+ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
11896, 103, 117mp2b 10 . . . . . . . . . . . 12 (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
119102, 118eqtrdi 2792 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120119oveq2d 7373 . . . . . . . . . 10 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121 9cn 12253 . . . . . . . . . . . 12 9 ∈ ℂ
122121, 51, 75divcli 11897 . . . . . . . . . . 11 (9 / 4) ∈ ℂ
123112, 97, 113divcli 11897 . . . . . . . . . . 11 (5 / (2↑5)) ∈ ℂ
124122, 123, 37mulassi 11166 . . . . . . . . . 10 (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125120, 124eqtr4di 2794 . . . . . . . . 9 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
12684, 125oveq12d 7375 . . . . . . . 8 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
12732, 51, 75divcli 11897 . . . . . . . . . 10 (3 / 4) ∈ ℂ
128127, 48, 71divcli 11897 . . . . . . . . 9 ((3 / 4) / (√‘2)) ∈ ℂ
129122, 123mulcli 11162 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130128, 129, 37adddiri 11168 . . . . . . . 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 2794 . . . . . . 7 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132 oveq2 7365 . . . . . . . . . . 11 (𝑛 = 64 → (2 · 𝑛) = (2 · 64))
133132fveq2d 6846 . . . . . . . . . 10 (𝑛 = 64 → (√‘(2 · 𝑛)) = (√‘(2 · 64)))
1343nnrei 12162 . . . . . . . . . . . 12 64 ∈ ℝ
1353nngt0i 12192 . . . . . . . . . . . . 13 0 < 64
13610, 134, 135ltleii 11278 . . . . . . . . . . . 12 0 ≤ 64
13753, 134, 54, 136sqrtmulii 15271 . . . . . . . . . . 11 (√‘(2 · 64)) = ((√‘2) · (√‘64))
13816oveq2i 7368 . . . . . . . . . . 11 ((√‘2) · (√‘64)) = ((√‘2) · 8)
139137, 138eqtri 2764 . . . . . . . . . 10 (√‘(2 · 64)) = ((√‘2) · 8)
140133, 139eqtrdi 2792 . . . . . . . . 9 (𝑛 = 64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141140oveq2d 7373 . . . . . . . 8 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
14248, 5mulcli 11162 . . . . . . . . . 10 ((√‘2) · 8) ∈ ℂ
143 rpmulcl 12938 . . . . . . . . . . . 12 (((√‘2) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((√‘2) · 8) ∈ ℝ+)
14465, 20, 143sylancr 587 . . . . . . . . . . 11 (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ+)
145 rpne0 12931 . . . . . . . . . . 11 (((√‘2) · 8) ∈ ℝ+ → ((√‘2) · 8) ≠ 0)
14619, 144, 145mp2b 10 . . . . . . . . . 10 ((√‘2) · 8) ≠ 0
147 divrec2 11830 . . . . . . . . . 10 (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
14837, 142, 146, 147mp3an 1461 . . . . . . . . 9 ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
14948, 5mulcomi 11163 . . . . . . . . . . . 12 ((√‘2) · 8) = (8 · (√‘2))
150149oveq2i 7368 . . . . . . . . . . 11 (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151 recdiv2 11868 . . . . . . . . . . . 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 2767 . . . . . . . . . 10 (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154153oveq1i 7367 . . . . . . . . 9 ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155148, 154eqtri 2764 . . . . . . . 8 ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156141, 155eqtrdi 2792 . . . . . . 7 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157131, 156oveq12d 7375 . . . . . 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 11161 . . . . . . 7 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
1595, 38reccli 11885 . . . . . . . 8 (1 / 8) ∈ ℂ
160159, 48, 71divcli 11897 . . . . . . 7 ((1 / 8) / (√‘2)) ∈ ℂ
161158, 160, 37adddiri 11168 . . . . . 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 2794 . . . . 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 7390 . . . . 5 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165162, 163, 164fvmpt 6948 . . . 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 12233 . . . . . . . 8 3 ∈ ℝ
168 4re 12237 . . . . . . . 8 4 ∈ ℝ
169167, 168, 75redivcli 11922 . . . . . . 7 (3 / 4) ∈ ℝ
170169, 47, 71redivcli 11922 . . . . . 6 ((3 / 4) / (√‘2)) ∈ ℝ
171 9re 12252 . . . . . . . 8 9 ∈ ℝ
172171, 168, 75redivcli 11922 . . . . . . 7 (9 / 4) ∈ ℝ
173 5re 12240 . . . . . . . 8 5 ∈ ℝ
17496nnrei 12162 . . . . . . . 8 (2↑5) ∈ ℝ
175173, 174, 113redivcli 11922 . . . . . . 7 (5 / (2↑5)) ∈ ℝ
176172, 175remulcli 11171 . . . . . 6 ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177170, 176readdcli 11170 . . . . 5 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
17811, 38rereccli 11920 . . . . . 6 (1 / 8) ∈ ℝ
179178, 47, 71redivcli 11922 . . . . 5 ((1 / 8) / (√‘2)) ∈ ℝ
180177, 179readdcli 11170 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181180, 36remulcli 11171 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182166, 181eqeltri 2834 . 2 (𝐹64) ∈ ℝ
183128, 129, 160add32i 11378 . . . . . 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 12244 . . . . . . . . . . 11 6 ∈ ℂ
185 ax-1cn 11109 . . . . . . . . . . 11 1 ∈ ℂ
186184, 185, 5, 38divdiri 11912 . . . . . . . . . 10 ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187 df-7 12221 . . . . . . . . . . 11 7 = (6 + 1)
188187oveq1i 7367 . . . . . . . . . 10 (7 / 8) = ((6 + 1) / 8)
189 divcan5 11857 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19032, 189mp3an1 1448 . . . . . . . . . . . . 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 12319 . . . . . . . . . . . . . 14 (3 · 2) = 6
19332, 89, 192mulcomli 11164 . . . . . . . . . . . . 13 (2 · 3) = 6
19451, 89, 58mulcomli 11164 . . . . . . . . . . . . 13 (2 · 4) = 8
195193, 194oveq12i 7369 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (6 / 8)
196191, 195eqtr3i 2766 . . . . . . . . . . 11 (3 / 4) = (6 / 8)
197196oveq1i 7367 . . . . . . . . . 10 ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
198186, 188, 1973eqtr4ri 2775 . . . . . . . . 9 ((3 / 4) + (1 / 8)) = (7 / 8)
199198oveq1i 7367 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
200127, 159, 48, 71divdiri 11912 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
201 7cn 12247 . . . . . . . . 9 7 ∈ ℂ
202201, 5, 48, 38, 71divdiv32i 11910 . . . . . . . 8 ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
203199, 200, 2023eqtr3i 2772 . . . . . . 7 (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
204203oveq1i 7367 . . . . . 6 ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205183, 204eqtri 2764 . . . . 5 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
206 4nn0 12432 . . . . . . . . . . . 12 4 ∈ ℕ0
207 9nn0 12437 . . . . . . . . . . . 12 9 ∈ ℕ0
208 0nn0 12428 . . . . . . . . . . . 12 0 ∈ ℕ0
209 9lt10 12749 . . . . . . . . . . . 12 9 < 10
210 4lt5 12330 . . . . . . . . . . . 12 4 < 5
211206, 90, 207, 208, 209, 210decltc 12647 . . . . . . . . . . 11 49 < 50
212 7t7e49 12732 . . . . . . . . . . 11 (7 · 7) = 49
21356oveq1i 7367 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
21448, 48, 112, 112mul4i 11352 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
215 5t2e10 12718 . . . . . . . . . . . . . . 15 (5 · 2) = 10
216112, 89, 215mulcomli 11164 . . . . . . . . . . . . . 14 (2 · 5) = 10
217216oveq1i 7367 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (10 · 5)
21889, 112, 112mulassi 11166 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (2 · (5 · 5))
21990dec0u 12639 . . . . . . . . . . . . 13 (10 · 5) = 50
220217, 218, 2193eqtr3i 2772 . . . . . . . . . . . 12 (2 · (5 · 5)) = 50
221213, 214, 2203eqtr3i 2772 . . . . . . . . . . 11 (((√‘2) · 5) · ((√‘2) · 5)) = 50
222211, 212, 2213brtr4i 5135 . . . . . . . . . 10 (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
223 7re 12246 . . . . . . . . . . . 12 7 ∈ ℝ
224 7pos 12264 . . . . . . . . . . . 12 0 < 7
22510, 223, 224ltleii 11278 . . . . . . . . . . 11 0 ≤ 7
226 nnrp 12926 . . . . . . . . . . . . . 14 (5 ∈ ℕ → 5 ∈ ℝ+)
227105, 226ax-mp 5 . . . . . . . . . . . . 13 5 ∈ ℝ+
228 rpmulcl 12938 . . . . . . . . . . . . 13 (((√‘2) ∈ ℝ+ ∧ 5 ∈ ℝ+) → ((√‘2) · 5) ∈ ℝ+)
22965, 227, 228mp2an 690 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ+
230 rpge0 12928 . . . . . . . . . . . 12 (((√‘2) · 5) ∈ ℝ+ → 0 ≤ ((√‘2) · 5))
231229, 230ax-mp 5 . . . . . . . . . . 11 0 ≤ ((√‘2) · 5)
232 rpre 12923 . . . . . . . . . . . . 13 (((√‘2) · 5) ∈ ℝ+ → ((√‘2) · 5) ∈ ℝ)
233229, 232ax-mp 5 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ
234223, 233lt2msqi 12067 . . . . . . . . . . 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 12927 . . . . . . . . . . 11 ((√‘2) ∈ ℝ+ → 0 < (√‘2))
23824, 64, 237mp2b 10 . . . . . . . . . 10 0 < (√‘2)
239 ltdivmul 12030 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240223, 173, 239mp3an12 1451 . . . . . . . . . 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 11922 . . . . . . . . 9 (7 / (√‘2)) ∈ ℝ
244243, 173, 11, 12ltdiv1ii 12084 . . . . . . . 8 ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
245242, 244mpbi 229 . . . . . . 7 ((7 / (√‘2)) / 8) < (5 / 8)
246 divsubdir 11849 . . . . . . . . . . 11 ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2475, 32, 246mp3an12 1451 . . . . . . . . . 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 12310 . . . . . . . . . . . 12 (5 + 3) = 8
250249oveq1i 7367 . . . . . . . . . . 11 ((5 + 3) − 3) = (8 − 3)
251112, 32pncan3oi 11417 . . . . . . . . . . 11 ((5 + 3) − 3) = 5
252250, 251eqtr3i 2766 . . . . . . . . . 10 (8 − 3) = 5
253252oveq1i 7367 . . . . . . . . 9 ((8 − 3) / 8) = (5 / 8)
2545, 38dividi 11888 . . . . . . . . . 10 (8 / 8) = 1
255254oveq1i 7367 . . . . . . . . 9 ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
256248, 253, 2553eqtr3ri 2773 . . . . . . . 8 (1 − (3 / 8)) = (5 / 8)
257 5lt8 12347 . . . . . . . . . . . . 13 5 < 8
25811, 173remulcli 11171 . . . . . . . . . . . . . 14 (8 · 5) ∈ ℝ
259173, 11, 258ltadd2i 11286 . . . . . . . . . . . . 13 (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
260257, 259mpbi 229 . . . . . . . . . . . 12 ((8 · 5) + 5) < ((8 · 5) + 8)
261 df-9 12223 . . . . . . . . . . . . . 14 9 = (8 + 1)
262261oveq1i 7367 . . . . . . . . . . . . 13 (9 · 5) = ((8 + 1) · 5)
2635, 185, 112adddiri 11168 . . . . . . . . . . . . 13 ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
264112mulid2i 11160 . . . . . . . . . . . . . 14 (1 · 5) = 5
265264oveq2i 7368 . . . . . . . . . . . . 13 ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
266262, 263, 2653eqtri 2768 . . . . . . . . . . . 12 (9 · 5) = ((8 · 5) + 5)
26786oveq2i 7368 . . . . . . . . . . . . 13 (8 · 6) = (8 · (5 + 1))
2685, 112, 185adddii 11167 . . . . . . . . . . . . 13 (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
2695mulid1i 11159 . . . . . . . . . . . . . 14 (8 · 1) = 8
270269oveq2i 7368 . . . . . . . . . . . . 13 ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
271267, 268, 2703eqtri 2768 . . . . . . . . . . . 12 (8 · 6) = ((8 · 5) + 8)
272260, 266, 2713brtr4i 5135 . . . . . . . . . . 11 (9 · 5) < (8 · 6)
273171, 173remulcli 11171 . . . . . . . . . . . 12 (9 · 5) ∈ ℝ
274 6re 12243 . . . . . . . . . . . . 13 6 ∈ ℝ
27511, 274remulcli 11171 . . . . . . . . . . . 12 (8 · 6) ∈ ℝ
276168, 174remulcli 11171 . . . . . . . . . . . 12 (4 · (2↑5)) ∈ ℝ
2772, 96nnmulcli 12178 . . . . . . . . . . . . 13 (4 · (2↑5)) ∈ ℕ
278277nngt0i 12192 . . . . . . . . . . . 12 0 < (4 · (2↑5))
279273, 275, 276, 278ltdiv1ii 12084 . . . . . . . . . . 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 11915 . . . . . . . . . 10 ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
282 nnexpcl 13980 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈ ℕ)
28333, 206, 282mp2an 690 . . . . . . . . . . . . 13 (2↑4) ∈ ℕ
284283nncni 12163 . . . . . . . . . . . 12 (2↑4) ∈ ℂ
285283nnne0i 12193 . . . . . . . . . . . 12 (2↑4) ≠ 0
286 divcan5 11857 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
28732, 286mp3an1 1448 . . . . . . . . . . . 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 12218 . . . . . . . . . . . . . . . 16 4 = (3 + 1)
290289oveq2i 7368 . . . . . . . . . . . . . . 15 (2↑4) = (2↑(3 + 1))
291 3nn0 12431 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
292 expp1 13974 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 3 ∈ ℕ0) → (2↑(3 + 1)) = ((2↑3) · 2))
29389, 291, 292mp2an 690 . . . . . . . . . . . . . . 15 (2↑(3 + 1)) = ((2↑3) · 2)
29422oveq1i 7367 . . . . . . . . . . . . . . 15 ((2↑3) · 2) = (8 · 2)
295290, 293, 2943eqtri 2768 . . . . . . . . . . . . . 14 (2↑4) = (8 · 2)
296295oveq1i 7367 . . . . . . . . . . . . 13 ((2↑4) · 3) = ((8 · 2) · 3)
2975, 89, 32mulassi 11166 . . . . . . . . . . . . 13 ((8 · 2) · 3) = (8 · (2 · 3))
298193oveq2i 7368 . . . . . . . . . . . . 13 (8 · (2 · 3)) = (8 · 6)
299296, 297, 2983eqtri 2768 . . . . . . . . . . . 12 ((2↑4) · 3) = (8 · 6)
300 4p3e7 12307 . . . . . . . . . . . . . . . 16 (4 + 3) = 7
301 5p2e7 12309 . . . . . . . . . . . . . . . 16 (5 + 2) = 7
302112, 89addcomi 11346 . . . . . . . . . . . . . . . 16 (5 + 2) = (2 + 5)
303300, 301, 3023eqtr2i 2770 . . . . . . . . . . . . . . 15 (4 + 3) = (2 + 5)
304303oveq2i 7368 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = (2↑(2 + 5))
305 expadd 14010 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
30689, 206, 291, 305mp3an 1461 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = ((2↑4) · (2↑3))
307 2nn0 12430 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
308 expadd 14010 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 5 ∈ ℕ0) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
30989, 307, 90, 308mp3an 1461 . . . . . . . . . . . . . 14 (2↑(2 + 5)) = ((2↑2) · (2↑5))
310304, 306, 3093eqtr3i 2772 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
31122oveq2i 7368 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑4) · 8)
312 sq2 14101 . . . . . . . . . . . . . 14 (2↑2) = 4
313312oveq1i 7367 . . . . . . . . . . . . 13 ((2↑2) · (2↑5)) = (4 · (2↑5))
314310, 311, 3133eqtr3i 2772 . . . . . . . . . . . 12 ((2↑4) · 8) = (4 · (2↑5))
315299, 314oveq12i 7369 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
316288, 315eqtr3i 2766 . . . . . . . . . 10 (3 / 8) = ((8 · 6) / (4 · (2↑5)))
317280, 281, 3163brtr4i 5135 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) < (3 / 8)
318167, 11, 38redivcli 11922 . . . . . . . . . 10 (3 / 8) ∈ ℝ
319 1re 11155 . . . . . . . . . 10 1 ∈ ℝ
320 ltsub2 11652 . . . . . . . . . 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 1461 . . . . . . . . 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 5128 . . . . . . 7 (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
324243, 11, 38redivcli 11922 . . . . . . . 8 ((7 / (√‘2)) / 8) ∈ ℝ
325173, 11, 38redivcli 11922 . . . . . . . 8 (5 / 8) ∈ ℝ
326319, 176resubcli 11463 . . . . . . . 8 (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
327324, 325, 326lttri 11281 . . . . . . 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 11716 . . . . . 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 5126 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
332 1lt2 12324 . . . . . . 7 1 < 2
333 rplogcl 25959 . . . . . . 7 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
33453, 332, 333mp2an 690 . . . . . 6 (log‘2) ∈ ℝ+
335 rpgt0 12927 . . . . . 6 ((log‘2) ∈ ℝ+ → 0 < (log‘2))
336334, 335ax-mp 5 . . . . 5 0 < (log‘2)
337180, 319, 36, 336ltmul1ii 12083 . . . 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))
33937mulid2i 11160 . . . 4 (1 · (log‘2)) = (log‘2)
340339eqcomi 2745 . . 3 (log‘2) = (1 · (log‘2))
341338, 166, 3403brtr4i 5135 . 2 (𝐹64) < (log‘2)
342182, 341pm3.2i 471 1 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943   class class class wbr 5105  cmpt 5188  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  3c3 12209  4c4 12210  5c5 12211  6c6 12212  7c7 12213  8c8 12214  9c9 12215  0cn0 12413  cz 12499  cdc 12618  +crp 12915  cexp 13967  csqrt 15118  logclog 25910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-cos 15953  df-pi 15955  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231  df-log 25912
This theorem is referenced by:  bposlem9  26640
  Copyright terms: Public domain W3C validator