Metamath Proof Explorer

Theorem iooshf

Description: Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008)

Ref Expression
Assertion iooshf ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A−B∈CD↔A∈C+BD+B

Proof

Step Hyp Ref Expression
1 ltaddsub ⊢C∈ℝ∧B∈ℝ∧A∈ℝ→C+B<A↔C<A−B
2 1 3com13 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+B<A↔C<A−B
3 2 3expa ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+B<A↔C<A−B
4 3 adantrr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→C+B<A↔C<A−B
5 ltsubadd ⊢A∈ℝ∧B∈ℝ∧D∈ℝ→A−B<D↔A<D+B
6 5 bicomd ⊢A∈ℝ∧B∈ℝ∧D∈ℝ→A<D+B↔A−B<D
7 6 3expa ⊢A∈ℝ∧B∈ℝ∧D∈ℝ→A<D+B↔A−B<D
8 7 adantrl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A<D+B↔A−B<D
9 4 8 anbi12d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→C+B<A∧A<D+B↔C<A−B∧A−B<D
10 readdcl ⊢C∈ℝ∧B∈ℝ→C+B∈ℝ
11 10 rexrd ⊢C∈ℝ∧B∈ℝ→C+B∈ℝ*
12 11 ad2ant2rl ⊢C∈ℝ∧D∈ℝ∧A∈ℝ∧B∈ℝ→C+B∈ℝ*
13 readdcl ⊢D∈ℝ∧B∈ℝ→D+B∈ℝ
14 13 rexrd ⊢D∈ℝ∧B∈ℝ→D+B∈ℝ*
15 14 ad2ant2l ⊢C∈ℝ∧D∈ℝ∧A∈ℝ∧B∈ℝ→D+B∈ℝ*
16 rexr ⊢A∈ℝ→A∈ℝ*
17 16 ad2antrl ⊢C∈ℝ∧D∈ℝ∧A∈ℝ∧B∈ℝ→A∈ℝ*
18 elioo5 ⊢C+B∈ℝ*∧D+B∈ℝ*∧A∈ℝ*→A∈C+BD+B↔C+B<A∧A<D+B
19 12 15 17 18 syl3anc ⊢C∈ℝ∧D∈ℝ∧A∈ℝ∧B∈ℝ→A∈C+BD+B↔C+B<A∧A<D+B
20 19 ancoms ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A∈C+BD+B↔C+B<A∧A<D+B
21 rexr ⊢C∈ℝ→C∈ℝ*
22 21 ad2antrl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→C∈ℝ*
23 rexr ⊢D∈ℝ→D∈ℝ*
24 23 ad2antll ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→D∈ℝ*
25 resubcl ⊢A∈ℝ∧B∈ℝ→A−B∈ℝ
26 25 rexrd ⊢A∈ℝ∧B∈ℝ→A−B∈ℝ*
27 26 adantr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A−B∈ℝ*
28 elioo5 ⊢C∈ℝ*∧D∈ℝ*∧A−B∈ℝ*→A−B∈CD↔C<A−B∧A−B<D
29 22 24 27 28 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A−B∈CD↔C<A−B∧A−B<D
30 9 20 29 3bitr4rd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A−B∈CD↔A∈C+BD+B