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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 − 𝐵 ) ∈ ( 𝐶 (,) 𝐷 ) ↔ 𝐴 ∈ ( ( 𝐶 + 𝐵 ) (,) ( 𝐷 + 𝐵 ) ) ) )