Metamath Proof Explorer

Theorem iooshift

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

Ref Expression
Hypotheses iooshift.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
iooshift.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
iooshift.3 ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
Assertion iooshift ( 𝜑 → ( ( 𝐴 + 𝑇 ) (,) ( 𝐵 + 𝑇 ) ) = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } )

Proof

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