iooshift

Description: An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	iooshift.1	$⊢ φ \to A \in ℝ$
	iooshift.2	$⊢ φ \to B \in ℝ$
	iooshift.3	$⊢ φ \to T \in ℝ$
Assertion	iooshift	$⊢ φ \to (A + T, B + T) = \{w \in ℂ \| \exists z \in (A, B) w = z + T\}$

Proof

Step	Hyp	Ref	Expression
1		iooshift.1	$⊢ φ \to A \in ℝ$
2		iooshift.2	$⊢ φ \to B \in ℝ$
3		iooshift.3	$⊢ φ \to T \in ℝ$
4		eqeq1	$⊢ w = x \to (w = z + T \leftrightarrow x = z + T)$
5	4	rexbidv	$⊢ w = x \to (\exists z \in (A, B) w = z + T \leftrightarrow \exists z \in (A, B) x = z + T)$
6	5	elrab	$⊢ x \in \{w \in ℂ \| \exists z \in (A, B) w = z + T\} \leftrightarrow (x \in ℂ \land \exists z \in (A, B) x = z + T)$
7		simprr	$⊢ (φ \land (x \in ℂ \land \exists z \in (A, B) x = z + T)) \to \exists z \in (A, B) x = z + T$
8		nfv	$⊢ Ⅎ z φ$
9		nfv	$⊢ Ⅎ z x \in ℂ$
10		nfre1	$⊢ Ⅎ z \exists z \in (A, B) x = z + T$
11	9 10	nfan	$⊢ Ⅎ z (x \in ℂ \land \exists z \in (A, B) x = z + T)$
12	8 11	nfan	$⊢ Ⅎ z (φ \land (x \in ℂ \land \exists z \in (A, B) x = z + T))$
13		nfv	$⊢ Ⅎ z x \in (A + T, B + T)$
14		simp3	$⊢ (φ \land z \in (A, B) \land x = z + T) \to x = z + T$
15	1 3	readdcld	$⊢ φ \to A + T \in ℝ$
16	15	rexrd	$⊢ φ \to A + T \in ℝ^{*}$
17	16	adantr	$⊢ (φ \land z \in (A, B)) \to A + T \in ℝ^{*}$
18	2 3	readdcld	$⊢ φ \to B + T \in ℝ$
19	18	rexrd	$⊢ φ \to B + T \in ℝ^{*}$
20	19	adantr	$⊢ (φ \land z \in (A, B)) \to B + T \in ℝ^{*}$
21		ioossre	$⊢ (A, B) \subseteq ℝ$
22	21	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
23	22	sselda	$⊢ (φ \land z \in (A, B)) \to z \in ℝ$
24	3	adantr	$⊢ (φ \land z \in (A, B)) \to T \in ℝ$
25	23 24	readdcld	$⊢ (φ \land z \in (A, B)) \to z + T \in ℝ$
26	1	adantr	$⊢ (φ \land z \in (A, B)) \to A \in ℝ$
27	26	rexrd	$⊢ (φ \land z \in (A, B)) \to A \in ℝ^{*}$
28	2	adantr	$⊢ (φ \land z \in (A, B)) \to B \in ℝ$
29	28	rexrd	$⊢ (φ \land z \in (A, B)) \to B \in ℝ^{*}$
30		simpr	$⊢ (φ \land z \in (A, B)) \to z \in (A, B)$
31		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land z \in (A, B)) \to A < z$
32	27 29 30 31	syl3anc	$⊢ (φ \land z \in (A, B)) \to A < z$
33	26 23 24 32	ltadd1dd	$⊢ (φ \land z \in (A, B)) \to A + T < z + T$
34		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land z \in (A, B)) \to z < B$
35	27 29 30 34	syl3anc	$⊢ (φ \land z \in (A, B)) \to z < B$
36	23 28 24 35	ltadd1dd	$⊢ (φ \land z \in (A, B)) \to z + T < B + T$
37	17 20 25 33 36	eliood	$⊢ (φ \land z \in (A, B)) \to z + T \in (A + T, B + T)$
38	37	3adant3	$⊢ (φ \land z \in (A, B) \land x = z + T) \to z + T \in (A + T, B + T)$
39	14 38	eqeltrd	$⊢ (φ \land z \in (A, B) \land x = z + T) \to x \in (A + T, B + T)$
40	39	3exp	$⊢ φ \to (z \in (A, B) \to (x = z + T \to x \in (A + T, B + T)))$
41	40	adantr	$⊢ (φ \land (x \in ℂ \land \exists z \in (A, B) x = z + T)) \to (z \in (A, B) \to (x = z + T \to x \in (A + T, B + T)))$
42	12 13 41	rexlimd	$⊢ (φ \land (x \in ℂ \land \exists z \in (A, B) x = z + T)) \to (\exists z \in (A, B) x = z + T \to x \in (A + T, B + T))$
43	7 42	mpd	$⊢ (φ \land (x \in ℂ \land \exists z \in (A, B) x = z + T)) \to x \in (A + T, B + T)$
44	6 43	sylan2b	$⊢ (φ \land x \in \{w \in ℂ \| \exists z \in (A, B) w = z + T\}) \to x \in (A + T, B + T)$
45		elioore	$⊢ x \in (A + T, B + T) \to x \in ℝ$
46	45	adantl	$⊢ (φ \land x \in (A + T, B + T)) \to x \in ℝ$
47	46	recnd	$⊢ (φ \land x \in (A + T, B + T)) \to x \in ℂ$
48	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
49	48	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to A \in ℝ^{*}$
50	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
51	50	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to B \in ℝ^{*}$
52	3	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to T \in ℝ$
53	46 52	resubcld	$⊢ (φ \land x \in (A + T, B + T)) \to x - T \in ℝ$
54	1	recnd	$⊢ φ \to A \in ℂ$
55	3	recnd	$⊢ φ \to T \in ℂ$
56	54 55	pncand	$⊢ φ \to A + T - T = A$
57	56	eqcomd	$⊢ φ \to A = A + T - T$
58	57	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to A = A + T - T$
59	15	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to A + T \in ℝ$
60	16	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to A + T \in ℝ^{*}$
61	19	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to B + T \in ℝ^{*}$
62		simpr	$⊢ (φ \land x \in (A + T, B + T)) \to x \in (A + T, B + T)$
63		ioogtlb	$⊢ (A + T \in ℝ^{} \land B + T \in ℝ^{} \land x \in (A + T, B + T)) \to A + T < x$
64	60 61 62 63	syl3anc	$⊢ (φ \land x \in (A + T, B + T)) \to A + T < x$
65	59 46 52 64	ltsub1dd	$⊢ (φ \land x \in (A + T, B + T)) \to A + T - T < x - T$
66	58 65	eqbrtrd	$⊢ (φ \land x \in (A + T, B + T)) \to A < x - T$
67	18	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to B + T \in ℝ$
68		iooltub	$⊢ (A + T \in ℝ^{} \land B + T \in ℝ^{} \land x \in (A + T, B + T)) \to x < B + T$
69	60 61 62 68	syl3anc	$⊢ (φ \land x \in (A + T, B + T)) \to x < B + T$
70	46 67 52 69	ltsub1dd	$⊢ (φ \land x \in (A + T, B + T)) \to x - T < B + T - T$
71	2	recnd	$⊢ φ \to B \in ℂ$
72	71 55	pncand	$⊢ φ \to B + T - T = B$
73	72	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to B + T - T = B$
74	70 73	breqtrd	$⊢ (φ \land x \in (A + T, B + T)) \to x - T < B$
75	49 51 53 66 74	eliood	$⊢ (φ \land x \in (A + T, B + T)) \to x - T \in (A, B)$
76	55	adantr	$⊢ (φ \land x \in (A + T, B + T)) \to T \in ℂ$
77	47 76	npcand	$⊢ (φ \land x \in (A + T, B + T)) \to x - T + T = x$
78	77	eqcomd	$⊢ (φ \land x \in (A + T, B + T)) \to x = x - T + T$
79		oveq1	$⊢ z = x - T \to z + T = x - T + T$
80	79	rspceeqv	$⊢ (x - T \in (A, B) \land x = x - T + T) \to \exists z \in (A, B) x = z + T$
81	75 78 80	syl2anc	$⊢ (φ \land x \in (A + T, B + T)) \to \exists z \in (A, B) x = z + T$
82	47 81 6	sylanbrc	$⊢ (φ \land x \in (A + T, B + T)) \to x \in \{w \in ℂ \| \exists z \in (A, B) w = z + T\}$
83	44 82	impbida	$⊢ φ \to (x \in \{w \in ℂ \| \exists z \in (A, B) w = z + T\} \leftrightarrow x \in (A + T, B + T))$
84	83	eqrdv	$⊢ φ \to \{w \in ℂ \| \exists z \in (A, B) w = z + T\} = (A + T, B + T)$
85	84	eqcomd	$⊢ φ \to (A + T, B + T) = \{w \in ℂ \| \exists z \in (A, B) w = z + T\}$

Metamath Proof Explorer

Theorem iooshift

Proof