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

Metamath Proof Explorer

Axiom ax-pre-lttri

Detailed syntax breakdown