Metamath Proof Explorer

Theorem knoppcnlem8

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem8.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppcnlem8.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppcnlem8.n ⊢ φ → N ∈ ℕ
knoppcnlem8.1 ⊢ φ → C ∈ ℝ
Assertion knoppcnlem8 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ

Proof

Step Hyp Ref Expression
1 knoppcnlem8.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem8.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem8.n ⊢ φ → N ∈ ℕ
4 knoppcnlem8.1 ⊢ φ → C ∈ ℝ
5 3 adantr ⊢ φ ∧ k ∈ ℕ 0 → N ∈ ℕ
6 4 adantr ⊢ φ ∧ k ∈ ℕ 0 → C ∈ ℝ
7 simpr ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
8 1 2 5 6 7 knoppcnlem7 ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k
9 simplr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → k ∈ ℕ 0
10 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
11 9 10 eleqtrdi ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → k ∈ ℤ ≥ 0
12 5 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ 0 … k → N ∈ ℕ
13 6 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ 0 … k → C ∈ ℝ
14 simplr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ 0 … k → w ∈ ℝ
15 elfznn0 ⊢ a ∈ 0 … k → a ∈ ℕ 0
16 15 adantl ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ 0 … k → a ∈ ℕ 0
17 1 2 12 13 14 16 knoppcnlem3 ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ 0 … k → F ⁡ w ⁡ a ∈ ℝ
18 17 recnd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ 0 … k → F ⁡ w ⁡ a ∈ ℂ
19 addcl ⊢ a ∈ ℂ ∧ b ∈ ℂ → a + b ∈ ℂ
20 19 adantl ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ a ∈ ℂ ∧ b ∈ ℂ → a + b ∈ ℂ
21 11 18 20 seqcl ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → seq 0 + F ⁡ w ⁡ k ∈ ℂ
22 21 fmpttd ⊢ φ ∧ k ∈ ℕ 0 → w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k : ℝ ⟶ ℂ
23 cnex ⊢ ℂ ∈ V
24 reex ⊢ ℝ ∈ V
25 23 24 pm3.2i ⊢ ℂ ∈ V ∧ ℝ ∈ V
26 elmapg ⊢ ℂ ∈ V ∧ ℝ ∈ V → w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k ∈ ℂ ℝ ↔ w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k : ℝ ⟶ ℂ
27 25 26 ax-mp ⊢ w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k ∈ ℂ ℝ ↔ w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k : ℝ ⟶ ℂ
28 22 27 sylibr ⊢ φ ∧ k ∈ ℕ 0 → w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k ∈ ℂ ℝ
29 8 28 eqeltrd ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ∈ ℂ ℝ
30 29 fmpttd ⊢ φ → k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k : ℕ 0 ⟶ ℂ ℝ
31 0z ⊢ 0 ∈ ℤ
32 seqfn ⊢ 0 ∈ ℤ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℤ ≥ 0
33 31 32 ax-mp ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℤ ≥ 0
34 10 fneq2i ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℕ 0 ↔ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℤ ≥ 0
35 33 34 mpbir ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℕ 0
36 dffn5 ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℕ 0 ↔ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k
37 35 36 mpbi ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k
38 37 feq1i ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ ↔ k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k : ℕ 0 ⟶ ℂ ℝ
39 30 38 sylibr ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ