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

Theorem bposlem8 26449
Description: Lemma for bpos 26451. 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 12264 . . . . 5 6 ∈ ℕ0
2 4nn 12066 . . . . 5 4 ∈ ℕ
31, 2decnncl 12467 . . . 4 64 ∈ ℕ
4 fveq2 6766 . . . . . . . . . . . . . 14 (𝑛 = 64 → (√‘𝑛) = (√‘64))
5 8cn 12080 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
65sqvali 13907 . . . . . . . . . . . . . . . . 17 (8↑2) = (8 · 8)
7 8t8e64 12568 . . . . . . . . . . . . . . . . 17 (8 · 8) = 64
86, 7eqtri 2766 . . . . . . . . . . . . . . . 16 (8↑2) = 64
98fveq2i 6769 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = (√‘64)
10 0re 10987 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
11 8re 12079 . . . . . . . . . . . . . . . . 17 8 ∈ ℝ
12 8pos 12095 . . . . . . . . . . . . . . . . 17 0 < 8
1310, 11, 12ltleii 11108 . . . . . . . . . . . . . . . 16 0 ≤ 8
1411sqrtsqi 15096 . . . . . . . . . . . . . . . 16 (0 ≤ 8 → (√‘(8↑2)) = 8)
1513, 14ax-mp 5 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = 8
169, 15eqtr3i 2768 . . . . . . . . . . . . . 14 (√‘64) = 8
174, 16eqtrdi 2794 . . . . . . . . . . . . 13 (𝑛 = 64 → (√‘𝑛) = 8)
1817fveq2d 6770 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19 8nn 12078 . . . . . . . . . . . . 13 8 ∈ ℕ
20 nnrp 12751 . . . . . . . . . . . . 13 (8 ∈ ℕ → 8 ∈ ℝ+)
21 fveq2 6766 . . . . . . . . . . . . . . . . 17 (𝑥 = 8 → (log‘𝑥) = (log‘8))
22 cu2 13927 . . . . . . . . . . . . . . . . . . 19 (2↑3) = 8
2322fveq2i 6769 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (log‘8)
24 2rp 12745 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
25 3z 12363 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℤ
26 relogexp 25761 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
2724, 25, 26mp2an 689 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (3 · (log‘2))
2823, 27eqtr3i 2768 . . . . . . . . . . . . . . . . 17 (log‘8) = (3 · (log‘2))
2921, 28eqtrdi 2794 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → 𝑥 = 8)
3129, 30oveq12d 7285 . . . . . . . . . . . . . . 15 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32 3cn 12064 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
33 2nn 12056 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
34 nnrp 12751 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℕ → 2 ∈ ℝ+)
35 relogcl 25741 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3633, 34, 35mp2b 10 . . . . . . . . . . . . . . . . 17 (log‘2) ∈ ℝ
3736recni 10999 . . . . . . . . . . . . . . . 16 (log‘2) ∈ ℂ
3819nnne0i 12023 . . . . . . . . . . . . . . . 16 8 ≠ 0
3932, 37, 5, 38div23i 11743 . . . . . . . . . . . . . . 15 ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
4031, 39eqtrdi 2794 . . . . . . . . . . . . . 14 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41 bposlem7.2 . . . . . . . . . . . . . 14 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
42 ovex 7300 . . . . . . . . . . . . . 14 ((3 / 8) · (log‘2)) ∈ V
4340, 41, 42fvmpt 6867 . . . . . . . . . . . . 13 (8 ∈ ℝ+ → (𝐺‘8) = ((3 / 8) · (log‘2)))
4419, 20, 43mp2b 10 . . . . . . . . . . . 12 (𝐺‘8) = ((3 / 8) · (log‘2))
4518, 44eqtrdi 2794 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
4645oveq2d 7283 . . . . . . . . . 10 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47 sqrt2re 15969 . . . . . . . . . . . . 13 (√‘2) ∈ ℝ
4847recni 10999 . . . . . . . . . . . 12 (√‘2) ∈ ℂ
4932, 5, 38divcli 11727 . . . . . . . . . . . 12 (3 / 8) ∈ ℂ
5048, 49, 37mulassi 10996 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51 4cn 12068 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
5248, 51, 48mul12i 11180 . . . . . . . . . . . . . . 15 ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53 2re 12057 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
54 0le2 12085 . . . . . . . . . . . . . . . . 17 0 ≤ 2
55 remsqsqrt 14978 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
5653, 54, 55mp2an 689 . . . . . . . . . . . . . . . 16 ((√‘2) · (√‘2)) = 2
5756oveq2i 7278 . . . . . . . . . . . . . . 15 (4 · ((√‘2) · (√‘2))) = (4 · 2)
58 4t2e8 12151 . . . . . . . . . . . . . . 15 (4 · 2) = 8
5952, 57, 583eqtri 2770 . . . . . . . . . . . . . 14 ((√‘2) · (4 · (√‘2))) = 8
6059oveq2i 7278 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
6151, 48mulcli 10992 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ∈ ℂ
62 nnrp 12751 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
632, 62ax-mp 5 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ+
64 rpsqrtcl 14986 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (√‘2) ∈ ℝ+)
6533, 34, 64mp2b 10 . . . . . . . . . . . . . . . . 17 (√‘2) ∈ ℝ+
66 rpmulcl 12763 . . . . . . . . . . . . . . . . 17 ((4 ∈ ℝ+ ∧ (√‘2) ∈ ℝ+) → (4 · (√‘2)) ∈ ℝ+)
6763, 65, 66mp2an 689 . . . . . . . . . . . . . . . 16 (4 · (√‘2)) ∈ ℝ+
68 rpne0 12756 . . . . . . . . . . . . . . . 16 ((4 · (√‘2)) ∈ ℝ+ → (4 · (√‘2)) ≠ 0)
6967, 68ax-mp 5 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ≠ 0
70 rpne0 12756 . . . . . . . . . . . . . . . 16 ((√‘2) ∈ ℝ+ → (√‘2) ≠ 0)
7124, 64, 70mp2b 10 . . . . . . . . . . . . . . 15 (√‘2) ≠ 0
72 divcan5 11687 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7332, 72mp3an1 1447 . . . . . . . . . . . . . . 15 ((((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7461, 69, 48, 71, 73mp4an 690 . . . . . . . . . . . . . 14 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2)))
75 4ne0 12091 . . . . . . . . . . . . . . 15 4 ≠ 0
76 divdiv1 11696 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7732, 76mp3an1 1447 . . . . . . . . . . . . . . 15 (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7851, 75, 48, 71, 77mp4an 690 . . . . . . . . . . . . . 14 ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2)))
7974, 78eqtr4i 2769 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
8048, 32, 5, 38divassi 11741 . . . . . . . . . . . . 13 (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
8160, 79, 803eqtr3ri 2775 . . . . . . . . . . . 12 ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
8281oveq1i 7277 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
8350, 82eqtr3i 2768 . . . . . . . . . 10 ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
8446, 83eqtrdi 2794 . . . . . . . . 9 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85 oveq1 7274 . . . . . . . . . . . . . 14 (𝑛 = 64 → (𝑛 / 2) = (64 / 2))
86 df-6 12050 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
8786oveq2i 7278 . . . . . . . . . . . . . . . . 17 (2↑6) = (2↑(5 + 1))
88 2exp6 16798 . . . . . . . . . . . . . . . . 17 (2↑6) = 64
89 2cn 12058 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
90 5nn0 12263 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ0
91 expp1 13799 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 5 ∈ ℕ0) → (2↑(5 + 1)) = ((2↑5) · 2))
9289, 90, 91mp2an 689 . . . . . . . . . . . . . . . . 17 (2↑(5 + 1)) = ((2↑5) · 2)
9387, 88, 923eqtr3i 2774 . . . . . . . . . . . . . . . 16 64 = ((2↑5) · 2)
9493oveq1i 7277 . . . . . . . . . . . . . . 15 (64 / 2) = (((2↑5) · 2) / 2)
95 nnexpcl 13805 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ ∧ 5 ∈ ℕ0) → (2↑5) ∈ ℕ)
9633, 90, 95mp2an 689 . . . . . . . . . . . . . . . . 17 (2↑5) ∈ ℕ
9796nncni 11993 . . . . . . . . . . . . . . . 16 (2↑5) ∈ ℂ
98 2ne0 12087 . . . . . . . . . . . . . . . 16 2 ≠ 0
9997, 89, 98divcan4i 11732 . . . . . . . . . . . . . . 15 (((2↑5) · 2) / 2) = (2↑5)
10094, 99eqtri 2766 . . . . . . . . . . . . . 14 (64 / 2) = (2↑5)
10185, 100eqtrdi 2794 . . . . . . . . . . . . 13 (𝑛 = 64 → (𝑛 / 2) = (2↑5))
102101fveq2d 6770 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103 nnrp 12751 . . . . . . . . . . . . 13 ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ+)
104 fveq2 6766 . . . . . . . . . . . . . . . . 17 (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105 5nn 12069 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℕ
106105nnzi 12354 . . . . . . . . . . . . . . . . . 18 5 ∈ ℤ
107 relogexp 25761 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
10824, 106, 107mp2an 689 . . . . . . . . . . . . . . . . 17 (log‘(2↑5)) = (5 · (log‘2))
109104, 108eqtrdi 2794 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → 𝑥 = (2↑5))
111109, 110oveq12d 7285 . . . . . . . . . . . . . . 15 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112 5cn 12071 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
11396nnne0i 12023 . . . . . . . . . . . . . . . 16 (2↑5) ≠ 0
114112, 37, 97, 113div23i 11743 . . . . . . . . . . . . . . 15 ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115111, 114eqtrdi 2794 . . . . . . . . . . . . . 14 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116 ovex 7300 . . . . . . . . . . . . . 14 ((5 / (2↑5)) · (log‘2)) ∈ V
117115, 41, 116fvmpt 6867 . . . . . . . . . . . . 13 ((2↑5) ∈ ℝ+ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
11896, 103, 117mp2b 10 . . . . . . . . . . . 12 (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
119102, 118eqtrdi 2794 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120119oveq2d 7283 . . . . . . . . . 10 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121 9cn 12083 . . . . . . . . . . . 12 9 ∈ ℂ
122121, 51, 75divcli 11727 . . . . . . . . . . 11 (9 / 4) ∈ ℂ
123112, 97, 113divcli 11727 . . . . . . . . . . 11 (5 / (2↑5)) ∈ ℂ
124122, 123, 37mulassi 10996 . . . . . . . . . 10 (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125120, 124eqtr4di 2796 . . . . . . . . 9 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
12684, 125oveq12d 7285 . . . . . . . 8 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
12732, 51, 75divcli 11727 . . . . . . . . . 10 (3 / 4) ∈ ℂ
128127, 48, 71divcli 11727 . . . . . . . . 9 ((3 / 4) / (√‘2)) ∈ ℂ
129122, 123mulcli 10992 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130128, 129, 37adddiri 10998 . . . . . . . 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 2796 . . . . . . 7 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132 oveq2 7275 . . . . . . . . . . 11 (𝑛 = 64 → (2 · 𝑛) = (2 · 64))
133132fveq2d 6770 . . . . . . . . . 10 (𝑛 = 64 → (√‘(2 · 𝑛)) = (√‘(2 · 64)))
1343nnrei 11992 . . . . . . . . . . . 12 64 ∈ ℝ
1353nngt0i 12022 . . . . . . . . . . . . 13 0 < 64
13610, 134, 135ltleii 11108 . . . . . . . . . . . 12 0 ≤ 64
13753, 134, 54, 136sqrtmulii 15108 . . . . . . . . . . 11 (√‘(2 · 64)) = ((√‘2) · (√‘64))
13816oveq2i 7278 . . . . . . . . . . 11 ((√‘2) · (√‘64)) = ((√‘2) · 8)
139137, 138eqtri 2766 . . . . . . . . . 10 (√‘(2 · 64)) = ((√‘2) · 8)
140133, 139eqtrdi 2794 . . . . . . . . 9 (𝑛 = 64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141140oveq2d 7283 . . . . . . . 8 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
14248, 5mulcli 10992 . . . . . . . . . 10 ((√‘2) · 8) ∈ ℂ
143 rpmulcl 12763 . . . . . . . . . . . 12 (((√‘2) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((√‘2) · 8) ∈ ℝ+)
14465, 20, 143sylancr 587 . . . . . . . . . . 11 (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ+)
145 rpne0 12756 . . . . . . . . . . 11 (((√‘2) · 8) ∈ ℝ+ → ((√‘2) · 8) ≠ 0)
14619, 144, 145mp2b 10 . . . . . . . . . 10 ((√‘2) · 8) ≠ 0
147 divrec2 11660 . . . . . . . . . 10 (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
14837, 142, 146, 147mp3an 1460 . . . . . . . . 9 ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
14948, 5mulcomi 10993 . . . . . . . . . . . 12 ((√‘2) · 8) = (8 · (√‘2))
150149oveq2i 7278 . . . . . . . . . . 11 (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151 recdiv2 11698 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2))))
1525, 38, 48, 71, 151mp4an 690 . . . . . . . . . . 11 ((1 / 8) / (√‘2)) = (1 / (8 · (√‘2)))
153150, 152eqtr4i 2769 . . . . . . . . . 10 (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154153oveq1i 7277 . . . . . . . . 9 ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155148, 154eqtri 2766 . . . . . . . 8 ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156141, 155eqtrdi 2794 . . . . . . 7 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157131, 156oveq12d 7285 . . . . . 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 10991 . . . . . . 7 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
1595, 38reccli 11715 . . . . . . . 8 (1 / 8) ∈ ℂ
160159, 48, 71divcli 11727 . . . . . . 7 ((1 / 8) / (√‘2)) ∈ ℂ
161158, 160, 37adddiri 10998 . . . . . 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 2796 . . . . 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 7300 . . . . 5 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165162, 163, 164fvmpt 6867 . . . 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 12063 . . . . . . . 8 3 ∈ ℝ
168 4re 12067 . . . . . . . 8 4 ∈ ℝ
169167, 168, 75redivcli 11752 . . . . . . 7 (3 / 4) ∈ ℝ
170169, 47, 71redivcli 11752 . . . . . 6 ((3 / 4) / (√‘2)) ∈ ℝ
171 9re 12082 . . . . . . . 8 9 ∈ ℝ
172171, 168, 75redivcli 11752 . . . . . . 7 (9 / 4) ∈ ℝ
173 5re 12070 . . . . . . . 8 5 ∈ ℝ
17496nnrei 11992 . . . . . . . 8 (2↑5) ∈ ℝ
175173, 174, 113redivcli 11752 . . . . . . 7 (5 / (2↑5)) ∈ ℝ
176172, 175remulcli 11001 . . . . . 6 ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177170, 176readdcli 11000 . . . . 5 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
17811, 38rereccli 11750 . . . . . 6 (1 / 8) ∈ ℝ
179178, 47, 71redivcli 11752 . . . . 5 ((1 / 8) / (√‘2)) ∈ ℝ
180177, 179readdcli 11000 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181180, 36remulcli 11001 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182166, 181eqeltri 2835 . 2 (𝐹64) ∈ ℝ
183128, 129, 160add32i 11208 . . . . . 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 12074 . . . . . . . . . . 11 6 ∈ ℂ
185 ax-1cn 10939 . . . . . . . . . . 11 1 ∈ ℂ
186184, 185, 5, 38divdiri 11742 . . . . . . . . . 10 ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187 df-7 12051 . . . . . . . . . . 11 7 = (6 + 1)
188187oveq1i 7277 . . . . . . . . . 10 (7 / 8) = ((6 + 1) / 8)
189 divcan5 11687 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19032, 189mp3an1 1447 . . . . . . . . . . . . 13 (((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19151, 75, 89, 98, 190mp4an 690 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (3 / 4)
192 3t2e6 12149 . . . . . . . . . . . . . 14 (3 · 2) = 6
19332, 89, 192mulcomli 10994 . . . . . . . . . . . . 13 (2 · 3) = 6
19451, 89, 58mulcomli 10994 . . . . . . . . . . . . 13 (2 · 4) = 8
195193, 194oveq12i 7279 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (6 / 8)
196191, 195eqtr3i 2768 . . . . . . . . . . 11 (3 / 4) = (6 / 8)
197196oveq1i 7277 . . . . . . . . . 10 ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
198186, 188, 1973eqtr4ri 2777 . . . . . . . . 9 ((3 / 4) + (1 / 8)) = (7 / 8)
199198oveq1i 7277 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
200127, 159, 48, 71divdiri 11742 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
201 7cn 12077 . . . . . . . . 9 7 ∈ ℂ
202201, 5, 48, 38, 71divdiv32i 11740 . . . . . . . 8 ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
203199, 200, 2023eqtr3i 2774 . . . . . . 7 (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
204203oveq1i 7277 . . . . . 6 ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205183, 204eqtri 2766 . . . . 5 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
206 4nn0 12262 . . . . . . . . . . . 12 4 ∈ ℕ0
207 9nn0 12267 . . . . . . . . . . . 12 9 ∈ ℕ0
208 0nn0 12258 . . . . . . . . . . . 12 0 ∈ ℕ0
209 9lt10 12578 . . . . . . . . . . . 12 9 < 10
210 4lt5 12160 . . . . . . . . . . . 12 4 < 5
211206, 90, 207, 208, 209, 210decltc 12476 . . . . . . . . . . 11 49 < 50
212 7t7e49 12561 . . . . . . . . . . 11 (7 · 7) = 49
21356oveq1i 7277 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
21448, 48, 112, 112mul4i 11182 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
215 5t2e10 12547 . . . . . . . . . . . . . . 15 (5 · 2) = 10
216112, 89, 215mulcomli 10994 . . . . . . . . . . . . . 14 (2 · 5) = 10
217216oveq1i 7277 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (10 · 5)
21889, 112, 112mulassi 10996 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (2 · (5 · 5))
21990dec0u 12468 . . . . . . . . . . . . 13 (10 · 5) = 50
220217, 218, 2193eqtr3i 2774 . . . . . . . . . . . 12 (2 · (5 · 5)) = 50
221213, 214, 2203eqtr3i 2774 . . . . . . . . . . 11 (((√‘2) · 5) · ((√‘2) · 5)) = 50
222211, 212, 2213brtr4i 5103 . . . . . . . . . 10 (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
223 7re 12076 . . . . . . . . . . . 12 7 ∈ ℝ
224 7pos 12094 . . . . . . . . . . . 12 0 < 7
22510, 223, 224ltleii 11108 . . . . . . . . . . 11 0 ≤ 7
226 nnrp 12751 . . . . . . . . . . . . . 14 (5 ∈ ℕ → 5 ∈ ℝ+)
227105, 226ax-mp 5 . . . . . . . . . . . . 13 5 ∈ ℝ+
228 rpmulcl 12763 . . . . . . . . . . . . 13 (((√‘2) ∈ ℝ+ ∧ 5 ∈ ℝ+) → ((√‘2) · 5) ∈ ℝ+)
22965, 227, 228mp2an 689 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ+
230 rpge0 12753 . . . . . . . . . . . 12 (((√‘2) · 5) ∈ ℝ+ → 0 ≤ ((√‘2) · 5))
231229, 230ax-mp 5 . . . . . . . . . . 11 0 ≤ ((√‘2) · 5)
232 rpre 12748 . . . . . . . . . . . . 13 (((√‘2) · 5) ∈ ℝ+ → ((√‘2) · 5) ∈ ℝ)
233229, 232ax-mp 5 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ
234223, 233lt2msqi 11897 . . . . . . . . . . 11 ((0 ≤ 7 ∧ 0 ≤ ((√‘2) · 5)) → (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))))
235225, 231, 234mp2an 689 . . . . . . . . . 10 (7 < ((√‘2) · 5) ↔ (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5)))
236222, 235mpbir 230 . . . . . . . . 9 7 < ((√‘2) · 5)
237 rpgt0 12752 . . . . . . . . . . 11 ((√‘2) ∈ ℝ+ → 0 < (√‘2))
23824, 64, 237mp2b 10 . . . . . . . . . 10 0 < (√‘2)
239 ltdivmul 11860 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240223, 173, 239mp3an12 1450 . . . . . . . . . 10 (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
24147, 238, 240mp2an 689 . . . . . . . . 9 ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
242236, 241mpbir 230 . . . . . . . 8 (7 / (√‘2)) < 5
243223, 47, 71redivcli 11752 . . . . . . . . 9 (7 / (√‘2)) ∈ ℝ
244243, 173, 11, 12ltdiv1ii 11914 . . . . . . . 8 ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
245242, 244mpbi 229 . . . . . . 7 ((7 / (√‘2)) / 8) < (5 / 8)
246 divsubdir 11679 . . . . . . . . . . 11 ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2475, 32, 246mp3an12 1450 . . . . . . . . . 10 ((8 ∈ ℂ ∧ 8 ≠ 0) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2485, 38, 247mp2an 689 . . . . . . . . 9 ((8 − 3) / 8) = ((8 / 8) − (3 / 8))
249 5p3e8 12140 . . . . . . . . . . . 12 (5 + 3) = 8
250249oveq1i 7277 . . . . . . . . . . 11 ((5 + 3) − 3) = (8 − 3)
251112, 32pncan3oi 11247 . . . . . . . . . . 11 ((5 + 3) − 3) = 5
252250, 251eqtr3i 2768 . . . . . . . . . 10 (8 − 3) = 5
253252oveq1i 7277 . . . . . . . . 9 ((8 − 3) / 8) = (5 / 8)
2545, 38dividi 11718 . . . . . . . . . 10 (8 / 8) = 1
255254oveq1i 7277 . . . . . . . . 9 ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
256248, 253, 2553eqtr3ri 2775 . . . . . . . 8 (1 − (3 / 8)) = (5 / 8)
257 5lt8 12177 . . . . . . . . . . . . 13 5 < 8
25811, 173remulcli 11001 . . . . . . . . . . . . . 14 (8 · 5) ∈ ℝ
259173, 11, 258ltadd2i 11116 . . . . . . . . . . . . 13 (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
260257, 259mpbi 229 . . . . . . . . . . . 12 ((8 · 5) + 5) < ((8 · 5) + 8)
261 df-9 12053 . . . . . . . . . . . . . 14 9 = (8 + 1)
262261oveq1i 7277 . . . . . . . . . . . . 13 (9 · 5) = ((8 + 1) · 5)
2635, 185, 112adddiri 10998 . . . . . . . . . . . . 13 ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
264112mulid2i 10990 . . . . . . . . . . . . . 14 (1 · 5) = 5
265264oveq2i 7278 . . . . . . . . . . . . 13 ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
266262, 263, 2653eqtri 2770 . . . . . . . . . . . 12 (9 · 5) = ((8 · 5) + 5)
26786oveq2i 7278 . . . . . . . . . . . . 13 (8 · 6) = (8 · (5 + 1))
2685, 112, 185adddii 10997 . . . . . . . . . . . . 13 (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
2695mulid1i 10989 . . . . . . . . . . . . . 14 (8 · 1) = 8
270269oveq2i 7278 . . . . . . . . . . . . 13 ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
271267, 268, 2703eqtri 2770 . . . . . . . . . . . 12 (8 · 6) = ((8 · 5) + 8)
272260, 266, 2713brtr4i 5103 . . . . . . . . . . 11 (9 · 5) < (8 · 6)
273171, 173remulcli 11001 . . . . . . . . . . . 12 (9 · 5) ∈ ℝ
274 6re 12073 . . . . . . . . . . . . 13 6 ∈ ℝ
27511, 274remulcli 11001 . . . . . . . . . . . 12 (8 · 6) ∈ ℝ
276168, 174remulcli 11001 . . . . . . . . . . . 12 (4 · (2↑5)) ∈ ℝ
2772, 96nnmulcli 12008 . . . . . . . . . . . . 13 (4 · (2↑5)) ∈ ℕ
278277nngt0i 12022 . . . . . . . . . . . 12 0 < (4 · (2↑5))
279273, 275, 276, 278ltdiv1ii 11914 . . . . . . . . . . 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 11745 . . . . . . . . . 10 ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
282 nnexpcl 13805 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈ ℕ)
28333, 206, 282mp2an 689 . . . . . . . . . . . . 13 (2↑4) ∈ ℕ
284283nncni 11993 . . . . . . . . . . . 12 (2↑4) ∈ ℂ
285283nnne0i 12023 . . . . . . . . . . . 12 (2↑4) ≠ 0
286 divcan5 11687 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
28732, 286mp3an1 1447 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
2885, 38, 284, 285, 287mp4an 690 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8)
289 df-4 12048 . . . . . . . . . . . . . . . 16 4 = (3 + 1)
290289oveq2i 7278 . . . . . . . . . . . . . . 15 (2↑4) = (2↑(3 + 1))
291 3nn0 12261 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
292 expp1 13799 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 3 ∈ ℕ0) → (2↑(3 + 1)) = ((2↑3) · 2))
29389, 291, 292mp2an 689 . . . . . . . . . . . . . . 15 (2↑(3 + 1)) = ((2↑3) · 2)
29422oveq1i 7277 . . . . . . . . . . . . . . 15 ((2↑3) · 2) = (8 · 2)
295290, 293, 2943eqtri 2770 . . . . . . . . . . . . . 14 (2↑4) = (8 · 2)
296295oveq1i 7277 . . . . . . . . . . . . 13 ((2↑4) · 3) = ((8 · 2) · 3)
2975, 89, 32mulassi 10996 . . . . . . . . . . . . 13 ((8 · 2) · 3) = (8 · (2 · 3))
298193oveq2i 7278 . . . . . . . . . . . . 13 (8 · (2 · 3)) = (8 · 6)
299296, 297, 2983eqtri 2770 . . . . . . . . . . . 12 ((2↑4) · 3) = (8 · 6)
300 4p3e7 12137 . . . . . . . . . . . . . . . 16 (4 + 3) = 7
301 5p2e7 12139 . . . . . . . . . . . . . . . 16 (5 + 2) = 7
302112, 89addcomi 11176 . . . . . . . . . . . . . . . 16 (5 + 2) = (2 + 5)
303300, 301, 3023eqtr2i 2772 . . . . . . . . . . . . . . 15 (4 + 3) = (2 + 5)
304303oveq2i 7278 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = (2↑(2 + 5))
305 expadd 13835 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
30689, 206, 291, 305mp3an 1460 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = ((2↑4) · (2↑3))
307 2nn0 12260 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
308 expadd 13835 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 5 ∈ ℕ0) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
30989, 307, 90, 308mp3an 1460 . . . . . . . . . . . . . 14 (2↑(2 + 5)) = ((2↑2) · (2↑5))
310304, 306, 3093eqtr3i 2774 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
31122oveq2i 7278 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑4) · 8)
312 sq2 13924 . . . . . . . . . . . . . 14 (2↑2) = 4
313312oveq1i 7277 . . . . . . . . . . . . 13 ((2↑2) · (2↑5)) = (4 · (2↑5))
314310, 311, 3133eqtr3i 2774 . . . . . . . . . . . 12 ((2↑4) · 8) = (4 · (2↑5))
315299, 314oveq12i 7279 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
316288, 315eqtr3i 2768 . . . . . . . . . 10 (3 / 8) = ((8 · 6) / (4 · (2↑5)))
317280, 281, 3163brtr4i 5103 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) < (3 / 8)
318167, 11, 38redivcli 11752 . . . . . . . . . 10 (3 / 8) ∈ ℝ
319 1re 10985 . . . . . . . . . 10 1 ∈ ℝ
320 ltsub2 11482 . . . . . . . . . 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 1460 . . . . . . . . 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 5096 . . . . . . 7 (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
324243, 11, 38redivcli 11752 . . . . . . . 8 ((7 / (√‘2)) / 8) ∈ ℝ
325173, 11, 38redivcli 11752 . . . . . . . 8 (5 / 8) ∈ ℝ
326319, 176resubcli 11293 . . . . . . . 8 (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
327324, 325, 326lttri 11111 . . . . . . 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 689 . . . . . 6 ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
329324, 176, 319ltaddsubi 11546 . . . . . 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 5094 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
332 1lt2 12154 . . . . . . 7 1 < 2
333 rplogcl 25769 . . . . . . 7 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
33453, 332, 333mp2an 689 . . . . . 6 (log‘2) ∈ ℝ+
335 rpgt0 12752 . . . . . 6 ((log‘2) ∈ ℝ+ → 0 < (log‘2))
336334, 335ax-mp 5 . . . . 5 0 < (log‘2)
337180, 319, 36, 336ltmul1ii 11913 . . . 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 10990 . . . 4 (1 · (log‘2)) = (log‘2)
340339eqcomi 2747 . . 3 (log‘2) = (1 · (log‘2))
341338, 166, 3403brtr4i 5103 . 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 1539  wcel 2106  wne 2943   class class class wbr 5073  cmpt 5156  cfv 6426  (class class class)co 7267  cc 10879  cr 10880  0cc0 10881  1c1 10882   + caddc 10884   · cmul 10886   < clt 11019  cle 11020  cmin 11215   / cdiv 11642  cn 11983  2c2 12038  3c3 12039  4c4 12040  5c5 12041  6c6 12042  7c7 12043  8c8 12044  9c9 12045  0cn0 12243  cz 12329  cdc 12447  +crp 12740  cexp 13792  csqrt 14954  logclog 25720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5208  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578  ax-inf2 9386  ax-cnex 10937  ax-resscn 10938  ax-1cn 10939  ax-icn 10940  ax-addcl 10941  ax-addrcl 10942  ax-mulcl 10943  ax-mulrcl 10944  ax-mulcom 10945  ax-addass 10946  ax-mulass 10947  ax-distr 10948  ax-i2m1 10949  ax-1ne0 10950  ax-1rid 10951  ax-rnegex 10952  ax-rrecex 10953  ax-cnre 10954  ax-pre-lttri 10955  ax-pre-lttrn 10956  ax-pre-ltadd 10957  ax-pre-mulgt0 10958  ax-pre-sup 10959  ax-addf 10960  ax-mulf 10961
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-pss 3905  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5074  df-opab 5136  df-mpt 5157  df-tr 5191  df-id 5484  df-eprel 5490  df-po 5498  df-so 5499  df-fr 5539  df-se 5540  df-we 5541  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-pred 6195  df-ord 6262  df-on 6263  df-lim 6264  df-suc 6265  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-isom 6435  df-riota 7224  df-ov 7270  df-oprab 7271  df-mpo 7272  df-of 7523  df-om 7703  df-1st 7820  df-2nd 7821  df-supp 7965  df-frecs 8084  df-wrecs 8115  df-recs 8189  df-rdg 8228  df-1o 8284  df-2o 8285  df-er 8485  df-map 8604  df-pm 8605  df-ixp 8673  df-en 8721  df-dom 8722  df-sdom 8723  df-fin 8724  df-fsupp 9116  df-fi 9157  df-sup 9188  df-inf 9189  df-oi 9256  df-card 9707  df-pnf 11021  df-mnf 11022  df-xr 11023  df-ltxr 11024  df-le 11025  df-sub 11217  df-neg 11218  df-div 11643  df-nn 11984  df-2 12046  df-3 12047  df-4 12048  df-5 12049  df-6 12050  df-7 12051  df-8 12052  df-9 12053  df-n0 12244  df-z 12330  df-dec 12448  df-uz 12593  df-q 12699  df-rp 12741  df-xneg 12858  df-xadd 12859  df-xmul 12860  df-ioo 13093  df-ioc 13094  df-ico 13095  df-icc 13096  df-fz 13250  df-fzo 13393  df-fl 13522  df-mod 13600  df-seq 13732  df-exp 13793  df-fac 13998  df-bc 14027  df-hash 14055  df-shft 14788  df-cj 14820  df-re 14821  df-im 14822  df-sqrt 14956  df-abs 14957  df-limsup 15190  df-clim 15207  df-rlim 15208  df-sum 15408  df-ef 15787  df-sin 15789  df-cos 15790  df-pi 15792  df-struct 16858  df-sets 16875  df-slot 16893  df-ndx 16905  df-base 16923  df-ress 16952  df-plusg 16985  df-mulr 16986  df-starv 16987  df-sca 16988  df-vsca 16989  df-ip 16990  df-tset 16991  df-ple 16992  df-ds 16994  df-unif 16995  df-hom 16996  df-cco 16997  df-rest 17143  df-topn 17144  df-0g 17162  df-gsum 17163  df-topgen 17164  df-pt 17165  df-prds 17168  df-xrs 17223  df-qtop 17228  df-imas 17229  df-xps 17231  df-mre 17305  df-mrc 17306  df-acs 17308  df-mgm 18336  df-sgrp 18385  df-mnd 18396  df-submnd 18441  df-mulg 18711  df-cntz 18933  df-cmn 19398  df-psmet 20599  df-xmet 20600  df-met 20601  df-bl 20602  df-mopn 20603  df-fbas 20604  df-fg 20605  df-cnfld 20608  df-top 22053  df-topon 22070  df-topsp 22092  df-bases 22106  df-cld 22180  df-ntr 22181  df-cls 22182  df-nei 22259  df-lp 22297  df-perf 22298  df-cn 22388  df-cnp 22389  df-haus 22476  df-tx 22723  df-hmeo 22916  df-fil 23007  df-fm 23099  df-flim 23100  df-flf 23101  df-xms 23483  df-ms 23484  df-tms 23485  df-cncf 24051  df-limc 25040  df-dv 25041  df-log 25722
This theorem is referenced by:  bposlem9  26450
  Copyright terms: Public domain W3C validator