Proof of Theorem bposlem8
Step | Hyp | Ref
| Expression |
1 | | 6nn0 12264 |
. . . . 5
⊢ 6 ∈
ℕ0 |
2 | | 4nn 12066 |
. . . . 5
⊢ 4 ∈
ℕ |
3 | 1, 2 | decnncl 12467 |
. . . 4
⊢ ;64 ∈ ℕ |
4 | | fveq2 6766 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = ;64 → (√‘𝑛) = (√‘;64)) |
5 | | 8cn 12080 |
. . . . . . . . . . . . . . . . . 18
⊢ 8 ∈
ℂ |
6 | 5 | sqvali 13907 |
. . . . . . . . . . . . . . . . 17
⊢
(8↑2) = (8 · 8) |
7 | | 8t8e64 12568 |
. . . . . . . . . . . . . . . . 17
⊢ (8
· 8) = ;64 |
8 | 6, 7 | eqtri 2766 |
. . . . . . . . . . . . . . . 16
⊢
(8↑2) = ;64 |
9 | 8 | fveq2i 6769 |
. . . . . . . . . . . . . . 15
⊢
(√‘(8↑2)) = (√‘;64) |
10 | | 0re 10987 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
11 | | 8re 12079 |
. . . . . . . . . . . . . . . . 17
⊢ 8 ∈
ℝ |
12 | | 8pos 12095 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
8 |
13 | 10, 11, 12 | ltleii 11108 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
8 |
14 | 11 | sqrtsqi 15096 |
. . . . . . . . . . . . . . . 16
⊢ (0 ≤ 8
→ (√‘(8↑2)) = 8) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(√‘(8↑2)) = 8 |
16 | 9, 15 | eqtr3i 2768 |
. . . . . . . . . . . . . 14
⊢
(√‘;64) =
8 |
17 | 4, 16 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑛 = ;64 → (√‘𝑛) = 8) |
18 | 17 | fveq2d 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 |
23 | 22 | fveq2i 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))) |
27 | 24, 25, 26 | mp2an 689 |
. . . . . . . . . . . . . . . . . 18
⊢
(log‘(2↑3)) = (3 · (log‘2)) |
28 | 23, 27 | eqtr3i 2768 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘8) = (3 · (log‘2)) |
29 | 21, 28 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 8 → (log‘𝑥) = (3 ·
(log‘2))) |
30 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 8 → 𝑥 = 8) |
31 | 29, 30 | oveq12d 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) ∈ ℝ) |
36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘2) ∈ ℝ |
37 | 36 | recni 10999 |
. . . . . . . . . . . . . . . 16
⊢
(log‘2) ∈ ℂ |
38 | 19 | nnne0i 12023 |
. . . . . . . . . . . . . . . 16
⊢ 8 ≠
0 |
39 | 32, 37, 5, 38 | div23i 11743 |
. . . . . . . . . . . . . . 15
⊢ ((3
· (log‘2)) / 8) = ((3 / 8) ·
(log‘2)) |
40 | 31, 39 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 8 → ((log‘𝑥) / 𝑥) = ((3 / 8) ·
(log‘2))) |
41 | | bposlem7.2 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦
((log‘𝑥) / 𝑥)) |
42 | | ovex 7300 |
. . . . . . . . . . . . . 14
⊢ ((3 / 8)
· (log‘2)) ∈ V |
43 | 40, 41, 42 | fvmpt 6867 |
. . . . . . . . . . . . 13
⊢ (8 ∈
ℝ+ → (𝐺‘8) = ((3 / 8) ·
(log‘2))) |
44 | 19, 20, 43 | mp2b 10 |
. . . . . . . . . . . 12
⊢ (𝐺‘8) = ((3 / 8) ·
(log‘2)) |
45 | 18, 44 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑛 = ;64 → (𝐺‘(√‘𝑛)) = ((3 / 8) ·
(log‘2))) |
46 | 45 | oveq2d 7283 |
. . . . . . . . . 10
⊢ (𝑛 = ;64 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2)
· ((3 / 8) · (log‘2)))) |
47 | | sqrt2re 15969 |
. . . . . . . . . . . . 13
⊢
(√‘2) ∈ ℝ |
48 | 47 | recni 10999 |
. . . . . . . . . . . 12
⊢
(√‘2) ∈ ℂ |
49 | 32, 5, 38 | divcli 11727 |
. . . . . . . . . . . 12
⊢ (3 / 8)
∈ ℂ |
50 | 48, 49, 37 | mulassi 10996 |
. . . . . . . . . . 11
⊢
(((√‘2) · (3 / 8)) · (log‘2)) =
((√‘2) · ((3 / 8) · (log‘2))) |
51 | | 4cn 12068 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℂ |
52 | 48, 51, 48 | mul12i 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) |
56 | 53, 54, 55 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢
((√‘2) · (√‘2)) = 2 |
57 | 56 | oveq2i 7278 |
. . . . . . . . . . . . . . 15
⊢ (4
· ((√‘2) · (√‘2))) = (4 ·
2) |
58 | | 4t2e8 12151 |
. . . . . . . . . . . . . . 15
⊢ (4
· 2) = 8 |
59 | 52, 57, 58 | 3eqtri 2770 |
. . . . . . . . . . . . . 14
⊢
((√‘2) · (4 · (√‘2))) =
8 |
60 | 59 | oveq2i 7278 |
. . . . . . . . . . . . 13
⊢
(((√‘2) · 3) / ((√‘2) · (4
· (√‘2)))) = (((√‘2) · 3) /
8) |
61 | 51, 48 | mulcli 10992 |
. . . . . . . . . . . . . . 15
⊢ (4
· (√‘2)) ∈ ℂ |
62 | | nnrp 12751 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
63 | 2, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℝ+ |
64 | | rpsqrtcl 14986 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
ℝ+ → (√‘2) ∈
ℝ+) |
65 | 33, 34, 64 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
⊢
(√‘2) ∈ ℝ+ |
66 | | rpmulcl 12763 |
. . . . . . . . . . . . . . . . 17
⊢ ((4
∈ ℝ+ ∧ (√‘2) ∈ ℝ+)
→ (4 · (√‘2)) ∈
ℝ+) |
67 | 63, 65, 66 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ (4
· (√‘2)) ∈ ℝ+ |
68 | | rpne0 12756 |
. . . . . . . . . . . . . . . 16
⊢ ((4
· (√‘2)) ∈ ℝ+ → (4 ·
(√‘2)) ≠ 0) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (4
· (√‘2)) ≠ 0 |
70 | | rpne0 12756 |
. . . . . . . . . . . . . . . 16
⊢
((√‘2) ∈ ℝ+ → (√‘2)
≠ 0) |
71 | 24, 64, 70 | mp2b 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)))) |
73 | 32, 72 | mp3an1 1447 |
. . . . . . . . . . . . . . 15
⊢ ((((4
· (√‘2)) ∈ ℂ ∧ (4 · (√‘2))
≠ 0) ∧ ((√‘2) ∈ ℂ ∧ (√‘2) ≠
0)) → (((√‘2) · 3) / ((√‘2) · (4
· (√‘2)))) = (3 / (4 ·
(√‘2)))) |
74 | 61, 69, 48, 71, 73 | mp4an 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)))) |
77 | 32, 76 | mp3an1 1447 |
. . . . . . . . . . . . . . 15
⊢ (((4
∈ ℂ ∧ 4 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧
(√‘2) ≠ 0)) → ((3 / 4) / (√‘2)) = (3 / (4
· (√‘2)))) |
78 | 51, 75, 48, 71, 77 | mp4an 690 |
. . . . . . . . . . . . . 14
⊢ ((3 / 4)
/ (√‘2)) = (3 / (4 · (√‘2))) |
79 | 74, 78 | eqtr4i 2769 |
. . . . . . . . . . . . 13
⊢
(((√‘2) · 3) / ((√‘2) · (4
· (√‘2)))) = ((3 / 4) / (√‘2)) |
80 | 48, 32, 5, 38 | divassi 11741 |
. . . . . . . . . . . . 13
⊢
(((√‘2) · 3) / 8) = ((√‘2) · (3 /
8)) |
81 | 60, 79, 80 | 3eqtr3ri 2775 |
. . . . . . . . . . . 12
⊢
((√‘2) · (3 / 8)) = ((3 / 4) /
(√‘2)) |
82 | 81 | oveq1i 7277 |
. . . . . . . . . . 11
⊢
(((√‘2) · (3 / 8)) · (log‘2)) = (((3 /
4) / (√‘2)) · (log‘2)) |
83 | 50, 82 | eqtr3i 2768 |
. . . . . . . . . 10
⊢
((√‘2) · ((3 / 8) · (log‘2))) = (((3 /
4) / (√‘2)) · (log‘2)) |
84 | 46, 83 | eqtrdi 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) |
87 | 86 | oveq2i 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)) |
92 | 89, 90, 91 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑(5 + 1)) = ((2↑5) · 2) |
93 | 87, 88, 92 | 3eqtr3i 2774 |
. . . . . . . . . . . . . . . 16
⊢ ;64 = ((2↑5) ·
2) |
94 | 93 | oveq1i 7277 |
. . . . . . . . . . . . . . 15
⊢ (;64 / 2) = (((2↑5) · 2) /
2) |
95 | | nnexpcl 13805 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℕ ∧ 5 ∈ ℕ0) → (2↑5) ∈
ℕ) |
96 | 33, 90, 95 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑5) ∈ ℕ |
97 | 96 | nncni 11993 |
. . . . . . . . . . . . . . . 16
⊢
(2↑5) ∈ ℂ |
98 | | 2ne0 12087 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
0 |
99 | 97, 89, 98 | divcan4i 11732 |
. . . . . . . . . . . . . . 15
⊢
(((2↑5) · 2) / 2) = (2↑5) |
100 | 94, 99 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢ (;64 / 2) = (2↑5) |
101 | 85, 100 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑛 = ;64 → (𝑛 / 2) = (2↑5)) |
102 | 101 | fveq2d 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 ∈
ℕ |
106 | 105 | nnzi 12354 |
. . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℤ |
107 | | relogexp 25761 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ+ ∧ 5 ∈ ℤ) →
(log‘(2↑5)) = (5 · (log‘2))) |
108 | 24, 106, 107 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘(2↑5)) = (5 · (log‘2)) |
109 | 104, 108 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (2↑5) →
(log‘𝑥) = (5 ·
(log‘2))) |
110 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (2↑5) → 𝑥 = (2↑5)) |
111 | 109, 110 | oveq12d 7285 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (2↑5) →
((log‘𝑥) / 𝑥) = ((5 · (log‘2))
/ (2↑5))) |
112 | | 5cn 12071 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℂ |
113 | 96 | nnne0i 12023 |
. . . . . . . . . . . . . . . 16
⊢
(2↑5) ≠ 0 |
114 | 112, 37, 97, 113 | div23i 11743 |
. . . . . . . . . . . . . . 15
⊢ ((5
· (log‘2)) / (2↑5)) = ((5 / (2↑5)) ·
(log‘2)) |
115 | 111, 114 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (2↑5) →
((log‘𝑥) / 𝑥) = ((5 / (2↑5)) ·
(log‘2))) |
116 | | ovex 7300 |
. . . . . . . . . . . . . 14
⊢ ((5 /
(2↑5)) · (log‘2)) ∈ V |
117 | 115, 41, 116 | fvmpt 6867 |
. . . . . . . . . . . . 13
⊢
((2↑5) ∈ ℝ+ → (𝐺‘(2↑5)) = ((5 / (2↑5))
· (log‘2))) |
118 | 96, 103, 117 | mp2b 10 |
. . . . . . . . . . . 12
⊢ (𝐺‘(2↑5)) = ((5 /
(2↑5)) · (log‘2)) |
119 | 102, 118 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑛 = ;64 → (𝐺‘(𝑛 / 2)) = ((5 / (2↑5)) ·
(log‘2))) |
120 | 119 | oveq2d 7283 |
. . . . . . . . . 10
⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · ((5 / (2↑5))
· (log‘2)))) |
121 | | 9cn 12083 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℂ |
122 | 121, 51, 75 | divcli 11727 |
. . . . . . . . . . 11
⊢ (9 / 4)
∈ ℂ |
123 | 112, 97, 113 | divcli 11727 |
. . . . . . . . . . 11
⊢ (5 /
(2↑5)) ∈ ℂ |
124 | 122, 123,
37 | mulassi 10996 |
. . . . . . . . . 10
⊢ (((9 / 4)
· (5 / (2↑5))) · (log‘2)) = ((9 / 4) · ((5 /
(2↑5)) · (log‘2))) |
125 | 120, 124 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑛 = ;64 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = (((9 / 4) · (5 /
(2↑5))) · (log‘2))) |
126 | 84, 125 | oveq12d 7285 |
. . . . . . . 8
⊢ (𝑛 = ;64 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = ((((3 / 4) / (√‘2))
· (log‘2)) + (((9 / 4) · (5 / (2↑5))) ·
(log‘2)))) |
127 | 32, 51, 75 | divcli 11727 |
. . . . . . . . . 10
⊢ (3 / 4)
∈ ℂ |
128 | 127, 48, 71 | divcli 11727 |
. . . . . . . . 9
⊢ ((3 / 4)
/ (√‘2)) ∈ ℂ |
129 | 122, 123 | mulcli 10992 |
. . . . . . . . 9
⊢ ((9 / 4)
· (5 / (2↑5))) ∈ ℂ |
130 | 128, 129,
37 | adddiri 10998 |
. . . . . . . 8
⊢ ((((3 /
4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ·
(log‘2)) = ((((3 / 4) / (√‘2)) · (log‘2)) + (((9
/ 4) · (5 / (2↑5))) · (log‘2))) |
131 | 126, 130 | eqtr4di 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)) |
133 | 132 | fveq2d 6770 |
. . . . . . . . . 10
⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = (√‘(2 ·
;64))) |
134 | 3 | nnrei 11992 |
. . . . . . . . . . . 12
⊢ ;64 ∈ ℝ |
135 | 3 | nngt0i 12022 |
. . . . . . . . . . . . 13
⊢ 0 <
;64 |
136 | 10, 134, 135 | ltleii 11108 |
. . . . . . . . . . . 12
⊢ 0 ≤
;64 |
137 | 53, 134, 54, 136 | sqrtmulii 15108 |
. . . . . . . . . . 11
⊢
(√‘(2 · ;64)) = ((√‘2) ·
(√‘;64)) |
138 | 16 | oveq2i 7278 |
. . . . . . . . . . 11
⊢
((√‘2) · (√‘;64)) = ((√‘2) ·
8) |
139 | 137, 138 | eqtri 2766 |
. . . . . . . . . 10
⊢
(√‘(2 · ;64)) = ((√‘2) ·
8) |
140 | 133, 139 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑛 = ;64 → (√‘(2 · 𝑛)) = ((√‘2) ·
8)) |
141 | 140 | oveq2d 7283 |
. . . . . . . 8
⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2
· 𝑛))) =
((log‘2) / ((√‘2) · 8))) |
142 | 48, 5 | mulcli 10992 |
. . . . . . . . . 10
⊢
((√‘2) · 8) ∈ ℂ |
143 | | rpmulcl 12763 |
. . . . . . . . . . . 12
⊢
(((√‘2) ∈ ℝ+ ∧ 8 ∈
ℝ+) → ((√‘2) · 8) ∈
ℝ+) |
144 | 65, 20, 143 | sylancr 587 |
. . . . . . . . . . 11
⊢ (8 ∈
ℕ → ((√‘2) · 8) ∈
ℝ+) |
145 | | rpne0 12756 |
. . . . . . . . . . 11
⊢
(((√‘2) · 8) ∈ ℝ+ →
((√‘2) · 8) ≠ 0) |
146 | 19, 144, 145 | mp2b 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))) |
148 | 37, 142, 146, 147 | mp3an 1460 |
. . . . . . . . 9
⊢
((log‘2) / ((√‘2) · 8)) = ((1 /
((√‘2) · 8)) · (log‘2)) |
149 | 48, 5 | mulcomi 10993 |
. . . . . . . . . . . 12
⊢
((√‘2) · 8) = (8 ·
(√‘2)) |
150 | 149 | oveq2i 7278 |
. . . . . . . . . . 11
⊢ (1 /
((√‘2) · 8)) = (1 / (8 ·
(√‘2))) |
151 | | recdiv2 11698 |
. . . . . . . . . . . 12
⊢ (((8
∈ ℂ ∧ 8 ≠ 0) ∧ ((√‘2) ∈ ℂ ∧
(√‘2) ≠ 0)) → ((1 / 8) / (√‘2)) = (1 / (8
· (√‘2)))) |
152 | 5, 38, 48, 71, 151 | mp4an 690 |
. . . . . . . . . . 11
⊢ ((1 / 8)
/ (√‘2)) = (1 / (8 · (√‘2))) |
153 | 150, 152 | eqtr4i 2769 |
. . . . . . . . . 10
⊢ (1 /
((√‘2) · 8)) = ((1 / 8) /
(√‘2)) |
154 | 153 | oveq1i 7277 |
. . . . . . . . 9
⊢ ((1 /
((√‘2) · 8)) · (log‘2)) = (((1 / 8) /
(√‘2)) · (log‘2)) |
155 | 148, 154 | eqtri 2766 |
. . . . . . . 8
⊢
((log‘2) / ((√‘2) · 8)) = (((1 / 8) /
(√‘2)) · (log‘2)) |
156 | 141, 155 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑛 = ;64 → ((log‘2) / (√‘(2
· 𝑛))) = (((1 / 8) /
(√‘2)) · (log‘2))) |
157 | 131, 156 | oveq12d 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)))) |
158 | 128, 129 | addcli 10991 |
. . . . . . 7
⊢ (((3 / 4)
/ (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈
ℂ |
159 | 5, 38 | reccli 11715 |
. . . . . . . 8
⊢ (1 / 8)
∈ ℂ |
160 | 159, 48, 71 | divcli 11727 |
. . . . . . 7
⊢ ((1 / 8)
/ (√‘2)) ∈ ℂ |
161 | 158, 160,
37 | adddiri 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))) |
162 | 157, 161 | eqtr4di 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 |
165 | 162, 163,
164 | fvmpt 6867 |
. . . 4
⊢ (;64 ∈ ℕ → (𝐹‘;64) = (((((3 / 4) / (√‘2)) + ((9 / 4)
· (5 / (2↑5)))) + ((1 / 8) / (√‘2))) ·
(log‘2))) |
166 | 3, 165 | ax-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 ∈
ℝ |
169 | 167, 168,
75 | redivcli 11752 |
. . . . . . 7
⊢ (3 / 4)
∈ ℝ |
170 | 169, 47, 71 | redivcli 11752 |
. . . . . 6
⊢ ((3 / 4)
/ (√‘2)) ∈ ℝ |
171 | | 9re 12082 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
172 | 171, 168,
75 | redivcli 11752 |
. . . . . . 7
⊢ (9 / 4)
∈ ℝ |
173 | | 5re 12070 |
. . . . . . . 8
⊢ 5 ∈
ℝ |
174 | 96 | nnrei 11992 |
. . . . . . . 8
⊢
(2↑5) ∈ ℝ |
175 | 173, 174,
113 | redivcli 11752 |
. . . . . . 7
⊢ (5 /
(2↑5)) ∈ ℝ |
176 | 172, 175 | remulcli 11001 |
. . . . . 6
⊢ ((9 / 4)
· (5 / (2↑5))) ∈ ℝ |
177 | 170, 176 | readdcli 11000 |
. . . . 5
⊢ (((3 / 4)
/ (√‘2)) + ((9 / 4) · (5 / (2↑5)))) ∈
ℝ |
178 | 11, 38 | rereccli 11750 |
. . . . . 6
⊢ (1 / 8)
∈ ℝ |
179 | 178, 47, 71 | redivcli 11752 |
. . . . 5
⊢ ((1 / 8)
/ (√‘2)) ∈ ℝ |
180 | 177, 179 | readdcli 11000 |
. . . 4
⊢ ((((3 /
4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) /
(√‘2))) ∈ ℝ |
181 | 180, 36 | remulcli 11001 |
. . 3
⊢ (((((3 /
4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) /
(√‘2))) · (log‘2)) ∈ ℝ |
182 | 166, 181 | eqeltri 2835 |
. 2
⊢ (𝐹‘;64) ∈ ℝ |
183 | 128, 129,
160 | add32i 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 ∈
ℂ |
186 | 184, 185,
5, 38 | divdiri 11742 |
. . . . . . . . . 10
⊢ ((6 + 1)
/ 8) = ((6 / 8) + (1 / 8)) |
187 | | df-7 12051 |
. . . . . . . . . . 11
⊢ 7 = (6 +
1) |
188 | 187 | oveq1i 7277 |
. . . . . . . . . 10
⊢ (7 / 8) =
((6 + 1) / 8) |
189 | | divcan5 11687 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · 3) / (2 · 4)) = (3 /
4)) |
190 | 32, 189 | mp3an1 1447 |
. . . . . . . . . . . . 13
⊢ (((4
∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((2 · 3) / (2 · 4)) = (3 / 4)) |
191 | 51, 75, 89, 98, 190 | mp4an 690 |
. . . . . . . . . . . 12
⊢ ((2
· 3) / (2 · 4)) = (3 / 4) |
192 | | 3t2e6 12149 |
. . . . . . . . . . . . . 14
⊢ (3
· 2) = 6 |
193 | 32, 89, 192 | mulcomli 10994 |
. . . . . . . . . . . . 13
⊢ (2
· 3) = 6 |
194 | 51, 89, 58 | mulcomli 10994 |
. . . . . . . . . . . . 13
⊢ (2
· 4) = 8 |
195 | 193, 194 | oveq12i 7279 |
. . . . . . . . . . . 12
⊢ ((2
· 3) / (2 · 4)) = (6 / 8) |
196 | 191, 195 | eqtr3i 2768 |
. . . . . . . . . . 11
⊢ (3 / 4) =
(6 / 8) |
197 | 196 | oveq1i 7277 |
. . . . . . . . . 10
⊢ ((3 / 4)
+ (1 / 8)) = ((6 / 8) + (1 / 8)) |
198 | 186, 188,
197 | 3eqtr4ri 2777 |
. . . . . . . . 9
⊢ ((3 / 4)
+ (1 / 8)) = (7 / 8) |
199 | 198 | oveq1i 7277 |
. . . . . . . 8
⊢ (((3 / 4)
+ (1 / 8)) / (√‘2)) = ((7 / 8) /
(√‘2)) |
200 | 127, 159,
48, 71 | divdiri 11742 |
. . . . . . . 8
⊢ (((3 / 4)
+ (1 / 8)) / (√‘2)) = (((3 / 4) / (√‘2)) + ((1 / 8) /
(√‘2))) |
201 | | 7cn 12077 |
. . . . . . . . 9
⊢ 7 ∈
ℂ |
202 | 201, 5, 48, 38, 71 | divdiv32i 11740 |
. . . . . . . 8
⊢ ((7 / 8)
/ (√‘2)) = ((7 / (√‘2)) / 8) |
203 | 199, 200,
202 | 3eqtr3i 2774 |
. . . . . . 7
⊢ (((3 / 4)
/ (√‘2)) + ((1 / 8) / (√‘2))) = ((7 /
(√‘2)) / 8) |
204 | 203 | oveq1i 7277 |
. . . . . 6
⊢ ((((3 /
4) / (√‘2)) + ((1 / 8) / (√‘2))) + ((9 / 4) · (5
/ (2↑5)))) = (((7 / (√‘2)) / 8) + ((9 / 4) · (5 /
(2↑5)))) |
205 | 183, 204 | eqtri 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 |
211 | 206, 90, 207, 208, 209, 210 | decltc 12476 |
. . . . . . . . . . 11
⊢ ;49 < ;50 |
212 | | 7t7e49 12561 |
. . . . . . . . . . 11
⊢ (7
· 7) = ;49 |
213 | 56 | oveq1i 7277 |
. . . . . . . . . . . 12
⊢
(((√‘2) · (√‘2)) · (5 · 5))
= (2 · (5 · 5)) |
214 | 48, 48, 112, 112 | mul4i 11182 |
. . . . . . . . . . . 12
⊢
(((√‘2) · (√‘2)) · (5 · 5))
= (((√‘2) · 5) · ((√‘2) ·
5)) |
215 | | 5t2e10 12547 |
. . . . . . . . . . . . . . 15
⊢ (5
· 2) = ;10 |
216 | 112, 89, 215 | mulcomli 10994 |
. . . . . . . . . . . . . 14
⊢ (2
· 5) = ;10 |
217 | 216 | oveq1i 7277 |
. . . . . . . . . . . . 13
⊢ ((2
· 5) · 5) = (;10
· 5) |
218 | 89, 112, 112 | mulassi 10996 |
. . . . . . . . . . . . 13
⊢ ((2
· 5) · 5) = (2 · (5 · 5)) |
219 | 90 | dec0u 12468 |
. . . . . . . . . . . . 13
⊢ (;10 · 5) = ;50 |
220 | 217, 218,
219 | 3eqtr3i 2774 |
. . . . . . . . . . . 12
⊢ (2
· (5 · 5)) = ;50 |
221 | 213, 214,
220 | 3eqtr3i 2774 |
. . . . . . . . . . 11
⊢
(((√‘2) · 5) · ((√‘2) · 5))
= ;50 |
222 | 211, 212,
221 | 3brtr4i 5103 |
. . . . . . . . . 10
⊢ (7
· 7) < (((√‘2) · 5) · ((√‘2)
· 5)) |
223 | | 7re 12076 |
. . . . . . . . . . . 12
⊢ 7 ∈
ℝ |
224 | | 7pos 12094 |
. . . . . . . . . . . 12
⊢ 0 <
7 |
225 | 10, 223, 224 | ltleii 11108 |
. . . . . . . . . . 11
⊢ 0 ≤
7 |
226 | | nnrp 12751 |
. . . . . . . . . . . . . 14
⊢ (5 ∈
ℕ → 5 ∈ ℝ+) |
227 | 105, 226 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ 5 ∈
ℝ+ |
228 | | rpmulcl 12763 |
. . . . . . . . . . . . 13
⊢
(((√‘2) ∈ ℝ+ ∧ 5 ∈
ℝ+) → ((√‘2) · 5) ∈
ℝ+) |
229 | 65, 227, 228 | mp2an 689 |
. . . . . . . . . . . 12
⊢
((√‘2) · 5) ∈
ℝ+ |
230 | | rpge0 12753 |
. . . . . . . . . . . 12
⊢
(((√‘2) · 5) ∈ ℝ+ → 0 ≤
((√‘2) · 5)) |
231 | 229, 230 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 0 ≤
((√‘2) · 5) |
232 | | rpre 12748 |
. . . . . . . . . . . . 13
⊢
(((√‘2) · 5) ∈ ℝ+ →
((√‘2) · 5) ∈ ℝ) |
233 | 229, 232 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((√‘2) · 5) ∈ ℝ |
234 | 223, 233 | lt2msqi 11897 |
. . . . . . . . . . 11
⊢ ((0 ≤
7 ∧ 0 ≤ ((√‘2) · 5)) → (7 <
((√‘2) · 5) ↔ (7 · 7) < (((√‘2)
· 5) · ((√‘2) · 5)))) |
235 | 225, 231,
234 | mp2an 689 |
. . . . . . . . . 10
⊢ (7 <
((√‘2) · 5) ↔ (7 · 7) < (((√‘2)
· 5) · ((√‘2) · 5))) |
236 | 222, 235 | mpbir 230 |
. . . . . . . . 9
⊢ 7 <
((√‘2) · 5) |
237 | | rpgt0 12752 |
. . . . . . . . . . 11
⊢
((√‘2) ∈ ℝ+ → 0 <
(√‘2)) |
238 | 24, 64, 237 | mp2b 10 |
. . . . . . . . . 10
⊢ 0 <
(√‘2) |
239 | | ltdivmul 11860 |
. . . . . . . . . . 11
⊢ ((7
∈ ℝ ∧ 5 ∈ ℝ ∧ ((√‘2) ∈ ℝ
∧ 0 < (√‘2))) → ((7 / (√‘2)) < 5 ↔
7 < ((√‘2) · 5))) |
240 | 223, 173,
239 | mp3an12 1450 |
. . . . . . . . . 10
⊢
(((√‘2) ∈ ℝ ∧ 0 < (√‘2))
→ ((7 / (√‘2)) < 5 ↔ 7 < ((√‘2)
· 5))) |
241 | 47, 238, 240 | mp2an 689 |
. . . . . . . . 9
⊢ ((7 /
(√‘2)) < 5 ↔ 7 < ((√‘2) ·
5)) |
242 | 236, 241 | mpbir 230 |
. . . . . . . 8
⊢ (7 /
(√‘2)) < 5 |
243 | 223, 47, 71 | redivcli 11752 |
. . . . . . . . 9
⊢ (7 /
(√‘2)) ∈ ℝ |
244 | 243, 173,
11, 12 | ltdiv1ii 11914 |
. . . . . . . 8
⊢ ((7 /
(√‘2)) < 5 ↔ ((7 / (√‘2)) / 8) < (5 /
8)) |
245 | 242, 244 | mpbi 229 |
. . . . . . 7
⊢ ((7 /
(√‘2)) / 8) < (5 / 8) |
246 | | divsubdir 11679 |
. . . . . . . . . . 11
⊢ ((8
∈ ℂ ∧ 3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0))
→ ((8 − 3) / 8) = ((8 / 8) − (3 / 8))) |
247 | 5, 32, 246 | mp3an12 1450 |
. . . . . . . . . 10
⊢ ((8
∈ ℂ ∧ 8 ≠ 0) → ((8 − 3) / 8) = ((8 / 8) − (3
/ 8))) |
248 | 5, 38, 247 | mp2an 689 |
. . . . . . . . 9
⊢ ((8
− 3) / 8) = ((8 / 8) − (3 / 8)) |
249 | | 5p3e8 12140 |
. . . . . . . . . . . 12
⊢ (5 + 3) =
8 |
250 | 249 | oveq1i 7277 |
. . . . . . . . . . 11
⊢ ((5 + 3)
− 3) = (8 − 3) |
251 | 112, 32 | pncan3oi 11247 |
. . . . . . . . . . 11
⊢ ((5 + 3)
− 3) = 5 |
252 | 250, 251 | eqtr3i 2768 |
. . . . . . . . . 10
⊢ (8
− 3) = 5 |
253 | 252 | oveq1i 7277 |
. . . . . . . . 9
⊢ ((8
− 3) / 8) = (5 / 8) |
254 | 5, 38 | dividi 11718 |
. . . . . . . . . 10
⊢ (8 / 8) =
1 |
255 | 254 | oveq1i 7277 |
. . . . . . . . 9
⊢ ((8 / 8)
− (3 / 8)) = (1 − (3 / 8)) |
256 | 248, 253,
255 | 3eqtr3ri 2775 |
. . . . . . . 8
⊢ (1
− (3 / 8)) = (5 / 8) |
257 | | 5lt8 12177 |
. . . . . . . . . . . . 13
⊢ 5 <
8 |
258 | 11, 173 | remulcli 11001 |
. . . . . . . . . . . . . 14
⊢ (8
· 5) ∈ ℝ |
259 | 173, 11, 258 | ltadd2i 11116 |
. . . . . . . . . . . . 13
⊢ (5 < 8
↔ ((8 · 5) + 5) < ((8 · 5) + 8)) |
260 | 257, 259 | mpbi 229 |
. . . . . . . . . . . 12
⊢ ((8
· 5) + 5) < ((8 · 5) + 8) |
261 | | df-9 12053 |
. . . . . . . . . . . . . 14
⊢ 9 = (8 +
1) |
262 | 261 | oveq1i 7277 |
. . . . . . . . . . . . 13
⊢ (9
· 5) = ((8 + 1) · 5) |
263 | 5, 185, 112 | adddiri 10998 |
. . . . . . . . . . . . 13
⊢ ((8 + 1)
· 5) = ((8 · 5) + (1 · 5)) |
264 | 112 | mulid2i 10990 |
. . . . . . . . . . . . . 14
⊢ (1
· 5) = 5 |
265 | 264 | oveq2i 7278 |
. . . . . . . . . . . . 13
⊢ ((8
· 5) + (1 · 5)) = ((8 · 5) + 5) |
266 | 262, 263,
265 | 3eqtri 2770 |
. . . . . . . . . . . 12
⊢ (9
· 5) = ((8 · 5) + 5) |
267 | 86 | oveq2i 7278 |
. . . . . . . . . . . . 13
⊢ (8
· 6) = (8 · (5 + 1)) |
268 | 5, 112, 185 | adddii 10997 |
. . . . . . . . . . . . 13
⊢ (8
· (5 + 1)) = ((8 · 5) + (8 · 1)) |
269 | 5 | mulid1i 10989 |
. . . . . . . . . . . . . 14
⊢ (8
· 1) = 8 |
270 | 269 | oveq2i 7278 |
. . . . . . . . . . . . 13
⊢ ((8
· 5) + (8 · 1)) = ((8 · 5) + 8) |
271 | 267, 268,
270 | 3eqtri 2770 |
. . . . . . . . . . . 12
⊢ (8
· 6) = ((8 · 5) + 8) |
272 | 260, 266,
271 | 3brtr4i 5103 |
. . . . . . . . . . 11
⊢ (9
· 5) < (8 · 6) |
273 | 171, 173 | remulcli 11001 |
. . . . . . . . . . . 12
⊢ (9
· 5) ∈ ℝ |
274 | | 6re 12073 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℝ |
275 | 11, 274 | remulcli 11001 |
. . . . . . . . . . . 12
⊢ (8
· 6) ∈ ℝ |
276 | 168, 174 | remulcli 11001 |
. . . . . . . . . . . 12
⊢ (4
· (2↑5)) ∈ ℝ |
277 | 2, 96 | nnmulcli 12008 |
. . . . . . . . . . . . 13
⊢ (4
· (2↑5)) ∈ ℕ |
278 | 277 | nngt0i 12022 |
. . . . . . . . . . . 12
⊢ 0 < (4
· (2↑5)) |
279 | 273, 275,
276, 278 | ltdiv1ii 11914 |
. . . . . . . . . . 11
⊢ ((9
· 5) < (8 · 6) ↔ ((9 · 5) / (4 ·
(2↑5))) < ((8 · 6) / (4 · (2↑5)))) |
280 | 272, 279 | mpbi 229 |
. . . . . . . . . 10
⊢ ((9
· 5) / (4 · (2↑5))) < ((8 · 6) / (4 ·
(2↑5))) |
281 | 121, 51, 112, 97, 75, 113 | divmuldivi 11745 |
. . . . . . . . . 10
⊢ ((9 / 4)
· (5 / (2↑5))) = ((9 · 5) / (4 ·
(2↑5))) |
282 | | nnexpcl 13805 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈
ℕ) |
283 | 33, 206, 282 | mp2an 689 |
. . . . . . . . . . . . 13
⊢
(2↑4) ∈ ℕ |
284 | 283 | nncni 11993 |
. . . . . . . . . . . 12
⊢
(2↑4) ∈ ℂ |
285 | 283 | nnne0i 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)) |
287 | 32, 286 | mp3an1 1447 |
. . . . . . . . . . . 12
⊢ (((8
∈ ℂ ∧ 8 ≠ 0) ∧ ((2↑4) ∈ ℂ ∧
(2↑4) ≠ 0)) → (((2↑4) · 3) / ((2↑4) · 8))
= (3 / 8)) |
288 | 5, 38, 284, 285, 287 | mp4an 690 |
. . . . . . . . . . 11
⊢
(((2↑4) · 3) / ((2↑4) · 8)) = (3 /
8) |
289 | | df-4 12048 |
. . . . . . . . . . . . . . . 16
⊢ 4 = (3 +
1) |
290 | 289 | oveq2i 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)) |
293 | 89, 291, 292 | mp2an 689 |
. . . . . . . . . . . . . . 15
⊢
(2↑(3 + 1)) = ((2↑3) · 2) |
294 | 22 | oveq1i 7277 |
. . . . . . . . . . . . . . 15
⊢
((2↑3) · 2) = (8 · 2) |
295 | 290, 293,
294 | 3eqtri 2770 |
. . . . . . . . . . . . . 14
⊢
(2↑4) = (8 · 2) |
296 | 295 | oveq1i 7277 |
. . . . . . . . . . . . 13
⊢
((2↑4) · 3) = ((8 · 2) · 3) |
297 | 5, 89, 32 | mulassi 10996 |
. . . . . . . . . . . . 13
⊢ ((8
· 2) · 3) = (8 · (2 · 3)) |
298 | 193 | oveq2i 7278 |
. . . . . . . . . . . . 13
⊢ (8
· (2 · 3)) = (8 · 6) |
299 | 296, 297,
298 | 3eqtri 2770 |
. . . . . . . . . . . 12
⊢
((2↑4) · 3) = (8 · 6) |
300 | | 4p3e7 12137 |
. . . . . . . . . . . . . . . 16
⊢ (4 + 3) =
7 |
301 | | 5p2e7 12139 |
. . . . . . . . . . . . . . . 16
⊢ (5 + 2) =
7 |
302 | 112, 89 | addcomi 11176 |
. . . . . . . . . . . . . . . 16
⊢ (5 + 2) =
(2 + 5) |
303 | 300, 301,
302 | 3eqtr2i 2772 |
. . . . . . . . . . . . . . 15
⊢ (4 + 3) =
(2 + 5) |
304 | 303 | oveq2i 7278 |
. . . . . . . . . . . . . 14
⊢
(2↑(4 + 3)) = (2↑(2 + 5)) |
305 | | expadd 13835 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 4 ∈ ℕ0 ∧ 3 ∈
ℕ0) → (2↑(4 + 3)) = ((2↑4) ·
(2↑3))) |
306 | 89, 206, 291, 305 | mp3an 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))) |
309 | 89, 307, 90, 308 | mp3an 1460 |
. . . . . . . . . . . . . 14
⊢
(2↑(2 + 5)) = ((2↑2) · (2↑5)) |
310 | 304, 306,
309 | 3eqtr3i 2774 |
. . . . . . . . . . . . 13
⊢
((2↑4) · (2↑3)) = ((2↑2) ·
(2↑5)) |
311 | 22 | oveq2i 7278 |
. . . . . . . . . . . . 13
⊢
((2↑4) · (2↑3)) = ((2↑4) ·
8) |
312 | | sq2 13924 |
. . . . . . . . . . . . . 14
⊢
(2↑2) = 4 |
313 | 312 | oveq1i 7277 |
. . . . . . . . . . . . 13
⊢
((2↑2) · (2↑5)) = (4 ·
(2↑5)) |
314 | 310, 311,
313 | 3eqtr3i 2774 |
. . . . . . . . . . . 12
⊢
((2↑4) · 8) = (4 · (2↑5)) |
315 | 299, 314 | oveq12i 7279 |
. . . . . . . . . . 11
⊢
(((2↑4) · 3) / ((2↑4) · 8)) = ((8 · 6) /
(4 · (2↑5))) |
316 | 288, 315 | eqtr3i 2768 |
. . . . . . . . . 10
⊢ (3 / 8) =
((8 · 6) / (4 · (2↑5))) |
317 | 280, 281,
316 | 3brtr4i 5103 |
. . . . . . . . 9
⊢ ((9 / 4)
· (5 / (2↑5))) < (3 / 8) |
318 | 167, 11, 38 | redivcli 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)))))) |
321 | 176, 318,
319, 320 | mp3an 1460 |
. . . . . . . . 9
⊢ (((9 / 4)
· (5 / (2↑5))) < (3 / 8) ↔ (1 − (3 / 8)) < (1
− ((9 / 4) · (5 / (2↑5))))) |
322 | 317, 321 | mpbi 229 |
. . . . . . . 8
⊢ (1
− (3 / 8)) < (1 − ((9 / 4) · (5 /
(2↑5)))) |
323 | 256, 322 | eqbrtrri 5096 |
. . . . . . 7
⊢ (5 / 8)
< (1 − ((9 / 4) · (5 / (2↑5)))) |
324 | 243, 11, 38 | redivcli 11752 |
. . . . . . . 8
⊢ ((7 /
(√‘2)) / 8) ∈ ℝ |
325 | 173, 11, 38 | redivcli 11752 |
. . . . . . . 8
⊢ (5 / 8)
∈ ℝ |
326 | 319, 176 | resubcli 11293 |
. . . . . . . 8
⊢ (1
− ((9 / 4) · (5 / (2↑5)))) ∈ ℝ |
327 | 324, 325,
326 | lttri 11111 |
. . . . . . 7
⊢ ((((7 /
(√‘2)) / 8) < (5 / 8) ∧ (5 / 8) < (1 − ((9 / 4)
· (5 / (2↑5))))) → ((7 / (√‘2)) / 8) < (1
− ((9 / 4) · (5 / (2↑5))))) |
328 | 245, 323,
327 | mp2an 689 |
. . . . . 6
⊢ ((7 /
(√‘2)) / 8) < (1 − ((9 / 4) · (5 /
(2↑5)))) |
329 | 324, 176,
319 | ltaddsubi 11546 |
. . . . . 6
⊢ ((((7 /
(√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) < 1 ↔
((7 / (√‘2)) / 8) < (1 − ((9 / 4) · (5 /
(2↑5))))) |
330 | 328, 329 | mpbir 230 |
. . . . 5
⊢ (((7 /
(√‘2)) / 8) + ((9 / 4) · (5 / (2↑5)))) <
1 |
331 | 205, 330 | eqbrtri 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) ∈
ℝ+) |
334 | 53, 332, 333 | mp2an 689 |
. . . . . 6
⊢
(log‘2) ∈ ℝ+ |
335 | | rpgt0 12752 |
. . . . . 6
⊢
((log‘2) ∈ ℝ+ → 0 <
(log‘2)) |
336 | 334, 335 | ax-mp 5 |
. . . . 5
⊢ 0 <
(log‘2) |
337 | 180, 319,
36, 336 | ltmul1ii 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))) |
338 | 331, 337 | mpbi 229 |
. . 3
⊢ (((((3 /
4) / (√‘2)) + ((9 / 4) · (5 / (2↑5)))) + ((1 / 8) /
(√‘2))) · (log‘2)) < (1 ·
(log‘2)) |
339 | 37 | mulid2i 10990 |
. . . 4
⊢ (1
· (log‘2)) = (log‘2) |
340 | 339 | eqcomi 2747 |
. . 3
⊢
(log‘2) = (1 · (log‘2)) |
341 | 338, 166,
340 | 3brtr4i 5103 |
. 2
⊢ (𝐹‘;64) < (log‘2) |
342 | 182, 341 | pm3.2i 471 |
1
⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)) |