Theorem knoppndvlem11

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 28-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem11.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppndvlem11.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppndvlem11.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	knoppndvlem11.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	knoppndvlem11.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
	knoppndvlem11.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
	knoppndvlem11.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	knoppndvlem11	⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem11.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndvlem11.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndvlem11.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		knoppndvlem11.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		knoppndvlem11.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
6		knoppndvlem11.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
7		knoppndvlem11.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8		fzfid	⊢ ( 𝜑 → ( 0 ... ( 𝐽 − 1 ) ) ∈ Fin )
9	7	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝑁 ∈ ℕ )
10	5	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
11	10	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝐶 ∈ ℝ )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝐵 ∈ ℝ )
14		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) → 𝑖 ∈ ℕ0 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝑖 ∈ ℕ0 )
16	1 2 9 12 13 15	knoppcnlem3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
17	16	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
18	3	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝐴 ∈ ℝ )
19	1 2 9 12 18 15	knoppcnlem3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
20	19	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
21	8 17 20	fsumsub	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) )
22	21	eqcomd	⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) )
23	22	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) = ( abs ‘ Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) )
24	17 20	subcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ∈ ℂ )
25	8 24	fsumcl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ∈ ℂ )
26	25	abscld	⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℝ )
27	24	abscld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℝ )
28	8 27	fsumrecl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℝ )
29	4 3	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
30	29	recnd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
31	30	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
32		2re	⊢ 2 ∈ ℝ
33	32	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
34		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
35	7 34	syl	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
36	33 35	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
37	11	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
38	37	abscld	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
39	36 38	remulcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
41	40 15	reexpcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ∈ ℝ )
42	8 41	fsumrecl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ∈ ℝ )
43	31 42	remulcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) ∈ ℝ )
44	8 24	fsumabs	⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) )
45	31	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
46	45 41	remulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) ∈ ℝ )
47	2 13 15	knoppcnlem1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) = ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) ) )
48	2 18 15	knoppcnlem1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) )
49	47 48	oveq12d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) ) − ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) )
50	12 15	reexpcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝐶 ↑ 𝑖 ) ∈ ℝ )
51	50	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝐶 ↑ 𝑖 ) ∈ ℂ )
52	36	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
53	52 15	reexpcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 2 · 𝑁 ) ↑ 𝑖 ) ∈ ℝ )
54	53 13	remulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ∈ ℝ )
55	1 54	dnicld2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) ∈ ℝ )
56	55	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) ∈ ℂ )
57	53 18	remulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ∈ ℝ )
58	1 57	dnicld2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ∈ ℝ )
59	58	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ∈ ℂ )
60	51 56 59	subdid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝐶 ↑ 𝑖 ) · ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) = ( ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) ) − ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) )
61	60	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) ) − ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) = ( ( 𝐶 ↑ 𝑖 ) · ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) )
62	49 61	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( 𝐶 ↑ 𝑖 ) · ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) )
63	62	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝐶 ↑ 𝑖 ) · ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) )
64	56 59	subcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ∈ ℂ )
65	51 64	absmuld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( 𝐶 ↑ 𝑖 ) · ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) = ( ( abs ‘ ( 𝐶 ↑ 𝑖 ) ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) )
66	37	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝐶 ∈ ℂ )
67	66 15	absexpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( 𝐶 ↑ 𝑖 ) ) = ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) )
68	67	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ ( 𝐶 ↑ 𝑖 ) ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) )
69	65 68	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( 𝐶 ↑ 𝑖 ) · ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) )
70	63 69	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) )
71	64	abscld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ∈ ℝ )
72	54 57	resubcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ∈ ℝ )
73	72	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ∈ ℂ )
74	73	abscld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ∈ ℝ )
75	38	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ 𝐶 ) ∈ ℝ )
76	75 15	reexpcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) ∈ ℝ )
77	66	absge0d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 0 ≤ ( abs ‘ 𝐶 ) )
78	75 15 77	expge0d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 0 ≤ ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) )
79	1 57 54	dnibnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ≤ ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) )
80	71 74 76 78 79	lemul2ad	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) ≤ ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) )
81	53	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 2 · 𝑁 ) ↑ 𝑖 ) ∈ ℂ )
82	13	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝐵 ∈ ℂ )
83	18	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝐴 ∈ ℂ )
84	81 82 83	subdid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( 𝐵 − 𝐴 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) )
85	84	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( 𝐵 − 𝐴 ) ) )
86	85	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) = ( abs ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( 𝐵 − 𝐴 ) ) ) )
87	30	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
88	81 87	absmuld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( abs ‘ ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
89	52	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( 2 · 𝑁 ) ∈ ℂ )
90	89 15	absexpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) = ( ( abs ‘ ( 2 · 𝑁 ) ) ↑ 𝑖 ) )
91	33	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
92	35	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
93	91 92	absmuld	⊢ ( 𝜑 → ( abs ‘ ( 2 · 𝑁 ) ) = ( ( abs ‘ 2 ) · ( abs ‘ 𝑁 ) ) )
94		0le2	⊢ 0 ≤ 2
95	32	absidi	⊢ ( 0 ≤ 2 → ( abs ‘ 2 ) = 2 )
96	94 95	ax-mp	⊢ ( abs ‘ 2 ) = 2
97	96	a1i	⊢ ( 𝜑 → ( abs ‘ 2 ) = 2 )
98		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
99		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
100		0le1	⊢ 0 ≤ 1
101	100	a1i	⊢ ( 𝜑 → 0 ≤ 1 )
102		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
103	7 102	syl	⊢ ( 𝜑 → 1 ≤ 𝑁 )
104	98 99 35 101 103	letrd	⊢ ( 𝜑 → 0 ≤ 𝑁 )
105	35 104	absidd	⊢ ( 𝜑 → ( abs ‘ 𝑁 ) = 𝑁 )
106	97 105	oveq12d	⊢ ( 𝜑 → ( ( abs ‘ 2 ) · ( abs ‘ 𝑁 ) ) = ( 2 · 𝑁 ) )
107	93 106	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( 2 · 𝑁 ) ) = ( 2 · 𝑁 ) )
108	107	oveq1d	⊢ ( 𝜑 → ( ( abs ‘ ( 2 · 𝑁 ) ) ↑ 𝑖 ) = ( ( 2 · 𝑁 ) ↑ 𝑖 ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ ( 2 · 𝑁 ) ) ↑ 𝑖 ) = ( ( 2 · 𝑁 ) ↑ 𝑖 ) )
110	90 109	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) = ( ( 2 · 𝑁 ) ↑ 𝑖 ) )
111	110	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
112	88 111	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
113	86 112	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
114	113	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) ) )
115	76	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) ∈ ℂ )
116	45	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ )
117	115 81 116	mulassd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) ) )
118	117	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) ) = ( ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) )
119	115 81	mulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) ∈ ℂ )
120	119 116	mulcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) = ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) ) )
121	115 81	mulcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) ) )
122	75	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ 𝐶 ) ∈ ℂ )
123	89 122 15	mulexpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) ) )
124	123	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) ) = ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) )
125	121 124	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) = ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) )
126	125	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( 2 · 𝑁 ) ↑ 𝑖 ) ) ) = ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
127	118 120 126	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( abs ‘ ( 𝐵 − 𝐴 ) ) ) ) = ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
128	114 127	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) − ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) = ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
129	80 128	breqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( abs ‘ 𝐶 ) ↑ 𝑖 ) · ( abs ‘ ( ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐵 ) ) − ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
130	70 129	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
131	8 27 46 130	fsumle	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
132	31	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ )
133	125 119	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ∈ ℂ )
134	8 132 133	fsummulc2	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
135	134	eqcomd	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) = ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
136	131 135	breqtrd	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
137	26 28 43 44 136	letrd	⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
138	23 137	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )