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 e. CC /\ M e. NN ) -> ( n e. ( ZZ>= ` M ) |-> ( A / n ) ) ~~> 0 )

Proof

Step Hyp Ref Expression
1 eluznn 
 |-  ( ( M e. NN /\ n e. ( ZZ>= ` M ) ) -> n e. NN )
2 eqidd 
 |-  ( n e. NN -> ( m e. NN |-> ( A / m ) ) = ( m e. NN |-> ( A / m ) ) )
3 oveq2 
 |-  ( m = n -> ( A / m ) = ( A / n ) )
4 3 adantl 
 |-  ( ( n e. NN /\ m = n ) -> ( A / m ) = ( A / n ) )
5 id 
 |-  ( n e. NN -> n e. NN )
6 ovexd 
 |-  ( n e. NN -> ( A / n ) e. _V )
7 2 4 5 6 fvmptd 
 |-  ( n e. NN -> ( ( m e. NN |-> ( A / m ) ) ` n ) = ( A / n ) )
8 7 eqcomd 
 |-  ( n e. NN -> ( A / n ) = ( ( m e. NN |-> ( A / m ) ) ` n ) )
9 1 8 syl 
 |-  ( ( M e. NN /\ n e. ( ZZ>= ` M ) ) -> ( A / n ) = ( ( m e. NN |-> ( A / m ) ) ` n ) )
10 9 adantll 
 |-  ( ( ( A e. CC /\ M e. NN ) /\ n e. ( ZZ>= ` M ) ) -> ( A / n ) = ( ( m e. NN |-> ( A / m ) ) ` n ) )
11 10 mpteq2dva 
 |-  ( ( A e. CC /\ M e. NN ) -> ( n e. ( ZZ>= ` M ) |-> ( A / n ) ) = ( n e. ( ZZ>= ` M ) |-> ( ( m e. NN |-> ( A / m ) ) ` n ) ) )
12 divcnv 
 |-  ( A e. CC -> ( m e. NN |-> ( A / m ) ) ~~> 0 )
13 12 adantr 
 |-  ( ( A e. CC /\ M e. NN ) -> ( m e. NN |-> ( A / m ) ) ~~> 0 )
14 simpr 
 |-  ( ( A e. CC /\ M e. NN ) -> M e. NN )
15 14 nnzd 
 |-  ( ( A e. CC /\ M e. NN ) -> M e. ZZ )
16 nnex 
 |-  NN e. _V
17 16 mptex 
 |-  ( m e. NN |-> ( A / m ) ) e. _V
18 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
19 eqid 
 |-  ( n e. ( ZZ>= ` M ) |-> ( ( m e. NN |-> ( A / m ) ) ` n ) ) = ( n e. ( ZZ>= ` M ) |-> ( ( m e. NN |-> ( A / m ) ) ` n ) )
20 18 19 climmpt 
 |-  ( ( M e. ZZ /\ ( m e. NN |-> ( A / m ) ) e. _V ) -> ( ( m e. NN |-> ( A / m ) ) ~~> 0 <-> ( n e. ( ZZ>= ` M ) |-> ( ( m e. NN |-> ( A / m ) ) ` n ) ) ~~> 0 ) )
21 15 17 20 sylancl 
 |-  ( ( A e. CC /\ M e. NN ) -> ( ( m e. NN |-> ( A / m ) ) ~~> 0 <-> ( n e. ( ZZ>= ` M ) |-> ( ( m e. NN |-> ( A / m ) ) ` n ) ) ~~> 0 ) )
22 13 21 mpbid 
 |-  ( ( A e. CC /\ M e. NN ) -> ( n e. ( ZZ>= ` M ) |-> ( ( m e. NN |-> ( A / m ) ) ` n ) ) ~~> 0 )
23 11 22 eqbrtrd 
 |-  ( ( A e. CC /\ M e. NN ) -> ( n e. ( ZZ>= ` M ) |-> ( A / n ) ) ~~> 0 )