Metamath Proof Explorer


Theorem sublt0d

Description: When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sublt0d.1 ( 𝜑𝐴 ∈ ℝ )
sublt0d.2 ( 𝜑𝐵 ∈ ℝ )
Assertion sublt0d ( 𝜑 → ( ( 𝐴𝐵 ) < 0 ↔ 𝐴 < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sublt0d.1 ( 𝜑𝐴 ∈ ℝ )
2 sublt0d.2 ( 𝜑𝐵 ∈ ℝ )
3 0red ( 𝜑 → 0 ∈ ℝ )
4 1 2 3 ltsubaddd ( 𝜑 → ( ( 𝐴𝐵 ) < 0 ↔ 𝐴 < ( 0 + 𝐵 ) ) )
5 2 recnd ( 𝜑𝐵 ∈ ℂ )
6 5 addid2d ( 𝜑 → ( 0 + 𝐵 ) = 𝐵 )
7 6 breq2d ( 𝜑 → ( 𝐴 < ( 0 + 𝐵 ) ↔ 𝐴 < 𝐵 ) )
8 4 7 bitrd ( 𝜑 → ( ( 𝐴𝐵 ) < 0 ↔ 𝐴 < 𝐵 ) )