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	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem106.t	$⊢ T = 2 π$
	fourierdlem106.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem106.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fourierdlem106.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
	fourierdlem106.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
	fourierdlem106.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem106.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem106.x	$⊢ φ \to X \in ℝ$
Assertion	fourierdlem106	$⊢ φ \to (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \land ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem106.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem106.t	$⊢ T = 2 π$
3		fourierdlem106.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourierdlem106.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fourierdlem106.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
6		fourierdlem106.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
7		fourierdlem106.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fourierdlem106.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fourierdlem106.x	$⊢ φ \to X \in ℝ$
10		eqid	$⊢ (k \in ℕ ⟼ \{w \in (ℝ^{(0 \dots k)}) \| ((w (0) = - π \land w (k) = π) \land \forall z \in (0 ..^k) w (z) < w (z + 1))\}) = (k \in ℕ ⟼ \{w \in (ℝ^{(0 \dots k)}) \| ((w (0) = - π \land w (k) = π) \land \forall z \in (0 ..^k) w (z) < w (z + 1))\})$
11		id	$⊢ y = x \to y = x$
12		oveq2	$⊢ y = x \to π - y = π - x$
13	12	oveq1d	$⊢ y = x \to \frac{π - y}{T} = \frac{π - x}{T}$
14	13	fveq2d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ = ⌊\frac{π - x}{T}⌋$
15	14	oveq1d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ T = ⌊\frac{π - x}{T}⌋ T$
16	11 15	oveq12d	$⊢ y = x \to y + ⌊\frac{π - y}{T}⌋ T = x + ⌊\frac{π - x}{T}⌋ T$
17	16	cbvmptv	$⊢ (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
18		eqid	$⊢ \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G) = \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)$
19		eqid	$⊢ \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1 = \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1$
20		isoeq1	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)))$
21	20	cbviotavw	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G))) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)))$
22	1 2 3 4 5 6 7 8 9 10 17 18 19 21	fourierdlem102	$⊢ φ \to (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \land ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$

Metamath Proof Explorer

Theorem fourierdlem106

Proof