Metamath Proof Explorer

Theorem ltsubadd2b

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

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℝ
2 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℂ
3 2 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ∈ ℂ
4 simpl ⊢ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℝ
5 4 recnd ⊢ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℂ
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℂ
7 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
8 7 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℂ
9 8 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ∈ ℂ
10 3 6 9 addsubd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B + C - A = B - A + C
11 10 eqcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B - A + C = B + C - A
12 11 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D < B - A + C ↔ D < B + C - A
13 simprr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D ∈ ℝ
14 simprl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℝ
15 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
16 15 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ
17 16 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B − A ∈ ℝ
18 13 14 17 ltsubaddd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D − C < B − A ↔ D < B - A + C
19 7 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ∈ ℝ
20 readdcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
21 20 ad2ant2lr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B + C ∈ ℝ
22 19 13 21 ltaddsub2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A + D < B + C ↔ D < B + C - A
23 12 18 22 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D − C < B − A ↔ A + D < B + C