Metamath Proof Explorer

Theorem knoppcnlem5

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

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

Proof

Step Hyp Ref Expression
1 knoppcnlem5.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem5.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem5.n ⊢ φ → N ∈ ℕ
4 knoppcnlem5.1 ⊢ φ → C ∈ ℝ
5 3 ad2antrr ⊢ φ ∧ m ∈ ℕ 0 ∧ z ∈ ℝ → N ∈ ℕ
6 4 ad2antrr ⊢ φ ∧ m ∈ ℕ 0 ∧ z ∈ ℝ → C ∈ ℝ
7 simpr ⊢ φ ∧ m ∈ ℕ 0 ∧ z ∈ ℝ → z ∈ ℝ
8 simplr ⊢ φ ∧ m ∈ ℕ 0 ∧ z ∈ ℝ → m ∈ ℕ 0
9 1 2 5 6 7 8 knoppcnlem3 ⊢ φ ∧ m ∈ ℕ 0 ∧ z ∈ ℝ → F ⁡ z ⁡ m ∈ ℝ
10 9 recnd ⊢ φ ∧ m ∈ ℕ 0 ∧ z ∈ ℝ → F ⁡ z ⁡ m ∈ ℂ
11 10 fmpttd ⊢ φ ∧ m ∈ ℕ 0 → z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℝ ⟶ ℂ
12 cnex ⊢ ℂ ∈ V
13 reex ⊢ ℝ ∈ V
14 12 13 pm3.2i ⊢ ℂ ∈ V ∧ ℝ ∈ V
15 elmapg ⊢ ℂ ∈ V ∧ ℝ ∈ V → z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ ℂ ℝ ↔ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℝ ⟶ ℂ
16 14 15 ax-mp ⊢ z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ ℂ ℝ ↔ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℝ ⟶ ℂ
17 11 16 sylibr ⊢ φ ∧ m ∈ ℕ 0 → z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ ℂ ℝ
18 17 fmpttd ⊢ φ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ