Metamath Proof Explorer

Theorem ltsub13

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004)

Ref Expression
Assertion ltsub13 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B−C↔C<B−A

Proof

Step Hyp Ref Expression
1 ltaddsub ⊢A∈ℝ∧C∈ℝ∧B∈ℝ→A+C<B↔A<B−C
2 ltaddsub2 ⊢A∈ℝ∧C∈ℝ∧B∈ℝ→A+C<B↔C<B−A
3 1 2 bitr3d ⊢A∈ℝ∧C∈ℝ∧B∈ℝ→A<B−C↔C<B−A
4 3 3com23 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B−C↔C<B−A