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 ⟼ A n ⇝ 0

Proof

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