fourierdlem97

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem97.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem97.g	$⊢ G = ℝ D F$
	fourierdlem97.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem97.a	$⊢ φ \to B \in ℝ$
	fourierdlem97.b	$⊢ φ \to A \in ℝ$
	fourierdlem97.t	$⊢ T = B - A$
	fourierdlem97.m	$⊢ φ \to M \in ℕ$
	fourierdlem97.q	$⊢ φ \to Q \in P (M)$
	fourierdlem97.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem97.qcn	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem97.c	$⊢ φ \to C \in ℝ$
	fourierdlem97.d	$⊢ φ \to D \in (C, +∞)$
	fourierdlem97.j	$⊢ φ \to J \in (0 ..^\|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
	fourierdlem97.v	$⊢ V = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
	fourierdlem97.h	$⊢ H = (s \in ℝ ⟼ if (s \in dom G, G (s), 0))$
Assertion	fourierdlem97	$⊢ φ \to ({G ↾}_{(V (J), V (J + 1))}) : (V (J), V (J + 1)) \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem97.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem97.g	$⊢ G = ℝ D F$
3		fourierdlem97.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
4		fourierdlem97.a	$⊢ φ \to B \in ℝ$
5		fourierdlem97.b	$⊢ φ \to A \in ℝ$
6		fourierdlem97.t	$⊢ T = B - A$
7		fourierdlem97.m	$⊢ φ \to M \in ℕ$
8		fourierdlem97.q	$⊢ φ \to Q \in P (M)$
9		fourierdlem97.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
10		fourierdlem97.qcn	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem97.c	$⊢ φ \to C \in ℝ$
12		fourierdlem97.d	$⊢ φ \to D \in (C, +∞)$
13		fourierdlem97.j	$⊢ φ \to J \in (0 ..^\|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
14		fourierdlem97.v	$⊢ V = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
15		fourierdlem97.h	$⊢ H = (s \in ℝ ⟼ if (s \in dom G, G (s), 0))$
16		ioossre	$⊢ (V (J), V (J + 1)) \subseteq ℝ$
17	16	a1i	$⊢ φ \to (V (J), V (J + 1)) \subseteq ℝ$
18	17	sselda	$⊢ (φ \land s \in (V (J), V (J + 1))) \to s \in ℝ$
19		iftrue	$⊢ s \in dom G \to if (s \in dom G, G (s), 0) = G (s)$
20	19	adantl	$⊢ (φ \land s \in dom G) \to if (s \in dom G, G (s), 0) = G (s)$
21		ssid	$⊢ ℝ \subseteq ℝ$
22		dvfre	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
23	1 21 22	sylancl	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
24	2	feq1i	$⊢ G : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
25	23 24	sylibr	$⊢ φ \to G : dom F_{ℝ}^{'} ⟶ ℝ$
26	25	adantr	$⊢ (φ \land s \in dom G) \to G : dom F_{ℝ}^{'} ⟶ ℝ$
27		id	$⊢ s \in dom G \to s \in dom G$
28	2	dmeqi	$⊢ dom G = dom F_{ℝ}^{'}$
29	27 28	eleqtrdi	$⊢ s \in dom G \to s \in dom F_{ℝ}^{'}$
30	29	adantl	$⊢ (φ \land s \in dom G) \to s \in dom F_{ℝ}^{'}$
31	26 30	ffvelrnd	$⊢ (φ \land s \in dom G) \to G (s) \in ℝ$
32	20 31	eqeltrd	$⊢ (φ \land s \in dom G) \to if (s \in dom G, G (s), 0) \in ℝ$
33	32	adantlr	$⊢ ((φ \land s \in ℝ) \land s \in dom G) \to if (s \in dom G, G (s), 0) \in ℝ$
34		iffalse	$⊢ \neg s \in dom G \to if (s \in dom G, G (s), 0) = 0$
35		0red	$⊢ \neg s \in dom G \to 0 \in ℝ$
36	34 35	eqeltrd	$⊢ \neg s \in dom G \to if (s \in dom G, G (s), 0) \in ℝ$
37	36	adantl	$⊢ ((φ \land s \in ℝ) \land \neg s \in dom G) \to if (s \in dom G, G (s), 0) \in ℝ$
38	33 37	pm2.61dan	$⊢ (φ \land s \in ℝ) \to if (s \in dom G, G (s), 0) \in ℝ$
39	18 38	syldan	$⊢ (φ \land s \in (V (J), V (J + 1))) \to if (s \in dom G, G (s), 0) \in ℝ$
40	15	fvmpt2	$⊢ (s \in ℝ \land if (s \in dom G, G (s), 0) \in ℝ) \to H (s) = if (s \in dom G, G (s), 0)$
41	18 39 40	syl2anc	$⊢ (φ \land s \in (V (J), V (J + 1))) \to H (s) = if (s \in dom G, G (s), 0)$
42		elioore	$⊢ D \in (C, +∞) \to D \in ℝ$
43	12 42	syl	$⊢ φ \to D \in ℝ$
44	11	rexrd	$⊢ φ \to C \in ℝ^{*}$
45		pnfxr	$⊢ +∞ \in ℝ^{*}$
46	45	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
47		ioogtlb	$⊢ (C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in (C, +∞)) \to C < D$
48	44 46 12 47	syl3anc	$⊢ φ \to C < D$
49		oveq1	$⊢ y = x \to y + h T = x + h T$
50	49	eleq1d	$⊢ y = x \to (y + h T \in ran Q \leftrightarrow x + h T \in ran Q)$
51	50	rexbidv	$⊢ y = x \to (\exists h \in ℤ y + h T \in ran Q \leftrightarrow \exists h \in ℤ x + h T \in ran Q)$
52	51	cbvrabv	$⊢ \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\} = \{x \in [C, D] \| \exists h \in ℤ x + h T \in ran Q\}$
53	52	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\} = \{C, D\} \cup \{x \in [C, D] \| \exists h \in ℤ x + h T \in ran Q\}$
54		oveq1	$⊢ k = l \to k T = l T$
55	54	oveq2d	$⊢ k = l \to y + k T = y + l T$
56	55	eleq1d	$⊢ k = l \to (y + k T \in ran Q \leftrightarrow y + l T \in ran Q)$
57	56	cbvrexvw	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists l \in ℤ y + l T \in ran Q$
58	57	a1i	$⊢ y \in [C, D] \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists l \in ℤ y + l T \in ran Q)$
59	58	rabbiia	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
60	59	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
61		oveq1	$⊢ l = h \to l T = h T$
62	61	oveq2d	$⊢ l = h \to y + l T = y + h T$
63	62	eleq1d	$⊢ l = h \to (y + l T \in ran Q \leftrightarrow y + h T \in ran Q)$
64	63	cbvrexvw	$⊢ \exists l \in ℤ y + l T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q$
65	64	a1i	$⊢ y \in [C, D] \to (\exists l \in ℤ y + l T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q)$
66	65	rabbiia	$⊢ \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}$
67	66	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}$
68	60 67	eqtri	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}$
69	68	fveq2i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| = \|\{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}\|$
70	69	oveq1i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}\| - 1$
71		oveq1	$⊢ k = h \to k T = h T$
72	71	oveq2d	$⊢ k = h \to Q (0) + k T = Q (0) + h T$
73	72	breq1d	$⊢ k = h \to (Q (0) + k T \leq V (J) \leftrightarrow Q (0) + h T \leq V (J))$
74	73	cbvrabv	$⊢ \{k \in ℤ \| Q (0) + k T \leq V (J)\} = \{h \in ℤ \| Q (0) + h T \leq V (J)\}$
75	74	supeq1i	$⊢ sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) = sup (\{h \in ℤ \| Q (0) + h T \leq V (J)\} ℝ <)$
76		fveq2	$⊢ j = e \to Q (j) = Q (e)$
77	76	oveq1d	$⊢ j = e \to Q (j) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T = Q (e) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T$
78	77	breq1d	$⊢ j = e \to (Q (j) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J) \leftrightarrow Q (e) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J))$
79	78	cbvrabv	$⊢ \{j \in (0 ..^M) \| Q (j) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J)\} = \{e \in (0 ..^M) \| Q (e) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J)\}$
80	79	supeq1i	$⊢ sup (\{j \in (0 ..^M) \| Q (j) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J)\} ℝ <) = sup (\{e \in (0 ..^M) \| Q (e) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J)\} ℝ <)$
81	6 3 7 8 11 43 48 53 70 14 13 75 80	fourierdlem64	$⊢ φ \to ((sup (\{j \in (0 ..^M) \| Q (j) + sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) T \leq V (J)\} ℝ <) \in (0 ..^M) \land sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) \in ℤ) \land \exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T))$
82	81	simprd	$⊢ φ \to \exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)$
83		simpl1	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to φ$
84		simpl2l	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to i \in (0 ..^M)$
85		cncff	$⊢ ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
86	10 85	syl	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
87		ffun	$⊢ G : dom F_{ℝ}^{'} ⟶ ℝ \to Fun G$
88	25 87	syl	$⊢ φ \to Fun G$
89	88	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Fun G$
90		ffvresb	$⊢ Fun G \to (({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \leftrightarrow \forall s \in (Q (i), Q (i + 1)) (s \in dom G \land G (s) \in ℂ))$
91	89 90	syl	$⊢ (φ \land i \in (0 ..^M)) \to (({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \leftrightarrow \forall s \in (Q (i), Q (i + 1)) (s \in dom G \land G (s) \in ℂ))$
92	86 91	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to \forall s \in (Q (i), Q (i + 1)) (s \in dom G \land G (s) \in ℂ)$
93	92	r19.21bi	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to (s \in dom G \land G (s) \in ℂ)$
94	93	simpld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in dom G$
95	94	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall s \in (Q (i), Q (i + 1)) s \in dom G$
96		dfss3	$⊢ (Q (i), Q (i + 1)) \subseteq dom G \leftrightarrow \forall s \in (Q (i), Q (i + 1)) s \in dom G$
97	95 96	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom G$
98	83 84 97	syl2anc	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to (Q (i), Q (i + 1)) \subseteq dom G$
99		simpl2	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to (i \in (0 ..^M) \land l \in ℤ)$
100	83 99	jca	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to (φ \land (i \in (0 ..^M) \land l \in ℤ))$
101		simpl3	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)$
102		simpr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to t \in (V (J), V (J + 1))$
103	101 102	sseldd	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to t \in (Q (i) + l T, Q (i + 1) + l T)$
104	3	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
105	7 104	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
106	8 105	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
107	106	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
108		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
109	107 108	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
110	109	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
111		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
112	111	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
113	110 112	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
114	113	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
115	114	adantrr	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i) \in ℝ^{*}$
116	115	adantr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i) \in ℝ^{*}$
117		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
118	117	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
119	110 118	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
120	119	adantrr	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i + 1) \in ℝ$
121	120	adantr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i + 1) \in ℝ$
122	121	rexrd	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i + 1) \in ℝ^{*}$
123		elioore	$⊢ t \in (Q (i) + l T, Q (i + 1) + l T) \to t \in ℝ$
124	123	adantl	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t \in ℝ$
125		zre	$⊢ l \in ℤ \to l \in ℝ$
126	125	adantl	$⊢ (i \in (0 ..^M) \land l \in ℤ) \to l \in ℝ$
127	126	ad2antlr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to l \in ℝ$
128	4 5	resubcld	$⊢ φ \to B - A \in ℝ$
129	6 128	eqeltrid	$⊢ φ \to T \in ℝ$
130	129	ad2antrr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to T \in ℝ$
131	127 130	remulcld	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to l T \in ℝ$
132	124 131	resubcld	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t - l T \in ℝ$
133	113	adantrr	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i) \in ℝ$
134	125	ad2antll	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to l \in ℝ$
135	129	adantr	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to T \in ℝ$
136	134 135	remulcld	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to l T \in ℝ$
137	133 136	readdcld	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i) + l T \in ℝ$
138	137	rexrd	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i) + l T \in ℝ^{*}$
139	138	adantr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i) + l T \in ℝ^{*}$
140	120 136	readdcld	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i + 1) + l T \in ℝ$
141	140	rexrd	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ)) \to Q (i + 1) + l T \in ℝ^{*}$
142	141	adantr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i + 1) + l T \in ℝ^{*}$
143		simpr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t \in (Q (i) + l T, Q (i + 1) + l T)$
144		ioogtlb	$⊢ (Q (i) + l T \in ℝ^{} \land Q (i + 1) + l T \in ℝ^{} \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i) + l T < t$
145	139 142 143 144	syl3anc	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i) + l T < t$
146	133	adantr	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i) \in ℝ$
147	146 131 124	ltaddsubd	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to (Q (i) + l T < t \leftrightarrow Q (i) < t - l T)$
148	145 147	mpbid	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to Q (i) < t - l T$
149		iooltub	$⊢ (Q (i) + l T \in ℝ^{} \land Q (i + 1) + l T \in ℝ^{} \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t < Q (i + 1) + l T$
150	139 142 143 149	syl3anc	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t < Q (i + 1) + l T$
151	124 131 121	ltsubaddd	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to (t - l T < Q (i + 1) \leftrightarrow t < Q (i + 1) + l T)$
152	150 151	mpbird	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t - l T < Q (i + 1)$
153	116 122 132 148 152	eliood	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (Q (i) + l T, Q (i + 1) + l T)) \to t - l T \in (Q (i), Q (i + 1))$
154	100 103 153	syl2anc	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to t - l T \in (Q (i), Q (i + 1))$
155	98 154	sseldd	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to t - l T \in dom G$
156		elioore	$⊢ t \in (V (J), V (J + 1)) \to t \in ℝ$
157		recn	$⊢ t \in ℝ \to t \in ℂ$
158	157	adantl	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to t \in ℂ$
159		zcn	$⊢ l \in ℤ \to l \in ℂ$
160	159	ad2antlr	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to l \in ℂ$
161	129	recnd	$⊢ φ \to T \in ℂ$
162	161	ad2antrr	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to T \in ℂ$
163	160 162	mulcld	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to l T \in ℂ$
164	158 163	npcand	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to t - l T + l T = t$
165	164	eqcomd	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to t = t - l T + l T$
166	165	adantr	$⊢ (((φ \land l \in ℤ) \land t \in ℝ) \land t - l T \in dom G) \to t = t - l T + l T$
167		ovex	$⊢ t - l T \in V$
168		eleq1	$⊢ s = t - l T \to (s \in dom G \leftrightarrow t - l T \in dom G)$
169	168	anbi2d	$⊢ s = t - l T \to (((φ \land l \in ℤ) \land s \in dom G) \leftrightarrow ((φ \land l \in ℤ) \land t - l T \in dom G))$
170		oveq1	$⊢ s = t - l T \to s + l T = t - l T + l T$
171	170	eleq1d	$⊢ s = t - l T \to (s + l T \in dom G \leftrightarrow t - l T + l T \in dom G)$
172	170	fveq2d	$⊢ s = t - l T \to G (s + l T) = G (t - l T + l T)$
173		fveq2	$⊢ s = t - l T \to G (s) = G (t - l T)$
174	172 173	eqeq12d	$⊢ s = t - l T \to (G (s + l T) = G (s) \leftrightarrow G (t - l T + l T) = G (t - l T))$
175	171 174	anbi12d	$⊢ s = t - l T \to ((s + l T \in dom G \land G (s + l T) = G (s)) \leftrightarrow (t - l T + l T \in dom G \land G (t - l T + l T) = G (t - l T)))$
176	169 175	imbi12d	$⊢ s = t - l T \to ((((φ \land l \in ℤ) \land s \in dom G) \to (s + l T \in dom G \land G (s + l T) = G (s))) \leftrightarrow (((φ \land l \in ℤ) \land t - l T \in dom G) \to (t - l T + l T \in dom G \land G (t - l T + l T) = G (t - l T))))$
177		ax-resscn	$⊢ ℝ \subseteq ℂ$
178	177	a1i	$⊢ φ \to ℝ \subseteq ℂ$
179	1 178	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
180	179	adantr	$⊢ (φ \land l \in ℤ) \to F : ℝ ⟶ ℂ$
181	125	adantl	$⊢ (φ \land l \in ℤ) \to l \in ℝ$
182	129	adantr	$⊢ (φ \land l \in ℤ) \to T \in ℝ$
183	181 182	remulcld	$⊢ (φ \land l \in ℤ) \to l T \in ℝ$
184	179	ad2antrr	$⊢ ((φ \land l \in ℤ) \land s \in ℝ) \to F : ℝ ⟶ ℂ$
185	129	ad2antrr	$⊢ ((φ \land l \in ℤ) \land s \in ℝ) \to T \in ℝ$
186		simplr	$⊢ ((φ \land l \in ℤ) \land s \in ℝ) \to l \in ℤ$
187		simpr	$⊢ ((φ \land l \in ℤ) \land s \in ℝ) \to s \in ℝ$
188	9	ad4ant14	$⊢ (((φ \land l \in ℤ) \land s \in ℝ) \land x \in ℝ) \to F (x + T) = F (x)$
189	184 185 186 187 188	fperiodmul	$⊢ ((φ \land l \in ℤ) \land s \in ℝ) \to F (s + l T) = F (s)$
190	180 183 189 2	fperdvper	$⊢ ((φ \land l \in ℤ) \land s \in dom G) \to (s + l T \in dom G \land G (s + l T) = G (s))$
191	167 176 190	vtocl	$⊢ ((φ \land l \in ℤ) \land t - l T \in dom G) \to (t - l T + l T \in dom G \land G (t - l T + l T) = G (t - l T))$
192	191	simpld	$⊢ ((φ \land l \in ℤ) \land t - l T \in dom G) \to t - l T + l T \in dom G$
193	192	adantlr	$⊢ (((φ \land l \in ℤ) \land t \in ℝ) \land t - l T \in dom G) \to t - l T + l T \in dom G$
194	166 193	eqeltrd	$⊢ (((φ \land l \in ℤ) \land t \in ℝ) \land t - l T \in dom G) \to t \in dom G$
195	194	ex	$⊢ ((φ \land l \in ℤ) \land t \in ℝ) \to (t - l T \in dom G \to t \in dom G)$
196	156 195	sylan2	$⊢ ((φ \land l \in ℤ) \land t \in (V (J), V (J + 1))) \to (t - l T \in dom G \to t \in dom G)$
197	196	adantlrl	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ)) \land t \in (V (J), V (J + 1))) \to (t - l T \in dom G \to t \in dom G)$
198	197	3adantl3	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to (t - l T \in dom G \to t \in dom G)$
199	155 198	mpd	$⊢ ((φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \land t \in (V (J), V (J + 1))) \to t \in dom G$
200	199	ralrimiva	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \to \forall t \in (V (J), V (J + 1)) t \in dom G$
201		dfss3	$⊢ (V (J), V (J + 1)) \subseteq dom G \leftrightarrow \forall t \in (V (J), V (J + 1)) t \in dom G$
202	200 201	sylibr	$⊢ (φ \land (i \in (0 ..^M) \land l \in ℤ) \land (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)) \to (V (J), V (J + 1)) \subseteq dom G$
203	202	3exp	$⊢ φ \to ((i \in (0 ..^M) \land l \in ℤ) \to ((V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T) \to (V (J), V (J + 1)) \subseteq dom G))$
204	203	rexlimdvv	$⊢ φ \to (\exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T) \to (V (J), V (J + 1)) \subseteq dom G)$
205	82 204	mpd	$⊢ φ \to (V (J), V (J + 1)) \subseteq dom G$
206	205	sselda	$⊢ (φ \land s \in (V (J), V (J + 1))) \to s \in dom G$
207	206	iftrued	$⊢ (φ \land s \in (V (J), V (J + 1))) \to if (s \in dom G, G (s), 0) = G (s)$
208	41 207	eqtr2d	$⊢ (φ \land s \in (V (J), V (J + 1))) \to G (s) = H (s)$
209	208	mpteq2dva	$⊢ φ \to (s \in (V (J), V (J + 1)) ⟼ G (s)) = (s \in (V (J), V (J + 1)) ⟼ H (s))$
210	28	a1i	$⊢ φ \to dom G = dom F_{ℝ}^{'}$
211	210	feq2d	$⊢ φ \to (G : dom G ⟶ ℝ \leftrightarrow G : dom F_{ℝ}^{'} ⟶ ℝ)$
212	25 211	mpbird	$⊢ φ \to G : dom G ⟶ ℝ$
213	212 205	feqresmpt	$⊢ φ \to {G ↾}_{(V (J), V (J + 1))} = (s \in (V (J), V (J + 1)) ⟼ G (s))$
214	38 15	fmptd	$⊢ φ \to H : ℝ ⟶ ℝ$
215	214 17	feqresmpt	$⊢ φ \to {H ↾}_{(V (J), V (J + 1))} = (s \in (V (J), V (J + 1)) ⟼ H (s))$
216	209 213 215	3eqtr4d	$⊢ φ \to {G ↾}_{(V (J), V (J + 1))} = {H ↾}_{(V (J), V (J + 1))}$
217	214 178	fssd	$⊢ φ \to H : ℝ ⟶ ℂ$
218	15	a1i	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to H = (s \in ℝ ⟼ if (s \in dom G, G (s), 0))$
219		eleq1	$⊢ s = x + T \to (s \in dom G \leftrightarrow x + T \in dom G)$
220		fveq2	$⊢ s = x + T \to G (s) = G (x + T)$
221	219 220	ifbieq1d	$⊢ s = x + T \to if (s \in dom G, G (s), 0) = if (x + T \in dom G, G (x + T), 0)$
222	179 129 9 2	fperdvper	$⊢ (φ \land x \in dom G) \to (x + T \in dom G \land G (x + T) = G (x))$
223	222	simpld	$⊢ (φ \land x \in dom G) \to x + T \in dom G$
224	223	iftrued	$⊢ (φ \land x \in dom G) \to if (x + T \in dom G, G (x + T), 0) = G (x + T)$
225	221 224	sylan9eqr	$⊢ ((φ \land x \in dom G) \land s = x + T) \to if (s \in dom G, G (s), 0) = G (x + T)$
226	225	adantllr	$⊢ (((φ \land x \in ℝ) \land x \in dom G) \land s = x + T) \to if (s \in dom G, G (s), 0) = G (x + T)$
227		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
228	129	adantr	$⊢ (φ \land x \in ℝ) \to T \in ℝ$
229	227 228	readdcld	$⊢ (φ \land x \in ℝ) \to x + T \in ℝ$
230	229	adantr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to x + T \in ℝ$
231	212	ad2antrr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to G : dom G ⟶ ℝ$
232	223	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to x + T \in dom G$
233	231 232	ffvelrnd	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to G (x + T) \in ℝ$
234	218 226 230 233	fvmptd	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to H (x + T) = G (x + T)$
235	222	simprd	$⊢ (φ \land x \in dom G) \to G (x + T) = G (x)$
236	235	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to G (x + T) = G (x)$
237		eleq1	$⊢ s = x \to (s \in dom G \leftrightarrow x \in dom G)$
238		fveq2	$⊢ s = x \to G (s) = G (x)$
239	237 238	ifbieq1d	$⊢ s = x \to if (s \in dom G, G (s), 0) = if (x \in dom G, G (x), 0)$
240	239	adantl	$⊢ (((φ \land x \in ℝ) \land x \in dom G) \land s = x) \to if (s \in dom G, G (s), 0) = if (x \in dom G, G (x), 0)$
241		simplr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to x \in ℝ$
242		simpr	$⊢ (φ \land x \in dom G) \to x \in dom G$
243	242	iftrued	$⊢ (φ \land x \in dom G) \to if (x \in dom G, G (x), 0) = G (x)$
244	212	ffvelrnda	$⊢ (φ \land x \in dom G) \to G (x) \in ℝ$
245	243 244	eqeltrd	$⊢ (φ \land x \in dom G) \to if (x \in dom G, G (x), 0) \in ℝ$
246	245	adantlr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to if (x \in dom G, G (x), 0) \in ℝ$
247	218 240 241 246	fvmptd	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to H (x) = if (x \in dom G, G (x), 0)$
248		simpr	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to x \in dom G$
249	248	iftrued	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to if (x \in dom G, G (x), 0) = G (x)$
250	247 249	eqtr2d	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to G (x) = H (x)$
251	234 236 250	3eqtrd	$⊢ ((φ \land x \in ℝ) \land x \in dom G) \to H (x + T) = H (x)$
252	229	recnd	$⊢ (φ \land x \in ℝ) \to x + T \in ℂ$
253	228	recnd	$⊢ (φ \land x \in ℝ) \to T \in ℂ$
254	252 253	negsubd	$⊢ (φ \land x \in ℝ) \to x + T + (- T) = x + T - T$
255	227	recnd	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
256	255 253	pncand	$⊢ (φ \land x \in ℝ) \to x + T - T = x$
257	254 256	eqtr2d	$⊢ (φ \land x \in ℝ) \to x = x + T + (- T)$
258	257	adantr	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to x = x + T + (- T)$
259		simpr	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to x + T \in dom G$
260		simpll	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to φ$
261	260 259	jca	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to (φ \land x + T \in dom G)$
262		eleq1	$⊢ y = x + T \to (y \in dom G \leftrightarrow x + T \in dom G)$
263	262	anbi2d	$⊢ y = x + T \to ((φ \land y \in dom G) \leftrightarrow (φ \land x + T \in dom G))$
264		oveq1	$⊢ y = x + T \to y + (- T) = x + T + (- T)$
265	264	eleq1d	$⊢ y = x + T \to (y + (- T) \in dom G \leftrightarrow x + T + (- T) \in dom G)$
266	264	fveq2d	$⊢ y = x + T \to G (y + (- T)) = G (x + T + (- T))$
267		fveq2	$⊢ y = x + T \to G (y) = G (x + T)$
268	266 267	eqeq12d	$⊢ y = x + T \to (G (y + (- T)) = G (y) \leftrightarrow G (x + T + (- T)) = G (x + T))$
269	265 268	anbi12d	$⊢ y = x + T \to ((y + (- T) \in dom G \land G (y + (- T)) = G (y)) \leftrightarrow (x + T + (- T) \in dom G \land G (x + T + (- T)) = G (x + T)))$
270	263 269	imbi12d	$⊢ y = x + T \to (((φ \land y \in dom G) \to (y + (- T) \in dom G \land G (y + (- T)) = G (y))) \leftrightarrow ((φ \land x + T \in dom G) \to (x + T + (- T) \in dom G \land G (x + T + (- T)) = G (x + T))))$
271	129	renegcld	$⊢ φ \to - T \in ℝ$
272	161	mulm1d	$⊢ φ \to -1 T = - T$
273	272	eqcomd	$⊢ φ \to - T = -1 T$
274	273	adantr	$⊢ (φ \land y \in ℝ) \to - T = -1 T$
275	274	oveq2d	$⊢ (φ \land y \in ℝ) \to y + (- T) = y + -1 T$
276	275	fveq2d	$⊢ (φ \land y \in ℝ) \to F (y + (- T)) = F (y + -1 T)$
277	179	adantr	$⊢ (φ \land y \in ℝ) \to F : ℝ ⟶ ℂ$
278	129	adantr	$⊢ (φ \land y \in ℝ) \to T \in ℝ$
279		1zzd	$⊢ (φ \land y \in ℝ) \to 1 \in ℤ$
280	279	znegcld	$⊢ (φ \land y \in ℝ) \to - 1 \in ℤ$
281		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
282	9	adantlr	$⊢ ((φ \land y \in ℝ) \land x \in ℝ) \to F (x + T) = F (x)$
283	277 278 280 281 282	fperiodmul	$⊢ (φ \land y \in ℝ) \to F (y + -1 T) = F (y)$
284	276 283	eqtrd	$⊢ (φ \land y \in ℝ) \to F (y + (- T)) = F (y)$
285	179 271 284 2	fperdvper	$⊢ (φ \land y \in dom G) \to (y + (- T) \in dom G \land G (y + (- T)) = G (y))$
286	270 285	vtoclg	$⊢ x + T \in dom G \to ((φ \land x + T \in dom G) \to (x + T + (- T) \in dom G \land G (x + T + (- T)) = G (x + T)))$
287	259 261 286	sylc	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to (x + T + (- T) \in dom G \land G (x + T + (- T)) = G (x + T))$
288	287	simpld	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to x + T + (- T) \in dom G$
289	258 288	eqeltrd	$⊢ ((φ \land x \in ℝ) \land x + T \in dom G) \to x \in dom G$
290	289	stoic1a	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to \neg x + T \in dom G$
291	290	iffalsed	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to if (x + T \in dom G, G (x + T), 0) = 0$
292	15	a1i	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to H = (s \in ℝ ⟼ if (s \in dom G, G (s), 0))$
293	221	adantl	$⊢ (((φ \land x \in ℝ) \land \neg x \in dom G) \land s = x + T) \to if (s \in dom G, G (s), 0) = if (x + T \in dom G, G (x + T), 0)$
294	229	adantr	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to x + T \in ℝ$
295		0red	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to 0 \in ℝ$
296	291 295	eqeltrd	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to if (x + T \in dom G, G (x + T), 0) \in ℝ$
297	292 293 294 296	fvmptd	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to H (x + T) = if (x + T \in dom G, G (x + T), 0)$
298		simpr	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to \neg x \in dom G$
299	298	iffalsed	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to if (x \in dom G, G (x), 0) = 0$
300	239 299	sylan9eqr	$⊢ (((φ \land x \in ℝ) \land \neg x \in dom G) \land s = x) \to if (s \in dom G, G (s), 0) = 0$
301		simplr	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to x \in ℝ$
302	292 300 301 295	fvmptd	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to H (x) = 0$
303	291 297 302	3eqtr4d	$⊢ ((φ \land x \in ℝ) \land \neg x \in dom G) \to H (x + T) = H (x)$
304	251 303	pm2.61dan	$⊢ (φ \land x \in ℝ) \to H (x + T) = H (x)$
305		elioore	$⊢ s \in (Q (i), Q (i + 1)) \to s \in ℝ$
306	305	adantl	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
307	305 38	sylan2	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to if (s \in dom G, G (s), 0) \in ℝ$
308	306 307 40	syl2anc	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to H (s) = if (s \in dom G, G (s), 0)$
309	308	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) = if (s \in dom G, G (s), 0)$
310	94	iftrued	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to if (s \in dom G, G (s), 0) = G (s)$
311	309 310	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) = G (s)$
312	311	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ H (s)) = (s \in (Q (i), Q (i + 1)) ⟼ G (s))$
313	214	adantr	$⊢ (φ \land i \in (0 ..^M)) \to H : ℝ ⟶ ℝ$
314		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
315	314	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
316	313 315	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ H (s))$
317	212	adantr	$⊢ (φ \land i \in (0 ..^M)) \to G : dom G ⟶ ℝ$
318	317 97	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {G ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ G (s))$
319	312 316 318	3eqtr4d	$⊢ (φ \land i \in (0 ..^M)) \to {H ↾}_{(Q (i), Q (i + 1))} = {G ↾}_{(Q (i), Q (i + 1))}$
320	319 10	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({H ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
321		eqid	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
322		oveq1	$⊢ z = y \to z + l T = y + l T$
323	322	eleq1d	$⊢ z = y \to (z + l T \in ran Q \leftrightarrow y + l T \in ran Q)$
324	323	rexbidv	$⊢ z = y \to (\exists l \in ℤ z + l T \in ran Q \leftrightarrow \exists l \in ℤ y + l T \in ran Q)$
325	324	cbvrabv	$⊢ \{z \in [C, D] \| \exists l \in ℤ z + l T \in ran Q\} = \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
326	325	uneq2i	$⊢ \{C, D\} \cup \{z \in [C, D] \| \exists l \in ℤ z + l T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
327	326	eqcomi	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{C, D\} \cup \{z \in [C, D] \| \exists l \in ℤ z + l T \in ran Q\}$
328	60	fveq2i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| = \|\{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}\|$
329	328	oveq1i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1$
330		isoeq5	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\} \to (g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
331	67 330	ax-mp	$⊢ g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\})$
332	331	iotabii	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\})) = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
333		isoeq1	$⊢ f = g \to (f {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}))$
334	333	cbviotavw	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\})) = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}))$
335	332 334 14	3eqtr4ri	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}))$
336		id	$⊢ v = x \to v = x$
337		oveq2	$⊢ v = x \to B - v = B - x$
338	337	oveq1d	$⊢ v = x \to \frac{B - v}{T} = \frac{B - x}{T}$
339	338	fveq2d	$⊢ v = x \to ⌊\frac{B - v}{T}⌋ = ⌊\frac{B - x}{T}⌋$
340	339	oveq1d	$⊢ v = x \to ⌊\frac{B - v}{T}⌋ T = ⌊\frac{B - x}{T}⌋ T$
341	336 340	oveq12d	$⊢ v = x \to v + ⌊\frac{B - v}{T}⌋ T = x + ⌊\frac{B - x}{T}⌋ T$
342	341	cbvmptv	$⊢ (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
343		eqeq1	$⊢ u = z \to (u = B \leftrightarrow z = B)$
344		id	$⊢ u = z \to u = z$
345	343 344	ifbieq2d	$⊢ u = z \to if (u = B, A, u) = if (z = B, A, z)$
346	345	cbvmptv	$⊢ (u \in (A, B] ⟼ if (u = B, A, u)) = (z \in (A, B] ⟼ if (z = B, A, z))$
347		eqid	$⊢ V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)) = V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1))$
348		eqid	$⊢ {H ↾}_{((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))), (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)))} = {H ↾}_{((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))), (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)))}$
349		eqid	$⊢ (z \in ((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))) + V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)), (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)) + V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1))) ⟼ ({H ↾}_{((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))), (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)))}) (z - (V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1))))) = (z \in ((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))) + V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)), (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)) + V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1))) ⟼ ({H ↾}_{((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))), (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)))}) (z - (V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)))))$
350		fveq2	$⊢ i = t \to Q (i) = Q (t)$
351	350	breq1d	$⊢ i = t \to (Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)) \leftrightarrow Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)))$
352	351	cbvrabv	$⊢ \{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\} = \{t \in (0 ..^M) \| Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\}$
353		fveq2	$⊢ w = x \to (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w) = (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)$
354	353	fveq2d	$⊢ w = x \to (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w)) = (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))$
355	354	eqcomd	$⊢ w = x \to (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)) = (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w))$
356	355	breq2d	$⊢ w = x \to (Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)) \leftrightarrow Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w)))$
357	356	rabbidv	$⊢ w = x \to \{t \in (0 ..^M) \| Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\} = \{t \in (0 ..^M) \| Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w))\}$
358	352 357	eqtr2id	$⊢ w = x \to \{t \in (0 ..^M) \| Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w))\} = \{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\}$
359	358	supeq1d	$⊢ w = x \to sup (\{t \in (0 ..^M) \| Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\} ℝ <)$
360	359	cbvmptv	$⊢ (w \in ℝ ⟼ sup (\{t \in (0 ..^M) \| Q (t) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (w))\} ℝ <)) = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\} ℝ <))$
361	3 6 7 8 217 304 320 11 12 321 327 329 335 342 346 13 347 348 349 360	fourierdlem90	$⊢ φ \to ({H ↾}_{(V (J), V (J + 1))}) : (V (J), V (J + 1)) \underset{cn}{⟶} ℂ$
362	216 361	eqeltrd	$⊢ φ \to ({G ↾}_{(V (J), V (J + 1))}) : (V (J), V (J + 1)) \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem fourierdlem97

Proof