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 |