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