Metamath Proof Explorer

Theorem knoppcnlem6

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

Ref Expression
Hypotheses knoppcnlem6.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppcnlem6.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppcnlem6.n ⊢ φ → N ∈ ℕ
knoppcnlem6.1 ⊢ φ → C ∈ ℝ
knoppcnlem6.2 ⊢ φ → C < 1
Assertion knoppcnlem6 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ dom ⁡ ⇝u ⁡ ℝ

Proof

Step Hyp Ref Expression
1 knoppcnlem6.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem6.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem6.n ⊢ φ → N ∈ ℕ
4 knoppcnlem6.1 ⊢ φ → C ∈ ℝ
5 knoppcnlem6.2 ⊢ φ → C < 1
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 0zd ⊢ φ → 0 ∈ ℤ
8 reex ⊢ ℝ ∈ V
9 8 a1i ⊢ φ → ℝ ∈ V
10 1 2 3 4 knoppcnlem5 ⊢ φ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ
11 nn0ex ⊢ ℕ 0 ∈ V
12 11 mptex ⊢ m ∈ ℕ 0 ⟼ C m ∈ V
13 12 a1i ⊢ φ → m ∈ ℕ 0 ⟼ C m ∈ V
14 eqid ⊢ m ∈ ℕ 0 ⟼ C m = m ∈ ℕ 0 ⟼ C m
15 14 a1i ⊢ φ ∧ k ∈ ℕ 0 → m ∈ ℕ 0 ⟼ C m = m ∈ ℕ 0 ⟼ C m
16 simpr ⊢ φ ∧ k ∈ ℕ 0 ∧ m = k → m = k
17 16 oveq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ m = k → C m = C k
18 simpr ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
19 ovexd ⊢ φ ∧ k ∈ ℕ 0 → C k ∈ V
20 15 17 18 19 fvmptd ⊢ φ ∧ k ∈ ℕ 0 → m ∈ ℕ 0 ⟼ C m ⁡ k = C k
21 4 recnd ⊢ φ → C ∈ ℂ
22 21 abscld ⊢ φ → C ∈ ℝ
23 22 adantr ⊢ φ ∧ k ∈ ℕ 0 → C ∈ ℝ
24 23 18 reexpcld ⊢ φ ∧ k ∈ ℕ 0 → C k ∈ ℝ
25 20 24 eqeltrd ⊢ φ ∧ k ∈ ℕ 0 → m ∈ ℕ 0 ⟼ C m ⁡ k ∈ ℝ
26 eqid ⊢ m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m
27 26 a1i ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m
28 simpr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ m = k → m = k
29 28 fveq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ m = k → F ⁡ z ⁡ m = F ⁡ z ⁡ k
30 29 mpteq2dv ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ m = k → z ∈ ℝ ⟼ F ⁡ z ⁡ m = z ∈ ℝ ⟼ F ⁡ z ⁡ k
31 18 adantrr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → k ∈ ℕ 0
32 8 mptex ⊢ z ∈ ℝ ⟼ F ⁡ z ⁡ k ∈ V
33 32 a1i ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → z ∈ ℝ ⟼ F ⁡ z ⁡ k ∈ V
34 27 30 31 33 fvmptd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = z ∈ ℝ ⟼ F ⁡ z ⁡ k
35 simpr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ z = w → z = w
36 35 fveq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ z = w → F ⁡ z = F ⁡ w
37 36 fveq1d ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ z = w → F ⁡ z ⁡ k = F ⁡ w ⁡ k
38 simprr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → w ∈ ℝ
39 fvexd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → F ⁡ w ⁡ k ∈ V
40 34 37 38 39 fvmptd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ w = F ⁡ w ⁡ k
41 40 fveq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ w = F ⁡ w ⁡ k
42 3 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → N ∈ ℕ
43 4 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → C ∈ ℝ
44 1 2 42 43 38 31 knoppcnlem4 ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → F ⁡ w ⁡ k ≤ m ∈ ℕ 0 ⟼ C m ⁡ k
45 41 44 eqbrtrd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ w ≤ m ∈ ℕ 0 ⟼ C m ⁡ k
46 22 recnd ⊢ φ → C ∈ ℂ
47 absidm ⊢ C ∈ ℂ → C = C
48 21 47 syl ⊢ φ → C = C
49 48 5 eqbrtrd ⊢ φ → C < 1
50 46 49 20 geolim ⊢ φ → seq 0 + m ∈ ℕ 0 ⟼ C m ⇝ 1 1 − C
51 seqex ⊢ seq 0 + m ∈ ℕ 0 ⟼ C m ∈ V
52 ovex ⊢ 1 1 − C ∈ V
53 51 52 breldm ⊢ seq 0 + m ∈ ℕ 0 ⟼ C m ⇝ 1 1 − C → seq 0 + m ∈ ℕ 0 ⟼ C m ∈ dom ⁡ ⇝
54 50 53 syl ⊢ φ → seq 0 + m ∈ ℕ 0 ⟼ C m ∈ dom ⁡ ⇝
55 6 7 9 10 13 25 45 54 mtest ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ dom ⁡ ⇝u ⁡ ℝ