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

Metamath Proof Explorer

Theorem axltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 ax-pre-ltadd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A  ( C + A )
2 ltxrlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A
3 2 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> A
4 readdcl 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C + A ) e. RR )
5 readdcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + B ) e. RR )
6 ltxrlt 
 |-  ( ( ( C + A ) e. RR /\ ( C + B ) e. RR ) -> ( ( C + A ) < ( C + B ) <-> ( C + A )
7 4 5 6 syl2an 
 |-  ( ( ( C e. RR /\ A e. RR ) /\ ( C e. RR /\ B e. RR ) ) -> ( ( C + A ) < ( C + B ) <-> ( C + A )
8 7 3impdi 
 |-  ( ( C e. RR /\ A e. RR /\ B e. RR ) -> ( ( C + A ) < ( C + B ) <-> ( C + A )
9 8 3coml 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) < ( C + B ) <-> ( C + A )
10 1 3 9 3imtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( C + A ) < ( C + B ) ) )