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

Metamath Proof Explorer

Theorem rexsub

Description: Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion rexsub 
|- ( ( A e. RR /\ B e. RR ) -> ( A +e -e B ) = ( A - B ) )

Proof

Step Hyp Ref Expression
1 rexneg 
 |-  ( B e. RR -> -e B = -u B )
2 1 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> -e B = -u B )
3 2 oveq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e -e B ) = ( A +e -u B ) )
4 renegcl 
 |-  ( B e. RR -> -u B e. RR )
5 rexadd 
 |-  ( ( A e. RR /\ -u B e. RR ) -> ( A +e -u B ) = ( A + -u B ) )
6 4 5 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e -u B ) = ( A + -u B ) )
7 recn 
 |-  ( A e. RR -> A e. CC )
8 recn 
 |-  ( B e. RR -> B e. CC )
9 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
10 7 8 9 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) = ( A - B ) )
11 3 6 10 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e -e B ) = ( A - B ) )