Metamath Proof Explorer


Axiom ax-pre-ltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by Theorem axpre-ltadd . Normally new proofs would use axltadd . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-ltadd
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A  ( C + A ) 

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cr
 |-  RR
2 0 1 wcel
 |-  A e. RR
3 cB
 |-  B
4 3 1 wcel
 |-  B e. RR
5 cC
 |-  C
6 5 1 wcel
 |-  C e. RR
7 2 4 6 w3a
 |-  ( A e. RR /\ B e. RR /\ C e. RR )
8 cltrr
 |-  
9 0 3 8 wbr
 |-  A 
10 caddc
 |-  +
11 5 0 10 co
 |-  ( C + A )
12 5 3 10 co
 |-  ( C + B )
13 11 12 8 wbr
 |-  ( C + A ) 
14 9 13 wi
 |-  ( A  ( C + A ) 
15 7 14 wi
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A  ( C + A )