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 )