Metamath Proof Explorer

Theorem ef01bndlem

Description: Lemma for sin01bnd and cos01bnd . (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Hypothesis ef01bnd.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion ef01bndlem ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) < ( ( 𝐴 ↑ 4 ) / 6 ) )

Proof

Step Hyp Ref Expression
1 ef01bnd.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 ax-icn ⊢ i ∈ ℂ
3 0xr ⊢ 0 ∈ ℝ*
4 1re ⊢ 1 ∈ ℝ
5 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) ) )
6 3 4 5 mp2an ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) )
7 6 simp1bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℝ )
8 7 recnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℂ )
9 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
10 2 8 9 sylancr ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( i · 𝐴 ) ∈ ℂ )
11 4nn0 ⊢ 4 ∈ ℕ0
12 1 eftlcl ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 4 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
13 10 11 12 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
14 13 abscld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
15 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 4 ∈ ℕ0 ) → ( 𝐴 ↑ 4 ) ∈ ℝ )
16 7 11 15 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ∈ ℝ )
17 4re ⊢ 4 ∈ ℝ
18 17 4 readdcli ⊢ ( 4 + 1 ) ∈ ℝ
19 faccl ⊢ ( 4 ∈ ℕ0 → ( ! ‘ 4 ) ∈ ℕ )
20 11 19 ax-mp ⊢ ( ! ‘ 4 ) ∈ ℕ
21 4nn ⊢ 4 ∈ ℕ
22 20 21 nnmulcli ⊢ ( ( ! ‘ 4 ) · 4 ) ∈ ℕ
23 nndivre ⊢ ( ( ( 4 + 1 ) ∈ ℝ ∧ ( ( ! ‘ 4 ) · 4 ) ∈ ℕ ) → ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ∈ ℝ )
24 18 22 23 mp2an ⊢ ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ∈ ℝ
25 remulcl ⊢ ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ∈ ℝ ) → ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) ∈ ℝ )
26 16 24 25 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) ∈ ℝ )
27 6nn ⊢ 6 ∈ ℕ
28 nndivre ⊢ ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝐴 ↑ 4 ) / 6 ) ∈ ℝ )
29 16 27 28 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) / 6 ) ∈ ℝ )
30 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ ( i · 𝐴 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ ( i · 𝐴 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
31 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ ( i · 𝐴 ) ) ↑ 4 ) / ( ! ‘ 4 ) ) · ( ( 1 / ( 4 + 1 ) ) ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ ( i · 𝐴 ) ) ↑ 4 ) / ( ! ‘ 4 ) ) · ( ( 1 / ( 4 + 1 ) ) ↑ 𝑛 ) ) )
32 21 a1i ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 4 ∈ ℕ )
33 absmul ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( i · 𝐴 ) ) = ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) )
34 2 8 33 sylancr ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( i · 𝐴 ) ) = ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) )
35 absi ⊢ ( abs ‘ i ) = 1
36 35 oveq1i ⊢ ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) = ( 1 · ( abs ‘ 𝐴 ) )
37 6 simp2bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < 𝐴 )
38 7 37 elrpd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℝ+ )
39 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
40 rpge0 ⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )
41 39 40 absidd ⊢ ( 𝐴 ∈ ℝ+ → ( abs ‘ 𝐴 ) = 𝐴 )
42 38 41 syl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ 𝐴 ) = 𝐴 )
43 42 oveq2d ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 · ( abs ‘ 𝐴 ) ) = ( 1 · 𝐴 ) )
44 36 43 syl5eq ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) = ( 1 · 𝐴 ) )
45 8 mulid2d ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 1 · 𝐴 ) = 𝐴 )
46 34 44 45 3eqtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( i · 𝐴 ) ) = 𝐴 )
47 6 simp3bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ≤ 1 )
48 46 47 eqbrtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ ( i · 𝐴 ) ) ≤ 1 )
49 1 30 31 32 10 48 eftlub ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( ( abs ‘ ( i · 𝐴 ) ) ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) )
50 46 oveq1d ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ ( i · 𝐴 ) ) ↑ 4 ) = ( 𝐴 ↑ 4 ) )
51 50 oveq1d ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( abs ‘ ( i · 𝐴 ) ) ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) = ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) )
52 49 51 breqtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) )
53 3pos ⊢ 0 < 3
54 0re ⊢ 0 ∈ ℝ
55 3re ⊢ 3 ∈ ℝ
56 5re ⊢ 5 ∈ ℝ
57 54 55 56 ltadd1i ⊢ ( 0 < 3 ↔ ( 0 + 5 ) < ( 3 + 5 ) )
58 53 57 mpbi ⊢ ( 0 + 5 ) < ( 3 + 5 )
59 5cn ⊢ 5 ∈ ℂ
60 59 addid2i ⊢ ( 0 + 5 ) = 5
61 cu2 ⊢ ( 2 ↑ 3 ) = 8
62 5p3e8 ⊢ ( 5 + 3 ) = 8
63 3cn ⊢ 3 ∈ ℂ
64 59 63 addcomi ⊢ ( 5 + 3 ) = ( 3 + 5 )
65 61 62 64 3eqtr2ri ⊢ ( 3 + 5 ) = ( 2 ↑ 3 )
66 58 60 65 3brtr3i ⊢ 5 < ( 2 ↑ 3 )
67 2re ⊢ 2 ∈ ℝ
68 1le2 ⊢ 1 ≤ 2
69 4z ⊢ 4 ∈ ℤ
70 3lt4 ⊢ 3 < 4
71 55 17 70 ltleii ⊢ 3 ≤ 4
72 3z ⊢ 3 ∈ ℤ
73 72 eluz1i ⊢ ( 4 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 4 ∈ ℤ ∧ 3 ≤ 4 ) )
74 69 71 73 mpbir2an ⊢ 4 ∈ ( ℤ≥ ‘ 3 )
75 leexp2a ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ 4 ∈ ( ℤ≥ ‘ 3 ) ) → ( 2 ↑ 3 ) ≤ ( 2 ↑ 4 ) )
76 67 68 74 75 mp3an ⊢ ( 2 ↑ 3 ) ≤ ( 2 ↑ 4 )
77 8re ⊢ 8 ∈ ℝ
78 61 77 eqeltri ⊢ ( 2 ↑ 3 ) ∈ ℝ
79 2nn ⊢ 2 ∈ ℕ
80 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 4 ∈ ℕ0 ) → ( 2 ↑ 4 ) ∈ ℕ )
81 79 11 80 mp2an ⊢ ( 2 ↑ 4 ) ∈ ℕ
82 81 nnrei ⊢ ( 2 ↑ 4 ) ∈ ℝ
83 56 78 82 ltletri ⊢ ( ( 5 < ( 2 ↑ 3 ) ∧ ( 2 ↑ 3 ) ≤ ( 2 ↑ 4 ) ) → 5 < ( 2 ↑ 4 ) )
84 66 76 83 mp2an ⊢ 5 < ( 2 ↑ 4 )
85 6re ⊢ 6 ∈ ℝ
86 85 82 remulcli ⊢ ( 6 · ( 2 ↑ 4 ) ) ∈ ℝ
87 6pos ⊢ 0 < 6
88 81 nngt0i ⊢ 0 < ( 2 ↑ 4 )
89 85 82 87 88 mulgt0ii ⊢ 0 < ( 6 · ( 2 ↑ 4 ) )
90 56 82 86 89 ltdiv1ii ⊢ ( 5 < ( 2 ↑ 4 ) ↔ ( 5 / ( 6 · ( 2 ↑ 4 ) ) ) < ( ( 2 ↑ 4 ) / ( 6 · ( 2 ↑ 4 ) ) ) )
91 84 90 mpbi ⊢ ( 5 / ( 6 · ( 2 ↑ 4 ) ) ) < ( ( 2 ↑ 4 ) / ( 6 · ( 2 ↑ 4 ) ) )
92 df-5 ⊢ 5 = ( 4 + 1 )
93 df-4 ⊢ 4 = ( 3 + 1 )
94 93 fveq2i ⊢ ( ! ‘ 4 ) = ( ! ‘ ( 3 + 1 ) )
95 3nn0 ⊢ 3 ∈ ℕ0
96 facp1 ⊢ ( 3 ∈ ℕ0 → ( ! ‘ ( 3 + 1 ) ) = ( ( ! ‘ 3 ) · ( 3 + 1 ) ) )
97 95 96 ax-mp ⊢ ( ! ‘ ( 3 + 1 ) ) = ( ( ! ‘ 3 ) · ( 3 + 1 ) )
98 sq2 ⊢ ( 2 ↑ 2 ) = 4
99 98 93 eqtr2i ⊢ ( 3 + 1 ) = ( 2 ↑ 2 )
100 99 oveq2i ⊢ ( ( ! ‘ 3 ) · ( 3 + 1 ) ) = ( ( ! ‘ 3 ) · ( 2 ↑ 2 ) )
101 94 97 100 3eqtri ⊢ ( ! ‘ 4 ) = ( ( ! ‘ 3 ) · ( 2 ↑ 2 ) )
102 101 oveq1i ⊢ ( ( ! ‘ 4 ) · ( 2 ↑ 2 ) ) = ( ( ( ! ‘ 3 ) · ( 2 ↑ 2 ) ) · ( 2 ↑ 2 ) )
103 98 oveq2i ⊢ ( ( ! ‘ 4 ) · ( 2 ↑ 2 ) ) = ( ( ! ‘ 4 ) · 4 )
104 fac3 ⊢ ( ! ‘ 3 ) = 6
105 6cn ⊢ 6 ∈ ℂ
106 104 105 eqeltri ⊢ ( ! ‘ 3 ) ∈ ℂ
107 17 recni ⊢ 4 ∈ ℂ
108 98 107 eqeltri ⊢ ( 2 ↑ 2 ) ∈ ℂ
109 106 108 108 mulassi ⊢ ( ( ( ! ‘ 3 ) · ( 2 ↑ 2 ) ) · ( 2 ↑ 2 ) ) = ( ( ! ‘ 3 ) · ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) )
110 102 103 109 3eqtr3i ⊢ ( ( ! ‘ 4 ) · 4 ) = ( ( ! ‘ 3 ) · ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) )
111 2p2e4 ⊢ ( 2 + 2 ) = 4
112 111 oveq2i ⊢ ( 2 ↑ ( 2 + 2 ) ) = ( 2 ↑ 4 )
113 2cn ⊢ 2 ∈ ℂ
114 2nn0 ⊢ 2 ∈ ℕ0
115 expadd ⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 2 ↑ ( 2 + 2 ) ) = ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) )
116 113 114 114 115 mp3an ⊢ ( 2 ↑ ( 2 + 2 ) ) = ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) )
117 112 116 eqtr3i ⊢ ( 2 ↑ 4 ) = ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) )
118 117 oveq2i ⊢ ( ( ! ‘ 3 ) · ( 2 ↑ 4 ) ) = ( ( ! ‘ 3 ) · ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) )
119 104 oveq1i ⊢ ( ( ! ‘ 3 ) · ( 2 ↑ 4 ) ) = ( 6 · ( 2 ↑ 4 ) )
120 110 118 119 3eqtr2ri ⊢ ( 6 · ( 2 ↑ 4 ) ) = ( ( ! ‘ 4 ) · 4 )
121 92 120 oveq12i ⊢ ( 5 / ( 6 · ( 2 ↑ 4 ) ) ) = ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) )
122 81 nncni ⊢ ( 2 ↑ 4 ) ∈ ℂ
123 122 mulid2i ⊢ ( 1 · ( 2 ↑ 4 ) ) = ( 2 ↑ 4 )
124 123 oveq1i ⊢ ( ( 1 · ( 2 ↑ 4 ) ) / ( 6 · ( 2 ↑ 4 ) ) ) = ( ( 2 ↑ 4 ) / ( 6 · ( 2 ↑ 4 ) ) )
125 81 nnne0i ⊢ ( 2 ↑ 4 ) ≠ 0
126 122 125 dividi ⊢ ( ( 2 ↑ 4 ) / ( 2 ↑ 4 ) ) = 1
127 126 oveq2i ⊢ ( ( 1 / 6 ) · ( ( 2 ↑ 4 ) / ( 2 ↑ 4 ) ) ) = ( ( 1 / 6 ) · 1 )
128 ax-1cn ⊢ 1 ∈ ℂ
129 85 87 gt0ne0ii ⊢ 6 ≠ 0
130 128 105 122 122 129 125 divmuldivi ⊢ ( ( 1 / 6 ) · ( ( 2 ↑ 4 ) / ( 2 ↑ 4 ) ) ) = ( ( 1 · ( 2 ↑ 4 ) ) / ( 6 · ( 2 ↑ 4 ) ) )
131 85 129 rereccli ⊢ ( 1 / 6 ) ∈ ℝ
132 131 recni ⊢ ( 1 / 6 ) ∈ ℂ
133 132 mulid1i ⊢ ( ( 1 / 6 ) · 1 ) = ( 1 / 6 )
134 127 130 133 3eqtr3i ⊢ ( ( 1 · ( 2 ↑ 4 ) ) / ( 6 · ( 2 ↑ 4 ) ) ) = ( 1 / 6 )
135 124 134 eqtr3i ⊢ ( ( 2 ↑ 4 ) / ( 6 · ( 2 ↑ 4 ) ) ) = ( 1 / 6 )
136 91 121 135 3brtr3i ⊢ ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) < ( 1 / 6 )
137 rpexpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 4 ∈ ℤ ) → ( 𝐴 ↑ 4 ) ∈ ℝ+ )
138 38 69 137 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ∈ ℝ+ )
139 elrp ⊢ ( ( 𝐴 ↑ 4 ) ∈ ℝ+ ↔ ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 4 ) ) )
140 ltmul2 ⊢ ( ( ( ( 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 ⊢ ( ( ( 𝐴 ↑ 4 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 4 ) ) → ( ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) < ( 1 / 6 ) ↔ ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) < ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) ) )
142 139 141 sylbi ⊢ ( ( 𝐴 ↑ 4 ) ∈ ℝ+ → ( ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) < ( 1 / 6 ) ↔ ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) < ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) ) )
143 138 142 syl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) < ( 1 / 6 ) ↔ ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) < ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) ) )
144 136 143 mpbii ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) < ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) )
145 16 recnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 4 ) ∈ ℂ )
146 divrec ⊢ ( ( ( 𝐴 ↑ 4 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( ( 𝐴 ↑ 4 ) / 6 ) = ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) )
147 105 129 146 mp3an23 ⊢ ( ( 𝐴 ↑ 4 ) ∈ ℂ → ( ( 𝐴 ↑ 4 ) / 6 ) = ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) )
148 145 147 syl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) / 6 ) = ( ( 𝐴 ↑ 4 ) · ( 1 / 6 ) ) )
149 144 148 breqtrrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 4 ) · ( ( 4 + 1 ) / ( ( ! ‘ 4 ) · 4 ) ) ) < ( ( 𝐴 ↑ 4 ) / 6 ) )
150 14 26 29 52 149 lelttrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) < ( ( 𝐴 ↑ 4 ) / 6 ) )