Theorem difrp

Description: Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014)

	Ref	Expression
Assertion	difrp	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) )

Proof

Step	Hyp	Ref	Expression
1		posdif	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
2		resubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
3	2	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
4		elrp	⊢ ( ( 𝐵 − 𝐴 ) ∈ ℝ+ ↔ ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ 0 < ( 𝐵 − 𝐴 ) ) )
5	4	baib	⊢ ( ( 𝐵 − 𝐴 ) ∈ ℝ → ( ( 𝐵 − 𝐴 ) ∈ ℝ+ ↔ 0 < ( 𝐵 − 𝐴 ) ) )
6	3 5	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 − 𝐴 ) ∈ ℝ+ ↔ 0 < ( 𝐵 − 𝐴 ) ) )
7	1 6	bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) )