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

Metamath Proof Explorer

Theorem ltaddsublt

Description: Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018)

Ref Expression
Assertion ltaddsublt ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( ( 𝐴 + 𝐵 ) − 𝐶 ) < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ltadd2 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( 𝐴 + 𝐵 ) < ( 𝐴 + 𝐶 ) ) )
2 1 3comr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( 𝐴 + 𝐵 ) < ( 𝐴 + 𝐶 ) ) )
3 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
4 3 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
5 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
6 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
7 4 5 6 ltsubaddd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) − 𝐶 ) < 𝐴 ↔ ( 𝐴 + 𝐵 ) < ( 𝐴 + 𝐶 ) ) )
8 2 7 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( ( 𝐴 + 𝐵 ) − 𝐶 ) < 𝐴 ) )