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 |
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 |
15 | 7 14 | wi | |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A |