Metamath Proof Explorer

Theorem ltsubadd

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℝ
2 simp2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B∈ℝ
3 1 2 resubcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B∈ℝ
4 simp3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈ℝ
5 ltadd1 ⊢A−B∈ℝ∧C∈ℝ∧B∈ℝ→A−B<C↔A-B+B<C+B
6 3 4 2 5 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B<C↔A-B+B<C+B
7 1 recnd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℂ
8 2 recnd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B∈ℂ
9 7 8 npcand ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A-B+B=A
10 9 breq1d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A-B+B<C+B↔A<C+B
11 6 10 bitrd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B<C↔A<C+B