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 ⊢A∈ℂ∧M∈ℕ→n∈ℤ≥M⟼An⇝0

Proof

Step Hyp Ref Expression
1 eluznn ⊢M∈ℕ∧n∈ℤ≥M→n∈ℕ
2 eqidd ⊢n∈ℕ→m∈ℕ⟼Am=m∈ℕ⟼Am
3 oveq2 ⊢m=n→Am=An
4 3 adantl ⊢n∈ℕ∧m=n→Am=An
5 id ⊢n∈ℕ→n∈ℕ
6 ovexd ⊢n∈ℕ→An∈V
7 2 4 5 6 fvmptd ⊢n∈ℕ→m∈ℕ⟼Am⁡n=An
8 7 eqcomd ⊢n∈ℕ→An=m∈ℕ⟼Am⁡n
9 1 8 syl ⊢M∈ℕ∧n∈ℤ≥M→An=m∈ℕ⟼Am⁡n
10 9 adantll ⊢A∈ℂ∧M∈ℕ∧n∈ℤ≥M→An=m∈ℕ⟼Am⁡n
11 10 mpteq2dva ⊢A∈ℂ∧M∈ℕ→n∈ℤ≥M⟼An=n∈ℤ≥M⟼m∈ℕ⟼Am⁡n
12 divcnv ⊢A∈ℂ→m∈ℕ⟼Am⇝0
13 12 adantr ⊢A∈ℂ∧M∈ℕ→m∈ℕ⟼Am⇝0
14 simpr ⊢A∈ℂ∧M∈ℕ→M∈ℕ
15 14 nnzd ⊢A∈ℂ∧M∈ℕ→M∈ℤ
16 nnex ⊢ℕ∈V
17 16 mptex ⊢m∈ℕ⟼Am∈V
18 eqid ⊢ℤ≥M=ℤ≥M
19 eqid ⊢n∈ℤ≥M⟼m∈ℕ⟼Am⁡n=n∈ℤ≥M⟼m∈ℕ⟼Am⁡n
20 18 19 climmpt ⊢M∈ℤ∧m∈ℕ⟼Am∈V→m∈ℕ⟼Am⇝0↔n∈ℤ≥M⟼m∈ℕ⟼Am⁡n⇝0
21 15 17 20 sylancl ⊢A∈ℂ∧M∈ℕ→m∈ℕ⟼Am⇝0↔n∈ℤ≥M⟼m∈ℕ⟼Am⁡n⇝0
22 13 21 mpbid ⊢A∈ℂ∧M∈ℕ→n∈ℤ≥M⟼m∈ℕ⟼Am⁡n⇝0
23 11 22 eqbrtrd ⊢A∈ℂ∧M∈ℕ→n∈ℤ≥M⟼An⇝0