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

Metamath Proof Explorer

Theorem ltadd12dd

Description: Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ltadd12dd.a ⊢ φ → A ∈ ℝ
ltadd12dd.b ⊢ φ → B ∈ ℝ
ltadd12dd.c ⊢ φ → C ∈ ℝ
ltadd12dd.d ⊢ φ → D ∈ ℝ
ltadd12dd.ac ⊢ φ → A < C
ltadd12dd.bd ⊢ φ → B < D
Assertion ltadd12dd ⊢ φ → A + B < C + D

Proof

Step Hyp Ref Expression
1 ltadd12dd.a ⊢ φ → A ∈ ℝ
2 ltadd12dd.b ⊢ φ → B ∈ ℝ
3 ltadd12dd.c ⊢ φ → C ∈ ℝ
4 ltadd12dd.d ⊢ φ → D ∈ ℝ
5 ltadd12dd.ac ⊢ φ → A < C
6 ltadd12dd.bd ⊢ φ → B < D
7 1 2 readdcld ⊢ φ → A + B ∈ ℝ
8 3 2 readdcld ⊢ φ → C + B ∈ ℝ
9 3 4 readdcld ⊢ φ → C + D ∈ ℝ
10 1 3 2 5 ltadd1dd ⊢ φ → A + B < C + B
11 2 4 3 6 ltadd2dd ⊢ φ → C + B < C + D
12 7 8 9 10 11 lttrd ⊢ φ → A + B < C + D