This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 · 𝑛 ) + 𝐵 ) / ( 𝐴 · 𝑛 ) ) )
clim1fr1.2 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
clim1fr1.3 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
clim1fr1.4 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion clim1fr1 ( 𝜑 → 𝐹 ⇝ 1 )

Proof

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