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

Metamath Proof Explorer

Theorem xle2add

Description: Extended real version of le2add . (Contributed by Mario Carneiro, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> A e. RR* )
2 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> C e. RR* )
3 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> B e. RR* )
4 xleadd1a 
 |-  ( ( ( A e. RR* /\ C e. RR* /\ B e. RR* ) /\ A <_ C ) -> ( A +e B ) <_ ( C +e B ) )
5 4 ex 
 |-  ( ( A e. RR* /\ C e. RR* /\ B e. RR* ) -> ( A <_ C -> ( A +e B ) <_ ( C +e B ) ) )
6 1 2 3 5 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( A <_ C -> ( A +e B ) <_ ( C +e B ) ) )
7 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> D e. RR* )
8 xleadd2a 
 |-  ( ( ( B e. RR* /\ D e. RR* /\ C e. RR* ) /\ B <_ D ) -> ( C +e B ) <_ ( C +e D ) )
9 8 ex 
 |-  ( ( B e. RR* /\ D e. RR* /\ C e. RR* ) -> ( B <_ D -> ( C +e B ) <_ ( C +e D ) ) )
10 3 7 2 9 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( B <_ D -> ( C +e B ) <_ ( C +e D ) ) )
11 xaddcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )
12 11 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( A +e B ) e. RR* )
13 xaddcl 
 |-  ( ( C e. RR* /\ B e. RR* ) -> ( C +e B ) e. RR* )
14 2 3 13 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( C +e B ) e. RR* )
15 xaddcl 
 |-  ( ( C e. RR* /\ D e. RR* ) -> ( C +e D ) e. RR* )
16 15 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( C +e D ) e. RR* )
17 xrletr 
 |-  ( ( ( A +e B ) e. RR* /\ ( C +e B ) e. RR* /\ ( C +e D ) e. RR* ) -> ( ( ( A +e B ) <_ ( C +e B ) /\ ( C +e B ) <_ ( C +e D ) ) -> ( A +e B ) <_ ( C +e D ) ) )
18 12 14 16 17 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( ( A +e B ) <_ ( C +e B ) /\ ( C +e B ) <_ ( C +e D ) ) -> ( A +e B ) <_ ( C +e D ) ) )
19 6 10 18 syl2and 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A <_ C /\ B <_ D ) -> ( A +e B ) <_ ( C +e D ) ) )