This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reposdif

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

Ref Expression
Assertion reposdif ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ 0 < B - ℝ A

Proof

Step Hyp Ref Expression
1 reltsub1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → A < B ↔ A - ℝ A < B - ℝ A
2 1 3anidm13 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A - ℝ A < B - ℝ A
3 resubid ⊢ A ∈ ℝ → A - ℝ A = 0
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ A = 0
5 4 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ A < B - ℝ A ↔ 0 < B - ℝ A
6 2 5 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ 0 < B - ℝ A