MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-pre-ltadd Structured version   Visualization version   Unicode version
Axiom ax-pre-ltadd 10012
Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd 9988. Normally new proofs would use axltadd 10111. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
ax-pre-ltadd |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
Detailed syntax breakdown of Axiom ax-pre-ltadd
StepHypRef Expression
1 cA . . . 4 class A
2 cr 9935 . . . 4 class RR
31, 2wcel 1990 . . 3 wff A e. RR
4 cB . . . 4 class B
54, 2wcel 1990 . . 3 wff B e. RR
6 cC . . . 4 class C
76, 2wcel 1990 . . 3 wff C e. RR
83, 5, 7w3a 1037 . 2 wff ( A e. RR /\ B e. RR /\ C e. RR )
9 cltrr 9940 . . . 4 class <RR
101, 4, 9wbr 4653 . . 3 wff A <RR B
11 caddc 9939 . . . . 5 class +
126, 1, 11co 6650 . . . 4 class ( C + A )
136, 4, 11co 6650 . . . 4 class ( C + B )
1412, 13, 9wbr 4653 . . 3 wff ( C + A ) <RR ( C + B )
1510, 14wi 4 . 2 wff ( A <RR B -> ( C + A ) <RR ( C + B ) )
168, 15wi 4 1 wff ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
Colors of variables: wff setvar class
This axiom is referenced by:  axltadd  10111
  Copyright terms: Public domain W3C validator