This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimneg

Description: Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses rlimneg.1 
|- ( ( ph /\ k e. A ) -> B e. V )
rlimneg.2 
|- ( ph -> ( k e. A |-> B ) ~~>r C )
Assertion rlimneg 
|- ( ph -> ( k e. A |-> -u B ) ~~>r -u C )

Proof

Step Hyp Ref Expression
1 rlimneg.1 
 |-  ( ( ph /\ k e. A ) -> B e. V )
2 rlimneg.2 
 |-  ( ph -> ( k e. A |-> B ) ~~>r C )
3 0cnd 
 |-  ( ( ph /\ k e. A ) -> 0 e. CC )
4 1 2 rlimmptrcl 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 1 ralrimiva 
 |-  ( ph -> A. k e. A B e. V )
6 dmmptg 
 |-  ( A. k e. A B e. V -> dom ( k e. A |-> B ) = A )
7 5 6 syl 
 |-  ( ph -> dom ( k e. A |-> B ) = A )
8 rlimss 
 |-  ( ( k e. A |-> B ) ~~>r C -> dom ( k e. A |-> B ) C_ RR )
9 2 8 syl 
 |-  ( ph -> dom ( k e. A |-> B ) C_ RR )
10 7 9 eqsstrrd 
 |-  ( ph -> A C_ RR )
11 0cn 
 |-  0 e. CC
12 rlimconst 
 |-  ( ( A C_ RR /\ 0 e. CC ) -> ( k e. A |-> 0 ) ~~>r 0 )
13 10 11 12 sylancl 
 |-  ( ph -> ( k e. A |-> 0 ) ~~>r 0 )
14 3 4 13 2 rlimsub 
 |-  ( ph -> ( k e. A |-> ( 0 - B ) ) ~~>r ( 0 - C ) )
15 df-neg 
 |-  -u B = ( 0 - B )
16 15 mpteq2i 
 |-  ( k e. A |-> -u B ) = ( k e. A |-> ( 0 - B ) )
17 df-neg 
 |-  -u C = ( 0 - C )
18 14 16 17 3brtr4g 
 |-  ( ph -> ( k e. A |-> -u B ) ~~>r -u C )