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

Metamath Proof Explorer

Theorem iooshf

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

Ref Expression
Assertion iooshf ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 − 𝐵 ) ∈ ( 𝐶 (,) 𝐷 ) ↔ 𝐴 ∈ ( ( 𝐶 + 𝐵 ) (,) ( 𝐷 + 𝐵 ) ) ) )

Proof

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