Metamath Proof Explorer

Theorem cncfshiftioo

Description: A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfshiftioo.a ⊢φ→A∈ℝ
cncfshiftioo.b ⊢φ→B∈ℝ
cncfshiftioo.c ⊢C=AB
cncfshiftioo.t ⊢φ→T∈ℝ
cncfshiftioo.d ⊢D=A+TB+T
cncfshiftioo.f ⊢φ→F:C⟶cnℂ
cncfshiftioo.g ⊢G=x∈D⟼F⁡x−T
Assertion cncfshiftioo ⊢φ→G:D⟶cnℂ

Proof

Step Hyp Ref Expression
1 cncfshiftioo.a ⊢φ→A∈ℝ
2 cncfshiftioo.b ⊢φ→B∈ℝ
3 cncfshiftioo.c ⊢C=AB
4 cncfshiftioo.t ⊢φ→T∈ℝ
5 cncfshiftioo.d ⊢D=A+TB+T
6 cncfshiftioo.f ⊢φ→F:C⟶cnℂ
7 cncfshiftioo.g ⊢G=x∈D⟼F⁡x−T
8 ioosscn ⊢AB⊆ℂ
9 8 a1i ⊢φ→AB⊆ℂ
10 4 recnd ⊢φ→T∈ℂ
11 eqeq1 ⊢w=x→w=z+T↔x=z+T
12 11 rexbidv ⊢w=x→∃z∈ABw=z+T↔∃z∈ABx=z+T
13 oveq1 ⊢z=y→z+T=y+T
14 13 eqeq2d ⊢z=y→x=z+T↔x=y+T
15 14 cbvrexvw ⊢∃z∈ABx=z+T↔∃y∈ABx=y+T
16 12 15 bitrdi ⊢w=x→∃z∈ABw=z+T↔∃y∈ABx=y+T
17 16 cbvrabv ⊢w∈ℂ|∃z∈ABw=z+T=x∈ℂ|∃y∈ABx=y+T
18 3 oveq1i ⊢C⟶cnℂ=AB⟶cnℂ
19 6 18 eleqtrdi ⊢φ→F:AB⟶cnℂ
20 eqid ⊢x∈w∈ℂ|∃z∈ABw=z+T⟼F⁡x−T=x∈w∈ℂ|∃z∈ABw=z+T⟼F⁡x−T
21 9 10 17 19 20 cncfshift ⊢φ→x∈w∈ℂ|∃z∈ABw=z+T⟼F⁡x−T:w∈ℂ|∃z∈ABw=z+T⟶cnℂ
22 1 2 4 iooshift ⊢φ→A+TB+T=w∈ℂ|∃z∈ABw=z+T
23 5 22 eqtrid ⊢φ→D=w∈ℂ|∃z∈ABw=z+T
24 23 mpteq1d ⊢φ→x∈D⟼F⁡x−T=x∈w∈ℂ|∃z∈ABw=z+T⟼F⁡x−T
25 7 24 eqtrid ⊢φ→G=x∈w∈ℂ|∃z∈ABw=z+T⟼F⁡x−T
26 23 oveq1d ⊢φ→D⟶cnℂ=w∈ℂ|∃z∈ABw=z+T⟶cnℂ
27 21 25 26 3eltr4d ⊢φ→G:D⟶cnℂ