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	eqtrid	⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( abs ‘ i ) · ( abs ‘ 𝐴 ) ) = ( 1 · 𝐴 ) )
45	8	mullidd	⊢ ( 𝐴 ∈ ( 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	addlidi	⊢ ( 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	mullidi	⊢ ( 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	mulridi	⊢ ( ( 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 ) )