Metamath Proof Explorer


Theorem iccshift

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

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

Proof

Step Hyp Ref Expression
1 iccshift.1 ( 𝜑𝐴 ∈ ℝ )
2 iccshift.2 ( 𝜑𝐵 ∈ ℝ )
3 iccshift.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 2 iccssred ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
16 15 sselda ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ∈ ℝ )
17 3 adantr ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑇 ∈ ℝ )
18 16 17 readdcld ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ )
19 1 adantr ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
20 simpr ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
21 2 adantr ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
22 elicc2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐴𝑧𝑧𝐵 ) ) )
23 19 21 22 syl2anc ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐴𝑧𝑧𝐵 ) ) )
24 20 23 mpbid ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 ∈ ℝ ∧ 𝐴𝑧𝑧𝐵 ) )
25 24 simp2d ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴𝑧 )
26 19 16 17 25 leadd1dd ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) )
27 24 simp3d ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧𝐵 )
28 16 21 17 27 leadd1dd ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) )
29 18 26 28 3jca ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) )
30 29 3adant3 ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) )
31 1 3 readdcld ( 𝜑 → ( 𝐴 + 𝑇 ) ∈ ℝ )
32 31 3ad2ant1 ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ )
33 2 3 readdcld ( 𝜑 → ( 𝐵 + 𝑇 ) ∈ ℝ )
34 33 3ad2ant1 ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ )
35 elicc2 ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ) → ( ( 𝑧 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) ) )
36 32 34 35 syl2anc ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( ( 𝑧 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) ) )
37 30 36 mpbird ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
38 14 37 eqeltrd ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
39 38 3exp ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑥 = ( 𝑧 + 𝑇 ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) )
40 39 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑥 = ( 𝑧 + 𝑇 ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) )
41 12 13 40 rexlimd ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) )
42 7 41 mpd ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
43 6 42 sylan2b ( ( 𝜑𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
44 31 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ )
45 33 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ )
46 simpr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
47 eliccre ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
48 44 45 46 47 syl3anc ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
49 48 recnd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℂ )
50 1 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 ∈ ℝ )
51 2 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐵 ∈ ℝ )
52 3 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑇 ∈ ℝ )
53 48 52 resubcld ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
54 1 recnd ( 𝜑𝐴 ∈ ℂ )
55 3 recnd ( 𝜑𝑇 ∈ ℂ )
56 54 55 pncand ( 𝜑 → ( ( 𝐴 + 𝑇 ) − 𝑇 ) = 𝐴 )
57 56 eqcomd ( 𝜑𝐴 = ( ( 𝐴 + 𝑇 ) − 𝑇 ) )
58 57 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 = ( ( 𝐴 + 𝑇 ) − 𝑇 ) )
59 elicc2 ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ) → ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ 𝑥𝑥 ≤ ( 𝐵 + 𝑇 ) ) ) )
60 44 45 59 syl2anc ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ 𝑥𝑥 ≤ ( 𝐵 + 𝑇 ) ) ) )
61 46 60 mpbid ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ 𝑥𝑥 ≤ ( 𝐵 + 𝑇 ) ) )
62 61 simp2d ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ≤ 𝑥 )
63 44 48 52 62 lesub1dd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐴 + 𝑇 ) − 𝑇 ) ≤ ( 𝑥𝑇 ) )
64 58 63 eqbrtrd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 ≤ ( 𝑥𝑇 ) )
65 61 simp3d ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑇 ) )
66 48 45 52 65 lesub1dd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥𝑇 ) ≤ ( ( 𝐵 + 𝑇 ) − 𝑇 ) )
67 2 recnd ( 𝜑𝐵 ∈ ℂ )
68 67 55 pncand ( 𝜑 → ( ( 𝐵 + 𝑇 ) − 𝑇 ) = 𝐵 )
69 68 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐵 + 𝑇 ) − 𝑇 ) = 𝐵 )
70 66 69 breqtrd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥𝑇 ) ≤ 𝐵 )
71 50 51 53 64 70 eliccd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) )
72 55 adantr ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑇 ∈ ℂ )
73 49 72 npcand ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝑥𝑇 ) + 𝑇 ) = 𝑥 )
74 73 eqcomd ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) )
75 oveq1 ( 𝑧 = ( 𝑥𝑇 ) → ( 𝑧 + 𝑇 ) = ( ( 𝑥𝑇 ) + 𝑇 ) )
76 75 rspceeqv ( ( ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) ) → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) )
77 71 74 76 syl2anc ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) )
78 49 77 6 sylanbrc ( ( 𝜑𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } )
79 43 78 impbida ( 𝜑 → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↔ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) )
80 79 eqrdv ( 𝜑 → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } = ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
81 80 eqcomd ( 𝜑 → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } )