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

Theorem bposlem8 25061
Description: Lemma for bpos 25063. 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 11351 . . . . 5 6 ∈ ℕ0
2 4nn 11225 . . . . 5 4 ∈ ℕ
31, 2decnncl 11556 . . . 4 64 ∈ ℕ
4 fveq2 6229 . . . . . . . . . . . . . 14 (𝑛 = 64 → (√‘𝑛) = (√‘64))
5 8cn 11144 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
65sqvali 12983 . . . . . . . . . . . . . . . . 17 (8↑2) = (8 · 8)
7 8t8e64 11700 . . . . . . . . . . . . . . . . 17 (8 · 8) = 64
86, 7eqtri 2673 . . . . . . . . . . . . . . . 16 (8↑2) = 64
98fveq2i 6232 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = (√‘64)
10 0re 10078 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
11 8re 11143 . . . . . . . . . . . . . . . . 17 8 ∈ ℝ
12 8pos 11159 . . . . . . . . . . . . . . . . 17 0 < 8
1310, 11, 12ltleii 10198 . . . . . . . . . . . . . . . 16 0 ≤ 8
1411sqrtsqi 14158 . . . . . . . . . . . . . . . 16 (0 ≤ 8 → (√‘(8↑2)) = 8)
1513, 14ax-mp 5 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = 8
169, 15eqtr3i 2675 . . . . . . . . . . . . . 14 (√‘64) = 8
174, 16syl6eq 2701 . . . . . . . . . . . . 13 (𝑛 = 64 → (√‘𝑛) = 8)
1817fveq2d 6233 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19 8nn 11229 . . . . . . . . . . . . 13 8 ∈ ℕ
20 nnrp 11880 . . . . . . . . . . . . 13 (8 ∈ ℕ → 8 ∈ ℝ+)
21 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑥 = 8 → (log‘𝑥) = (log‘8))
22 cu2 13003 . . . . . . . . . . . . . . . . . . 19 (2↑3) = 8
2322fveq2i 6232 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (log‘8)
24 2rp 11875 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
25 3z 11448 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℤ
26 relogexp 24387 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
2724, 25, 26mp2an 708 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (3 · (log‘2))
2823, 27eqtr3i 2675 . . . . . . . . . . . . . . . . 17 (log‘8) = (3 · (log‘2))
2921, 28syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → 𝑥 = 8)
3129, 30oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32 3cn 11133 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
33 2nn 11223 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
34 nnrp 11880 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℕ → 2 ∈ ℝ+)
35 relogcl 24367 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3633, 34, 35mp2b 10 . . . . . . . . . . . . . . . . 17 (log‘2) ∈ ℝ
3736recni 10090 . . . . . . . . . . . . . . . 16 (log‘2) ∈ ℂ
3819nnne0i 11093 . . . . . . . . . . . . . . . 16 8 ≠ 0
3932, 37, 5, 38div23i 10821 . . . . . . . . . . . . . . 15 ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
4031, 39syl6eq 2701 . . . . . . . . . . . . . 14 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41 bposlem7.2 . . . . . . . . . . . . . 14 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
42 ovex 6718 . . . . . . . . . . . . . 14 ((3 / 8) · (log‘2)) ∈ V
4340, 41, 42fvmpt 6321 . . . . . . . . . . . . 13 (8 ∈ ℝ+ → (𝐺‘8) = ((3 / 8) · (log‘2)))
4419, 20, 43mp2b 10 . . . . . . . . . . . 12 (𝐺‘8) = ((3 / 8) · (log‘2))
4518, 44syl6eq 2701 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
4645oveq2d 6706 . . . . . . . . . 10 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47 sqrt2re 15024 . . . . . . . . . . . . 13 (√‘2) ∈ ℝ
4847recni 10090 . . . . . . . . . . . 12 (√‘2) ∈ ℂ
4932, 5, 38divcli 10805 . . . . . . . . . . . 12 (3 / 8) ∈ ℂ
5048, 49, 37mulassi 10087 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51 4cn 11136 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
5248, 51, 48mul12i 10269 . . . . . . . . . . . . . . 15 ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53 2re 11128 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
54 0le2 11149 . . . . . . . . . . . . . . . . 17 0 ≤ 2
55 remsqsqrt 14041 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
5653, 54, 55mp2an 708 . . . . . . . . . . . . . . . 16 ((√‘2) · (√‘2)) = 2
5756oveq2i 6701 . . . . . . . . . . . . . . 15 (4 · ((√‘2) · (√‘2))) = (4 · 2)
58 4t2e8 11219 . . . . . . . . . . . . . . 15 (4 · 2) = 8
5952, 57, 583eqtri 2677 . . . . . . . . . . . . . 14 ((√‘2) · (4 · (√‘2))) = 8
6059oveq2i 6701 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
6151, 48mulcli 10083 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ∈ ℂ
62 nnrp 11880 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
632, 62ax-mp 5 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ+
64 rpsqrtcl 14049 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (√‘2) ∈ ℝ+)
6533, 34, 64mp2b 10 . . . . . . . . . . . . . . . . 17 (√‘2) ∈ ℝ+
66 rpmulcl 11893 . . . . . . . . . . . . . . . . 17 ((4 ∈ ℝ+ ∧ (√‘2) ∈ ℝ+) → (4 · (√‘2)) ∈ ℝ+)
6763, 65, 66mp2an 708 . . . . . . . . . . . . . . . 16 (4 · (√‘2)) ∈ ℝ+
68 rpne0 11886 . . . . . . . . . . . . . . . 16 ((4 · (√‘2)) ∈ ℝ+ → (4 · (√‘2)) ≠ 0)
6967, 68ax-mp 5 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ≠ 0
70 rpne0 11886 . . . . . . . . . . . . . . . 16 ((√‘2) ∈ ℝ+ → (√‘2) ≠ 0)
7124, 64, 70mp2b 10 . . . . . . . . . . . . . . 15 (√‘2) ≠ 0
72 divcan5 10765 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7332, 72mp3an1 1451 . . . . . . . . . . . . . . 15 ((((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7461, 69, 48, 71, 73mp4an 709 . . . . . . . . . . . . . 14 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2)))
75 4ne0 11155 . . . . . . . . . . . . . . 15 4 ≠ 0
76 divdiv1 10774 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7732, 76mp3an1 1451 . . . . . . . . . . . . . . 15 (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7851, 75, 48, 71, 77mp4an 709 . . . . . . . . . . . . . 14 ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2)))
7974, 78eqtr4i 2676 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
8048, 32, 5, 38divassi 10819 . . . . . . . . . . . . 13 (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
8160, 79, 803eqtr3ri 2682 . . . . . . . . . . . 12 ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
8281oveq1i 6700 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
8350, 82eqtr3i 2675 . . . . . . . . . 10 ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
8446, 83syl6eq 2701 . . . . . . . . 9 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85 oveq1 6697 . . . . . . . . . . . . . 14 (𝑛 = 64 → (𝑛 / 2) = (64 / 2))
86 df-6 11121 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
8786oveq2i 6701 . . . . . . . . . . . . . . . . 17 (2↑6) = (2↑(5 + 1))
88 2exp6 15842 . . . . . . . . . . . . . . . . 17 (2↑6) = 64
89 2cn 11129 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
90 5nn0 11350 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ0
91 expp1 12907 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 5 ∈ ℕ0) → (2↑(5 + 1)) = ((2↑5) · 2))
9289, 90, 91mp2an 708 . . . . . . . . . . . . . . . . 17 (2↑(5 + 1)) = ((2↑5) · 2)
9387, 88, 923eqtr3i 2681 . . . . . . . . . . . . . . . 16 64 = ((2↑5) · 2)
9493oveq1i 6700 . . . . . . . . . . . . . . 15 (64 / 2) = (((2↑5) · 2) / 2)
95 nnexpcl 12913 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ ∧ 5 ∈ ℕ0) → (2↑5) ∈ ℕ)
9633, 90, 95mp2an 708 . . . . . . . . . . . . . . . . 17 (2↑5) ∈ ℕ
9796nncni 11068 . . . . . . . . . . . . . . . 16 (2↑5) ∈ ℂ
98 2ne0 11151 . . . . . . . . . . . . . . . 16 2 ≠ 0
9997, 89, 98divcan4i 10810 . . . . . . . . . . . . . . 15 (((2↑5) · 2) / 2) = (2↑5)
10094, 99eqtri 2673 . . . . . . . . . . . . . 14 (64 / 2) = (2↑5)
10185, 100syl6eq 2701 . . . . . . . . . . . . 13 (𝑛 = 64 → (𝑛 / 2) = (2↑5))
102101fveq2d 6233 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103 nnrp 11880 . . . . . . . . . . . . 13 ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ+)
104 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105 5nn 11226 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℕ
106105nnzi 11439 . . . . . . . . . . . . . . . . . 18 5 ∈ ℤ
107 relogexp 24387 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
10824, 106, 107mp2an 708 . . . . . . . . . . . . . . . . 17 (log‘(2↑5)) = (5 · (log‘2))
109104, 108syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → 𝑥 = (2↑5))
111109, 110oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112 5cn 11138 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
11396nnne0i 11093 . . . . . . . . . . . . . . . 16 (2↑5) ≠ 0
114112, 37, 97, 113div23i 10821 . . . . . . . . . . . . . . 15 ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115111, 114syl6eq 2701 . . . . . . . . . . . . . 14 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116 ovex 6718 . . . . . . . . . . . . . 14 ((5 / (2↑5)) · (log‘2)) ∈ V
117115, 41, 116fvmpt 6321 . . . . . . . . . . . . 13 ((2↑5) ∈ ℝ+ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
11896, 103, 117mp2b 10 . . . . . . . . . . . 12 (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
119102, 118syl6eq 2701 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120119oveq2d 6706 . . . . . . . . . 10 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121 9cn 11146 . . . . . . . . . . . 12 9 ∈ ℂ
122121, 51, 75divcli 10805 . . . . . . . . . . 11 (9 / 4) ∈ ℂ
123112, 97, 113divcli 10805 . . . . . . . . . . 11 (5 / (2↑5)) ∈ ℂ
124122, 123, 37mulassi 10087 . . . . . . . . . 10 (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125120, 124syl6eqr 2703 . . . . . . . . 9 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
12684, 125oveq12d 6708 . . . . . . . 8 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
12732, 51, 75divcli 10805 . . . . . . . . . 10 (3 / 4) ∈ ℂ
128127, 48, 71divcli 10805 . . . . . . . . 9 ((3 / 4) / (√‘2)) ∈ ℂ
129122, 123mulcli 10083 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130128, 129, 37adddiri 10089 . . . . . . . 8 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2)))
131126, 130syl6eqr 2703 . . . . . . 7 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132 oveq2 6698 . . . . . . . . . . 11 (𝑛 = 64 → (2 · 𝑛) = (2 · 64))
133132fveq2d 6233 . . . . . . . . . 10 (𝑛 = 64 → (√‘(2 · 𝑛)) = (√‘(2 · 64)))
1343nnrei 11067 . . . . . . . . . . . 12 64 ∈ ℝ
1353nngt0i 11092 . . . . . . . . . . . . 13 0 < 64
13610, 134, 135ltleii 10198 . . . . . . . . . . . 12 0 ≤ 64
13753, 134, 54, 136sqrtmulii 14170 . . . . . . . . . . 11 (√‘(2 · 64)) = ((√‘2) · (√‘64))
13816oveq2i 6701 . . . . . . . . . . 11 ((√‘2) · (√‘64)) = ((√‘2) · 8)
139137, 138eqtri 2673 . . . . . . . . . 10 (√‘(2 · 64)) = ((√‘2) · 8)
140133, 139syl6eq 2701 . . . . . . . . 9 (𝑛 = 64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141140oveq2d 6706 . . . . . . . 8 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
14248, 5mulcli 10083 . . . . . . . . . 10 ((√‘2) · 8) ∈ ℂ
143 rpmulcl 11893 . . . . . . . . . . . 12 (((√‘2) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((√‘2) · 8) ∈ ℝ+)
14465, 20, 143sylancr 696 . . . . . . . . . . 11 (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ+)
145 rpne0 11886 . . . . . . . . . . 11 (((√‘2) · 8) ∈ ℝ+ → ((√‘2) · 8) ≠ 0)
14619, 144, 145mp2b 10 . . . . . . . . . 10 ((√‘2) · 8) ≠ 0
147 divrec2 10740 . . . . . . . . . 10 (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
14837, 142, 146, 147mp3an 1464 . . . . . . . . 9 ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
14948, 5mulcomi 10084 . . . . . . . . . . . 12 ((√‘2) · 8) = (8 · (√‘2))
150149oveq2i 6701 . . . . . . . . . . 11 (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151 recdiv2 10776 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2))))
1525, 38, 48, 71, 151mp4an 709 . . . . . . . . . . 11 ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2)))
153150, 152eqtr4i 2676 . . . . . . . . . 10 (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154153oveq1i 6700 . . . . . . . . 9 ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155148, 154eqtri 2673 . . . . . . . 8 ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156141, 155syl6eq 2701 . . . . . . 7 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157131, 156oveq12d 6708 . . . . . 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 10082 . . . . . . 7 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
1595, 38reccli 10793 . . . . . . . 8 (1 / 8) ∈ ℂ
160159, 48, 71divcli 10805 . . . . . . 7 ((1 / 8) / (√‘2)) ∈ ℂ
161158, 160, 37adddiri 10089 . . . . . 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, 161syl6eqr 2703 . . . . 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 6718 . . . . 5 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165162, 163, 164fvmpt 6321 . . . 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 11132 . . . . . . . 8 3 ∈ ℝ
168 4re 11135 . . . . . . . 8 4 ∈ ℝ
169167, 168, 75redivcli 10830 . . . . . . 7 (3 / 4) ∈ ℝ
170169, 47, 71redivcli 10830 . . . . . 6 ((3 / 4) / (√‘2)) ∈ ℝ
171 9re 11145 . . . . . . . 8 9 ∈ ℝ
172171, 168, 75redivcli 10830 . . . . . . 7 (9 / 4) ∈ ℝ
173 5re 11137 . . . . . . . 8 5 ∈ ℝ
17496nnrei 11067 . . . . . . . 8 (2↑5) ∈ ℝ
175173, 174, 113redivcli 10830 . . . . . . 7 (5 / (2↑5)) ∈ ℝ
176172, 175remulcli 10092 . . . . . 6 ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177170, 176readdcli 10091 . . . . 5 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
17811, 38rereccli 10828 . . . . . 6 (1 / 8) ∈ ℝ
179178, 47, 71redivcli 10830 . . . . 5 ((1 / 8) / (√‘2)) ∈ ℝ
180177, 179readdcli 10091 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181180, 36remulcli 10092 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182166, 181eqeltri 2726 . 2 (𝐹64) ∈ ℝ
183128, 129, 160add32i 10297 . . . . . 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 11140 . . . . . . . . . . 11 6 ∈ ℂ
185 ax-1cn 10032 . . . . . . . . . . 11 1 ∈ ℂ
186184, 185, 5, 38divdiri 10820 . . . . . . . . . 10 ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187 df-7 11122 . . . . . . . . . . 11 7 = (6 + 1)
188187oveq1i 6700 . . . . . . . . . 10 (7 / 8) = ((6 + 1) / 8)
189 divcan5 10765 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19032, 189mp3an1 1451 . . . . . . . . . . . . 13 (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19151, 75, 89, 98, 190mp4an 709 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (3 / 4)
192 3t2e6 11217 . . . . . . . . . . . . . 14 (3 · 2) = 6
19332, 89, 192mulcomli 10085 . . . . . . . . . . . . 13 (2 · 3) = 6
19451, 89, 58mulcomli 10085 . . . . . . . . . . . . 13 (2 · 4) = 8
195193, 194oveq12i 6702 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (6 / 8)
196191, 195eqtr3i 2675 . . . . . . . . . . 11 (3 / 4) = (6 / 8)
197196oveq1i 6700 . . . . . . . . . 10 ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
198186, 188, 1973eqtr4ri 2684 . . . . . . . . 9 ((3 / 4) + (1 / 8)) = (7 / 8)
199198oveq1i 6700 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
200127, 159, 48, 71divdiri 10820 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
201 7cn 11142 . . . . . . . . 9 7 ∈ ℂ
202201, 5, 48, 38, 71divdiv32i 10818 . . . . . . . 8 ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
203199, 200, 2023eqtr3i 2681 . . . . . . 7 (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
204203oveq1i 6700 . . . . . 6 ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205183, 204eqtri 2673 . . . . 5 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
206 4nn0 11349 . . . . . . . . . . . 12 4 ∈ ℕ0
207 9nn0 11354 . . . . . . . . . . . 12 9 ∈ ℕ0
208 0nn0 11345 . . . . . . . . . . . 12 0 ∈ ℕ0
209 9lt10 11711 . . . . . . . . . . . 12 9 < 10
210 4lt5 11238 . . . . . . . . . . . 12 4 < 5
211206, 90, 207, 208, 209, 210decltc 11570 . . . . . . . . . . 11 49 < 50
212 7t7e49 11691 . . . . . . . . . . 11 (7 · 7) = 49
21356oveq1i 6700 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
21448, 48, 112, 112mul4i 10271 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
215 5t2e10 11672 . . . . . . . . . . . . . . 15 (5 · 2) = 10
216112, 89, 215mulcomli 10085 . . . . . . . . . . . . . 14 (2 · 5) = 10
217216oveq1i 6700 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (10 · 5)
21889, 112, 112mulassi 10087 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (2 · (5 · 5))
21990dec0u 11558 . . . . . . . . . . . . 13 (10 · 5) = 50
220217, 218, 2193eqtr3i 2681 . . . . . . . . . . . 12 (2 · (5 · 5)) = 50
221213, 214, 2203eqtr3i 2681 . . . . . . . . . . 11 (((√‘2) · 5) · ((√‘2) · 5)) = 50
222211, 212, 2213brtr4i 4715 . . . . . . . . . 10 (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
223 7re 11141 . . . . . . . . . . . 12 7 ∈ ℝ
224 7pos 11158 . . . . . . . . . . . 12 0 < 7
22510, 223, 224ltleii 10198 . . . . . . . . . . 11 0 ≤ 7
226 nnrp 11880 . . . . . . . . . . . . . 14 (5 ∈ ℕ → 5 ∈ ℝ+)
227105, 226ax-mp 5 . . . . . . . . . . . . 13 5 ∈ ℝ+
228 rpmulcl 11893 . . . . . . . . . . . . 13 (((√‘2) ∈ ℝ+ ∧ 5 ∈ ℝ+) → ((√‘2) · 5) ∈ ℝ+)
22965, 227, 228mp2an 708 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ+
230 rpge0 11883 . . . . . . . . . . . 12 (((√‘2) · 5) ∈ ℝ+ → 0 ≤ ((√‘2) · 5))
231229, 230ax-mp 5 . . . . . . . . . . 11 0 ≤ ((√‘2) · 5)
232 rpre 11877 . . . . . . . . . . . . 13 (((√‘2) · 5) ∈ ℝ+ → ((√‘2) · 5) ∈ ℝ)
233229, 232ax-mp 5 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ
234223, 233lt2msqi 10974 . . . . . . . . . . 11 ((0 ≤ 7 ∧ 0 ≤ ((√‘2) · 5)) → (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))))
235225, 231, 234mp2an 708 . . . . . . . . . 10 (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5)))
236222, 235mpbir 221 . . . . . . . . 9 7 < ((√‘2) · 5)
237 rpgt0 11882 . . . . . . . . . . 11 ((√‘2) ∈ ℝ+ → 0 < (√‘2))
23824, 64, 237mp2b 10 . . . . . . . . . 10 0 < (√‘2)
239 ltdivmul 10936 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240223, 173, 239mp3an12 1454 . . . . . . . . . 10 (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
24147, 238, 240mp2an 708 . . . . . . . . 9 ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
242236, 241mpbir 221 . . . . . . . 8 (7 / (√‘2)) < 5
243223, 47, 71redivcli 10830 . . . . . . . . 9 (7 / (√‘2)) ∈ ℝ
244243, 173, 11, 12ltdiv1ii 10991 . . . . . . . 8 ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
245242, 244mpbi 220 . . . . . . 7 ((7 / (√‘2)) / 8) < (5 / 8)
246 divsubdir 10759 . . . . . . . . . . 11 ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2475, 32, 246mp3an12 1454 . . . . . . . . . 10 ((8 ∈ ℂ ∧ 8 ≠ 0) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2485, 38, 247mp2an 708 . . . . . . . . 9 ((8 − 3) / 8) = ((8 / 8) − (3 / 8))
249 5p3e8 11204 . . . . . . . . . . . 12 (5 + 3) = 8
250249oveq1i 6700 . . . . . . . . . . 11 ((5 + 3) − 3) = (8 − 3)
251112, 32pncan3oi 10335 . . . . . . . . . . 11 ((5 + 3) − 3) = 5
252250, 251eqtr3i 2675 . . . . . . . . . 10 (8 − 3) = 5
253252oveq1i 6700 . . . . . . . . 9 ((8 − 3) / 8) = (5 / 8)
2545, 38dividi 10796 . . . . . . . . . 10 (8 / 8) = 1
255254oveq1i 6700 . . . . . . . . 9 ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
256248, 253, 2553eqtr3ri 2682 . . . . . . . 8 (1 − (3 / 8)) = (5 / 8)
257 5lt8 11255 . . . . . . . . . . . . 13 5 < 8
25811, 173remulcli 10092 . . . . . . . . . . . . . 14 (8 · 5) ∈ ℝ
259173, 11, 258ltadd2i 10206 . . . . . . . . . . . . 13 (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
260257, 259mpbi 220 . . . . . . . . . . . 12 ((8 · 5) + 5) < ((8 · 5) + 8)
261 df-9 11124 . . . . . . . . . . . . . 14 9 = (8 + 1)
262261oveq1i 6700 . . . . . . . . . . . . 13 (9 · 5) = ((8 + 1) · 5)
2635, 185, 112adddiri 10089 . . . . . . . . . . . . 13 ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
264112mulid2i 10081 . . . . . . . . . . . . . 14 (1 · 5) = 5
265264oveq2i 6701 . . . . . . . . . . . . 13 ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
266262, 263, 2653eqtri 2677 . . . . . . . . . . . 12 (9 · 5) = ((8 · 5) + 5)
26786oveq2i 6701 . . . . . . . . . . . . 13 (8 · 6) = (8 · (5 + 1))
2685, 112, 185adddii 10088 . . . . . . . . . . . . 13 (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
2695mulid1i 10080 . . . . . . . . . . . . . 14 (8 · 1) = 8
270269oveq2i 6701 . . . . . . . . . . . . 13 ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
271267, 268, 2703eqtri 2677 . . . . . . . . . . . 12 (8 · 6) = ((8 · 5) + 8)
272260, 266, 2713brtr4i 4715 . . . . . . . . . . 11 (9 · 5) < (8 · 6)
273171, 173remulcli 10092 . . . . . . . . . . . 12 (9 · 5) ∈ ℝ
274 6re 11139 . . . . . . . . . . . . 13 6 ∈ ℝ
27511, 274remulcli 10092 . . . . . . . . . . . 12 (8 · 6) ∈ ℝ
276168, 174remulcli 10092 . . . . . . . . . . . 12 (4 · (2↑5)) ∈ ℝ
2772, 96nnmulcli 11082 . . . . . . . . . . . . 13 (4 · (2↑5)) ∈ ℕ
278277nngt0i 11092 . . . . . . . . . . . 12 0 < (4 · (2↑5))
279273, 275, 276, 278ltdiv1ii 10991 . . . . . . . . . . 11 ((9 · 5) < (8 · 6) ↔ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5))))
280272, 279mpbi 220 . . . . . . . . . 10 ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5)))
281121, 51, 112, 97, 75, 113divmuldivi 10823 . . . . . . . . . 10 ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
282 nnexpcl 12913 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈ ℕ)
28333, 206, 282mp2an 708 . . . . . . . . . . . . 13 (2↑4) ∈ ℕ
284283nncni 11068 . . . . . . . . . . . 12 (2↑4) ∈ ℂ
285283nnne0i 11093 . . . . . . . . . . . 12 (2↑4) ≠ 0
286 divcan5 10765 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
28732, 286mp3an1 1451 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
2885, 38, 284, 285, 287mp4an 709 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8)
289 df-4 11119 . . . . . . . . . . . . . . . 16 4 = (3 + 1)
290289oveq2i 6701 . . . . . . . . . . . . . . 15 (2↑4) = (2↑(3 + 1))
291 3nn0 11348 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
292 expp1 12907 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 3 ∈ ℕ0) → (2↑(3 + 1)) = ((2↑3) · 2))
29389, 291, 292mp2an 708 . . . . . . . . . . . . . . 15 (2↑(3 + 1)) = ((2↑3) · 2)
29422oveq1i 6700 . . . . . . . . . . . . . . 15 ((2↑3) · 2) = (8 · 2)
295290, 293, 2943eqtri 2677 . . . . . . . . . . . . . 14 (2↑4) = (8 · 2)
296295oveq1i 6700 . . . . . . . . . . . . 13 ((2↑4) · 3) = ((8 · 2) · 3)
2975, 89, 32mulassi 10087 . . . . . . . . . . . . 13 ((8 · 2) · 3) = (8 · (2 · 3))
298193oveq2i 6701 . . . . . . . . . . . . 13 (8 · (2 · 3)) = (8 · 6)
299296, 297, 2983eqtri 2677 . . . . . . . . . . . 12 ((2↑4) · 3) = (8 · 6)
300 4p3e7 11201 . . . . . . . . . . . . . . . 16 (4 + 3) = 7
301 5p2e7 11203 . . . . . . . . . . . . . . . 16 (5 + 2) = 7
302112, 89addcomi 10265 . . . . . . . . . . . . . . . 16 (5 + 2) = (2 + 5)
303300, 301, 3023eqtr2i 2679 . . . . . . . . . . . . . . 15 (4 + 3) = (2 + 5)
304303oveq2i 6701 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = (2↑(2 + 5))
305 expadd 12942 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
30689, 206, 291, 305mp3an 1464 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = ((2↑4) · (2↑3))
307 2nn0 11347 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
308 expadd 12942 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 5 ∈ ℕ0) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
30989, 307, 90, 308mp3an 1464 . . . . . . . . . . . . . 14 (2↑(2 + 5)) = ((2↑2) · (2↑5))
310304, 306, 3093eqtr3i 2681 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
31122oveq2i 6701 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑4) · 8)
312 sq2 13000 . . . . . . . . . . . . . 14 (2↑2) = 4
313312oveq1i 6700 . . . . . . . . . . . . 13 ((2↑2) · (2↑5)) = (4 · (2↑5))
314310, 311, 3133eqtr3i 2681 . . . . . . . . . . . 12 ((2↑4) · 8) = (4 · (2↑5))
315299, 314oveq12i 6702 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
316288, 315eqtr3i 2675 . . . . . . . . . 10 (3 / 8) = ((8 · 6) / (4 · (2↑5)))
317280, 281, 3163brtr4i 4715 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) < (3 / 8)
318167, 11, 38redivcli 10830 . . . . . . . . . 10 (3 / 8) ∈ ℝ
319 1re 10077 . . . . . . . . . 10 1 ∈ ℝ
320 ltsub2 10563 . . . . . . . . . 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 1464 . . . . . . . . 9 (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5)))))
322317, 321mpbi 220 . . . . . . . 8 (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))
323256, 322eqbrtrri 4708 . . . . . . 7 (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
324243, 11, 38redivcli 10830 . . . . . . . 8 ((7 / (√‘2)) / 8) ∈ ℝ
325173, 11, 38redivcli 10830 . . . . . . . 8 (5 / 8) ∈ ℝ
326319, 176resubcli 10381 . . . . . . . 8 (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
327324, 325, 326lttri 10201 . . . . . . 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 708 . . . . . 6 ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
329324, 176, 319ltaddsubi 10627 . . . . . 6 ((((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
330328, 329mpbir 221 . . . . 5 (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1
331205, 330eqbrtri 4706 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
332 1lt2 11232 . . . . . . 7 1 < 2
333 rplogcl 24395 . . . . . . 7 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
33453, 332, 333mp2an 708 . . . . . 6 (log‘2) ∈ ℝ+
335 rpgt0 11882 . . . . . 6 ((log‘2) ∈ ℝ+ → 0 < (log‘2))
336334, 335ax-mp 5 . . . . 5 0 < (log‘2)
337180, 319, 36, 336ltmul1ii 10990 . . . 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 220 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2))
33937mulid2i 10081 . . . 4 (1 · (log‘2)) = (log‘2)
340339eqcomi 2660 . . 3 (log‘2) = (1 · (log‘2))
341338, 166, 3403brtr4i 4715 . 2 (𝐹64) < (log‘2)
342182, 341pm3.2i 470 1 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wcel 2030  wne 2823   class class class wbr 4685  cmpt 4762  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  2c2 11108  3c3 11109  4c4 11110  5c5 11111  6c6 11112  7c7 11113  8c8 11114  9c9 11115  0cn0 11330  cz 11415  cdc 11531  +crp 11870  cexp 12900  csqrt 14017  logclog 24346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348
This theorem is referenced by:  bposlem9  25062
  Copyright terms: Public domain W3C validator