Proof of Theorem ef01bndlem
Step | Hyp | Ref
| Expression |
1 | | ax-icn 9874 |
. . . . 5
⊢ i ∈
ℂ |
2 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
3 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
4 | | elioc2 12107 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
5 | 2, 3, 4 | mp2an 704 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
6 | 5 | simp1bi 1069 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
7 | 6 | recnd 9947 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
8 | | mulcl 9899 |
. . . . 5
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
9 | 1, 7, 8 | sylancr 694 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
10 | | 4nn0 11188 |
. . . 4
⊢ 4 ∈
ℕ0 |
11 | | ef01bnd.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
12 | 11 | eftlcl 14676 |
. . . 4
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘) ∈ ℂ) |
13 | 9, 10, 12 | sylancl 693 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘) ∈ ℂ) |
14 | 13 | abscld 14023 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ∈ ℝ) |
15 | | reexpcl 12739 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
16 | 6, 10, 15 | sylancl 693 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
17 | | 4re 10974 |
. . . . 5
⊢ 4 ∈
ℝ |
18 | 17, 3 | readdcli 9932 |
. . . 4
⊢ (4 + 1)
∈ ℝ |
19 | | faccl 12932 |
. . . . . 6
⊢ (4 ∈
ℕ0 → (!‘4) ∈ ℕ) |
20 | 10, 19 | ax-mp 5 |
. . . . 5
⊢
(!‘4) ∈ ℕ |
21 | | 4nn 11064 |
. . . . 5
⊢ 4 ∈
ℕ |
22 | 20, 21 | nnmulcli 10921 |
. . . 4
⊢
((!‘4) · 4) ∈ ℕ |
23 | | nndivre 10933 |
. . . 4
⊢ (((4 + 1)
∈ ℝ ∧ ((!‘4) · 4) ∈ ℕ) → ((4 + 1) /
((!‘4) · 4)) ∈ ℝ) |
24 | 18, 22, 23 | mp2an 704 |
. . 3
⊢ ((4 + 1)
/ ((!‘4) · 4)) ∈ ℝ |
25 | | remulcl 9900 |
. . 3
⊢ (((𝐴↑4) ∈ ℝ ∧
((4 + 1) / ((!‘4) · 4)) ∈ ℝ) → ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) ∈ ℝ) |
26 | 16, 24, 25 | sylancl 693 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) ∈ ℝ) |
27 | | 6nn 11066 |
. . 3
⊢ 6 ∈
ℕ |
28 | | nndivre 10933 |
. . 3
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
29 | 16, 27, 28 | sylancl 693 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
30 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘(i · 𝐴))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘(i · 𝐴))↑𝑛) / (!‘𝑛))) |
31 | | eqid 2610 |
. . . 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 13882 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (abs‘(i · 𝐴)) = ((abs‘i) ·
(abs‘𝐴))) |
34 | 1, 7, 33 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
= ((abs‘i) · (abs‘𝐴))) |
35 | | absi 13874 |
. . . . . . . 8
⊢
(abs‘i) = 1 |
36 | 35 | oveq1i 6559 |
. . . . . . 7
⊢
((abs‘i) · (abs‘𝐴)) = (1 · (abs‘𝐴)) |
37 | 5 | simp2bi 1070 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
38 | 6, 37 | elrpd 11745 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ+) |
39 | | rpre 11715 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
40 | | rpge0 11721 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 0 ≤ 𝐴) |
41 | 39, 40 | absidd 14009 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (abs‘𝐴) =
𝐴) |
42 | 38, 41 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
(abs‘𝐴) = 𝐴) |
43 | 42 | oveq2d 6565 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (1
· (abs‘𝐴)) =
(1 · 𝐴)) |
44 | 36, 43 | syl5eq 2656 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
((abs‘i) · (abs‘𝐴)) = (1 · 𝐴)) |
45 | 7 | mulid2d 9937 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
· 𝐴) = 𝐴) |
46 | 34, 44, 45 | 3eqtrd 2648 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
= 𝐴) |
47 | 5 | simp3bi 1071 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
48 | 46, 47 | eqbrtrd 4605 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
≤ 1) |
49 | 11, 30, 31, 32, 9, 48 | eftlub 14678 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ≤ (((abs‘(i · 𝐴))↑4) · ((4 + 1) /
((!‘4) · 4)))) |
50 | 46 | oveq1d 6564 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((abs‘(i · 𝐴))↑4) = (𝐴↑4)) |
51 | 50 | oveq1d 6564 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(((abs‘(i · 𝐴))↑4) · ((4 + 1) / ((!‘4)
· 4))) = ((𝐴↑4)
· ((4 + 1) / ((!‘4) · 4)))) |
52 | 49, 51 | breqtrd 4609 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ≤ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4)))) |
53 | | 3pos 10991 |
. . . . . . . . 9
⊢ 0 <
3 |
54 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
55 | | 3re 10971 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
56 | | 5re 10976 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
57 | 54, 55, 56 | ltadd1i 10461 |
. . . . . . . . 9
⊢ (0 < 3
↔ (0 + 5) < (3 + 5)) |
58 | 53, 57 | mpbi 219 |
. . . . . . . 8
⊢ (0 + 5)
< (3 + 5) |
59 | | 5cn 10977 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
60 | 59 | addid2i 10103 |
. . . . . . . 8
⊢ (0 + 5) =
5 |
61 | | cu2 12825 |
. . . . . . . . 9
⊢
(2↑3) = 8 |
62 | | 5p3e8 11043 |
. . . . . . . . 9
⊢ (5 + 3) =
8 |
63 | | 3nn 11063 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
64 | 63 | nncni 10907 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
65 | 59, 64 | addcomi 10106 |
. . . . . . . . 9
⊢ (5 + 3) =
(3 + 5) |
66 | 61, 62, 65 | 3eqtr2ri 2639 |
. . . . . . . 8
⊢ (3 + 5) =
(2↑3) |
67 | 58, 60, 66 | 3brtr3i 4612 |
. . . . . . 7
⊢ 5 <
(2↑3) |
68 | | 2re 10967 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
69 | | 1le2 11118 |
. . . . . . . 8
⊢ 1 ≤
2 |
70 | | 4z 11288 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
71 | | 3lt4 11074 |
. . . . . . . . . 10
⊢ 3 <
4 |
72 | 55, 17, 71 | ltleii 10039 |
. . . . . . . . 9
⊢ 3 ≤
4 |
73 | 63 | nnzi 11278 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
74 | 73 | eluz1i 11571 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
75 | 70, 72, 74 | mpbir2an 957 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
76 | | leexp2a 12778 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ 4 ∈ (ℤ≥‘3))
→ (2↑3) ≤ (2↑4)) |
77 | 68, 69, 75, 76 | mp3an 1416 |
. . . . . . 7
⊢
(2↑3) ≤ (2↑4) |
78 | | 8re 10982 |
. . . . . . . . 9
⊢ 8 ∈
ℝ |
79 | 61, 78 | eqeltri 2684 |
. . . . . . . 8
⊢
(2↑3) ∈ ℝ |
80 | | 2nn 11062 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
81 | | nnexpcl 12735 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈
ℕ) |
82 | 80, 10, 81 | mp2an 704 |
. . . . . . . . 9
⊢
(2↑4) ∈ ℕ |
83 | 82 | nnrei 10906 |
. . . . . . . 8
⊢
(2↑4) ∈ ℝ |
84 | 56, 79, 83 | ltletri 10044 |
. . . . . . 7
⊢ ((5 <
(2↑3) ∧ (2↑3) ≤ (2↑4)) → 5 <
(2↑4)) |
85 | 67, 77, 84 | mp2an 704 |
. . . . . 6
⊢ 5 <
(2↑4) |
86 | | 6re 10978 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
87 | 86, 83 | remulcli 9933 |
. . . . . . 7
⊢ (6
· (2↑4)) ∈ ℝ |
88 | | 6pos 10996 |
. . . . . . . 8
⊢ 0 <
6 |
89 | 82 | nngt0i 10931 |
. . . . . . . 8
⊢ 0 <
(2↑4) |
90 | 86, 83, 88, 89 | mulgt0ii 10049 |
. . . . . . 7
⊢ 0 < (6
· (2↑4)) |
91 | 56, 83, 87, 90 | ltdiv1ii 10832 |
. . . . . 6
⊢ (5 <
(2↑4) ↔ (5 / (6 · (2↑4))) < ((2↑4) / (6 ·
(2↑4)))) |
92 | 85, 91 | mpbi 219 |
. . . . 5
⊢ (5 / (6
· (2↑4))) < ((2↑4) / (6 ·
(2↑4))) |
93 | | df-5 10959 |
. . . . . 6
⊢ 5 = (4 +
1) |
94 | | df-4 10958 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
95 | 94 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(!‘4) = (!‘(3 + 1)) |
96 | | 3nn0 11187 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
97 | | facp1 12927 |
. . . . . . . . . . 11
⊢ (3 ∈
ℕ0 → (!‘(3 + 1)) = ((!‘3) · (3 +
1))) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . 10
⊢
(!‘(3 + 1)) = ((!‘3) · (3 + 1)) |
99 | | sq2 12822 |
. . . . . . . . . . . 12
⊢
(2↑2) = 4 |
100 | 99, 94 | eqtr2i 2633 |
. . . . . . . . . . 11
⊢ (3 + 1) =
(2↑2) |
101 | 100 | oveq2i 6560 |
. . . . . . . . . 10
⊢
((!‘3) · (3 + 1)) = ((!‘3) ·
(2↑2)) |
102 | 95, 98, 101 | 3eqtri 2636 |
. . . . . . . . 9
⊢
(!‘4) = ((!‘3) · (2↑2)) |
103 | 102 | oveq1i 6559 |
. . . . . . . 8
⊢
((!‘4) · (2↑2)) = (((!‘3) · (2↑2))
· (2↑2)) |
104 | 99 | oveq2i 6560 |
. . . . . . . 8
⊢
((!‘4) · (2↑2)) = ((!‘4) ·
4) |
105 | | fac3 12929 |
. . . . . . . . . 10
⊢
(!‘3) = 6 |
106 | | 6cn 10979 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
107 | 105, 106 | eqeltri 2684 |
. . . . . . . . 9
⊢
(!‘3) ∈ ℂ |
108 | 17 | recni 9931 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
109 | 99, 108 | eqeltri 2684 |
. . . . . . . . 9
⊢
(2↑2) ∈ ℂ |
110 | 107, 109,
109 | mulassi 9928 |
. . . . . . . 8
⊢
(((!‘3) · (2↑2)) · (2↑2)) = ((!‘3)
· ((2↑2) · (2↑2))) |
111 | 103, 104,
110 | 3eqtr3i 2640 |
. . . . . . 7
⊢
((!‘4) · 4) = ((!‘3) · ((2↑2) ·
(2↑2))) |
112 | | 2p2e4 11021 |
. . . . . . . . . 10
⊢ (2 + 2) =
4 |
113 | 112 | oveq2i 6560 |
. . . . . . . . 9
⊢
(2↑(2 + 2)) = (2↑4) |
114 | | 2cn 10968 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
115 | | 2nn0 11186 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
116 | | expadd 12764 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈
ℕ0) → (2↑(2 + 2)) = ((2↑2) ·
(2↑2))) |
117 | 114, 115,
115, 116 | mp3an 1416 |
. . . . . . . . 9
⊢
(2↑(2 + 2)) = ((2↑2) · (2↑2)) |
118 | 113, 117 | eqtr3i 2634 |
. . . . . . . 8
⊢
(2↑4) = ((2↑2) · (2↑2)) |
119 | 118 | oveq2i 6560 |
. . . . . . 7
⊢
((!‘3) · (2↑4)) = ((!‘3) · ((2↑2)
· (2↑2))) |
120 | 105 | oveq1i 6559 |
. . . . . . 7
⊢
((!‘3) · (2↑4)) = (6 ·
(2↑4)) |
121 | 111, 119,
120 | 3eqtr2ri 2639 |
. . . . . 6
⊢ (6
· (2↑4)) = ((!‘4) · 4) |
122 | 93, 121 | oveq12i 6561 |
. . . . 5
⊢ (5 / (6
· (2↑4))) = ((4 + 1) / ((!‘4) · 4)) |
123 | 82 | nncni 10907 |
. . . . . . . 8
⊢
(2↑4) ∈ ℂ |
124 | 123 | mulid2i 9922 |
. . . . . . 7
⊢ (1
· (2↑4)) = (2↑4) |
125 | 124 | oveq1i 6559 |
. . . . . 6
⊢ ((1
· (2↑4)) / (6 · (2↑4))) = ((2↑4) / (6 ·
(2↑4))) |
126 | 82 | nnne0i 10932 |
. . . . . . . . 9
⊢
(2↑4) ≠ 0 |
127 | 123, 126 | dividi 10637 |
. . . . . . . 8
⊢
((2↑4) / (2↑4)) = 1 |
128 | 127 | oveq2i 6560 |
. . . . . . 7
⊢ ((1 / 6)
· ((2↑4) / (2↑4))) = ((1 / 6) · 1) |
129 | | ax-1cn 9873 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
130 | 86, 88 | gt0ne0ii 10443 |
. . . . . . . 8
⊢ 6 ≠
0 |
131 | 129, 106,
123, 123, 130, 126 | divmuldivi 10664 |
. . . . . . 7
⊢ ((1 / 6)
· ((2↑4) / (2↑4))) = ((1 · (2↑4)) / (6 ·
(2↑4))) |
132 | 86, 130 | rereccli 10669 |
. . . . . . . . 9
⊢ (1 / 6)
∈ ℝ |
133 | 132 | recni 9931 |
. . . . . . . 8
⊢ (1 / 6)
∈ ℂ |
134 | 133 | mulid1i 9921 |
. . . . . . 7
⊢ ((1 / 6)
· 1) = (1 / 6) |
135 | 128, 131,
134 | 3eqtr3i 2640 |
. . . . . 6
⊢ ((1
· (2↑4)) / (6 · (2↑4))) = (1 / 6) |
136 | 125, 135 | eqtr3i 2634 |
. . . . 5
⊢
((2↑4) / (6 · (2↑4))) = (1 / 6) |
137 | 92, 122, 136 | 3brtr3i 4612 |
. . . 4
⊢ ((4 + 1)
/ ((!‘4) · 4)) < (1 / 6) |
138 | | rpexpcl 12741 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 4 ∈ ℤ) → (𝐴↑4) ∈
ℝ+) |
139 | 38, 70, 138 | sylancl 693 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ+) |
140 | | elrp 11710 |
. . . . . 6
⊢ ((𝐴↑4) ∈
ℝ+ ↔ ((𝐴↑4) ∈ ℝ ∧ 0 < (𝐴↑4))) |
141 | | ltmul2 10753 |
. . . . . . 7
⊢ ((((4 +
1) / ((!‘4) · 4)) ∈ ℝ ∧ (1 / 6) ∈ ℝ
∧ ((𝐴↑4) ∈
ℝ ∧ 0 < (𝐴↑4))) → (((4 + 1) / ((!‘4)
· 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
142 | 24, 132, 141 | mp3an12 1406 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 0
< (𝐴↑4)) →
(((4 + 1) / ((!‘4) · 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
143 | 140, 142 | sylbi 206 |
. . . . 5
⊢ ((𝐴↑4) ∈
ℝ+ → (((4 + 1) / ((!‘4) · 4)) < (1 / 6)
↔ ((𝐴↑4) ·
((4 + 1) / ((!‘4) · 4))) < ((𝐴↑4) · (1 /
6)))) |
144 | 139, 143 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((4 + 1)
/ ((!‘4) · 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
145 | 137, 144 | mpbii 222 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) < ((𝐴↑4) · (1 / 6))) |
146 | 16 | recnd 9947 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℂ) |
147 | | divrec 10580 |
. . . . 5
⊢ (((𝐴↑4) ∈ ℂ ∧ 6
∈ ℂ ∧ 6 ≠ 0) → ((𝐴↑4) / 6) = ((𝐴↑4) · (1 / 6))) |
148 | 106, 130,
147 | mp3an23 1408 |
. . . 4
⊢ ((𝐴↑4) ∈ ℂ →
((𝐴↑4) / 6) = ((𝐴↑4) · (1 /
6))) |
149 | 146, 148 | syl 17 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) = ((𝐴↑4) · (1 /
6))) |
150 | 145, 149 | breqtrrd 4611 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) < ((𝐴↑4) / 6)) |
151 | 14, 26, 29, 52, 150 | lelttrd 10074 |
1
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) |