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

Theorem bposlem8 25859
Description: Lemma for bpos 25861. 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 11910 . . . . 5 6 ∈ ℕ0
2 4nn 11712 . . . . 5 4 ∈ ℕ
31, 2decnncl 12110 . . . 4 64 ∈ ℕ
4 fveq2 6663 . . . . . . . . . . . . . 14 (𝑛 = 64 → (√‘𝑛) = (√‘64))
5 8cn 11726 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
65sqvali 13535 . . . . . . . . . . . . . . . . 17 (8↑2) = (8 · 8)
7 8t8e64 12211 . . . . . . . . . . . . . . . . 17 (8 · 8) = 64
86, 7eqtri 2842 . . . . . . . . . . . . . . . 16 (8↑2) = 64
98fveq2i 6666 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = (√‘64)
10 0re 10635 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
11 8re 11725 . . . . . . . . . . . . . . . . 17 8 ∈ ℝ
12 8pos 11741 . . . . . . . . . . . . . . . . 17 0 < 8
1310, 11, 12ltleii 10755 . . . . . . . . . . . . . . . 16 0 ≤ 8
1411sqrtsqi 14726 . . . . . . . . . . . . . . . 16 (0 ≤ 8 → (√‘(8↑2)) = 8)
1513, 14ax-mp 5 . . . . . . . . . . . . . . 15 (√‘(8↑2)) = 8
169, 15eqtr3i 2844 . . . . . . . . . . . . . 14 (√‘64) = 8
174, 16syl6eq 2870 . . . . . . . . . . . . 13 (𝑛 = 64 → (√‘𝑛) = 8)
1817fveq2d 6667 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = (𝐺‘8))
19 8nn 11724 . . . . . . . . . . . . 13 8 ∈ ℕ
20 nnrp 12392 . . . . . . . . . . . . 13 (8 ∈ ℕ → 8 ∈ ℝ+)
21 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑥 = 8 → (log‘𝑥) = (log‘8))
22 cu2 13555 . . . . . . . . . . . . . . . . . . 19 (2↑3) = 8
2322fveq2i 6666 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (log‘8)
24 2rp 12386 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
25 3z 12007 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℤ
26 relogexp 25171 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
2724, 25, 26mp2an 690 . . . . . . . . . . . . . . . . . 18 (log‘(2↑3)) = (3 · (log‘2))
2823, 27eqtr3i 2844 . . . . . . . . . . . . . . . . 17 (log‘8) = (3 · (log‘2))
2921, 28syl6eq 2870 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → (log‘𝑥) = (3 · (log‘2)))
30 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 8 → 𝑥 = 8)
3129, 30oveq12d 7166 . . . . . . . . . . . . . . 15 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 · (log‘2)) / 8))
32 3cn 11710 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
33 2nn 11702 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
34 nnrp 12392 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℕ → 2 ∈ ℝ+)
35 relogcl 25151 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3633, 34, 35mp2b 10 . . . . . . . . . . . . . . . . 17 (log‘2) ∈ ℝ
3736recni 10647 . . . . . . . . . . . . . . . 16 (log‘2) ∈ ℂ
3819nnne0i 11669 . . . . . . . . . . . . . . . 16 8 ≠ 0
3932, 37, 5, 38div23i 11390 . . . . . . . . . . . . . . 15 ((3 · (log‘2)) / 8) = ((3 / 8) · (log‘2))
4031, 39syl6eq 2870 . . . . . . . . . . . . . 14 (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) · (log‘2)))
41 bposlem7.2 . . . . . . . . . . . . . 14 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
42 ovex 7181 . . . . . . . . . . . . . 14 ((3 / 8) · (log‘2)) ∈ V
4340, 41, 42fvmpt 6761 . . . . . . . . . . . . 13 (8 ∈ ℝ+ → (𝐺‘8) = ((3 / 8) · (log‘2)))
4419, 20, 43mp2b 10 . . . . . . . . . . . 12 (𝐺‘8) = ((3 / 8) · (log‘2))
4518, 44syl6eq 2870 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(√‘𝑛)) = ((3 / 8) · (log‘2)))
4645oveq2d 7164 . . . . . . . . . 10 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · ((3 / 8) · (log‘2))))
47 sqrt2re 15595 . . . . . . . . . . . . 13 (√‘2) ∈ ℝ
4847recni 10647 . . . . . . . . . . . 12 (√‘2) ∈ ℂ
4932, 5, 38divcli 11374 . . . . . . . . . . . 12 (3 / 8) ∈ ℂ
5048, 49, 37mulassi 10644 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = ((√‘2) · ((3 / 8) · (log‘2)))
51 4cn 11714 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
5248, 51, 48mul12i 10827 . . . . . . . . . . . . . . 15 ((√‘2) · (4 · (√‘2))) = (4 · ((√‘2) · (√‘2)))
53 2re 11703 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
54 0le2 11731 . . . . . . . . . . . . . . . . 17 0 ≤ 2
55 remsqsqrt 14608 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
5653, 54, 55mp2an 690 . . . . . . . . . . . . . . . 16 ((√‘2) · (√‘2)) = 2
5756oveq2i 7159 . . . . . . . . . . . . . . 15 (4 · ((√‘2) · (√‘2))) = (4 · 2)
58 4t2e8 11797 . . . . . . . . . . . . . . 15 (4 · 2) = 8
5952, 57, 583eqtri 2846 . . . . . . . . . . . . . 14 ((√‘2) · (4 · (√‘2))) = 8
6059oveq2i 7159 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (((√‘2) · 3) / 8)
6151, 48mulcli 10640 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ∈ ℂ
62 nnrp 12392 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
632, 62ax-mp 5 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ+
64 rpsqrtcl 14616 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ → (√‘2) ∈ ℝ+)
6533, 34, 64mp2b 10 . . . . . . . . . . . . . . . . 17 (√‘2) ∈ ℝ+
66 rpmulcl 12404 . . . . . . . . . . . . . . . . 17 ((4 ∈ ℝ+ ∧ (√‘2) ∈ ℝ+) → (4 · (√‘2)) ∈ ℝ+)
6763, 65, 66mp2an 690 . . . . . . . . . . . . . . . 16 (4 · (√‘2)) ∈ ℝ+
68 rpne0 12397 . . . . . . . . . . . . . . . 16 ((4 · (√‘2)) ∈ ℝ+ → (4 · (√‘2)) ≠ 0)
6967, 68ax-mp 5 . . . . . . . . . . . . . . 15 (4 · (√‘2)) ≠ 0
70 rpne0 12397 . . . . . . . . . . . . . . . 16 ((√‘2) ∈ ℝ+ → (√‘2) ≠ 0)
7124, 64, 70mp2b 10 . . . . . . . . . . . . . . 15 (√‘2) ≠ 0
72 divcan5 11334 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ ((4 · (√‘2)) ∈ ℂ ∧ (4 · (√‘2)) ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = (3 / (4 · (√‘2))))
7332, 72mp3an1 1442 . . . . . . . . . . . . . . 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 11737 . . . . . . . . . . . . . . 15 4 ≠ 0
76 divdiv1 11343 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4 · (√‘2))))
7732, 76mp3an1 1442 . . . . . . . . . . . . . . 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 2845 . . . . . . . . . . . . 13 (((√‘2) · 3) / ((√‘2) · (4 · (√‘2)))) = ((3 / 4) / (√‘2))
8048, 32, 5, 38divassi 11388 . . . . . . . . . . . . 13 (((√‘2) · 3) / 8) = ((√‘2) · (3 / 8))
8160, 79, 803eqtr3ri 2851 . . . . . . . . . . . 12 ((√‘2) · (3 / 8)) = ((3 / 4) / (√‘2))
8281oveq1i 7158 . . . . . . . . . . 11 (((√‘2) · (3 / 8)) · (log‘2)) = (((3 / 4) / (√‘2)) · (log‘2))
8350, 82eqtr3i 2844 . . . . . . . . . 10 ((√‘2) · ((3 / 8) · (log‘2))) = (((3 / 4) / (√‘2)) · (log‘2))
8446, 83syl6eq 2870 . . . . . . . . 9 (𝑛 = 64 → ((√‘2) · (𝐺‘(√‘𝑛))) = (((3 / 4) / (√‘2)) · (log‘2)))
85 oveq1 7155 . . . . . . . . . . . . . 14 (𝑛 = 64 → (𝑛 / 2) = (64 / 2))
86 df-6 11696 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
8786oveq2i 7159 . . . . . . . . . . . . . . . . 17 (2↑6) = (2↑(5 + 1))
88 2exp6 16414 . . . . . . . . . . . . . . . . 17 (2↑6) = 64
89 2cn 11704 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
90 5nn0 11909 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ0
91 expp1 13428 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 5 ∈ ℕ0) → (2↑(5 + 1)) = ((2↑5) · 2))
9289, 90, 91mp2an 690 . . . . . . . . . . . . . . . . 17 (2↑(5 + 1)) = ((2↑5) · 2)
9387, 88, 923eqtr3i 2850 . . . . . . . . . . . . . . . 16 64 = ((2↑5) · 2)
9493oveq1i 7158 . . . . . . . . . . . . . . 15 (64 / 2) = (((2↑5) · 2) / 2)
95 nnexpcl 13434 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ ∧ 5 ∈ ℕ0) → (2↑5) ∈ ℕ)
9633, 90, 95mp2an 690 . . . . . . . . . . . . . . . . 17 (2↑5) ∈ ℕ
9796nncni 11640 . . . . . . . . . . . . . . . 16 (2↑5) ∈ ℂ
98 2ne0 11733 . . . . . . . . . . . . . . . 16 2 ≠ 0
9997, 89, 98divcan4i 11379 . . . . . . . . . . . . . . 15 (((2↑5) · 2) / 2) = (2↑5)
10094, 99eqtri 2842 . . . . . . . . . . . . . 14 (64 / 2) = (2↑5)
10185, 100syl6eq 2870 . . . . . . . . . . . . 13 (𝑛 = 64 → (𝑛 / 2) = (2↑5))
102101fveq2d 6667 . . . . . . . . . . . 12 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = (𝐺‘(2↑5)))
103 nnrp 12392 . . . . . . . . . . . . 13 ((2↑5) ∈ ℕ → (2↑5) ∈ ℝ+)
104 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑥 = (2↑5) → (log‘𝑥) = (log‘(2↑5)))
105 5nn 11715 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℕ
106105nnzi 11998 . . . . . . . . . . . . . . . . . 18 5 ∈ ℤ
107 relogexp 25171 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ 5 ∈ ℤ) → (log‘(2↑5)) = (5 · (log‘2)))
10824, 106, 107mp2an 690 . . . . . . . . . . . . . . . . 17 (log‘(2↑5)) = (5 · (log‘2))
109104, 108syl6eq 2870 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → (log‘𝑥) = (5 · (log‘2)))
110 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = (2↑5) → 𝑥 = (2↑5))
111109, 110oveq12d 7166 . . . . . . . . . . . . . . 15 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 · (log‘2)) / (2↑5)))
112 5cn 11717 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
11396nnne0i 11669 . . . . . . . . . . . . . . . 16 (2↑5) ≠ 0
114112, 37, 97, 113div23i 11390 . . . . . . . . . . . . . . 15 ((5 · (log‘2)) / (2↑5)) = ((5 / (2↑5)) · (log‘2))
115111, 114syl6eq 2870 . . . . . . . . . . . . . 14 (𝑥 = (2↑5) → ((log‘𝑥) / 𝑥) = ((5 / (2↑5)) · (log‘2)))
116 ovex 7181 . . . . . . . . . . . . . 14 ((5 / (2↑5)) · (log‘2)) ∈ V
117115, 41, 116fvmpt 6761 . . . . . . . . . . . . 13 ((2↑5) ∈ ℝ+ → (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2)))
11896, 103, 117mp2b 10 . . . . . . . . . . . 12 (𝐺‘(2↑5)) = ((5 / (2↑5)) · (log‘2))
119102, 118syl6eq 2870 . . . . . . . . . . 11 (𝑛 = 64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) · (log‘2)))
120119oveq2d 7164 . . . . . . . . . 10 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5)) · (log‘2))))
121 9cn 11729 . . . . . . . . . . . 12 9 ∈ ℂ
122121, 51, 75divcli 11374 . . . . . . . . . . 11 (9 / 4) ∈ ℂ
123112, 97, 113divcli 11374 . . . . . . . . . . 11 (5 / (2↑5)) ∈ ℂ
124122, 123, 37mulassi 10644 . . . . . . . . . 10 (((9 / 4) · (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 / (2↑5)) · (log‘2)))
125120, 124syl6eqr 2872 . . . . . . . . 9 (𝑛 = 64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 / (2↑5))) · (log‘2)))
12684, 125oveq12d 7166 . . . . . . . 8 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9 / 4) · (5 / (2↑5))) · (log‘2))))
12732, 51, 75divcli 11374 . . . . . . . . . 10 (3 / 4) ∈ ℂ
128127, 48, 71divcli 11374 . . . . . . . . 9 ((3 / 4) / (√‘2)) ∈ ℂ
129122, 123mulcli 10640 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) ∈ ℂ
130128, 129, 37adddiri 10646 . . . . . . . 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 2872 . . . . . . 7 (𝑛 = 64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) · (log‘2)))
132 oveq2 7156 . . . . . . . . . . 11 (𝑛 = 64 → (2 · 𝑛) = (2 · 64))
133132fveq2d 6667 . . . . . . . . . 10 (𝑛 = 64 → (√‘(2 · 𝑛)) = (√‘(2 · 64)))
1343nnrei 11639 . . . . . . . . . . . 12 64 ∈ ℝ
1353nngt0i 11668 . . . . . . . . . . . . 13 0 < 64
13610, 134, 135ltleii 10755 . . . . . . . . . . . 12 0 ≤ 64
13753, 134, 54, 136sqrtmulii 14738 . . . . . . . . . . 11 (√‘(2 · 64)) = ((√‘2) · (√‘64))
13816oveq2i 7159 . . . . . . . . . . 11 ((√‘2) · (√‘64)) = ((√‘2) · 8)
139137, 138eqtri 2842 . . . . . . . . . 10 (√‘(2 · 64)) = ((√‘2) · 8)
140133, 139syl6eq 2870 . . . . . . . . 9 (𝑛 = 64 → (√‘(2 · 𝑛)) = ((√‘2) · 8))
141140oveq2d 7164 . . . . . . . 8 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / ((√‘2) · 8)))
14248, 5mulcli 10640 . . . . . . . . . 10 ((√‘2) · 8) ∈ ℂ
143 rpmulcl 12404 . . . . . . . . . . . 12 (((√‘2) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((√‘2) · 8) ∈ ℝ+)
14465, 20, 143sylancr 589 . . . . . . . . . . 11 (8 ∈ ℕ → ((√‘2) · 8) ∈ ℝ+)
145 rpne0 12397 . . . . . . . . . . 11 (((√‘2) · 8) ∈ ℝ+ → ((√‘2) · 8) ≠ 0)
14619, 144, 145mp2b 10 . . . . . . . . . 10 ((√‘2) · 8) ≠ 0
147 divrec2 11307 . . . . . . . . . 10 (((log‘2) ∈ ℂ ∧ ((√‘2) · 8) ∈ ℂ ∧ ((√‘2) · 8) ≠ 0) → ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2)))
14837, 142, 146, 147mp3an 1455 . . . . . . . . 9 ((log‘2) / ((√‘2) · 8)) = ((1 / ((√‘2) · 8)) · (log‘2))
14948, 5mulcomi 10641 . . . . . . . . . . . 12 ((√‘2) · 8) = (8 · (√‘2))
150149oveq2i 7159 . . . . . . . . . . 11 (1 / ((√‘2) · 8)) = (1 / (8 · (√‘2)))
151 recdiv2 11345 . . . . . . . . . . . 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 2845 . . . . . . . . . 10 (1 / ((√‘2) · 8)) = ((1 / 8) / (√‘2))
154153oveq1i 7158 . . . . . . . . 9 ((1 / ((√‘2) · 8)) · (log‘2)) = (((1 / 8) / (√‘2)) · (log‘2))
155148, 154eqtri 2842 . . . . . . . 8 ((log‘2) / ((√‘2) · 8)) = (((1 / 8) / (√‘2)) · (log‘2))
156141, 155syl6eq 2870 . . . . . . 7 (𝑛 = 64 → ((log‘2) / (√‘(2 · 𝑛))) = (((1 / 8) / (√‘2)) · (log‘2)))
157131, 156oveq12d 7166 . . . . . 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 10639 . . . . . . 7 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℂ
1595, 38reccli 11362 . . . . . . . 8 (1 / 8) ∈ ℂ
160159, 48, 71divcli 11374 . . . . . . 7 ((1 / 8) / (√‘2)) ∈ ℂ
161158, 160, 37adddiri 10646 . . . . . 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 2872 . . . . 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 7181 . . . . 5 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ V
165162, 163, 164fvmpt 6761 . . . 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 11709 . . . . . . . 8 3 ∈ ℝ
168 4re 11713 . . . . . . . 8 4 ∈ ℝ
169167, 168, 75redivcli 11399 . . . . . . 7 (3 / 4) ∈ ℝ
170169, 47, 71redivcli 11399 . . . . . 6 ((3 / 4) / (√‘2)) ∈ ℝ
171 9re 11728 . . . . . . . 8 9 ∈ ℝ
172171, 168, 75redivcli 11399 . . . . . . 7 (9 / 4) ∈ ℝ
173 5re 11716 . . . . . . . 8 5 ∈ ℝ
17496nnrei 11639 . . . . . . . 8 (2↑5) ∈ ℝ
175173, 174, 113redivcli 11399 . . . . . . 7 (5 / (2↑5)) ∈ ℝ
176172, 175remulcli 10649 . . . . . 6 ((9 / 4) · (5 / (2↑5))) ∈ ℝ
177170, 176readdcli 10648 . . . . 5 (((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
17811, 38rereccli 11397 . . . . . 6 (1 / 8) ∈ ℝ
179178, 47, 71redivcli 11399 . . . . 5 ((1 / 8) / (√‘2)) ∈ ℝ
180177, 179readdcli 10648 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ∈ ℝ
181180, 36remulcli 10649 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) ∈ ℝ
182166, 181eqeltri 2907 . 2 (𝐹64) ∈ ℝ
183128, 129, 160add32i 10855 . . . . . 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 11720 . . . . . . . . . . 11 6 ∈ ℂ
185 ax-1cn 10587 . . . . . . . . . . 11 1 ∈ ℂ
186184, 185, 5, 38divdiri 11389 . . . . . . . . . 10 ((6 + 1) / 8) = ((6 / 8) + (1 / 8))
187 df-7 11697 . . . . . . . . . . 11 7 = (6 + 1)
188187oveq1i 7158 . . . . . . . . . 10 (7 / 8) = ((6 + 1) / 8)
189 divcan5 11334 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 / 4))
19032, 189mp3an1 1442 . . . . . . . . . . . . 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 11795 . . . . . . . . . . . . . 14 (3 · 2) = 6
19332, 89, 192mulcomli 10642 . . . . . . . . . . . . 13 (2 · 3) = 6
19451, 89, 58mulcomli 10642 . . . . . . . . . . . . 13 (2 · 4) = 8
195193, 194oveq12i 7160 . . . . . . . . . . . 12 ((2 · 3) / (2 · 4)) = (6 / 8)
196191, 195eqtr3i 2844 . . . . . . . . . . 11 (3 / 4) = (6 / 8)
197196oveq1i 7158 . . . . . . . . . 10 ((3 / 4) + (1 / 8)) = ((6 / 8) + (1 / 8))
198186, 188, 1973eqtr4ri 2853 . . . . . . . . 9 ((3 / 4) + (1 / 8)) = (7 / 8)
199198oveq1i 7158 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = ((7 / 8) / (√‘2))
200127, 159, 48, 71divdiri 11389 . . . . . . . 8 (((3 / 4) + (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2)))
201 7cn 11723 . . . . . . . . 9 7 ∈ ℂ
202201, 5, 48, 38, 71divdiv32i 11387 . . . . . . . 8 ((7 / 8) / (√‘2)) = ((7 / (√‘2)) / 8)
203199, 200, 2023eqtr3i 2850 . . . . . . 7 (((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) = ((7 / (√‘2)) / 8)
204203oveq1i 7158 . . . . . 6 ((((3 / 4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5 / (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
205183, 204eqtri 2842 . . . . 5 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5))))
206 4nn0 11908 . . . . . . . . . . . 12 4 ∈ ℕ0
207 9nn0 11913 . . . . . . . . . . . 12 9 ∈ ℕ0
208 0nn0 11904 . . . . . . . . . . . 12 0 ∈ ℕ0
209 9lt10 12221 . . . . . . . . . . . 12 9 < 10
210 4lt5 11806 . . . . . . . . . . . 12 4 < 5
211206, 90, 207, 208, 209, 210decltc 12119 . . . . . . . . . . 11 49 < 50
212 7t7e49 12204 . . . . . . . . . . 11 (7 · 7) = 49
21356oveq1i 7158 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (2 · (5 · 5))
21448, 48, 112, 112mul4i 10829 . . . . . . . . . . . 12 (((√‘2) · (√‘2)) · (5 · 5)) = (((√‘2) · 5) · ((√‘2) · 5))
215 5t2e10 12190 . . . . . . . . . . . . . . 15 (5 · 2) = 10
216112, 89, 215mulcomli 10642 . . . . . . . . . . . . . 14 (2 · 5) = 10
217216oveq1i 7158 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (10 · 5)
21889, 112, 112mulassi 10644 . . . . . . . . . . . . 13 ((2 · 5) · 5) = (2 · (5 · 5))
21990dec0u 12111 . . . . . . . . . . . . 13 (10 · 5) = 50
220217, 218, 2193eqtr3i 2850 . . . . . . . . . . . 12 (2 · (5 · 5)) = 50
221213, 214, 2203eqtr3i 2850 . . . . . . . . . . 11 (((√‘2) · 5) · ((√‘2) · 5)) = 50
222211, 212, 2213brtr4i 5087 . . . . . . . . . 10 (7 · 7) < (((√‘2) · 5) · ((√‘2) · 5))
223 7re 11722 . . . . . . . . . . . 12 7 ∈ ℝ
224 7pos 11740 . . . . . . . . . . . 12 0 < 7
22510, 223, 224ltleii 10755 . . . . . . . . . . 11 0 ≤ 7
226 nnrp 12392 . . . . . . . . . . . . . 14 (5 ∈ ℕ → 5 ∈ ℝ+)
227105, 226ax-mp 5 . . . . . . . . . . . . 13 5 ∈ ℝ+
228 rpmulcl 12404 . . . . . . . . . . . . 13 (((√‘2) ∈ ℝ+ ∧ 5 ∈ ℝ+) → ((√‘2) · 5) ∈ ℝ+)
22965, 227, 228mp2an 690 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ+
230 rpge0 12394 . . . . . . . . . . . 12 (((√‘2) · 5) ∈ ℝ+ → 0 ≤ ((√‘2) · 5))
231229, 230ax-mp 5 . . . . . . . . . . 11 0 ≤ ((√‘2) · 5)
232 rpre 12389 . . . . . . . . . . . . 13 (((√‘2) · 5) ∈ ℝ+ → ((√‘2) · 5) ∈ ℝ)
233229, 232ax-mp 5 . . . . . . . . . . . 12 ((√‘2) · 5) ∈ ℝ
234223, 233lt2msqi 11544 . . . . . . . . . . 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 233 . . . . . . . . 9 7 < ((√‘2) · 5)
237 rpgt0 12393 . . . . . . . . . . 11 ((√‘2) ∈ ℝ+ → 0 < (√‘2))
23824, 64, 237mp2b 10 . . . . . . . . . 10 0 < (√‘2)
239 ltdivmul 11507 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ ∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
240223, 173, 239mp3an12 1445 . . . . . . . . . 10 (((√‘2) ∈ ℝ ∧ 0 < (√‘2)) → ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5)))
24147, 238, 240mp2an 690 . . . . . . . . 9 ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2) · 5))
242236, 241mpbir 233 . . . . . . . 8 (7 / (√‘2)) < 5
243223, 47, 71redivcli 11399 . . . . . . . . 9 (7 / (√‘2)) ∈ ℝ
244243, 173, 11, 12ltdiv1ii 11561 . . . . . . . 8 ((7 / (√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 / 8))
245242, 244mpbi 232 . . . . . . 7 ((7 / (√‘2)) / 8) < (5 / 8)
246 divsubdir 11326 . . . . . . . . . . 11 ((8 ∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → ((8 − 3) / 8) = ((8 / 8) − (3 / 8)))
2475, 32, 246mp3an12 1445 . . . . . . . . . 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 11786 . . . . . . . . . . . 12 (5 + 3) = 8
250249oveq1i 7158 . . . . . . . . . . 11 ((5 + 3) − 3) = (8 − 3)
251112, 32pncan3oi 10894 . . . . . . . . . . 11 ((5 + 3) − 3) = 5
252250, 251eqtr3i 2844 . . . . . . . . . 10 (8 − 3) = 5
253252oveq1i 7158 . . . . . . . . 9 ((8 − 3) / 8) = (5 / 8)
2545, 38dividi 11365 . . . . . . . . . 10 (8 / 8) = 1
255254oveq1i 7158 . . . . . . . . 9 ((8 / 8) − (3 / 8)) = (1 − (3 / 8))
256248, 253, 2553eqtr3ri 2851 . . . . . . . 8 (1 − (3 / 8)) = (5 / 8)
257 5lt8 11823 . . . . . . . . . . . . 13 5 < 8
25811, 173remulcli 10649 . . . . . . . . . . . . . 14 (8 · 5) ∈ ℝ
259173, 11, 258ltadd2i 10763 . . . . . . . . . . . . 13 (5 < 8 ↔ ((8 · 5) + 5) < ((8 · 5) + 8))
260257, 259mpbi 232 . . . . . . . . . . . 12 ((8 · 5) + 5) < ((8 · 5) + 8)
261 df-9 11699 . . . . . . . . . . . . . 14 9 = (8 + 1)
262261oveq1i 7158 . . . . . . . . . . . . 13 (9 · 5) = ((8 + 1) · 5)
2635, 185, 112adddiri 10646 . . . . . . . . . . . . 13 ((8 + 1) · 5) = ((8 · 5) + (1 · 5))
264112mulid2i 10638 . . . . . . . . . . . . . 14 (1 · 5) = 5
265264oveq2i 7159 . . . . . . . . . . . . 13 ((8 · 5) + (1 · 5)) = ((8 · 5) + 5)
266262, 263, 2653eqtri 2846 . . . . . . . . . . . 12 (9 · 5) = ((8 · 5) + 5)
26786oveq2i 7159 . . . . . . . . . . . . 13 (8 · 6) = (8 · (5 + 1))
2685, 112, 185adddii 10645 . . . . . . . . . . . . 13 (8 · (5 + 1)) = ((8 · 5) + (8 · 1))
2695mulid1i 10637 . . . . . . . . . . . . . 14 (8 · 1) = 8
270269oveq2i 7159 . . . . . . . . . . . . 13 ((8 · 5) + (8 · 1)) = ((8 · 5) + 8)
271267, 268, 2703eqtri 2846 . . . . . . . . . . . 12 (8 · 6) = ((8 · 5) + 8)
272260, 266, 2713brtr4i 5087 . . . . . . . . . . 11 (9 · 5) < (8 · 6)
273171, 173remulcli 10649 . . . . . . . . . . . 12 (9 · 5) ∈ ℝ
274 6re 11719 . . . . . . . . . . . . 13 6 ∈ ℝ
27511, 274remulcli 10649 . . . . . . . . . . . 12 (8 · 6) ∈ ℝ
276168, 174remulcli 10649 . . . . . . . . . . . 12 (4 · (2↑5)) ∈ ℝ
2772, 96nnmulcli 11654 . . . . . . . . . . . . 13 (4 · (2↑5)) ∈ ℕ
278277nngt0i 11668 . . . . . . . . . . . 12 0 < (4 · (2↑5))
279273, 275, 276, 278ltdiv1ii 11561 . . . . . . . . . . 11 ((9 · 5) < (8 · 6) ↔ ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5))))
280272, 279mpbi 232 . . . . . . . . . 10 ((9 · 5) / (4 · (2↑5))) < ((8 · 6) / (4 · (2↑5)))
281121, 51, 112, 97, 75, 113divmuldivi 11392 . . . . . . . . . 10 ((9 / 4) · (5 / (2↑5))) = ((9 · 5) / (4 · (2↑5)))
282 nnexpcl 13434 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈ ℕ)
28333, 206, 282mp2an 690 . . . . . . . . . . . . 13 (2↑4) ∈ ℕ
284283nncni 11640 . . . . . . . . . . . 12 (2↑4) ∈ ℂ
285283nnne0i 11669 . . . . . . . . . . . 12 (2↑4) ≠ 0
286 divcan5 11334 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧ (2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8)) = (3 / 8))
28732, 286mp3an1 1442 . . . . . . . . . . . 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 11694 . . . . . . . . . . . . . . . 16 4 = (3 + 1)
290289oveq2i 7159 . . . . . . . . . . . . . . 15 (2↑4) = (2↑(3 + 1))
291 3nn0 11907 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
292 expp1 13428 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 3 ∈ ℕ0) → (2↑(3 + 1)) = ((2↑3) · 2))
29389, 291, 292mp2an 690 . . . . . . . . . . . . . . 15 (2↑(3 + 1)) = ((2↑3) · 2)
29422oveq1i 7158 . . . . . . . . . . . . . . 15 ((2↑3) · 2) = (8 · 2)
295290, 293, 2943eqtri 2846 . . . . . . . . . . . . . 14 (2↑4) = (8 · 2)
296295oveq1i 7158 . . . . . . . . . . . . 13 ((2↑4) · 3) = ((8 · 2) · 3)
2975, 89, 32mulassi 10644 . . . . . . . . . . . . 13 ((8 · 2) · 3) = (8 · (2 · 3))
298193oveq2i 7159 . . . . . . . . . . . . 13 (8 · (2 · 3)) = (8 · 6)
299296, 297, 2983eqtri 2846 . . . . . . . . . . . 12 ((2↑4) · 3) = (8 · 6)
300 4p3e7 11783 . . . . . . . . . . . . . . . 16 (4 + 3) = 7
301 5p2e7 11785 . . . . . . . . . . . . . . . 16 (5 + 2) = 7
302112, 89addcomi 10823 . . . . . . . . . . . . . . . 16 (5 + 2) = (2 + 5)
303300, 301, 3023eqtr2i 2848 . . . . . . . . . . . . . . 15 (4 + 3) = (2 + 5)
304303oveq2i 7159 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = (2↑(2 + 5))
305 expadd 13463 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(4 + 3)) = ((2↑4) · (2↑3)))
30689, 206, 291, 305mp3an 1455 . . . . . . . . . . . . . 14 (2↑(4 + 3)) = ((2↑4) · (2↑3))
307 2nn0 11906 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
308 expadd 13463 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 5 ∈ ℕ0) → (2↑(2 + 5)) = ((2↑2) · (2↑5)))
30989, 307, 90, 308mp3an 1455 . . . . . . . . . . . . . 14 (2↑(2 + 5)) = ((2↑2) · (2↑5))
310304, 306, 3093eqtr3i 2850 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑2) · (2↑5))
31122oveq2i 7159 . . . . . . . . . . . . 13 ((2↑4) · (2↑3)) = ((2↑4) · 8)
312 sq2 13552 . . . . . . . . . . . . . 14 (2↑2) = 4
313312oveq1i 7158 . . . . . . . . . . . . 13 ((2↑2) · (2↑5)) = (4 · (2↑5))
314310, 311, 3133eqtr3i 2850 . . . . . . . . . . . 12 ((2↑4) · 8) = (4 · (2↑5))
315299, 314oveq12i 7160 . . . . . . . . . . 11 (((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) / (4 · (2↑5)))
316288, 315eqtr3i 2844 . . . . . . . . . 10 (3 / 8) = ((8 · 6) / (4 · (2↑5)))
317280, 281, 3163brtr4i 5087 . . . . . . . . 9 ((9 / 4) · (5 / (2↑5))) < (3 / 8)
318167, 11, 38redivcli 11399 . . . . . . . . . 10 (3 / 8) ∈ ℝ
319 1re 10633 . . . . . . . . . 10 1 ∈ ℝ
320 ltsub2 11129 . . . . . . . . . 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 1455 . . . . . . . . 9 (((9 / 4) · (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5)))))
322317, 321mpbi 232 . . . . . . . 8 (1 − (3 / 8)) < (1 − ((9 / 4) · (5 / (2↑5))))
323256, 322eqbrtrri 5080 . . . . . . 7 (5 / 8) < (1 − ((9 / 4) · (5 / (2↑5))))
324243, 11, 38redivcli 11399 . . . . . . . 8 ((7 / (√‘2)) / 8) ∈ ℝ
325173, 11, 38redivcli 11399 . . . . . . . 8 (5 / 8) ∈ ℝ
326319, 176resubcli 10940 . . . . . . . 8 (1 − ((9 / 4) · (5 / (2↑5)))) ∈ ℝ
327324, 325, 326lttri 10758 . . . . . . 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 11193 . . . . . 6 ((((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔ ((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 / (2↑5)))))
330328, 329mpbir 233 . . . . 5 (((7 / (√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1
331205, 330eqbrtri 5078 . . . 4 ((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) < 1
332 1lt2 11800 . . . . . . 7 1 < 2
333 rplogcl 25179 . . . . . . 7 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
33453, 332, 333mp2an 690 . . . . . 6 (log‘2) ∈ ℝ+
335 rpgt0 12393 . . . . . 6 ((log‘2) ∈ ℝ+ → 0 < (log‘2))
336334, 335ax-mp 5 . . . . 5 0 < (log‘2)
337180, 319, 36, 336ltmul1ii 11560 . . . 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 232 . . 3 (((((3 / 4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) / (√‘2))) · (log‘2)) < (1 · (log‘2))
33937mulid2i 10638 . . . 4 (1 · (log‘2)) = (log‘2)
340339eqcomi 2828 . . 3 (log‘2) = (1 · (log‘2))
341338, 166, 3403brtr4i 5087 . 2 (𝐹64) < (log‘2)
342182, 341pm3.2i 473 1 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398   = wceq 1531  wcel 2108  wne 3014   class class class wbr 5057  cmpt 5137  cfv 6348  (class class class)co 7148  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667  cle 10668  cmin 10862   / cdiv 11289  cn 11630  2c2 11684  3c3 11685  4c4 11686  5c5 11687  6c6 11688  7c7 11689  8c8 11690  9c9 11691  0cn0 11889  cz 11973  cdc 12090  +crp 12381  cexp 13421  csqrt 14584  logclog 25130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-fal 1544  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-supp 7823  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12885  df-fzo 13026  df-fl 13154  df-mod 13230  df-seq 13362  df-exp 13422  df-fac 13626  df-bc 13655  df-hash 13683  df-shft 14418  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-fbas 20534  df-fg 20535  df-cnfld 20538  df-top 21494  df-topon 21511  df-topsp 21533  df-bases 21546  df-cld 21619  df-ntr 21620  df-cls 21621  df-nei 21698  df-lp 21736  df-perf 21737  df-cn 21827  df-cnp 21828  df-haus 21915  df-tx 22162  df-hmeo 22355  df-fil 22446  df-fm 22538  df-flim 22539  df-flf 22540  df-xms 22922  df-ms 22923  df-tms 22924  df-cncf 23478  df-limc 24456  df-dv 24457  df-log 25132
This theorem is referenced by:  bposlem9  25860
  Copyright terms: Public domain W3C validator