Metamath Proof Explorer

Theorem clim1fr1

Description: A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses clim1fr1.1 ⊢ F = n ∈ ℕ ⟼ A ⁢ n + B A ⁢ n
clim1fr1.2 ⊢ φ → A ∈ ℂ
clim1fr1.3 ⊢ φ → A ≠ 0
clim1fr1.4 ⊢ φ → B ∈ ℂ
Assertion clim1fr1 ⊢ φ → F ⇝ 1

Proof

Step Hyp Ref Expression
1 clim1fr1.1 ⊢ F = n ∈ ℕ ⟼ A ⁢ n + B A ⁢ n
2 clim1fr1.2 ⊢ φ → A ∈ ℂ
3 clim1fr1.3 ⊢ φ → A ≠ 0
4 clim1fr1.4 ⊢ φ → B ∈ ℂ
5 nnuz ⊢ ℕ = ℤ ≥ 1
6 1zzd ⊢ φ → 1 ∈ ℤ
7 nnex ⊢ ℕ ∈ V
8 7 mptex ⊢ n ∈ ℕ ⟼ 1 ∈ V
9 8 a1i ⊢ φ → n ∈ ℕ ⟼ 1 ∈ V
10 1cnd ⊢ φ → 1 ∈ ℂ
11 eqidd ⊢ k ∈ ℕ → n ∈ ℕ ⟼ 1 = n ∈ ℕ ⟼ 1
12 eqidd ⊢ k ∈ ℕ ∧ n = k → 1 = 1
13 id ⊢ k ∈ ℕ → k ∈ ℕ
14 1cnd ⊢ k ∈ ℕ → 1 ∈ ℂ
15 11 12 13 14 fvmptd ⊢ k ∈ ℕ → n ∈ ℕ ⟼ 1 ⁡ k = 1
16 15 adantl ⊢ φ ∧ k ∈ ℕ → n ∈ ℕ ⟼ 1 ⁡ k = 1
17 5 6 9 10 16 climconst ⊢ φ → n ∈ ℕ ⟼ 1 ⇝ 1
18 7 mptex ⊢ n ∈ ℕ ⟼ A ⁢ n + B A ⁢ n ∈ V
19 1 18 eqeltri ⊢ F ∈ V
20 19 a1i ⊢ φ → F ∈ V
21 4 adantr ⊢ φ ∧ n ∈ ℕ → B ∈ ℂ
22 2 adantr ⊢ φ ∧ n ∈ ℕ → A ∈ ℂ
23 nncn ⊢ n ∈ ℕ → n ∈ ℂ
24 23 adantl ⊢ φ ∧ n ∈ ℕ → n ∈ ℂ
25 3 adantr ⊢ φ ∧ n ∈ ℕ → A ≠ 0
26 nnne0 ⊢ n ∈ ℕ → n ≠ 0
27 26 adantl ⊢ φ ∧ n ∈ ℕ → n ≠ 0
28 21 22 24 25 27 divdiv1d ⊢ φ ∧ n ∈ ℕ → B A n = B A ⁢ n
29 28 mpteq2dva ⊢ φ → n ∈ ℕ ⟼ B A n = n ∈ ℕ ⟼ B A ⁢ n
30 4 2 3 divcld ⊢ φ → B A ∈ ℂ
31 divcnv ⊢ B A ∈ ℂ → n ∈ ℕ ⟼ B A n ⇝ 0
32 30 31 syl ⊢ φ → n ∈ ℕ ⟼ B A n ⇝ 0
33 29 32 eqbrtrrd ⊢ φ → n ∈ ℕ ⟼ B A ⁢ n ⇝ 0
34 eqid ⊢ n ∈ ℕ ⟼ 1 = n ∈ ℕ ⟼ 1
35 1cnd ⊢ n ∈ ℕ → 1 ∈ ℂ
36 34 35 fmpti ⊢ n ∈ ℕ ⟼ 1 : ℕ ⟶ ℂ
37 36 a1i ⊢ φ → n ∈ ℕ ⟼ 1 : ℕ ⟶ ℂ
38 37 ffvelrnda ⊢ φ ∧ k ∈ ℕ → n ∈ ℕ ⟼ 1 ⁡ k ∈ ℂ
39 22 24 mulcld ⊢ φ ∧ n ∈ ℕ → A ⁢ n ∈ ℂ
40 22 24 25 27 mulne0d ⊢ φ ∧ n ∈ ℕ → A ⁢ n ≠ 0
41 21 39 40 divcld ⊢ φ ∧ n ∈ ℕ → B A ⁢ n ∈ ℂ
42 41 fmpttd ⊢ φ → n ∈ ℕ ⟼ B A ⁢ n : ℕ ⟶ ℂ
43 42 ffvelrnda ⊢ φ ∧ k ∈ ℕ → n ∈ ℕ ⟼ B A ⁢ n ⁡ k ∈ ℂ
44 oveq2 ⊢ n = k → A ⁢ n = A ⁢ k
45 44 oveq1d ⊢ n = k → A ⁢ n + B = A ⁢ k + B
46 45 44 oveq12d ⊢ n = k → A ⁢ n + B A ⁢ n = A ⁢ k + B A ⁢ k
47 simpr ⊢ φ ∧ k ∈ ℕ → k ∈ ℕ
48 2 adantr ⊢ φ ∧ k ∈ ℕ → A ∈ ℂ
49 47 nncnd ⊢ φ ∧ k ∈ ℕ → k ∈ ℂ
50 48 49 mulcld ⊢ φ ∧ k ∈ ℕ → A ⁢ k ∈ ℂ
51 4 adantr ⊢ φ ∧ k ∈ ℕ → B ∈ ℂ
52 50 51 addcld ⊢ φ ∧ k ∈ ℕ → A ⁢ k + B ∈ ℂ
53 3 adantr ⊢ φ ∧ k ∈ ℕ → A ≠ 0
54 47 nnne0d ⊢ φ ∧ k ∈ ℕ → k ≠ 0
55 48 49 53 54 mulne0d ⊢ φ ∧ k ∈ ℕ → A ⁢ k ≠ 0
56 52 50 55 divcld ⊢ φ ∧ k ∈ ℕ → A ⁢ k + B A ⁢ k ∈ ℂ
57 1 46 47 56 fvmptd3 ⊢ φ ∧ k ∈ ℕ → F ⁡ k = A ⁢ k + B A ⁢ k
58 50 51 50 55 divdird ⊢ φ ∧ k ∈ ℕ → A ⁢ k + B A ⁢ k = A ⁢ k A ⁢ k + B A ⁢ k
59 50 55 dividd ⊢ φ ∧ k ∈ ℕ → A ⁢ k A ⁢ k = 1
60 59 oveq1d ⊢ φ ∧ k ∈ ℕ → A ⁢ k A ⁢ k + B A ⁢ k = 1 + B A ⁢ k
61 58 60 eqtrd ⊢ φ ∧ k ∈ ℕ → A ⁢ k + B A ⁢ k = 1 + B A ⁢ k
62 16 eqcomd ⊢ φ ∧ k ∈ ℕ → 1 = n ∈ ℕ ⟼ 1 ⁡ k
63 eqidd ⊢ φ ∧ k ∈ ℕ → n ∈ ℕ ⟼ B A ⁢ n = n ∈ ℕ ⟼ B A ⁢ n
64 simpr ⊢ φ ∧ k ∈ ℕ ∧ n = k → n = k
65 64 oveq2d ⊢ φ ∧ k ∈ ℕ ∧ n = k → A ⁢ n = A ⁢ k
66 65 oveq2d ⊢ φ ∧ k ∈ ℕ ∧ n = k → B A ⁢ n = B A ⁢ k
67 51 50 55 divcld ⊢ φ ∧ k ∈ ℕ → B A ⁢ k ∈ ℂ
68 63 66 47 67 fvmptd ⊢ φ ∧ k ∈ ℕ → n ∈ ℕ ⟼ B A ⁢ n ⁡ k = B A ⁢ k
69 68 eqcomd ⊢ φ ∧ k ∈ ℕ → B A ⁢ k = n ∈ ℕ ⟼ B A ⁢ n ⁡ k
70 62 69 oveq12d ⊢ φ ∧ k ∈ ℕ → 1 + B A ⁢ k = n ∈ ℕ ⟼ 1 ⁡ k + n ∈ ℕ ⟼ B A ⁢ n ⁡ k
71 57 61 70 3eqtrd ⊢ φ ∧ k ∈ ℕ → F ⁡ k = n ∈ ℕ ⟼ 1 ⁡ k + n ∈ ℕ ⟼ B A ⁢ n ⁡ k
72 5 6 17 20 33 38 43 71 climadd ⊢ φ → F ⇝ 1 + 0
73 1p0e1 ⊢ 1 + 0 = 1
74 72 73 breqtrdi ⊢ φ → F ⇝ 1