knoppcnlem10

	Ref	Expression
Hypotheses	knoppcnlem10.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppcnlem10.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppcnlem10.n	$⊢ φ \to N \in ℕ$
	knoppcnlem10.1	$⊢ φ \to C \in ℝ$
	knoppcnlem10.2	$⊢ φ \to M \in ℕ_{0}$
Assertion	knoppcnlem10	$⊢ φ \to (z \in ℝ ⟼ F (z) (M)) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem10.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppcnlem10.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppcnlem10.n	$⊢ φ \to N \in ℕ$
4		knoppcnlem10.1	$⊢ φ \to C \in ℝ$
5		knoppcnlem10.2	$⊢ φ \to M \in ℕ_{0}$
6		simpr	$⊢ (φ \land z \in ℝ) \to z \in ℝ$
7	5	adantr	$⊢ (φ \land z \in ℝ) \to M \in ℕ_{0}$
8	2 6 7	knoppcnlem1	$⊢ (φ \land z \in ℝ) \to F (z) (M) = C^{M} T ({2 \cdot N}^{M} z)$
9	8	mpteq2dva	$⊢ φ \to (z \in ℝ ⟼ F (z) (M)) = (z \in ℝ ⟼ C^{M} T ({2 \cdot N}^{M} z))$
10		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
11	10	a1i	$⊢ φ \to topGen (ran (.)) \in TopOn (ℝ)$
12		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
13	12	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
14	13	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
15	4	recnd	$⊢ φ \to C \in ℂ$
16	15 5	expcld	$⊢ φ \to C^{M} \in ℂ$
17	11 14 16	cnmptc	$⊢ φ \to (z \in ℝ ⟼ C^{M}) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
18		2re	$⊢ 2 \in ℝ$
19	18	a1i	$⊢ φ \to 2 \in ℝ$
20		nnre	$⊢ N \in ℕ \to N \in ℝ$
21	3 20	syl	$⊢ φ \to N \in ℝ$
22	19 21	remulcld	$⊢ φ \to 2 \cdot N \in ℝ$
23	22 5	reexpcld	$⊢ φ \to {2 \cdot N}^{M} \in ℝ$
24	23	recnd	$⊢ φ \to {2 \cdot N}^{M} \in ℂ$
25	11 14 24	cnmptc	$⊢ φ \to (z \in ℝ ⟼ {2 \cdot N}^{M}) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
26	12	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
27	26	oveq2i	$⊢ topGen (ran (.)) Cn topGen (ran (.)) = topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
28	13	topontopi	$⊢ TopOpen (ℂ_{fld}) \in Top$
29		cnrest2r	$⊢ TopOpen (ℂ_{fld}) \in Top \to topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \subseteq topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
30	28 29	ax-mp	$⊢ topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \subseteq topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
31	27 30	eqsstri	$⊢ topGen (ran (.)) Cn topGen (ran (.)) \subseteq topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
32	11	cnmptid	$⊢ φ \to (z \in ℝ ⟼ z) \in (topGen (ran (.)) Cn topGen (ran (.)))$
33	31 32	sselid	$⊢ φ \to (z \in ℝ ⟼ z) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
34	12	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
35	34	a1i	$⊢ φ \to \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
36	11 25 33 35	cnmpt12f	$⊢ φ \to (z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
37	23	adantr	$⊢ (φ \land z \in ℝ) \to {2 \cdot N}^{M} \in ℝ$
38	37 6	remulcld	$⊢ (φ \land z \in ℝ) \to {2 \cdot N}^{M} z \in ℝ$
39	38	fmpttd	$⊢ φ \to (z \in ℝ ⟼ {2 \cdot N}^{M} z) : ℝ ⟶ ℝ$
40	39	frnd	$⊢ φ \to ran (z \in ℝ ⟼ {2 \cdot N}^{M} z) \subseteq ℝ$
41		ax-resscn	$⊢ ℝ \subseteq ℂ$
42	41	a1i	$⊢ φ \to ℝ \subseteq ℂ$
43	14 40 42	3jca	$⊢ φ \to (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (z \in ℝ ⟼ {2 \cdot N}^{M} z) \subseteq ℝ \land ℝ \subseteq ℂ)$
44		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (z \in ℝ ⟼ {2 \cdot N}^{M} z) \subseteq ℝ \land ℝ \subseteq ℂ) \to ((z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld})) \leftrightarrow (z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
45	43 44	syl	$⊢ φ \to ((z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld})) \leftrightarrow (z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
46	36 45	mpbid	$⊢ φ \to (z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
47	46 27	eleqtrrdi	$⊢ φ \to (z \in ℝ ⟼ {2 \cdot N}^{M} z) \in (topGen (ran (.)) Cn topGen (ran (.)))$
48		ssid	$⊢ ℂ \subseteq ℂ$
49	41 48	pm3.2i	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ)$
50		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
51	49 50	ax-mp	$⊢ ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
52	1	dnicn	$⊢ T : ℝ \underset{cn}{⟶} ℝ$
53	52	a1i	$⊢ φ \to T : ℝ \underset{cn}{⟶} ℝ$
54	51 53	sselid	$⊢ φ \to T : ℝ \underset{cn}{⟶} ℂ$
55	13	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
56	12 26 55	cncfcn	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℂ = topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
57	49 56	ax-mp	$⊢ ℝ \underset{cn}{⟶} ℂ = topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
58	54 57	eleqtrdi	$⊢ φ \to T \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
59	11 47 58	cnmpt11f	$⊢ φ \to (z \in ℝ ⟼ T ({2 \cdot N}^{M} z)) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
60	11 17 59 35	cnmpt12f	$⊢ φ \to (z \in ℝ ⟼ C^{M} T ({2 \cdot N}^{M} z)) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
61	9 60	eqeltrd	$⊢ φ \to (z \in ℝ ⟼ F (z) (M)) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$

Metamath Proof Explorer

Theorem knoppcnlem10

Proof