iooshf

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

		Ref	Expression
	Assertion	iooshf	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - B \in (C, D) \leftrightarrow A \in (C + B, D + B))$

Proof

Step	Hyp	Ref	Expression
1		ltaddsub	$⊢ (C \in ℝ \land B \in ℝ \land A \in ℝ) \to (C + B < A \leftrightarrow C < A - B)$
2	1	3com13	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (C + B < A \leftrightarrow C < A - B)$
3	2	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to (C + B < A \leftrightarrow C < A - B)$
4	3	adantrr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (C + B < A \leftrightarrow C < A - B)$
5		ltsubadd	$⊢ (A \in ℝ \land B \in ℝ \land D \in ℝ) \to (A - B < D \leftrightarrow A < D + B)$
6	5	bicomd	$⊢ (A \in ℝ \land B \in ℝ \land D \in ℝ) \to (A < D + B \leftrightarrow A - B < D)$
7	6	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land D \in ℝ) \to (A < D + B \leftrightarrow A - B < D)$
8	7	adantrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A < D + B \leftrightarrow A - B < D)$
9	4 8	anbi12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((C + B < A \land A < D + B) \leftrightarrow (C < A - B \land A - B < D))$
10		readdcl	$⊢ (C \in ℝ \land B \in ℝ) \to C + B \in ℝ$
11	10	rexrd	$⊢ (C \in ℝ \land B \in ℝ) \to C + B \in ℝ^{*}$
12	11	ad2ant2rl	$⊢ ((C \in ℝ \land D \in ℝ) \land (A \in ℝ \land B \in ℝ)) \to C + B \in ℝ^{*}$
13		readdcl	$⊢ (D \in ℝ \land B \in ℝ) \to D + B \in ℝ$
14	13	rexrd	$⊢ (D \in ℝ \land B \in ℝ) \to D + B \in ℝ^{*}$
15	14	ad2ant2l	$⊢ ((C \in ℝ \land D \in ℝ) \land (A \in ℝ \land B \in ℝ)) \to D + B \in ℝ^{*}$
16		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
17	16	ad2antrl	$⊢ ((C \in ℝ \land D \in ℝ) \land (A \in ℝ \land B \in ℝ)) \to A \in ℝ^{*}$
18		elioo5	$⊢ (C + B \in ℝ^{} \land D + B \in ℝ^{} \land A \in ℝ^{*}) \to (A \in (C + B, D + B) \leftrightarrow (C + B < A \land A < D + B))$
19	12 15 17 18	syl3anc	$⊢ ((C \in ℝ \land D \in ℝ) \land (A \in ℝ \land B \in ℝ)) \to (A \in (C + B, D + B) \leftrightarrow (C + B < A \land A < D + B))$
20	19	ancoms	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A \in (C + B, D + B) \leftrightarrow (C + B < A \land A < D + B))$
21		rexr	$⊢ C \in ℝ \to C \in ℝ^{*}$
22	21	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℝ^{*}$
23		rexr	$⊢ D \in ℝ \to D \in ℝ^{*}$
24	23	ad2antll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℝ^{*}$
25		resubcl	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ$
26	25	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ^{*}$
27	26	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A - B \in ℝ^{*}$
28		elioo5	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land A - B \in ℝ^{*}) \to (A - B \in (C, D) \leftrightarrow (C < A - B \land A - B < D))$
29	22 24 27 28	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - B \in (C, D) \leftrightarrow (C < A - B \land A - B < D))$
30	9 20 29	3bitr4rd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - B \in (C, D) \leftrightarrow A \in (C + B, D + B))$

Metamath Proof Explorer

Theorem iooshf

Proof