knoppndvlem10

	Ref	Expression
Hypotheses	knoppndvlem10.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppndvlem10.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppndvlem10.a	$⊢ A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
	knoppndvlem10.b	$⊢ B = (\frac{{2 \cdot N}^{- J}}{2}) (M + 1)$
	knoppndvlem10.c	$⊢ φ \to C \in (- 1, 1)$
	knoppndvlem10.j	$⊢ φ \to J \in ℕ_{0}$
	knoppndvlem10.m	$⊢ φ \to M \in ℤ$
	knoppndvlem10.n	$⊢ φ \to N \in ℕ$
Assertion	knoppndvlem10	$⊢ φ \to \|F (B) (J) - F (A) (J)\| = \frac{{\|C\|}^{J}}{2}$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem10.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppndvlem10.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppndvlem10.a	$⊢ A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
4		knoppndvlem10.b	$⊢ B = (\frac{{2 \cdot N}^{- J}}{2}) (M + 1)$
5		knoppndvlem10.c	$⊢ φ \to C \in (- 1, 1)$
6		knoppndvlem10.j	$⊢ φ \to J \in ℕ_{0}$
7		knoppndvlem10.m	$⊢ φ \to M \in ℤ$
8		knoppndvlem10.n	$⊢ φ \to N \in ℕ$
9	5	adantr	$⊢ (φ \land 2 ∥ M) \to C \in (- 1, 1)$
10	6	adantr	$⊢ (φ \land 2 ∥ M) \to J \in ℕ_{0}$
11	7	peano2zd	$⊢ φ \to M + 1 \in ℤ$
12	11	adantr	$⊢ (φ \land 2 ∥ M) \to M + 1 \in ℤ$
13	8	adantr	$⊢ (φ \land 2 ∥ M) \to N \in ℕ$
14		notnot	$⊢ 2 ∥ M \to \neg \neg 2 ∥ M$
15	14	adantl	$⊢ (φ \land 2 ∥ M) \to \neg \neg 2 ∥ M$
16	7	adantr	$⊢ (φ \land 2 ∥ M) \to M \in ℤ$
17		oddp1even	$⊢ M \in ℤ \to (\neg 2 ∥ M \leftrightarrow 2 ∥ (M + 1))$
18	16 17	syl	$⊢ (φ \land 2 ∥ M) \to (\neg 2 ∥ M \leftrightarrow 2 ∥ (M + 1))$
19	15 18	mtbid	$⊢ (φ \land 2 ∥ M) \to \neg 2 ∥ (M + 1)$
20	1 2 4 9 10 12 13 19	knoppndvlem9	$⊢ (φ \land 2 ∥ M) \to F (B) (J) = \frac{C^{J}}{2}$
21	15	notnotrd	$⊢ (φ \land 2 ∥ M) \to 2 ∥ M$
22	1 2 3 9 10 16 13 21	knoppndvlem8	$⊢ (φ \land 2 ∥ M) \to F (A) (J) = 0$
23	20 22	oveq12d	$⊢ (φ \land 2 ∥ M) \to F (B) (J) - F (A) (J) = (\frac{C^{J}}{2}) - 0$
24	5	knoppndvlem3	$⊢ φ \to (C \in ℝ \land \|C\| < 1)$
25	24	simpld	$⊢ φ \to C \in ℝ$
26	25	recnd	$⊢ φ \to C \in ℂ$
27	26 6	expcld	$⊢ φ \to C^{J} \in ℂ$
28		2cnd	$⊢ φ \to 2 \in ℂ$
29		2ne0	$⊢ 2 \neq 0$
30	29	a1i	$⊢ φ \to 2 \neq 0$
31	27 28 30	divcld	$⊢ φ \to \frac{C^{J}}{2} \in ℂ$
32	31	subid1d	$⊢ φ \to (\frac{C^{J}}{2}) - 0 = \frac{C^{J}}{2}$
33	32	adantr	$⊢ (φ \land 2 ∥ M) \to (\frac{C^{J}}{2}) - 0 = \frac{C^{J}}{2}$
34	23 33	eqtrd	$⊢ (φ \land 2 ∥ M) \to F (B) (J) - F (A) (J) = \frac{C^{J}}{2}$
35	34	fveq2d	$⊢ (φ \land 2 ∥ M) \to \|F (B) (J) - F (A) (J)\| = \|\frac{C^{J}}{2}\|$
36	4	a1i	$⊢ φ \to B = (\frac{{2 \cdot N}^{- J}}{2}) (M + 1)$
37	6	nn0zd	$⊢ φ \to J \in ℤ$
38	8 37 11	knoppndvlem1	$⊢ φ \to (\frac{{2 \cdot N}^{- J}}{2}) (M + 1) \in ℝ$
39	36 38	eqeltrd	$⊢ φ \to B \in ℝ$
40	1 2 8 25 39 6	knoppcnlem3	$⊢ φ \to F (B) (J) \in ℝ$
41	40	recnd	$⊢ φ \to F (B) (J) \in ℂ$
42	3	a1i	$⊢ φ \to A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
43	8 37 7	knoppndvlem1	$⊢ φ \to (\frac{{2 \cdot N}^{- J}}{2}) \cdot M \in ℝ$
44	42 43	eqeltrd	$⊢ φ \to A \in ℝ$
45	1 2 8 25 44 6	knoppcnlem3	$⊢ φ \to F (A) (J) \in ℝ$
46	45	recnd	$⊢ φ \to F (A) (J) \in ℂ$
47	41 46	abssubd	$⊢ φ \to \|F (B) (J) - F (A) (J)\| = \|F (A) (J) - F (B) (J)\|$
48	47	adantr	$⊢ (φ \land \neg 2 ∥ M) \to \|F (B) (J) - F (A) (J)\| = \|F (A) (J) - F (B) (J)\|$
49	5	adantr	$⊢ (φ \land \neg 2 ∥ M) \to C \in (- 1, 1)$
50	6	adantr	$⊢ (φ \land \neg 2 ∥ M) \to J \in ℕ_{0}$
51	7	adantr	$⊢ (φ \land \neg 2 ∥ M) \to M \in ℤ$
52	8	adantr	$⊢ (φ \land \neg 2 ∥ M) \to N \in ℕ$
53		simpr	$⊢ (φ \land \neg 2 ∥ M) \to \neg 2 ∥ M$
54	1 2 3 49 50 51 52 53	knoppndvlem9	$⊢ (φ \land \neg 2 ∥ M) \to F (A) (J) = \frac{C^{J}}{2}$
55	11	adantr	$⊢ (φ \land \neg 2 ∥ M) \to M + 1 \in ℤ$
56	51 17	syl	$⊢ (φ \land \neg 2 ∥ M) \to (\neg 2 ∥ M \leftrightarrow 2 ∥ (M + 1))$
57	53 56	mpbid	$⊢ (φ \land \neg 2 ∥ M) \to 2 ∥ (M + 1)$
58	1 2 4 49 50 55 52 57	knoppndvlem8	$⊢ (φ \land \neg 2 ∥ M) \to F (B) (J) = 0$
59	54 58	oveq12d	$⊢ (φ \land \neg 2 ∥ M) \to F (A) (J) - F (B) (J) = (\frac{C^{J}}{2}) - 0$
60	32	adantr	$⊢ (φ \land \neg 2 ∥ M) \to (\frac{C^{J}}{2}) - 0 = \frac{C^{J}}{2}$
61	59 60	eqtrd	$⊢ (φ \land \neg 2 ∥ M) \to F (A) (J) - F (B) (J) = \frac{C^{J}}{2}$
62	61	fveq2d	$⊢ (φ \land \neg 2 ∥ M) \to \|F (A) (J) - F (B) (J)\| = \|\frac{C^{J}}{2}\|$
63	48 62	eqtrd	$⊢ (φ \land \neg 2 ∥ M) \to \|F (B) (J) - F (A) (J)\| = \|\frac{C^{J}}{2}\|$
64	35 63	pm2.61dan	$⊢ φ \to \|F (B) (J) - F (A) (J)\| = \|\frac{C^{J}}{2}\|$
65	27 28 30	absdivd	$⊢ φ \to \|\frac{C^{J}}{2}\| = \frac{\|C^{J}\|}{\|2\|}$
66	26 6	absexpd	$⊢ φ \to \|C^{J}\| = {\|C\|}^{J}$
67		0le2	$⊢ 0 \leq 2$
68		2re	$⊢ 2 \in ℝ$
69	68	absidi	$⊢ 0 \leq 2 \to \|2\| = 2$
70	67 69	ax-mp	$⊢ \|2\| = 2$
71	70	a1i	$⊢ φ \to \|2\| = 2$
72	66 71	oveq12d	$⊢ φ \to \frac{\|C^{J}\|}{\|2\|} = \frac{{\|C\|}^{J}}{2}$
73	65 72	eqtrd	$⊢ φ \to \|\frac{C^{J}}{2}\| = \frac{{\|C\|}^{J}}{2}$
74	64 73	eqtrd	$⊢ φ \to \|F (B) (J) - F (A) (J)\| = \frac{{\|C\|}^{J}}{2}$

Metamath Proof Explorer

Theorem knoppndvlem10

Proof