This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < 𝐶 ↔ 𝐴 < ( 𝐶 − 𝐵 ) ) )