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 B C A < B C + A < C + B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class
2 0 1 wcel wff A
3 cB class B
4 3 1 wcel wff B
5 cC class C
6 5 1 wcel wff C
7 2 4 6 w3a wff A B C
8 cltrr class <
9 0 3 8 wbr wff A < B
10 caddc class +
11 5 0 10 co class C + A
12 5 3 10 co class C + B
13 11 12 8 wbr wff C + A < C + B
14 9 13 wi wff A < B C + A < C + B
15 7 14 wi wff A B C A < B C + A < C + B