Description: Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by Theorem axpre-lttrn . Note: The more general version for extended reals is axlttrn . Normally new proofs would use lttr . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | ax-pre-lttrn | |- ( ( 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 | 3 5 8 | wbr | |- B |
11 | 9 10 | wa | |- ( A |
12 | 0 5 8 | wbr | |- A |
13 | 11 12 | wi | |- ( ( A |
14 | 7 13 | wi | |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A |