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

Metamath Proof Explorer

Theorem sublimc

Description: Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sublimc.f 
|- F = ( x e. A |-> B )
sublimc.2 
|- G = ( x e. A |-> C )
sublimc.3 
|- H = ( x e. A |-> ( B - C ) )
sublimc.4 
|- ( ( ph /\ x e. A ) -> B e. CC )
sublimc.5 
|- ( ( ph /\ x e. A ) -> C e. CC )
sublimc.6 
|- ( ph -> E e. ( F limCC D ) )
sublimc.7 
|- ( ph -> I e. ( G limCC D ) )
Assertion sublimc 
|- ( ph -> ( E - I ) e. ( H limCC D ) )

Proof

Step Hyp Ref Expression
1 sublimc.f 
 |-  F = ( x e. A |-> B )
2 sublimc.2 
 |-  G = ( x e. A |-> C )
3 sublimc.3 
 |-  H = ( x e. A |-> ( B - C ) )
4 sublimc.4 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 sublimc.5 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
6 sublimc.6 
 |-  ( ph -> E e. ( F limCC D ) )
7 sublimc.7 
 |-  ( ph -> I e. ( G limCC D ) )
8 eqid 
 |-  ( x e. A |-> -u C ) = ( x e. A |-> -u C )
9 eqid 
 |-  ( x e. A |-> ( B + -u C ) ) = ( x e. A |-> ( B + -u C ) )
10 5 negcld 
 |-  ( ( ph /\ x e. A ) -> -u C e. CC )
11 2 8 5 7 neglimc 
 |-  ( ph -> -u I e. ( ( x e. A |-> -u C ) limCC D ) )
12 1 8 9 4 10 6 11 addlimc 
 |-  ( ph -> ( E + -u I ) e. ( ( x e. A |-> ( B + -u C ) ) limCC D ) )
13 limccl 
 |-  ( F limCC D ) C_ CC
14 13 6 sselid 
 |-  ( ph -> E e. CC )
15 limccl 
 |-  ( G limCC D ) C_ CC
16 15 7 sselid 
 |-  ( ph -> I e. CC )
17 14 16 negsubd 
 |-  ( ph -> ( E + -u I ) = ( E - I ) )
18 17 eqcomd 
 |-  ( ph -> ( E - I ) = ( E + -u I ) )
19 4 5 negsubd 
 |-  ( ( ph /\ x e. A ) -> ( B + -u C ) = ( B - C ) )
20 19 eqcomd 
 |-  ( ( ph /\ x e. A ) -> ( B - C ) = ( B + -u C ) )
21 20 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( B - C ) ) = ( x e. A |-> ( B + -u C ) ) )
22 3 21 eqtrid 
 |-  ( ph -> H = ( x e. A |-> ( B + -u C ) ) )
23 22 oveq1d 
 |-  ( ph -> ( H limCC D ) = ( ( x e. A |-> ( B + -u C ) ) limCC D ) )
24 12 18 23 3eltr4d 
 |-  ( ph -> ( E - I ) e. ( H limCC D ) )