Proof of Theorem ef01bndlem
Step | Hyp | Ref
| Expression |
1 | | ax-icn 7869 |
. . . . 5
⊢ i ∈
ℂ |
2 | | 0xr 7966 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
3 | | 1re 7919 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
4 | | elioc2 9893 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
5 | 2, 3, 4 | mp2an 424 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
6 | 5 | simp1bi 1007 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
7 | 6 | recnd 7948 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
8 | | mulcl 7901 |
. . . . 5
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
9 | 1, 7, 8 | sylancr 412 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (i
· 𝐴) ∈
ℂ) |
10 | | 4nn0 9154 |
. . . 4
⊢ 4 ∈
ℕ0 |
11 | | ef01bnd.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) |
12 | 11 | eftlcl 11651 |
. . . 4
⊢ (((i
· 𝐴) ∈ ℂ
∧ 4 ∈ ℕ0) → Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘) ∈ ℂ) |
13 | 9, 10, 12 | sylancl 411 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘) ∈ ℂ) |
14 | 13 | abscld 11145 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ∈ ℝ) |
15 | | reexpcl 10493 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 4 ∈
ℕ0) → (𝐴↑4) ∈ ℝ) |
16 | 6, 10, 15 | sylancl 411 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ) |
17 | | 4re 8955 |
. . . . 5
⊢ 4 ∈
ℝ |
18 | 17, 3 | readdcli 7933 |
. . . 4
⊢ (4 + 1)
∈ ℝ |
19 | | faccl 10669 |
. . . . . 6
⊢ (4 ∈
ℕ0 → (!‘4) ∈ ℕ) |
20 | 10, 19 | ax-mp 5 |
. . . . 5
⊢
(!‘4) ∈ ℕ |
21 | | 4nn 9041 |
. . . . 5
⊢ 4 ∈
ℕ |
22 | 20, 21 | nnmulcli 8900 |
. . . 4
⊢
((!‘4) · 4) ∈ ℕ |
23 | | nndivre 8914 |
. . . 4
⊢ (((4 + 1)
∈ ℝ ∧ ((!‘4) · 4) ∈ ℕ) → ((4 + 1) /
((!‘4) · 4)) ∈ ℝ) |
24 | 18, 22, 23 | mp2an 424 |
. . 3
⊢ ((4 + 1)
/ ((!‘4) · 4)) ∈ ℝ |
25 | | remulcl 7902 |
. . 3
⊢ (((𝐴↑4) ∈ ℝ ∧
((4 + 1) / ((!‘4) · 4)) ∈ ℝ) → ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) ∈ ℝ) |
26 | 16, 24, 25 | sylancl 411 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) ∈ ℝ) |
27 | | 6nn 9043 |
. . 3
⊢ 6 ∈
ℕ |
28 | | nndivre 8914 |
. . 3
⊢ (((𝐴↑4) ∈ ℝ ∧ 6
∈ ℕ) → ((𝐴↑4) / 6) ∈
ℝ) |
29 | 16, 27, 28 | sylancl 411 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) ∈
ℝ) |
30 | | eqid 2170 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘(i · 𝐴))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘(i · 𝐴))↑𝑛) / (!‘𝑛))) |
31 | | eqid 2170 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘(i · 𝐴))↑4) / (!‘4)) · ((1 / (4
+ 1))↑𝑛))) = (𝑛 ∈ ℕ0
↦ ((((abs‘(i · 𝐴))↑4) / (!‘4)) · ((1 / (4
+ 1))↑𝑛))) |
32 | 21 | a1i 9 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → 4 ∈
ℕ) |
33 | | absmul 11033 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (abs‘(i · 𝐴)) = ((abs‘i) ·
(abs‘𝐴))) |
34 | 1, 7, 33 | sylancr 412 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
= ((abs‘i) · (abs‘𝐴))) |
35 | | absi 11023 |
. . . . . . . 8
⊢
(abs‘i) = 1 |
36 | 35 | oveq1i 5863 |
. . . . . . 7
⊢
((abs‘i) · (abs‘𝐴)) = (1 · (abs‘𝐴)) |
37 | 5 | simp2bi 1008 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
38 | 6, 37 | elrpd 9650 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ+) |
39 | | rpre 9617 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
40 | | rpge0 9623 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 0 ≤ 𝐴) |
41 | 39, 40 | absidd 11131 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (abs‘𝐴) =
𝐴) |
42 | 38, 41 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,]1) →
(abs‘𝐴) = 𝐴) |
43 | 42 | oveq2d 5869 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (1
· (abs‘𝐴)) =
(1 · 𝐴)) |
44 | 36, 43 | eqtrid 2215 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) →
((abs‘i) · (abs‘𝐴)) = (1 · 𝐴)) |
45 | 7 | mulid2d 7938 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (1
· 𝐴) = 𝐴) |
46 | 34, 44, 45 | 3eqtrd 2207 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
= 𝐴) |
47 | 5 | simp3bi 1009 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
48 | 46, 47 | eqbrtrd 4011 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
(abs‘(i · 𝐴))
≤ 1) |
49 | 11, 30, 31, 32, 9, 48 | eftlub 11653 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ≤ (((abs‘(i · 𝐴))↑4) · ((4 + 1) /
((!‘4) · 4)))) |
50 | 46 | oveq1d 5868 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) →
((abs‘(i · 𝐴))↑4) = (𝐴↑4)) |
51 | 50 | oveq1d 5868 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(((abs‘(i · 𝐴))↑4) · ((4 + 1) / ((!‘4)
· 4))) = ((𝐴↑4)
· ((4 + 1) / ((!‘4) · 4)))) |
52 | 49, 51 | breqtrd 4015 |
. 2
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) ≤ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4)))) |
53 | | 3pos 8972 |
. . . . . . . . 9
⊢ 0 <
3 |
54 | | 0re 7920 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
55 | | 3re 8952 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
56 | | 5re 8957 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
57 | 54, 55, 56 | ltadd1i 8421 |
. . . . . . . . 9
⊢ (0 < 3
↔ (0 + 5) < (3 + 5)) |
58 | 53, 57 | mpbi 144 |
. . . . . . . 8
⊢ (0 + 5)
< (3 + 5) |
59 | | 5cn 8958 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
60 | 59 | addid2i 8062 |
. . . . . . . 8
⊢ (0 + 5) =
5 |
61 | | cu2 10574 |
. . . . . . . . 9
⊢
(2↑3) = 8 |
62 | | 5p3e8 9025 |
. . . . . . . . 9
⊢ (5 + 3) =
8 |
63 | | 3cn 8953 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
64 | 59, 63 | addcomi 8063 |
. . . . . . . . 9
⊢ (5 + 3) =
(3 + 5) |
65 | 61, 62, 64 | 3eqtr2ri 2198 |
. . . . . . . 8
⊢ (3 + 5) =
(2↑3) |
66 | 58, 60, 65 | 3brtr3i 4018 |
. . . . . . 7
⊢ 5 <
(2↑3) |
67 | | 2re 8948 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
68 | | 1le2 9086 |
. . . . . . . 8
⊢ 1 ≤
2 |
69 | | 4z 9242 |
. . . . . . . . 9
⊢ 4 ∈
ℤ |
70 | | 3lt4 9050 |
. . . . . . . . . 10
⊢ 3 <
4 |
71 | 55, 17, 70 | ltleii 8022 |
. . . . . . . . 9
⊢ 3 ≤
4 |
72 | | 3z 9241 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
73 | 72 | eluz1i 9494 |
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
74 | 69, 71, 73 | mpbir2an 937 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘3) |
75 | | leexp2a 10529 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ 4 ∈ (ℤ≥‘3))
→ (2↑3) ≤ (2↑4)) |
76 | 67, 68, 74, 75 | mp3an 1332 |
. . . . . . 7
⊢
(2↑3) ≤ (2↑4) |
77 | | 8re 8963 |
. . . . . . . . 9
⊢ 8 ∈
ℝ |
78 | 61, 77 | eqeltri 2243 |
. . . . . . . 8
⊢
(2↑3) ∈ ℝ |
79 | | 2nn 9039 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
80 | | nnexpcl 10489 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 4 ∈ ℕ0) → (2↑4) ∈
ℕ) |
81 | 79, 10, 80 | mp2an 424 |
. . . . . . . . 9
⊢
(2↑4) ∈ ℕ |
82 | 81 | nnrei 8887 |
. . . . . . . 8
⊢
(2↑4) ∈ ℝ |
83 | 56, 78, 82 | ltletri 8026 |
. . . . . . 7
⊢ ((5 <
(2↑3) ∧ (2↑3) ≤ (2↑4)) → 5 <
(2↑4)) |
84 | 66, 76, 83 | mp2an 424 |
. . . . . 6
⊢ 5 <
(2↑4) |
85 | | 6re 8959 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
86 | 85, 82 | remulcli 7934 |
. . . . . . 7
⊢ (6
· (2↑4)) ∈ ℝ |
87 | | 6pos 8979 |
. . . . . . . 8
⊢ 0 <
6 |
88 | 81 | nngt0i 8908 |
. . . . . . . 8
⊢ 0 <
(2↑4) |
89 | 85, 82, 87, 88 | mulgt0ii 8030 |
. . . . . . 7
⊢ 0 < (6
· (2↑4)) |
90 | 56, 82, 86, 89 | ltdiv1ii 8845 |
. . . . . 6
⊢ (5 <
(2↑4) ↔ (5 / (6 · (2↑4))) < ((2↑4) / (6 ·
(2↑4)))) |
91 | 84, 90 | mpbi 144 |
. . . . 5
⊢ (5 / (6
· (2↑4))) < ((2↑4) / (6 ·
(2↑4))) |
92 | | df-5 8940 |
. . . . . 6
⊢ 5 = (4 +
1) |
93 | | df-4 8939 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
94 | 93 | fveq2i 5499 |
. . . . . . . . . 10
⊢
(!‘4) = (!‘(3 + 1)) |
95 | | 3nn0 9153 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
96 | | facp1 10664 |
. . . . . . . . . . 11
⊢ (3 ∈
ℕ0 → (!‘(3 + 1)) = ((!‘3) · (3 +
1))) |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . 10
⊢
(!‘(3 + 1)) = ((!‘3) · (3 + 1)) |
98 | | sq2 10571 |
. . . . . . . . . . . 12
⊢
(2↑2) = 4 |
99 | 98, 93 | eqtr2i 2192 |
. . . . . . . . . . 11
⊢ (3 + 1) =
(2↑2) |
100 | 99 | oveq2i 5864 |
. . . . . . . . . 10
⊢
((!‘3) · (3 + 1)) = ((!‘3) ·
(2↑2)) |
101 | 94, 97, 100 | 3eqtri 2195 |
. . . . . . . . 9
⊢
(!‘4) = ((!‘3) · (2↑2)) |
102 | 101 | oveq1i 5863 |
. . . . . . . 8
⊢
((!‘4) · (2↑2)) = (((!‘3) · (2↑2))
· (2↑2)) |
103 | 98 | oveq2i 5864 |
. . . . . . . 8
⊢
((!‘4) · (2↑2)) = ((!‘4) ·
4) |
104 | | fac3 10666 |
. . . . . . . . . 10
⊢
(!‘3) = 6 |
105 | | 6cn 8960 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
106 | 104, 105 | eqeltri 2243 |
. . . . . . . . 9
⊢
(!‘3) ∈ ℂ |
107 | 17 | recni 7932 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
108 | 98, 107 | eqeltri 2243 |
. . . . . . . . 9
⊢
(2↑2) ∈ ℂ |
109 | 106, 108,
108 | mulassi 7929 |
. . . . . . . 8
⊢
(((!‘3) · (2↑2)) · (2↑2)) = ((!‘3)
· ((2↑2) · (2↑2))) |
110 | 102, 103,
109 | 3eqtr3i 2199 |
. . . . . . 7
⊢
((!‘4) · 4) = ((!‘3) · ((2↑2) ·
(2↑2))) |
111 | | 2p2e4 9005 |
. . . . . . . . . 10
⊢ (2 + 2) =
4 |
112 | 111 | oveq2i 5864 |
. . . . . . . . 9
⊢
(2↑(2 + 2)) = (2↑4) |
113 | | 2cn 8949 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
114 | | 2nn0 9152 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
115 | | expadd 10518 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈
ℕ0) → (2↑(2 + 2)) = ((2↑2) ·
(2↑2))) |
116 | 113, 114,
114, 115 | mp3an 1332 |
. . . . . . . . 9
⊢
(2↑(2 + 2)) = ((2↑2) · (2↑2)) |
117 | 112, 116 | eqtr3i 2193 |
. . . . . . . 8
⊢
(2↑4) = ((2↑2) · (2↑2)) |
118 | 117 | oveq2i 5864 |
. . . . . . 7
⊢
((!‘3) · (2↑4)) = ((!‘3) · ((2↑2)
· (2↑2))) |
119 | 104 | oveq1i 5863 |
. . . . . . 7
⊢
((!‘3) · (2↑4)) = (6 ·
(2↑4)) |
120 | 110, 118,
119 | 3eqtr2ri 2198 |
. . . . . 6
⊢ (6
· (2↑4)) = ((!‘4) · 4) |
121 | 92, 120 | oveq12i 5865 |
. . . . 5
⊢ (5 / (6
· (2↑4))) = ((4 + 1) / ((!‘4) · 4)) |
122 | 81 | nncni 8888 |
. . . . . . . 8
⊢
(2↑4) ∈ ℂ |
123 | 122 | mulid2i 7923 |
. . . . . . 7
⊢ (1
· (2↑4)) = (2↑4) |
124 | 123 | oveq1i 5863 |
. . . . . 6
⊢ ((1
· (2↑4)) / (6 · (2↑4))) = ((2↑4) / (6 ·
(2↑4))) |
125 | 82, 88 | gt0ap0ii 8547 |
. . . . . . . . 9
⊢
(2↑4) # 0 |
126 | 122, 125 | dividapi 8662 |
. . . . . . . 8
⊢
((2↑4) / (2↑4)) = 1 |
127 | 126 | oveq2i 5864 |
. . . . . . 7
⊢ ((1 / 6)
· ((2↑4) / (2↑4))) = ((1 / 6) · 1) |
128 | | ax-1cn 7867 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
129 | 85, 87 | gt0ap0ii 8547 |
. . . . . . . 8
⊢ 6 #
0 |
130 | 128, 105,
122, 122, 129, 125 | divmuldivapi 8689 |
. . . . . . 7
⊢ ((1 / 6)
· ((2↑4) / (2↑4))) = ((1 · (2↑4)) / (6 ·
(2↑4))) |
131 | 85, 129 | rerecclapi 8694 |
. . . . . . . . 9
⊢ (1 / 6)
∈ ℝ |
132 | 131 | recni 7932 |
. . . . . . . 8
⊢ (1 / 6)
∈ ℂ |
133 | 132 | mulid1i 7922 |
. . . . . . 7
⊢ ((1 / 6)
· 1) = (1 / 6) |
134 | 127, 130,
133 | 3eqtr3i 2199 |
. . . . . 6
⊢ ((1
· (2↑4)) / (6 · (2↑4))) = (1 / 6) |
135 | 124, 134 | eqtr3i 2193 |
. . . . 5
⊢
((2↑4) / (6 · (2↑4))) = (1 / 6) |
136 | 91, 121, 135 | 3brtr3i 4018 |
. . . 4
⊢ ((4 + 1)
/ ((!‘4) · 4)) < (1 / 6) |
137 | | rpexpcl 10495 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 4 ∈ ℤ) → (𝐴↑4) ∈
ℝ+) |
138 | 38, 69, 137 | sylancl 411 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℝ+) |
139 | | elrp 9612 |
. . . . . 6
⊢ ((𝐴↑4) ∈
ℝ+ ↔ ((𝐴↑4) ∈ ℝ ∧ 0 < (𝐴↑4))) |
140 | | ltmul2 8772 |
. . . . . . 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 1322 |
. . . . . 6
⊢ (((𝐴↑4) ∈ ℝ ∧ 0
< (𝐴↑4)) →
(((4 + 1) / ((!‘4) · 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
142 | 139, 141 | sylbi 120 |
. . . . 5
⊢ ((𝐴↑4) ∈
ℝ+ → (((4 + 1) / ((!‘4) · 4)) < (1 / 6)
↔ ((𝐴↑4) ·
((4 + 1) / ((!‘4) · 4))) < ((𝐴↑4) · (1 /
6)))) |
143 | 138, 142 | syl 14 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (((4 + 1)
/ ((!‘4) · 4)) < (1 / 6) ↔ ((𝐴↑4) · ((4 + 1) / ((!‘4)
· 4))) < ((𝐴↑4) · (1 /
6)))) |
144 | 136, 143 | mpbii 147 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) < ((𝐴↑4) · (1 / 6))) |
145 | 16 | recnd 7948 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑4) ∈
ℂ) |
146 | | divrecap 8605 |
. . . . 5
⊢ (((𝐴↑4) ∈ ℂ ∧ 6
∈ ℂ ∧ 6 # 0) → ((𝐴↑4) / 6) = ((𝐴↑4) · (1 / 6))) |
147 | 105, 129,
146 | mp3an23 1324 |
. . . 4
⊢ ((𝐴↑4) ∈ ℂ →
((𝐴↑4) / 6) = ((𝐴↑4) · (1 /
6))) |
148 | 145, 147 | syl 14 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) / 6) = ((𝐴↑4) · (1 /
6))) |
149 | 144, 148 | breqtrrd 4017 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑4) · ((4 + 1) /
((!‘4) · 4))) < ((𝐴↑4) / 6)) |
150 | 14, 26, 29, 52, 149 | lelttrd 8044 |
1
⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) |