Metamath Proof Explorer

Theorem divrcnv

Description: The sequence of reciprocals of real numbers, multiplied by the factor A , converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion divrcnv 
|- ( A e. CC -> ( n e. RR+ |-> ( A / n ) ) ~~>r 0 )

Proof

Step Hyp Ref Expression
1 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
2 rerpdivcl 
 |-  ( ( ( abs ` A ) e. RR /\ x e. RR+ ) -> ( ( abs ` A ) / x ) e. RR )
3 1 2 sylan 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( ( abs ` A ) / x ) e. RR )
4 simpll 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> A e. CC )
5 rpcn 
 |-  ( n e. RR+ -> n e. CC )
6 5 ad2antrl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> n e. CC )
7 rpne0 
 |-  ( n e. RR+ -> n =/= 0 )
8 7 ad2antrl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> n =/= 0 )
9 4 6 8 absdivd 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( abs ` ( A / n ) ) = ( ( abs ` A ) / ( abs ` n ) ) )
10 rpre 
 |-  ( n e. RR+ -> n e. RR )
11 10 ad2antrl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> n e. RR )
12 rpge0 
 |-  ( n e. RR+ -> 0 <_ n )
13 12 ad2antrl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> 0 <_ n )
14 11 13 absidd 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( abs ` n ) = n )
15 14 oveq2d 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( ( abs ` A ) / ( abs ` n ) ) = ( ( abs ` A ) / n ) )
16 9 15 eqtrd 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( abs ` ( A / n ) ) = ( ( abs ` A ) / n ) )
17 simprr 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( ( abs ` A ) / x ) < n )
18 4 abscld 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( abs ` A ) e. RR )
19 rpre 
 |-  ( x e. RR+ -> x e. RR )
20 19 ad2antlr 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> x e. RR )
21 rpgt0 
 |-  ( x e. RR+ -> 0 < x )
22 21 ad2antlr 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> 0 < x )
23 rpgt0 
 |-  ( n e. RR+ -> 0 < n )
24 23 ad2antrl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> 0 < n )
25 ltdiv23 
 |-  ( ( ( abs ` A ) e. RR /\ ( x e. RR /\ 0 < x ) /\ ( n e. RR /\ 0 < n ) ) -> ( ( ( abs ` A ) / x ) < n <-> ( ( abs ` A ) / n ) < x ) )
26 18 20 22 11 24 25 syl122anc 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( ( ( abs ` A ) / x ) < n <-> ( ( abs ` A ) / n ) < x ) )
27 17 26 mpbid 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( ( abs ` A ) / n ) < x )
28 16 27 eqbrtrd 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ ( n e. RR+ /\ ( ( abs ` A ) / x ) < n ) ) -> ( abs ` ( A / n ) ) < x )
29 28 expr 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ n e. RR+ ) -> ( ( ( abs ` A ) / x ) < n -> ( abs ` ( A / n ) ) < x ) )
30 29 ralrimiva 
 |-  ( ( A e. CC /\ x e. RR+ ) -> A. n e. RR+ ( ( ( abs ` A ) / x ) < n -> ( abs ` ( A / n ) ) < x ) )
31 breq1 
 |-  ( y = ( ( abs ` A ) / x ) -> ( y < n <-> ( ( abs ` A ) / x ) < n ) )
32 31 rspceaimv 
 |-  ( ( ( ( abs ` A ) / x ) e. RR /\ A. n e. RR+ ( ( ( abs ` A ) / x ) < n -> ( abs ` ( A / n ) ) < x ) ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( A / n ) ) < x ) )
33 3 30 32 syl2anc 
 |-  ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( A / n ) ) < x ) )
34 33 ralrimiva 
 |-  ( A e. CC -> A. x e. RR+ E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( A / n ) ) < x ) )
35 simpl 
 |-  ( ( A e. CC /\ n e. RR+ ) -> A e. CC )
36 5 adantl 
 |-  ( ( A e. CC /\ n e. RR+ ) -> n e. CC )
37 7 adantl 
 |-  ( ( A e. CC /\ n e. RR+ ) -> n =/= 0 )
38 35 36 37 divcld 
 |-  ( ( A e. CC /\ n e. RR+ ) -> ( A / n ) e. CC )
39 38 ralrimiva 
 |-  ( A e. CC -> A. n e. RR+ ( A / n ) e. CC )
40 rpssre 
 |-  RR+ C_ RR
41 40 a1i 
 |-  ( A e. CC -> RR+ C_ RR )
42 39 41 rlim0lt 
 |-  ( A e. CC -> ( ( n e. RR+ |-> ( A / n ) ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( A / n ) ) < x ) ) )
43 34 42 mpbird 
 |-  ( A e. CC -> ( n e. RR+ |-> ( A / n ) ) ~~>r 0 )