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

Metamath Proof Explorer

Theorem reltsubadd2

Description: 'Less than' relationship between addition and subtraction. Compare ltsubadd2 . (Contributed by SN, 13-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
2 readdcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
3 2 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
4 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
5 reltsub1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < ( 𝐵 + 𝐶 ) ↔ ( 𝐴 −ℝ 𝐵 ) < ( ( 𝐵 + 𝐶 ) −ℝ 𝐵 ) ) )
6 1 3 4 5 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < ( 𝐵 + 𝐶 ) ↔ ( 𝐴 −ℝ 𝐵 ) < ( ( 𝐵 + 𝐶 ) −ℝ 𝐵 ) ) )
7 repncan2 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) −ℝ 𝐵 ) = 𝐶 )
8 7 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) −ℝ 𝐵 ) = 𝐶 )
9 8 breq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) < ( ( 𝐵 + 𝐶 ) −ℝ 𝐵 ) ↔ ( 𝐴 −ℝ 𝐵 ) < 𝐶 ) )
10 6 9 bitr2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) < 𝐶 ↔ 𝐴 < ( 𝐵 + 𝐶 ) ) )