Metamath Proof Explorer


Theorem ltaddsub

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

Ref Expression
Assertion ltaddsub ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < 𝐶𝐴 < ( 𝐶𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lesubadd ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐶𝐵 ) ≤ 𝐴𝐶 ≤ ( 𝐴 + 𝐵 ) ) )
2 1 3com13 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶𝐵 ) ≤ 𝐴𝐶 ≤ ( 𝐴 + 𝐵 ) ) )
3 resubcl ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶𝐵 ) ∈ ℝ )
4 lenlt ( ( ( 𝐶𝐵 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐶𝐵 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 𝐶𝐵 ) ) )
5 3 4 stoic3 ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐶𝐵 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 𝐶𝐵 ) ) )
6 5 3com13 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶𝐵 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 𝐶𝐵 ) ) )
7 readdcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
8 lenlt ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 + 𝐵 ) ∈ ℝ ) → ( 𝐶 ≤ ( 𝐴 + 𝐵 ) ↔ ¬ ( 𝐴 + 𝐵 ) < 𝐶 ) )
9 7 8 sylan2 ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( 𝐶 ≤ ( 𝐴 + 𝐵 ) ↔ ¬ ( 𝐴 + 𝐵 ) < 𝐶 ) )
10 9 3impb ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ≤ ( 𝐴 + 𝐵 ) ↔ ¬ ( 𝐴 + 𝐵 ) < 𝐶 ) )
11 10 3coml ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ≤ ( 𝐴 + 𝐵 ) ↔ ¬ ( 𝐴 + 𝐵 ) < 𝐶 ) )
12 2 6 11 3bitr3rd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( 𝐴 + 𝐵 ) < 𝐶 ↔ ¬ 𝐴 < ( 𝐶𝐵 ) ) )
13 12 con4bid ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < 𝐶𝐴 < ( 𝐶𝐵 ) ) )