Metamath Proof Explorer

Theorem fourierdlem106

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem106.f ⊢φ→F:ℝ⟶ℝ
fourierdlem106.t ⊢T=2⁢π
fourierdlem106.per ⊢φ∧x∈ℝ→F⁡x+T=F⁡x
fourierdlem106.g ⊢G=Fℝ′↾−ππ
fourierdlem106.dmdv ⊢φ→−ππ∖dom⁡G∈Fin
fourierdlem106.dvcn ⊢φ→G:dom⁡G⟶cnℂ
fourierdlem106.rlim ⊢φ∧x∈−ππ∖dom⁡G→G↾x+∞limℂx≠∅
fourierdlem106.llim ⊢φ∧x∈−ππ∖dom⁡G→G↾−∞xlimℂx≠∅
fourierdlem106.x ⊢φ→X∈ℝ
Assertion fourierdlem106 ⊢φ→F↾−∞XlimℂX≠∅∧F↾X+∞limℂX≠∅

Proof

Step Hyp Ref Expression
1 fourierdlem106.f ⊢φ→F:ℝ⟶ℝ
2 fourierdlem106.t ⊢T=2⁢π
3 fourierdlem106.per ⊢φ∧x∈ℝ→F⁡x+T=F⁡x
4 fourierdlem106.g ⊢G=Fℝ′↾−ππ
5 fourierdlem106.dmdv ⊢φ→−ππ∖dom⁡G∈Fin
6 fourierdlem106.dvcn ⊢φ→G:dom⁡G⟶cnℂ
7 fourierdlem106.rlim ⊢φ∧x∈−ππ∖dom⁡G→G↾x+∞limℂx≠∅
8 fourierdlem106.llim ⊢φ∧x∈−ππ∖dom⁡G→G↾−∞xlimℂx≠∅
9 fourierdlem106.x ⊢φ→X∈ℝ
10 eqid ⊢k∈ℕ⟼w∈ℝ0…k|w⁡0=−π∧w⁡k=π∧∀z∈0..^kw⁡z<w⁡z+1=k∈ℕ⟼w∈ℝ0…k|w⁡0=−π∧w⁡k=π∧∀z∈0..^kw⁡z<w⁡z+1
11 id ⊢y=x→y=x
12 oveq2 ⊢y=x→π−y=π−x
13 12 oveq1d ⊢y=x→π−yT=π−xT
14 13 fveq2d ⊢y=x→π−yT=π−xT
15 14 oveq1d ⊢y=x→π−yT⁢T=π−xT⁢T
16 11 15 oveq12d ⊢y=x→y+π−yT⁢T=x+π−xT⁢T
17 16 cbvmptv ⊢y∈ℝ⟼y+π−yT⁢T=x∈ℝ⟼x+π−xT⁢T
18 eqid ⊢−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G=−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G
19 eqid ⊢−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G−1=−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G−1
20 isoeq1 ⊢g=f→gIsom<,<0…−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G−1−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G↔fIsom<,<0…−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G−1−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G
21 20 cbviotavw ⊢ιg|gIsom<,<0…−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G−1−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G=ιf|fIsom<,<0…−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G−1−ππy∈ℝ⟼y+π−yT⁢T⁡X∪−ππ∖dom⁡G
22 1 2 3 4 5 6 7 8 9 10 17 18 19 21 fourierdlem102 ⊢φ→F↾−∞XlimℂX≠∅∧F↾X+∞limℂX≠∅