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 )