Metamath Proof Explorer

Theorem leaddsub

Description: 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005)

Ref Expression
Assertion leaddsub ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+B≤C↔A≤C−B

Proof

Step Hyp Ref Expression
1 ltsubadd ⊢C∈ℝ∧B∈ℝ∧A∈ℝ→C−B<A↔C<A+B
2 1 3com13 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C−B<A↔C<A+B
3 resubcl ⊢C∈ℝ∧B∈ℝ→C−B∈ℝ
4 ltnle ⊢C−B∈ℝ∧A∈ℝ→C−B<A↔¬A≤C−B
5 3 4 stoic3 ⊢C∈ℝ∧B∈ℝ∧A∈ℝ→C−B<A↔¬A≤C−B
6 5 3com13 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C−B<A↔¬A≤C−B
7 readdcl ⊢A∈ℝ∧B∈ℝ→A+B∈ℝ
8 ltnle ⊢C∈ℝ∧A+B∈ℝ→C<A+B↔¬A+B≤C
9 7 8 sylan2 ⊢C∈ℝ∧A∈ℝ∧B∈ℝ→C<A+B↔¬A+B≤C
10 9 3impb ⊢C∈ℝ∧A∈ℝ∧B∈ℝ→C<A+B↔¬A+B≤C
11 10 3coml ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C<A+B↔¬A+B≤C
12 2 6 11 3bitr3rd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→¬A+B≤C↔¬A≤C−B
13 12 con4bid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+B≤C↔A≤C−B