Metamath Proof Explorer

Theorem xleadd2a

Description: Commuted form of xleadd1a . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xleadd2a 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( C +e A ) <_ ( C +e B ) )

Proof

Step Hyp Ref Expression
1 xleadd1a 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) <_ ( B +e C ) )
2 xaddcom 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A +e C ) = ( C +e A ) )
3 2 3adant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A +e C ) = ( C +e A ) )
4 3 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) = ( C +e A ) )
5 xaddcom 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B +e C ) = ( C +e B ) )
6 5 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B +e C ) = ( C +e B ) )
7 6 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B +e C ) = ( C +e B ) )
8 1 4 7 3brtr3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( C +e A ) <_ ( C +e B ) )