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 ) ) )