Theorem xleadd1

Description: Weakened version of xleadd1a under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		rexr	|- ( C e. RR -> C e. RR* )
2		xleadd1a	|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) <_ ( B +e C ) )
3	2	ex	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ B -> ( A +e C ) <_ ( B +e C ) ) )
4	1 3	syl3an3	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A <_ B -> ( A +e C ) <_ ( B +e C ) ) )
5		simp1	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> A e. RR* )
6	1	3ad2ant3	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> C e. RR* )
7		xaddcl	|- ( ( A e. RR* /\ C e. RR* ) -> ( A +e C ) e. RR* )
8	5 6 7	syl2anc	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A +e C ) e. RR* )
9		simp2	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> B e. RR* )
10		xaddcl	|- ( ( B e. RR* /\ C e. RR* ) -> ( B +e C ) e. RR* )
11	9 6 10	syl2anc	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( B +e C ) e. RR* )
12		xnegcl	|- ( C e. RR* -> -e C e. RR* )
13	6 12	syl	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> -e C e. RR* )
14		xleadd1a	|- ( ( ( ( A +e C ) e. RR* /\ ( B +e C ) e. RR* /\ -e C e. RR* ) /\ ( A +e C ) <_ ( B +e C ) ) -> ( ( A +e C ) +e -e C ) <_ ( ( B +e C ) +e -e C ) )
15	14	ex	|- ( ( ( A +e C ) e. RR* /\ ( B +e C ) e. RR* /\ -e C e. RR* ) -> ( ( A +e C ) <_ ( B +e C ) -> ( ( A +e C ) +e -e C ) <_ ( ( B +e C ) +e -e C ) ) )
16	8 11 13 15	syl3anc	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( ( A +e C ) <_ ( B +e C ) -> ( ( A +e C ) +e -e C ) <_ ( ( B +e C ) +e -e C ) ) )
17		xpncan	|- ( ( A e. RR* /\ C e. RR ) -> ( ( A +e C ) +e -e C ) = A )
18	17	3adant2	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( ( A +e C ) +e -e C ) = A )
19		xpncan	|- ( ( B e. RR* /\ C e. RR ) -> ( ( B +e C ) +e -e C ) = B )
20	19	3adant1	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( ( B +e C ) +e -e C ) = B )
21	18 20	breq12d	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( ( ( A +e C ) +e -e C ) <_ ( ( B +e C ) +e -e C ) <-> A <_ B ) )
22	16 21	sylibd	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( ( A +e C ) <_ ( B +e C ) -> A <_ B ) )
23	4 22	impbid	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A <_ B <-> ( A +e C ) <_ ( B +e C ) ) )