Theorem xreqnltd

Description: A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	xreqnltd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xreqnltd.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	xreqnltd	⊢ ( 𝜑 → ¬ 𝐴 < 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		xreqnltd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xreqnltd.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	2 1	eqeltrrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
4		xrlttri3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ) )
5	1 3 4	syl2anc	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ) )
6	2 5	mpbid	⊢ ( 𝜑 → ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
7	6	simpld	⊢ ( 𝜑 → ¬ 𝐴 < 𝐵 )