Metamath Proof Explorer

Theorem knoppndvlem4

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

Ref Expression
Hypotheses knoppndvlem4.t ${⊢}{T}=\left({x}\in ℝ⟼\left|⌊{x}+\left(\frac{1}{2}\right)⌋-{x}\right|\right)$
knoppndvlem4.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
knoppndvlem4.w ${⊢}{W}=\left({w}\in ℝ⟼\sum _{{i}\in {ℕ}_{0}}{F}\left({w}\right)\left({i}\right)\right)$
knoppndvlem4.a ${⊢}{\phi }\to {A}\in ℝ$
knoppndvlem4.c ${⊢}{\phi }\to {C}\in \left(-1,1\right)$
knoppndvlem4.n ${⊢}{\phi }\to {N}\in ℕ$
Assertion knoppndvlem4 ${⊢}{\phi }\to seq0\left(+,{F}\left({A}\right)\right)⇝{W}\left({A}\right)$

Proof

Step Hyp Ref Expression
1 knoppndvlem4.t ${⊢}{T}=\left({x}\in ℝ⟼\left|⌊{x}+\left(\frac{1}{2}\right)⌋-{x}\right|\right)$
2 knoppndvlem4.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
3 knoppndvlem4.w ${⊢}{W}=\left({w}\in ℝ⟼\sum _{{i}\in {ℕ}_{0}}{F}\left({w}\right)\left({i}\right)\right)$
4 knoppndvlem4.a ${⊢}{\phi }\to {A}\in ℝ$
5 knoppndvlem4.c ${⊢}{\phi }\to {C}\in \left(-1,1\right)$
6 knoppndvlem4.n ${⊢}{\phi }\to {N}\in ℕ$
7 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
8 0zd ${⊢}{\phi }\to 0\in ℤ$
9 5 knoppndvlem3 ${⊢}{\phi }\to \left({C}\in ℝ\wedge \left|{C}\right|<1\right)$
10 9 simpld ${⊢}{\phi }\to {C}\in ℝ$
11 1 2 6 10 knoppcnlem8 ${⊢}{\phi }\to seq0\left({\circ }_{f}+,\left({m}\in {ℕ}_{0}⟼\left({z}\in ℝ⟼{F}\left({z}\right)\left({m}\right)\right)\right)\right):{ℕ}_{0}⟶{ℂ}^{ℝ}$
12 seqex ${⊢}seq0\left(+,{F}\left({A}\right)\right)\in \mathrm{V}$
13 12 a1i ${⊢}{\phi }\to seq0\left(+,{F}\left({A}\right)\right)\in \mathrm{V}$
14 6 adantr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {N}\in ℕ$
15 10 adantr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {C}\in ℝ$
16 simpr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
17 1 2 14 15 16 knoppcnlem7 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to seq0\left({\circ }_{f}+,\left({m}\in {ℕ}_{0}⟼\left({z}\in ℝ⟼{F}\left({z}\right)\left({m}\right)\right)\right)\right)\left({k}\right)=\left({v}\in ℝ⟼seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)\right)$
18 17 fveq1d ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to seq0\left({\circ }_{f}+,\left({m}\in {ℕ}_{0}⟼\left({z}\in ℝ⟼{F}\left({z}\right)\left({m}\right)\right)\right)\right)\left({k}\right)\left({A}\right)=\left({v}\in ℝ⟼seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)\right)\left({A}\right)$
19 eqid ${⊢}\left({v}\in ℝ⟼seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)\right)=\left({v}\in ℝ⟼seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)\right)$
20 fveq2 ${⊢}{v}={A}\to {F}\left({v}\right)={F}\left({A}\right)$
21 20 seqeq3d ${⊢}{v}={A}\to seq0\left(+,{F}\left({v}\right)\right)=seq0\left(+,{F}\left({A}\right)\right)$
22 21 fveq1d ${⊢}{v}={A}\to seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)=seq0\left(+,{F}\left({A}\right)\right)\left({k}\right)$
23 fvexd ${⊢}{\phi }\to seq0\left(+,{F}\left({A}\right)\right)\left({k}\right)\in \mathrm{V}$
24 19 22 4 23 fvmptd3 ${⊢}{\phi }\to \left({v}\in ℝ⟼seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)\right)\left({A}\right)=seq0\left(+,{F}\left({A}\right)\right)\left({k}\right)$
25 24 adantr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \left({v}\in ℝ⟼seq0\left(+,{F}\left({v}\right)\right)\left({k}\right)\right)\left({A}\right)=seq0\left(+,{F}\left({A}\right)\right)\left({k}\right)$
26 18 25 eqtrd ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to seq0\left({\circ }_{f}+,\left({m}\in {ℕ}_{0}⟼\left({z}\in ℝ⟼{F}\left({z}\right)\left({m}\right)\right)\right)\right)\left({k}\right)\left({A}\right)=seq0\left(+,{F}\left({A}\right)\right)\left({k}\right)$
27 9 simprd ${⊢}{\phi }\to \left|{C}\right|<1$
28 1 2 3 6 10 27 knoppcnlem9
29 7 8 11 4 13 26 28 ulmclm ${⊢}{\phi }\to seq0\left(+,{F}\left({A}\right)\right)⇝{W}\left({A}\right)$