Metamath Proof Explorer


Axiom ax-pre-lttri

Description: Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by Theorem axpre-lttri . Note: The more general version for extended reals is axlttri . Normally new proofs would use xrlttri . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-lttri
|- ( ( A e. RR /\ B e. RR ) -> ( A  -. ( A = B \/ B 

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 2 4 wa
 |-  ( A e. RR /\ B e. RR )
6 cltrr
 |-  
7 0 3 6 wbr
 |-  A 
8 0 3 wceq
 |-  A = B
9 3 0 6 wbr
 |-  B 
10 8 9 wo
 |-  ( A = B \/ B 
11 10 wn
 |-  -. ( A = B \/ B 
12 7 11 wb
 |-  ( A  -. ( A = B \/ B 
13 5 12 wi
 |-  ( ( A e. RR /\ B e. RR ) -> ( A  -. ( A = B \/ B