Theorem knoppndvlem15

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 6-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem15.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndvlem15.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndvlem15.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppndvlem15.a	⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
5		knoppndvlem15.b	⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) )
6		knoppndvlem15.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
7		knoppndvlem15.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
8		knoppndvlem15.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9		knoppndvlem15.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10		knoppndvlem15.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
11	6	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
12	11	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
13	12	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
14	13	abscld	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
15	14 7	reexpcld	⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ∈ ℝ )
16		2re	⊢ 2 ∈ ℝ
17	16	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
18		2ne0	⊢ 2 ≠ 0
19	18	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
20	15 17 19	redivcld	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ )
21		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
22	9	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
23	17 22	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
24	23 14	remulcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
25	24 21	resubcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ )
26		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
27		0lt1	⊢ 0 < 1
28	27	a1i	⊢ ( 𝜑 → 0 < 1 )
29	6 9 10	knoppndvlem12	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 ∧ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
30	29	simprd	⊢ ( 𝜑 → 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
31	26 21 25 28 30	lttrd	⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
32	25 31	jca	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
33		gt0ne0	⊢ ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
34	32 33	syl	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
35	21 25 34	redivcld	⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
36	21 35	resubcld	⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
37	20 36	remulcld	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
38	4	a1i	⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
39	7	nn0zd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
40	9 39 8	knoppndvlem1	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )
41	38 40	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
42	1 2 9 12 41 7	knoppcnlem3	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ∈ ℝ )
43	42	recnd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ∈ ℂ )
44	5	a1i	⊢ ( 𝜑 → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) )
45	8	peano2zd	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
46	9 39 45	knoppndvlem1	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) ∈ ℝ )
47	44 46	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
48	1 2 9 12 47 7	knoppcnlem3	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ∈ ℝ )
49	48	recnd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ∈ ℂ )
50	43 49	subcld	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ∈ ℂ )
51	50	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ∈ ℝ )
52	1 2 47 12 9	knoppndvlem5	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
53	52	recnd	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
54	1 2 41 12 9	knoppndvlem5	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
55	54	recnd	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
56	53 55	subcld	⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ∈ ℂ )
57	56	abscld	⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℝ )
58	51 57	resubcld	⊢ ( 𝜑 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) ∈ ℝ )
59	50 56	subcld	⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℂ )
60	59	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) ∈ ℝ )
61	20 35	jca	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ ) )
62		remulcl	⊢ ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ ) → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
63	61 62	syl	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
64	20 63	jca	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ ) )
65		resubcl	⊢ ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ ) → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
66	64 65	syl	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
67	20	recnd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℂ )
68		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
69	35	recnd	⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℂ )
70	67 68 69	subdid	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
71	67	mulridd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
72	71	oveq1d	⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
73	66	leidd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
74	72 73	eqbrtrd	⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
75	70 74	eqbrtrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
76	20 35	remulcld	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
77	20	leidd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ≤ ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
78	43 49	abssubd	⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) )
79	1 2 4 5 6 7 8 9	knoppndvlem10	⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
80	78 79	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
81	80	eqcomd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
82	77 81	breqtrd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ≤ ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
83	1 2 4 5 6 7 8 9 10	knoppndvlem14	⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
84	20 57 51 76 82 83	le2subd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
85	37 66 58 75 84	letrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
86	50 56	abs2difd	⊢ ( 𝜑 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) ≤ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
87	37 58 60 85 86	letrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
88	50 56	abssubd	⊢ ( 𝜑 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) = ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) )
89	87 88	breqtrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) )
90	1 2 3 5 6 7 45 9	knoppndvlem6	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) )
91		elnn0uz	⊢ ( 𝐽 ∈ ℕ0 ↔ 𝐽 ∈ ( ℤ≥ ‘ 0 ) )
92	7 91	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 0 ) )
93	9	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝑁 ∈ ℕ )
94	12	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ ℝ )
95	47	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐵 ∈ ℝ )
96		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝐽 ) → 𝑖 ∈ ℕ0 )
97	96	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝑖 ∈ ℕ0 )
98	1 2 93 94 95 97	knoppcnlem3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
99	98	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
100		fveq2	⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) )
101	92 99 100	fsumm1	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) )
102	90 101	eqtrd	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) )
103	1 2 3 4 6 7 8 9	knoppndvlem6	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
104	41	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐴 ∈ ℝ )
105	1 2 93 94 104 97	knoppcnlem3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
106	105	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
107		fveq2	⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) )
108	92 106 107	fsumm1	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) )
109	103 108	eqtrd	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) )
110	102 109	oveq12d	⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) )
111	53 55 43 49	subadd4d	⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) )
112	111	eqcomd	⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
113	110 112	eqtrd	⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
114	113	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) = ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) )
115	114	eqcomd	⊢ ( 𝜑 → ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) = ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) )
116	89 115	breqtrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) )