Theorem reposdif

Description: Comparison of two numbers whose difference is positive. Compare posdif . (Contributed by SN, 13-Feb-2024)

	Ref	Expression
Assertion	reposdif	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 −ℝ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reltsub1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 −ℝ 𝐴 ) < ( 𝐵 −ℝ 𝐴 ) ) )
2	1	3anidm13	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 −ℝ 𝐴 ) < ( 𝐵 −ℝ 𝐴 ) ) )
3		resubid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 −ℝ 𝐴 ) = 0 )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐴 ) = 0 )
5	4	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐴 ) < ( 𝐵 −ℝ 𝐴 ) ↔ 0 < ( 𝐵 −ℝ 𝐴 ) ) )
6	2 5	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 −ℝ 𝐴 ) ) )