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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵𝐵 < 𝐴 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cr
2 0 1 wcel 𝐴 ∈ ℝ
3 cB 𝐵
4 3 1 wcel 𝐵 ∈ ℝ
5 2 4 wa ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ )
6 cltrr <
7 0 3 6 wbr 𝐴 < 𝐵
8 0 3 wceq 𝐴 = 𝐵
9 3 0 6 wbr 𝐵 < 𝐴
10 8 9 wo ( 𝐴 = 𝐵𝐵 < 𝐴 )
11 10 wn ¬ ( 𝐴 = 𝐵𝐵 < 𝐴 )
12 7 11 wb ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵𝐵 < 𝐴 ) )
13 5 12 wi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵𝐵 < 𝐴 ) ) )