Theorem reposdif

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

	Ref	Expression
Assertion	reposdif	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow 0<B{-}_{ℝ}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		reltsub1	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\in ℝ\right)\to \left(A<B\leftrightarrow A{-}_{ℝ}A<B{-}_{ℝ}A\right)$$
2	1	3anidm13	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow A{-}_{ℝ}A<B{-}_{ℝ}A\right)$$
3		resubid	$$⊢A\in ℝ\to A{-}_{ℝ}A=0$$
4	3	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{-}_{ℝ}A=0$$
5	4	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{-}_{ℝ}A<B{-}_{ℝ}A\leftrightarrow 0<B{-}_{ℝ}A\right)$$
6	2 5	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow 0<B{-}_{ℝ}A\right)$$