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=x∈ℝ⟼x+12−x
knoppndvlem4.f ⊢F=y∈ℝ⟼n∈ℕ0⟼Cn⁢T⁡2⋅ Nn⁢y
knoppndvlem4.w ⊢W=w∈ℝ⟼∑i∈ℕ0F⁡w⁡i
knoppndvlem4.a ⊢φ→A∈ℝ
knoppndvlem4.c ⊢φ→C∈−11
knoppndvlem4.n ⊢φ→N∈ℕ
Assertion knoppndvlem4 ⊢φ→seq0+F⁡A⇝W⁡A

Proof

Step Hyp Ref Expression
1 knoppndvlem4.t ⊢T=x∈ℝ⟼x+12−x
2 knoppndvlem4.f ⊢F=y∈ℝ⟼n∈ℕ0⟼Cn⁢T⁡2⋅ Nn⁢y
3 knoppndvlem4.w ⊢W=w∈ℝ⟼∑i∈ℕ0F⁡w⁡i
4 knoppndvlem4.a ⊢φ→A∈ℝ
5 knoppndvlem4.c ⊢φ→C∈−11
6 knoppndvlem4.n ⊢φ→N∈ℕ
7 nn0uz ⊢ℕ0=ℤ≥0
8 0zd ⊢φ→0∈ℤ
9 5 knoppndvlem3 ⊢φ→C∈ℝ∧C<1
10 9 simpld ⊢φ→C∈ℝ
11 1 2 6 10 knoppcnlem8 ⊢φ→seq0∘f⁡+m∈ℕ0⟼z∈ℝ⟼F⁡z⁡m:ℕ0⟶ℂℝ
12 seqex ⊢seq0+F⁡A∈V
13 12 a1i ⊢φ→seq0+F⁡A∈V
14 6 adantr ⊢φ∧k∈ℕ0→N∈ℕ
15 10 adantr ⊢φ∧k∈ℕ0→C∈ℝ
16 simpr ⊢φ∧k∈ℕ0→k∈ℕ0
17 1 2 14 15 16 knoppcnlem7 ⊢φ∧k∈ℕ0→seq0∘f⁡+m∈ℕ0⟼z∈ℝ⟼F⁡z⁡m⁡k=v∈ℝ⟼seq0+F⁡v⁡k
18 17 fveq1d ⊢φ∧k∈ℕ0→seq0∘f⁡+m∈ℕ0⟼z∈ℝ⟼F⁡z⁡m⁡k⁡A=v∈ℝ⟼seq0+F⁡v⁡k⁡A
19 eqid ⊢v∈ℝ⟼seq0+F⁡v⁡k=v∈ℝ⟼seq0+F⁡v⁡k
20 fveq2 ⊢v=A→F⁡v=F⁡A
21 20 seqeq3d ⊢v=A→seq0+F⁡v=seq0+F⁡A
22 21 fveq1d ⊢v=A→seq0+F⁡v⁡k=seq0+F⁡A⁡k
23 fvexd ⊢φ→seq0+F⁡A⁡k∈V
24 19 22 4 23 fvmptd3 ⊢φ→v∈ℝ⟼seq0+F⁡v⁡k⁡A=seq0+F⁡A⁡k
25 24 adantr ⊢φ∧k∈ℕ0→v∈ℝ⟼seq0+F⁡v⁡k⁡A=seq0+F⁡A⁡k
26 18 25 eqtrd ⊢φ∧k∈ℕ0→seq0∘f⁡+m∈ℕ0⟼z∈ℝ⟼F⁡z⁡m⁡k⁡A=seq0+F⁡A⁡k
27 9 simprd ⊢φ→C<1
28 1 2 3 6 10 27 knoppcnlem9 ⊢φ→seq0∘f⁡+m∈ℕ0⟼z∈ℝ⟼F⁡z⁡m⇝u⁡ℝW
29 7 8 11 4 13 26 28 ulmclm ⊢φ→seq0+F⁡A⇝W⁡A