iccshift

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

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

Proof

Step	Hyp	Ref	Expression
1		iccshift.1	$⊢ φ \to A \in ℝ$
2		iccshift.2	$⊢ φ \to B \in ℝ$
3		iccshift.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 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
16	15	sselda	$⊢ (φ \land z \in [A, B]) \to z \in ℝ$
17	3	adantr	$⊢ (φ \land z \in [A, B]) \to T \in ℝ$
18	16 17	readdcld	$⊢ (φ \land z \in [A, B]) \to z + T \in ℝ$
19	1	adantr	$⊢ (φ \land z \in [A, B]) \to A \in ℝ$
20		simpr	$⊢ (φ \land z \in [A, B]) \to z \in [A, B]$
21	2	adantr	$⊢ (φ \land z \in [A, B]) \to B \in ℝ$
22		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
23	19 21 22	syl2anc	$⊢ (φ \land z \in [A, B]) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
24	20 23	mpbid	$⊢ (φ \land z \in [A, B]) \to (z \in ℝ \land A \leq z \land z \leq B)$
25	24	simp2d	$⊢ (φ \land z \in [A, B]) \to A \leq z$
26	19 16 17 25	leadd1dd	$⊢ (φ \land z \in [A, B]) \to A + T \leq z + T$
27	24	simp3d	$⊢ (φ \land z \in [A, B]) \to z \leq B$
28	16 21 17 27	leadd1dd	$⊢ (φ \land z \in [A, B]) \to z + T \leq B + T$
29	18 26 28	3jca	$⊢ (φ \land z \in [A, B]) \to (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T)$
30	29	3adant3	$⊢ (φ \land z \in [A, B] \land x = z + T) \to (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T)$
31	1 3	readdcld	$⊢ φ \to A + T \in ℝ$
32	31	3ad2ant1	$⊢ (φ \land z \in [A, B] \land x = z + T) \to A + T \in ℝ$
33	2 3	readdcld	$⊢ φ \to B + T \in ℝ$
34	33	3ad2ant1	$⊢ (φ \land z \in [A, B] \land x = z + T) \to B + T \in ℝ$
35		elicc2	$⊢ (A + T \in ℝ \land B + T \in ℝ) \to (z + T \in [A + T, B + T] \leftrightarrow (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T))$
36	32 34 35	syl2anc	$⊢ (φ \land z \in [A, B] \land x = z + T) \to (z + T \in [A + T, B + T] \leftrightarrow (z + T \in ℝ \land A + T \leq z + T \land z + T \leq B + T))$
37	30 36	mpbird	$⊢ (φ \land z \in [A, B] \land x = z + T) \to z + T \in [A + T, B + T]$
38	14 37	eqeltrd	$⊢ (φ \land z \in [A, B] \land x = z + T) \to x \in [A + T, B + T]$
39	38	3exp	$⊢ φ \to (z \in [A, B] \to (x = z + T \to x \in [A + T, B + T]))$
40	39	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]))$
41	12 13 40	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])$
42	7 41	mpd	$⊢ (φ \land (x \in ℂ \land \exists z \in [A, B] x = z + T)) \to x \in [A + T, B + T]$
43	6 42	sylan2b	$⊢ (φ \land x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\}) \to x \in [A + T, B + T]$
44	31	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \in ℝ$
45	33	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T \in ℝ$
46		simpr	$⊢ (φ \land x \in [A + T, B + T]) \to x \in [A + T, B + T]$
47		eliccre	$⊢ (A + T \in ℝ \land B + T \in ℝ \land x \in [A + T, B + T]) \to x \in ℝ$
48	44 45 46 47	syl3anc	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℝ$
49	48	recnd	$⊢ (φ \land x \in [A + T, B + T]) \to x \in ℂ$
50	1	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to A \in ℝ$
51	2	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	48 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		elicc2	$⊢ (A + T \in ℝ \land B + T \in ℝ) \to (x \in [A + T, B + T] \leftrightarrow (x \in ℝ \land A + T \leq x \land x \leq B + T))$
60	44 45 59	syl2anc	$⊢ (φ \land x \in [A + T, B + T]) \to (x \in [A + T, B + T] \leftrightarrow (x \in ℝ \land A + T \leq x \land x \leq B + T))$
61	46 60	mpbid	$⊢ (φ \land x \in [A + T, B + T]) \to (x \in ℝ \land A + T \leq x \land x \leq B + T)$
62	61	simp2d	$⊢ (φ \land x \in [A + T, B + T]) \to A + T \leq x$
63	44 48 52 62	lesub1dd	$⊢ (φ \land x \in [A + T, B + T]) \to A + T - T \leq x - T$
64	58 63	eqbrtrd	$⊢ (φ \land x \in [A + T, B + T]) \to A \leq x - T$
65	61	simp3d	$⊢ (φ \land x \in [A + T, B + T]) \to x \leq B + T$
66	48 45 52 65	lesub1dd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \leq B + T - T$
67	2	recnd	$⊢ φ \to B \in ℂ$
68	67 55	pncand	$⊢ φ \to B + T - T = B$
69	68	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to B + T - T = B$
70	66 69	breqtrd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \leq B$
71	50 51 53 64 70	eliccd	$⊢ (φ \land x \in [A + T, B + T]) \to x - T \in [A, B]$
72	55	adantr	$⊢ (φ \land x \in [A + T, B + T]) \to T \in ℂ$
73	49 72	npcand	$⊢ (φ \land x \in [A + T, B + T]) \to x - T + T = x$
74	73	eqcomd	$⊢ (φ \land x \in [A + T, B + T]) \to x = x - T + T$
75		oveq1	$⊢ z = x - T \to z + T = x - T + T$
76	75	rspceeqv	$⊢ (x - T \in [A, B] \land x = x - T + T) \to \exists z \in [A, B] x = z + T$
77	71 74 76	syl2anc	$⊢ (φ \land x \in [A + T, B + T]) \to \exists z \in [A, B] x = z + T$
78	49 77 6	sylanbrc	$⊢ (φ \land x \in [A + T, B + T]) \to x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\}$
79	43 78	impbida	$⊢ φ \to (x \in \{w \in ℂ \| \exists z \in [A, B] w = z + T\} \leftrightarrow x \in [A + T, B + T])$
80	79	eqrdv	$⊢ φ \to \{w \in ℂ \| \exists z \in [A, B] w = z + T\} = [A + T, B + T]$
81	80	eqcomd	$⊢ φ \to [A + T, B + T] = \{w \in ℂ \| \exists z \in [A, B] w = z + T\}$

Metamath Proof Explorer

Theorem iccshift

Proof