Metamath Proof Explorer

Theorem ltsubaddb

Description: Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020)

Ref Expression
Assertion ltsubaddb ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A − C < B − D ↔ A + D < B + C

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ∈ ℝ
2 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ∈ ℂ
3 simprl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℝ
4 3 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℂ
5 simprr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D ∈ ℝ
6 5 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D ∈ ℂ
7 2 4 6 addsubd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B + C - D = B - D + C
8 7 eqcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B - D + C = B + C - D
9 8 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < B - D + C ↔ A < B + C - D
10 simpll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ∈ ℝ
11 resubcl ⊢ B ∈ ℝ ∧ D ∈ ℝ → B − D ∈ ℝ
12 11 ad2ant2l ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B − D ∈ ℝ
13 10 3 12 ltsubaddd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A − C < B − D ↔ A < B - D + C
14 readdcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
15 14 ad2ant2lr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B + C ∈ ℝ
16 10 5 15 ltaddsubd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A + D < B + C ↔ A < B + C - D
17 9 13 16 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A − C < B − D ↔ A + D < B + C