Proof of Theorem ef01bndlem
| Step | Hyp | Ref
| Expression |
| 1 | | ax-icn 11214 |
. . . . 5
⊢ i ∈
ℂ |
| 2 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 3 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 4 | | elioc2 13450 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
| 6 | 5 | simp1bi 1146 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
| 7 | 6 | recnd 11289 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
| 8 | | mulcl 11239 |
. . . . 5
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 9 | 1, 7, 8 | sylancr 587 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
| 10 | | 4nn0 12545 |
. . . 4
⊢ 4 ∈
ℕ0 |
| 11 | | ef01bnd.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
| 12 | 11 | eftlcl 16143 |
. . . 4
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘) ∈ ℂ) |
| 13 | 9, 10, 12 | sylancl 586 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘) ∈ ℂ) |
| 14 | 13 | abscld 15475 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ∈ ℝ) |
| 15 | | reexpcl 14119 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
| 16 | 6, 10, 15 | sylancl 586 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
| 17 | | 4re 12350 |
. . . . 5
⊢ 4 ∈
ℝ |
| 18 | 17, 3 | readdcli 11276 |
. . . 4
⊢ (4 + 1)
∈ ℝ |
| 19 | | faccl 14322 |
. . . . . 6
⊢ (4 ∈
ℕ0 → (!‘4) ∈ ℕ) |
| 20 | 10, 19 | ax-mp 5 |
. . . . 5
⊢
(!‘4) ∈ ℕ |
| 21 | | 4nn 12349 |
. . . . 5
⊢ 4 ∈
ℕ |
| 22 | 20, 21 | nnmulcli 12291 |
. . . 4
⊢
((!‘4) · 4) ∈ ℕ |
| 23 | | nndivre 12307 |
. . . 4
⊢ (((4 + 1)
∈ ℝ ∧ ((!‘4) · 4) ∈ ℕ) → ((4 + 1) /
((!‘4) · 4)) ∈ ℝ) |
| 24 | 18, 22, 23 | mp2an 692 |
. . 3
⊢ ((4 + 1)
/ ((!‘4) · 4)) ∈ ℝ |
| 25 | | remulcl 11240 |
. . 3
⊢ (((𝐴↑4) ∈ ℝ ∧
((4 + 1) / ((!‘4) · 4)) ∈ ℝ) → ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) ∈ ℝ) |
| 26 | 16, 24, 25 | sylancl 586 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) ∈ ℝ) |
| 27 | | 6nn 12355 |
. . 3
⊢ 6 ∈
ℕ |
| 28 | | nndivre 12307 |
. . 3
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
| 29 | 16, 27, 28 | sylancl 586 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
| 30 | | eqid 2737 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘(i · 𝐴))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘(i · 𝐴))↑𝑛) / (!‘𝑛))) |
| 31 | | eqid 2737 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘(i · 𝐴))↑4) / (!‘4)) · ((1 / (4
+ 1))↑𝑛))) = (𝑛 ∈ ℕ0
↦ ((((abs‘(i · 𝐴))↑4) / (!‘4)) · ((1 / (4
+ 1))↑𝑛))) |
| 32 | 21 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
ℕ) |
| 33 | | absmul 15333 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (abs‘(i · 𝐴)) = ((abs‘i) ·
(abs‘𝐴))) |
| 34 | 1, 7, 33 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
= ((abs‘i) · (abs‘𝐴))) |
| 35 | | absi 15325 |
. . . . . . . 8
⊢
(abs‘i) = 1 |
| 36 | 35 | oveq1i 7441 |
. . . . . . 7
⊢
((abs‘i) · (abs‘𝐴)) = (1 · (abs‘𝐴)) |
| 37 | 5 | simp2bi 1147 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
| 38 | 6, 37 | elrpd 13074 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ+) |
| 39 | | rpre 13043 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 40 | | rpge0 13048 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 0 ≤ 𝐴) |
| 41 | 39, 40 | absidd 15461 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (abs‘𝐴) =
𝐴) |
| 42 | 38, 41 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
(abs‘𝐴) = 𝐴) |
| 43 | 42 | oveq2d 7447 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (1
· (abs‘𝐴)) =
(1 · 𝐴)) |
| 44 | 36, 43 | eqtrid 2789 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
((abs‘i) · (abs‘𝐴)) = (1 · 𝐴)) |
| 45 | 7 | mullidd 11279 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
· 𝐴) = 𝐴) |
| 46 | 34, 44, 45 | 3eqtrd 2781 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
= 𝐴) |
| 47 | 5 | simp3bi 1148 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
| 48 | 46, 47 | eqbrtrd 5165 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
≤ 1) |
| 49 | 11, 30, 31, 32, 9, 48 | eftlub 16145 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ≤ (((abs‘(i · 𝐴))↑4) · ((4 + 1) /
((!‘4) · 4)))) |
| 50 | 46 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((abs‘(i · 𝐴))↑4) = (𝐴↑4)) |
| 51 | 50 | oveq1d 7446 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(((abs‘(i · 𝐴))↑4) · ((4 + 1) / ((!‘4)
· 4))) = ((𝐴↑4)
· ((4 + 1) / ((!‘4) · 4)))) |
| 52 | 49, 51 | breqtrd 5169 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ≤ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4)))) |
| 53 | | 3pos 12371 |
. . . . . . . . 9
⊢ 0 <
3 |
| 54 | | 0re 11263 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
| 55 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 56 | | 5re 12353 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
| 57 | 54, 55, 56 | ltadd1i 11817 |
. . . . . . . . 9
⊢ (0 < 3
↔ (0 + 5) < (3 + 5)) |
| 58 | 53, 57 | mpbi 230 |
. . . . . . . 8
⊢ (0 + 5)
< (3 + 5) |
| 59 | | 5cn 12354 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
| 60 | 59 | addlidi 11449 |
. . . . . . . 8
⊢ (0 + 5) =
5 |
| 61 | | cu2 14239 |
. . . . . . . . 9
⊢
(2↑3) = 8 |
| 62 | | 5p3e8 12423 |
. . . . . . . . 9
⊢ (5 + 3) =
8 |
| 63 | | 3cn 12347 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
| 64 | 59, 63 | addcomi 11452 |
. . . . . . . . 9
⊢ (5 + 3) =
(3 + 5) |
| 65 | 61, 62, 64 | 3eqtr2ri 2772 |
. . . . . . . 8
⊢ (3 + 5) =
(2↑3) |
| 66 | 58, 60, 65 | 3brtr3i 5172 |
. . . . . . 7
⊢ 5 <
(2↑3) |
| 67 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 68 | | 1le2 12475 |
. . . . . . . 8
⊢ 1 ≤
2 |
| 69 | | 4z 12651 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
| 70 | | 3lt4 12440 |
. . . . . . . . . 10
⊢ 3 <
4 |
| 71 | 55, 17, 70 | ltleii 11384 |
. . . . . . . . 9
⊢ 3 ≤
4 |
| 72 | | 3z 12650 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
| 73 | 72 | eluz1i 12886 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
| 74 | 69, 71, 73 | mpbir2an 711 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
| 75 | | leexp2a 14212 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ 4 ∈ (ℤ≥‘3))
→ (2↑3) ≤ (2↑4)) |
| 76 | 67, 68, 74, 75 | mp3an 1463 |
. . . . . . 7
⊢
(2↑3) ≤ (2↑4) |
| 77 | | 8re 12362 |
. . . . . . . . 9
⊢ 8 ∈
ℝ |
| 78 | 61, 77 | eqeltri 2837 |
. . . . . . . 8
⊢
(2↑3) ∈ ℝ |
| 79 | | 2nn 12339 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
| 80 | | nnexpcl 14115 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈
ℕ) |
| 81 | 79, 10, 80 | mp2an 692 |
. . . . . . . . 9
⊢
(2↑4) ∈ ℕ |
| 82 | 81 | nnrei 12275 |
. . . . . . . 8
⊢
(2↑4) ∈ ℝ |
| 83 | 56, 78, 82 | ltletri 11389 |
. . . . . . 7
⊢ ((5 <
(2↑3) ∧ (2↑3) ≤ (2↑4)) → 5 <
(2↑4)) |
| 84 | 66, 76, 83 | mp2an 692 |
. . . . . 6
⊢ 5 <
(2↑4) |
| 85 | | 6re 12356 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
| 86 | 85, 82 | remulcli 11277 |
. . . . . . 7
⊢ (6
· (2↑4)) ∈ ℝ |
| 87 | | 6pos 12376 |
. . . . . . . 8
⊢ 0 <
6 |
| 88 | 81 | nngt0i 12305 |
. . . . . . . 8
⊢ 0 <
(2↑4) |
| 89 | 85, 82, 87, 88 | mulgt0ii 11394 |
. . . . . . 7
⊢ 0 < (6
· (2↑4)) |
| 90 | 56, 82, 86, 89 | ltdiv1ii 12197 |
. . . . . 6
⊢ (5 <
(2↑4) ↔ (5 / (6 · (2↑4))) < ((2↑4) / (6 ·
(2↑4)))) |
| 91 | 84, 90 | mpbi 230 |
. . . . 5
⊢ (5 / (6
· (2↑4))) < ((2↑4) / (6 ·
(2↑4))) |
| 92 | | df-5 12332 |
. . . . . 6
⊢ 5 = (4 +
1) |
| 93 | | df-4 12331 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
| 94 | 93 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(!‘4) = (!‘(3 + 1)) |
| 95 | | 3nn0 12544 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
| 96 | | facp1 14317 |
. . . . . . . . . . 11
⊢ (3 ∈
ℕ0 → (!‘(3 + 1)) = ((!‘3) · (3 +
1))) |
| 97 | 95, 96 | ax-mp 5 |
. . . . . . . . . 10
⊢
(!‘(3 + 1)) = ((!‘3) · (3 + 1)) |
| 98 | | sq2 14236 |
. . . . . . . . . . . 12
⊢
(2↑2) = 4 |
| 99 | 98, 93 | eqtr2i 2766 |
. . . . . . . . . . 11
⊢ (3 + 1) =
(2↑2) |
| 100 | 99 | oveq2i 7442 |
. . . . . . . . . 10
⊢
((!‘3) · (3 + 1)) = ((!‘3) ·
(2↑2)) |
| 101 | 94, 97, 100 | 3eqtri 2769 |
. . . . . . . . 9
⊢
(!‘4) = ((!‘3) · (2↑2)) |
| 102 | 101 | oveq1i 7441 |
. . . . . . . 8
⊢
((!‘4) · (2↑2)) = (((!‘3) · (2↑2))
· (2↑2)) |
| 103 | 98 | oveq2i 7442 |
. . . . . . . 8
⊢
((!‘4) · (2↑2)) = ((!‘4) ·
4) |
| 104 | | fac3 14319 |
. . . . . . . . . 10
⊢
(!‘3) = 6 |
| 105 | | 6cn 12357 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
| 106 | 104, 105 | eqeltri 2837 |
. . . . . . . . 9
⊢
(!‘3) ∈ ℂ |
| 107 | 17 | recni 11275 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
| 108 | 98, 107 | eqeltri 2837 |
. . . . . . . . 9
⊢
(2↑2) ∈ ℂ |
| 109 | 106, 108,
108 | mulassi 11272 |
. . . . . . . 8
⊢
(((!‘3) · (2↑2)) · (2↑2)) = ((!‘3)
· ((2↑2) · (2↑2))) |
| 110 | 102, 103,
109 | 3eqtr3i 2773 |
. . . . . . 7
⊢
((!‘4) · 4) = ((!‘3) · ((2↑2) ·
(2↑2))) |
| 111 | | 2p2e4 12401 |
. . . . . . . . . 10
⊢ (2 + 2) =
4 |
| 112 | 111 | oveq2i 7442 |
. . . . . . . . 9
⊢
(2↑(2 + 2)) = (2↑4) |
| 113 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 114 | | 2nn0 12543 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
| 115 | | expadd 14145 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈
ℕ0) → (2↑(2 + 2)) = ((2↑2) ·
(2↑2))) |
| 116 | 113, 114,
114, 115 | mp3an 1463 |
. . . . . . . . 9
⊢
(2↑(2 + 2)) = ((2↑2) · (2↑2)) |
| 117 | 112, 116 | eqtr3i 2767 |
. . . . . . . 8
⊢
(2↑4) = ((2↑2) · (2↑2)) |
| 118 | 117 | oveq2i 7442 |
. . . . . . 7
⊢
((!‘3) · (2↑4)) = ((!‘3) · ((2↑2)
· (2↑2))) |
| 119 | 104 | oveq1i 7441 |
. . . . . . 7
⊢
((!‘3) · (2↑4)) = (6 ·
(2↑4)) |
| 120 | 110, 118,
119 | 3eqtr2ri 2772 |
. . . . . 6
⊢ (6
· (2↑4)) = ((!‘4) · 4) |
| 121 | 92, 120 | oveq12i 7443 |
. . . . 5
⊢ (5 / (6
· (2↑4))) = ((4 + 1) / ((!‘4) · 4)) |
| 122 | 81 | nncni 12276 |
. . . . . . . 8
⊢
(2↑4) ∈ ℂ |
| 123 | 122 | mullidi 11266 |
. . . . . . 7
⊢ (1
· (2↑4)) = (2↑4) |
| 124 | 123 | oveq1i 7441 |
. . . . . 6
⊢ ((1
· (2↑4)) / (6 · (2↑4))) = ((2↑4) / (6 ·
(2↑4))) |
| 125 | 81 | nnne0i 12306 |
. . . . . . . . 9
⊢
(2↑4) ≠ 0 |
| 126 | 122, 125 | dividi 12000 |
. . . . . . . 8
⊢
((2↑4) / (2↑4)) = 1 |
| 127 | 126 | oveq2i 7442 |
. . . . . . 7
⊢ ((1 / 6)
· ((2↑4) / (2↑4))) = ((1 / 6) · 1) |
| 128 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 129 | 85, 87 | gt0ne0ii 11799 |
. . . . . . . 8
⊢ 6 ≠
0 |
| 130 | 128, 105,
122, 122, 129, 125 | divmuldivi 12027 |
. . . . . . 7
⊢ ((1 / 6)
· ((2↑4) / (2↑4))) = ((1 · (2↑4)) / (6 ·
(2↑4))) |
| 131 | 85, 129 | rereccli 12032 |
. . . . . . . . 9
⊢ (1 / 6)
∈ ℝ |
| 132 | 131 | recni 11275 |
. . . . . . . 8
⊢ (1 / 6)
∈ ℂ |
| 133 | 132 | mulridi 11265 |
. . . . . . 7
⊢ ((1 / 6)
· 1) = (1 / 6) |
| 134 | 127, 130,
133 | 3eqtr3i 2773 |
. . . . . 6
⊢ ((1
· (2↑4)) / (6 · (2↑4))) = (1 / 6) |
| 135 | 124, 134 | eqtr3i 2767 |
. . . . 5
⊢
((2↑4) / (6 · (2↑4))) = (1 / 6) |
| 136 | 91, 121, 135 | 3brtr3i 5172 |
. . . 4
⊢ ((4 + 1)
/ ((!‘4) · 4)) < (1 / 6) |
| 137 | | rpexpcl 14121 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 4 ∈ ℤ) → (𝐴↑4) ∈
ℝ+) |
| 138 | 38, 69, 137 | sylancl 586 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ+) |
| 139 | | elrp 13036 |
. . . . . 6
⊢ ((𝐴↑4) ∈
ℝ+ ↔ ((𝐴↑4) ∈ ℝ ∧ 0 < (𝐴↑4))) |
| 140 | | ltmul2 12118 |
. . . . . . 7
⊢ ((((4 +
1) / ((!‘4) · 4)) ∈ ℝ ∧ (1 / 6) ∈ ℝ
∧ ((𝐴↑4) ∈
ℝ ∧ 0 < (𝐴↑4))) → (((4 + 1) / ((!‘4)
· 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
| 141 | 24, 131, 140 | mp3an12 1453 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 0
< (𝐴↑4)) →
(((4 + 1) / ((!‘4) · 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
| 142 | 139, 141 | sylbi 217 |
. . . . 5
⊢ ((𝐴↑4) ∈
ℝ+ → (((4 + 1) / ((!‘4) · 4)) < (1 / 6)
↔ ((𝐴↑4) ·
((4 + 1) / ((!‘4) · 4))) < ((𝐴↑4) · (1 /
6)))) |
| 143 | 138, 142 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((4 + 1)
/ ((!‘4) · 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
| 144 | 136, 143 | mpbii 233 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) < ((𝐴↑4) · (1 / 6))) |
| 145 | 16 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℂ) |
| 146 | | divrec 11938 |
. . . . 5
⊢ (((𝐴↑4) ∈ ℂ ∧ 6
∈ ℂ ∧ 6 ≠ 0) → ((𝐴↑4) / 6) = ((𝐴↑4) · (1 / 6))) |
| 147 | 105, 129,
146 | mp3an23 1455 |
. . . 4
⊢ ((𝐴↑4) ∈ ℂ →
((𝐴↑4) / 6) = ((𝐴↑4) · (1 /
6))) |
| 148 | 145, 147 | syl 17 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) = ((𝐴↑4) · (1 /
6))) |
| 149 | 144, 148 | breqtrrd 5171 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) < ((𝐴↑4) / 6)) |
| 150 | 14, 26, 29, 52, 149 | lelttrd 11419 |
1
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) |