knoppndvlem9

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem9.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppndvlem9.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppndvlem9.a	$⊢ A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
4		knoppndvlem9.c	$⊢ φ \to C \in (- 1, 1)$
5		knoppndvlem9.j	$⊢ φ \to J \in ℕ_{0}$
6		knoppndvlem9.m	$⊢ φ \to M \in ℤ$
7		knoppndvlem9.n	$⊢ φ \to N \in ℕ$
8		knoppndvlem9.1	$⊢ φ \to \neg 2 ∥ M$
9	1 2 3 5 6 7	knoppndvlem7	$⊢ φ \to F (A) (J) = C^{J} T (\frac{M}{2})$
10		odd2np1	$⊢ M \in ℤ \to (\neg 2 ∥ M \leftrightarrow \exists m \in ℤ 2 m + 1 = M)$
11	6 10	syl	$⊢ φ \to (\neg 2 ∥ M \leftrightarrow \exists m \in ℤ 2 m + 1 = M)$
12	8 11	mpbid	$⊢ φ \to \exists m \in ℤ 2 m + 1 = M$
13		eqcom	$⊢ 2 m + 1 = M \leftrightarrow M = 2 m + 1$
14	13	biimpi	$⊢ 2 m + 1 = M \to M = 2 m + 1$
15	14	oveq1d	$⊢ 2 m + 1 = M \to \frac{M}{2} = \frac{2 m + 1}{2}$
16	15	adantl	$⊢ (m \in ℤ \land 2 m + 1 = M) \to \frac{M}{2} = \frac{2 m + 1}{2}$
17	16	adantl	$⊢ (φ \land (m \in ℤ \land 2 m + 1 = M)) \to \frac{M}{2} = \frac{2 m + 1}{2}$
18		2cnd	$⊢ (φ \land m \in ℤ) \to 2 \in ℂ$
19		zcn	$⊢ m \in ℤ \to m \in ℂ$
20	19	adantl	$⊢ (φ \land m \in ℤ) \to m \in ℂ$
21	18 20	mulcld	$⊢ (φ \land m \in ℤ) \to 2 m \in ℂ$
22		1cnd	$⊢ (φ \land m \in ℤ) \to 1 \in ℂ$
23		2ne0	$⊢ 2 \neq 0$
24	23	a1i	$⊢ (φ \land m \in ℤ) \to 2 \neq 0$
25	21 22 18 24	divdird	$⊢ (φ \land m \in ℤ) \to \frac{2 m + 1}{2} = (\frac{2 m}{2}) + (\frac{1}{2})$
26	20 18 24	divcan3d	$⊢ (φ \land m \in ℤ) \to \frac{2 m}{2} = m$
27	26	oveq1d	$⊢ (φ \land m \in ℤ) \to (\frac{2 m}{2}) + (\frac{1}{2}) = m + (\frac{1}{2})$
28	25 27	eqtrd	$⊢ (φ \land m \in ℤ) \to \frac{2 m + 1}{2} = m + (\frac{1}{2})$
29	28	adantrr	$⊢ (φ \land (m \in ℤ \land 2 m + 1 = M)) \to \frac{2 m + 1}{2} = m + (\frac{1}{2})$
30	17 29	eqtrd	$⊢ (φ \land (m \in ℤ \land 2 m + 1 = M)) \to \frac{M}{2} = m + (\frac{1}{2})$
31	30	fveq2d	$⊢ (φ \land (m \in ℤ \land 2 m + 1 = M)) \to T (\frac{M}{2}) = T (m + (\frac{1}{2}))$
32		id	$⊢ m \in ℤ \to m \in ℤ$
33	1 32	dnizphlfeqhlf	$⊢ m \in ℤ \to T (m + (\frac{1}{2})) = \frac{1}{2}$
34	33	adantl	$⊢ (φ \land m \in ℤ) \to T (m + (\frac{1}{2})) = \frac{1}{2}$
35	34	adantrr	$⊢ (φ \land (m \in ℤ \land 2 m + 1 = M)) \to T (m + (\frac{1}{2})) = \frac{1}{2}$
36	31 35	eqtrd	$⊢ (φ \land (m \in ℤ \land 2 m + 1 = M)) \to T (\frac{M}{2}) = \frac{1}{2}$
37	12 36	rexlimddv	$⊢ φ \to T (\frac{M}{2}) = \frac{1}{2}$
38	37	oveq2d	$⊢ φ \to C^{J} T (\frac{M}{2}) = C^{J} (\frac{1}{2})$
39	4	knoppndvlem3	$⊢ φ \to (C \in ℝ \land \|C\| < 1)$
40	39	simpld	$⊢ φ \to C \in ℝ$
41	40	recnd	$⊢ φ \to C \in ℂ$
42	41 5	expcld	$⊢ φ \to C^{J} \in ℂ$
43		1cnd	$⊢ φ \to 1 \in ℂ$
44		2cnd	$⊢ φ \to 2 \in ℂ$
45	23	a1i	$⊢ φ \to 2 \neq 0$
46	42 43 44 45	div12d	$⊢ φ \to C^{J} (\frac{1}{2}) = 1 (\frac{C^{J}}{2})$
47	42 44 45	divcld	$⊢ φ \to \frac{C^{J}}{2} \in ℂ$
48	47	mulid2d	$⊢ φ \to 1 (\frac{C^{J}}{2}) = \frac{C^{J}}{2}$
49	46 48	eqtrd	$⊢ φ \to C^{J} (\frac{1}{2}) = \frac{C^{J}}{2}$
50	9 38 49	3eqtrd	$⊢ φ \to F (A) (J) = \frac{C^{J}}{2}$

Metamath Proof Explorer

Theorem knoppndvlem9

Proof