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

Metamath Proof Explorer

Theorem divcnvg

Description: The sequence of reciprocals of positive integers, multiplied by the factor A , converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion divcnvg ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐴 / 𝑛 ) ) ⇝ 0 )

Proof

Step Hyp Ref Expression
1 eluznn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ℕ )
2 eqidd ⊢ ( 𝑛 ∈ ℕ → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) )
3 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐴 / 𝑚 ) = ( 𝐴 / 𝑛 ) )
4 3 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 = 𝑛 ) → ( 𝐴 / 𝑚 ) = ( 𝐴 / 𝑛 ) )
5 id ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
6 ovexd ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 / 𝑛 ) ∈ V )
7 2 4 5 6 fvmptd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) = ( 𝐴 / 𝑛 ) )
8 7 eqcomd ⊢ ( 𝑛 ∈ ℕ → ( 𝐴 / 𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) )
9 1 8 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 / 𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) )
10 9 adantll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 / 𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) )
11 10 mpteq2dva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐴 / 𝑛 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) ) )
12 divcnv ⊢ ( 𝐴 ∈ ℂ → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
13 12 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
14 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
15 14 nnzd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℤ )
16 nnex ⊢ ℕ ∈ V
17 16 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ∈ V
18 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
19 eqid ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) )
20 18 19 climmpt ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ∈ V ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) ) ⇝ 0 ) )
21 15 17 20 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) ) ⇝ 0 ) )
22 13 21 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ‘ 𝑛 ) ) ⇝ 0 )
23 11 22 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐴 / 𝑛 ) ) ⇝ 0 )