fourierdlem75

Description: Given a piecewise smooth function F , the derived function H has a limit at the lower bound of each interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem75.xre	$⊢ φ \to X \in ℝ$
	fourierdlem75.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem75.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem75.x	$⊢ φ \to X \in ran V$
	fourierdlem75.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem75.w	$⊢ φ \to W \in ℝ$
	fourierdlem75.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem75.m	$⊢ φ \to M \in ℕ$
	fourierdlem75.v	$⊢ φ \to V \in P (M)$
	fourierdlem75.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
	fourierdlem75.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem75.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem75.g	$⊢ G = ℝ D F$
	fourierdlem75.gcn	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
	fourierdlem75.e	$⊢ φ \to E \in (({G ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem75.a	$⊢ A = if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)})$
Assertion	fourierdlem75	$⊢ (φ \land i \in (0 ..^M)) \to A \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem75.xre	$⊢ φ \to X \in ℝ$
2		fourierdlem75.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
3		fourierdlem75.f	$⊢ φ \to F : ℝ ⟶ ℝ$
4		fourierdlem75.x	$⊢ φ \to X \in ran V$
5		fourierdlem75.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
6		fourierdlem75.w	$⊢ φ \to W \in ℝ$
7		fourierdlem75.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
8		fourierdlem75.m	$⊢ φ \to M \in ℕ$
9		fourierdlem75.v	$⊢ φ \to V \in P (M)$
10		fourierdlem75.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
11		fourierdlem75.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
12		fourierdlem75.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
13		fourierdlem75.g	$⊢ G = ℝ D F$
14		fourierdlem75.gcn	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
15		fourierdlem75.e	$⊢ φ \to E \in (({G ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
16		fourierdlem75.a	$⊢ A = if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)})$
17	1	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to X \in ℝ$
18	2	fourierdlem2	$⊢ M \in ℕ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
19	8 18	syl	$⊢ φ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
20	9 19	mpbid	$⊢ φ \to (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1)))$
21	20	simpld	$⊢ φ \to V \in (ℝ^{(0 \dots M)})$
22		elmapi	$⊢ V \in (ℝ^{(0 \dots M)}) \to V : (0 \dots M) ⟶ ℝ$
23	21 22	syl	$⊢ φ \to V : (0 \dots M) ⟶ ℝ$
24	23	adantr	$⊢ (φ \land i \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
25		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
26	25	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
27	24 26	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ$
28	27	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to V (i + 1) \in ℝ$
29		eqcom	$⊢ V (i) = X \leftrightarrow X = V (i)$
30	29	bilani	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to X = V (i)$
31	20	simprrd	$⊢ φ \to \forall i \in (0 ..^M) V (i) < V (i + 1)$
32	31	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to V (i) < V (i + 1)$
33	32	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to V (i) < V (i + 1)$
34	30 33	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to X < V (i + 1)$
35	3	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℝ$
36		ioossre	$⊢ (X, V (i + 1)) \subseteq ℝ$
37	36	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (X, V (i + 1)) \subseteq ℝ$
38	35 37	fssresd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(X, V (i + 1))}) : (X, V (i + 1)) ⟶ ℝ$
39	38	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to ({F ↾}_{(X, V (i + 1))}) : (X, V (i + 1)) ⟶ ℝ$
40		limcresi	$⊢ ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \subseteq ({({F ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X$
41	40 5	sselid	$⊢ φ \to Y \in (({({F ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X)$
42	41	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Y \in (({({F ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X)$
43		pnfxr	$⊢ +∞ \in ℝ^{*}$
44	43	a1i	$⊢ (φ \land i \in (0 ..^M)) \to +∞ \in ℝ^{*}$
45	27	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ^{*}$
46	27	ltpnfd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) < +∞$
47	45 44 46	xrltled	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \leq +∞$
48		iooss2	$⊢ (+∞ \in ℝ^{*} \land V (i + 1) \leq +∞) \to (X, V (i + 1)) \subseteq (X, +∞)$
49	44 47 48	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (X, V (i + 1)) \subseteq (X, +∞)$
50	49	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))} = {F ↾}_{(X, V (i + 1))}$
51	50	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X = ({F ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X$
52	42 51	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to Y \in (({F ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X)$
53	52	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to Y \in (({F ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X)$
54		eqid	$⊢ ℝ D ({F ↾}_{(X, V (i + 1))}) = ℝ D ({F ↾}_{(X, V (i + 1))})$
55		ax-resscn	$⊢ ℝ \subseteq ℂ$
56	55	a1i	$⊢ φ \to ℝ \subseteq ℂ$
57	3 56	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
58		ssid	$⊢ ℝ \subseteq ℝ$
59	58	a1i	$⊢ φ \to ℝ \subseteq ℝ$
60	36	a1i	$⊢ φ \to (X, V (i + 1)) \subseteq ℝ$
61		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
62		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
63	61 62	dvres	$⊢ ((ℝ \subseteq ℂ \land F : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land (X, V (i + 1)) \subseteq ℝ)) \to ℝ D ({F ↾}_{(X, V (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((X, V (i + 1)))}$
64	56 57 59 60 63	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{(X, V (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((X, V (i + 1)))}$
65	13	eqcomi	$⊢ ℝ D F = G$
66		ioontr	$⊢ int (topGen (ran (.))) ((X, V (i + 1))) = (X, V (i + 1))$
67	65 66	reseq12i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((X, V (i + 1)))} = {G ↾}_{(X, V (i + 1))}$
68	64 67	eqtrdi	$⊢ φ \to ℝ D ({F ↾}_{(X, V (i + 1))}) = {G ↾}_{(X, V (i + 1))}$
69	68	adantr	$⊢ (φ \land V (i) = X) \to ℝ D ({F ↾}_{(X, V (i + 1))}) = {G ↾}_{(X, V (i + 1))}$
70	69	dmeqd	$⊢ (φ \land V (i) = X) \to dom {({F ↾}_{(X, V (i + 1))})}_{ℝ}^{'} = dom ({G ↾}_{(X, V (i + 1))})$
71	70	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to dom {({F ↾}_{(X, V (i + 1))})}_{ℝ}^{'} = dom ({G ↾}_{(X, V (i + 1))})$
72	14	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to ({G ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
73		oveq1	$⊢ V (i) = X \to (V (i), V (i + 1)) = (X, V (i + 1))$
74	73	reseq2d	$⊢ V (i) = X \to {G ↾}_{(V (i), V (i + 1))} = {G ↾}_{(X, V (i + 1))}$
75	74	feq1d	$⊢ V (i) = X \to (({G ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ \leftrightarrow ({G ↾}_{(X, V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ)$
76	75	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to (({G ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ \leftrightarrow ({G ↾}_{(X, V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ)$
77	72 76	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to ({G ↾}_{(X, V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
78	73	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to (V (i), V (i + 1)) = (X, V (i + 1))$
79	78	feq2d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to (({G ↾}_{(X, V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ \leftrightarrow ({G ↾}_{(X, V (i + 1))}) : (X, V (i + 1)) ⟶ ℂ)$
80	77 79	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to ({G ↾}_{(X, V (i + 1))}) : (X, V (i + 1)) ⟶ ℂ$
81		fdm	$⊢ ({G ↾}_{(X, V (i + 1))}) : (X, V (i + 1)) ⟶ ℂ \to dom ({G ↾}_{(X, V (i + 1))}) = (X, V (i + 1))$
82	80 81	syl	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to dom ({G ↾}_{(X, V (i + 1))}) = (X, V (i + 1))$
83	71 82	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to dom {({F ↾}_{(X, V (i + 1))})}_{ℝ}^{'} = (X, V (i + 1))$
84		limcresi	$⊢ ({G ↾}_{(X, +∞)}) {lim}_{ℂ} X \subseteq ({({G ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X$
85	84 15	sselid	$⊢ φ \to E \in (({({G ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X)$
86	85	adantr	$⊢ (φ \land i \in (0 ..^M)) \to E \in (({({G ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X)$
87	49	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({G ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))} = {G ↾}_{(X, V (i + 1))}$
88	68	adantr	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(X, V (i + 1))}) = {G ↾}_{(X, V (i + 1))}$
89	87 88	eqtr4d	$⊢ (φ \land i \in (0 ..^M)) \to {({G ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))} = ℝ D ({F ↾}_{(X, V (i + 1))})$
90	89	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({({G ↾}_{(X, +∞)}) ↾}_{(X, V (i + 1))}) {lim}_{ℂ} X = {({F ↾}_{(X, V (i + 1))})}_{ℝ}^{'} {lim}_{ℂ} X$
91	86 90	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to E \in ({({F ↾}_{(X, V (i + 1))})}_{ℝ}^{'} {lim}_{ℂ} X)$
92	91	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to E \in ({({F ↾}_{(X, V (i + 1))})}_{ℝ}^{'} {lim}_{ℂ} X)$
93		eqid	$⊢ (s \in (0, V (i + 1) - X) ⟼ \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s}) = (s \in (0, V (i + 1) - X) ⟼ \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s})$
94		oveq2	$⊢ x = s \to X + x = X + s$
95	94	fveq2d	$⊢ x = s \to ({F ↾}_{(X, V (i + 1))}) (X + x) = ({F ↾}_{(X, V (i + 1))}) (X + s)$
96	95	oveq1d	$⊢ x = s \to ({F ↾}_{(X, V (i + 1))}) (X + x) - Y = ({F ↾}_{(X, V (i + 1))}) (X + s) - Y$
97	96	cbvmptv	$⊢ (x \in (0, V (i + 1) - X) ⟼ ({F ↾}_{(X, V (i + 1))}) (X + x) - Y) = (s \in (0, V (i + 1) - X) ⟼ ({F ↾}_{(X, V (i + 1))}) (X + s) - Y)$
98		id	$⊢ x = s \to x = s$
99	98	cbvmptv	$⊢ (x \in (0, V (i + 1) - X) ⟼ x) = (s \in (0, V (i + 1) - X) ⟼ s)$
100	17 28 34 39 53 54 83 92 93 97 99	fourierdlem61	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to E \in ((s \in (0, V (i + 1) - X) ⟼ \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s}) {lim}_{ℂ} 0)$
101		iftrue	$⊢ V (i) = X \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) = E$
102	16 101	eqtrid	$⊢ V (i) = X \to A = E$
103	102	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to A = E$
104	7	reseq1i	$⊢ {H ↾}_{(Q (i), Q (i + 1))} = {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(Q (i), Q (i + 1))}$
105	104	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to {H ↾}_{(Q (i), Q (i + 1))} = {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(Q (i), Q (i + 1))}$
106		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
107		pire	$⊢ π \in ℝ$
108	107	renegcli	$⊢ - π \in ℝ$
109	108	rexri	$⊢ - π \in ℝ^{*}$
110	109	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
111	107	rexri	$⊢ π \in ℝ^{*}$
112	111	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
113	108	a1i	$⊢ (φ \land i \in (0 \dots M)) \to - π \in ℝ$
114	107	a1i	$⊢ (φ \land i \in (0 \dots M)) \to π \in ℝ$
115	108	a1i	$⊢ φ \to - π \in ℝ$
116	115 1	readdcld	$⊢ φ \to - π + X \in ℝ$
117	107	a1i	$⊢ φ \to π \in ℝ$
118	117 1	readdcld	$⊢ φ \to π + X \in ℝ$
119	116 118	iccssred	$⊢ φ \to [- π + X, π + X] \subseteq ℝ$
120	119	adantr	$⊢ (φ \land i \in (0 \dots M)) \to [- π + X, π + X] \subseteq ℝ$
121	2 8 9	fourierdlem15	$⊢ φ \to V : (0 \dots M) ⟶ [- π + X, π + X]$
122	121	ffvelcdmda	$⊢ (φ \land i \in (0 \dots M)) \to V (i) \in [- π + X, π + X]$
123	120 122	sseldd	$⊢ (φ \land i \in (0 \dots M)) \to V (i) \in ℝ$
124	1	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℝ$
125	123 124	resubcld	$⊢ (φ \land i \in (0 \dots M)) \to V (i) - X \in ℝ$
126	115	recnd	$⊢ φ \to - π \in ℂ$
127	1	recnd	$⊢ φ \to X \in ℂ$
128	126 127	pncand	$⊢ φ \to (- π) + X - X = - π$
129	128	eqcomd	$⊢ φ \to - π = (- π) + X - X$
130	129	adantr	$⊢ (φ \land i \in (0 \dots M)) \to - π = (- π) + X - X$
131	116	adantr	$⊢ (φ \land i \in (0 \dots M)) \to - π + X \in ℝ$
132	118	adantr	$⊢ (φ \land i \in (0 \dots M)) \to π + X \in ℝ$
133		elicc2	$⊢ (- π + X \in ℝ \land π + X \in ℝ) \to (V (i) \in [- π + X, π + X] \leftrightarrow (V (i) \in ℝ \land - π + X \leq V (i) \land V (i) \leq π + X))$
134	131 132 133	syl2anc	$⊢ (φ \land i \in (0 \dots M)) \to (V (i) \in [- π + X, π + X] \leftrightarrow (V (i) \in ℝ \land - π + X \leq V (i) \land V (i) \leq π + X))$
135	122 134	mpbid	$⊢ (φ \land i \in (0 \dots M)) \to (V (i) \in ℝ \land - π + X \leq V (i) \land V (i) \leq π + X)$
136	135	simp2d	$⊢ (φ \land i \in (0 \dots M)) \to - π + X \leq V (i)$
137	131 123 124 136	lesub1dd	$⊢ (φ \land i \in (0 \dots M)) \to (- π) + X - X \leq V (i) - X$
138	130 137	eqbrtrd	$⊢ (φ \land i \in (0 \dots M)) \to - π \leq V (i) - X$
139	135	simp3d	$⊢ (φ \land i \in (0 \dots M)) \to V (i) \leq π + X$
140	123 132 124 139	lesub1dd	$⊢ (φ \land i \in (0 \dots M)) \to V (i) - X \leq π + X - X$
141	114	recnd	$⊢ (φ \land i \in (0 \dots M)) \to π \in ℂ$
142	127	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℂ$
143	141 142	pncand	$⊢ (φ \land i \in (0 \dots M)) \to π + X - X = π$
144	140 143	breqtrd	$⊢ (φ \land i \in (0 \dots M)) \to V (i) - X \leq π$
145	113 114 125 138 144	eliccd	$⊢ (φ \land i \in (0 \dots M)) \to V (i) - X \in [- π, π]$
146	145 11	fmptd	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
147	146	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
148		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
149	110 112 147 148	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
150	106 149	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
151	150	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
152	151	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
153		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
154		simpr	$⊢ (φ \land i \in (0 \dots M)) \to i \in (0 \dots M)$
155	11	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in [- π, π]) \to Q (i) = V (i) - X$
156	154 145 155	syl2anc	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) = V (i) - X$
157	156	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land V (i) = X) \to Q (i) = V (i) - X$
158		oveq1	$⊢ V (i) = X \to V (i) - X = X - X$
159	158	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land V (i) = X) \to V (i) - X = X - X$
160	127	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land V (i) = X) \to X \in ℂ$
161	160	subidd	$⊢ ((φ \land i \in (0 \dots M)) \land V (i) = X) \to X - X = 0$
162	157 159 161	3eqtrd	$⊢ ((φ \land i \in (0 \dots M)) \land V (i) = X) \to Q (i) = 0$
163	153 162	sylanl2	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to Q (i) = 0$
164		fveq2	$⊢ i = j \to V (i) = V (j)$
165	164	oveq1d	$⊢ i = j \to V (i) - X = V (j) - X$
166	165	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ V (i) - X) = (j \in (0 \dots M) ⟼ V (j) - X)$
167	11 166	eqtri	$⊢ Q = (j \in (0 \dots M) ⟼ V (j) - X)$
168	167	a1i	$⊢ (φ \land i \in (0 ..^M)) \to Q = (j \in (0 \dots M) ⟼ V (j) - X)$
169		fveq2	$⊢ j = i + 1 \to V (j) = V (i + 1)$
170	169	oveq1d	$⊢ j = i + 1 \to V (j) - X = V (i + 1) - X$
171	170	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to V (j) - X = V (i + 1) - X$
172	1	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
173	27 172	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) - X \in ℝ$
174	168 171 26 173	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = V (i + 1) - X$
175	174	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to Q (i + 1) = V (i + 1) - X$
176	163 175	oveq12d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to (Q (i), Q (i + 1)) = (0, V (i + 1) - X)$
177		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \land s = 0) \to s \in (Q (i), Q (i + 1))$
178	8	adantr	$⊢ (φ \land s = 0) \to M \in ℕ$
179	115 117 1 2 12 8 9 11	fourierdlem14	$⊢ φ \to Q \in O (M)$
180	179	adantr	$⊢ (φ \land s = 0) \to Q \in O (M)$
181		simpr	$⊢ (φ \land s = 0) \to s = 0$
182		ffn	$⊢ V : (0 \dots M) ⟶ [- π + X, π + X] \to V Fn (0 \dots M)$
183		fvelrnb	$⊢ V Fn (0 \dots M) \to (X \in ran V \leftrightarrow \exists i \in (0 \dots M) V (i) = X)$
184	121 182 183	3syl	$⊢ φ \to (X \in ran V \leftrightarrow \exists i \in (0 \dots M) V (i) = X)$
185	4 184	mpbid	$⊢ φ \to \exists i \in (0 \dots M) V (i) = X$
186	162	ex	$⊢ (φ \land i \in (0 \dots M)) \to (V (i) = X \to Q (i) = 0)$
187	186	reximdva	$⊢ φ \to (\exists i \in (0 \dots M) V (i) = X \to \exists i \in (0 \dots M) Q (i) = 0)$
188	185 187	mpd	$⊢ φ \to \exists i \in (0 \dots M) Q (i) = 0$
189	125 11	fmptd	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
190		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
191		fvelrnb	$⊢ Q Fn (0 \dots M) \to (0 \in ran Q \leftrightarrow \exists i \in (0 \dots M) Q (i) = 0)$
192	189 190 191	3syl	$⊢ φ \to (0 \in ran Q \leftrightarrow \exists i \in (0 \dots M) Q (i) = 0)$
193	188 192	mpbird	$⊢ φ \to 0 \in ran Q$
194	193	adantr	$⊢ (φ \land s = 0) \to 0 \in ran Q$
195	181 194	eqeltrd	$⊢ (φ \land s = 0) \to s \in ran Q$
196	12 178 180 195	fourierdlem12	$⊢ ((φ \land s = 0) \land i \in (0 ..^M)) \to \neg s \in (Q (i), Q (i + 1))$
197	196	an32s	$⊢ ((φ \land i \in (0 ..^M)) \land s = 0) \to \neg s \in (Q (i), Q (i + 1))$
198	197	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \land s = 0) \to \neg s \in (Q (i), Q (i + 1))$
199	177 198	pm2.65da	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to \neg s = 0$
200	199	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to \neg s = 0$
201	200	iffalsed	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) = \frac{F (X + s) - if (0 < s, Y, W)}{s}$
202	163	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to 0 = Q (i)$
203	202	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to 0 = Q (i)$
204		elioo3g	$⊢ s \in (Q (i), Q (i + 1)) \leftrightarrow ((Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land s \in ℝ^{*}) \land (Q (i) < s \land s < Q (i + 1)))$
205	204	biimpi	$⊢ s \in (Q (i), Q (i + 1)) \to ((Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land s \in ℝ^{*}) \land (Q (i) < s \land s < Q (i + 1)))$
206	205	simprld	$⊢ s \in (Q (i), Q (i + 1)) \to Q (i) < s$
207	206	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to Q (i) < s$
208	203 207	eqbrtrd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to 0 < s$
209	208	iftrued	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to if (0 < s, Y, W) = Y$
210	209	oveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) - if (0 < s, Y, W) = F (X + s) - Y$
211	210	oveq1d	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to \frac{F (X + s) - if (0 < s, Y, W)}{s} = \frac{F (X + s) - Y}{s}$
212	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
213	212	ad3antrrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to X \in ℝ^{*}$
214	45	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to V (i + 1) \in ℝ^{*}$
215	172	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to X \in ℝ$
216		elioore	$⊢ s \in (Q (i), Q (i + 1)) \to s \in ℝ$
217	216	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
218	215 217	readdcld	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to X + s \in ℝ$
219	217 208	elrpd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to s \in ℝ^{+}$
220	215 219	ltaddrpd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to X < X + s$
221	216	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
222	189	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
223	222 26	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
224	223	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ$
225	1	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X \in ℝ$
226	205	simprrd	$⊢ s \in (Q (i), Q (i + 1)) \to s < Q (i + 1)$
227	226	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s < Q (i + 1)$
228	221 224 225 227	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s < X + Q (i + 1)$
229	174	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i + 1) = X + V (i + 1) - X$
230	127	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℂ$
231	27	recnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℂ$
232	230 231	pncan3d	$⊢ (φ \land i \in (0 ..^M)) \to X + V (i + 1) - X = V (i + 1)$
233	229 232	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i + 1) = V (i + 1)$
234	233	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + Q (i + 1) = V (i + 1)$
235	228 234	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s < V (i + 1)$
236	235	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to X + s < V (i + 1)$
237	213 214 218 220 236	eliood	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to X + s \in (X, V (i + 1))$
238		fvres	$⊢ X + s \in (X, V (i + 1)) \to ({F ↾}_{(X, V (i + 1))}) (X + s) = F (X + s)$
239	237 238	syl	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to ({F ↾}_{(X, V (i + 1))}) (X + s) = F (X + s)$
240	239	eqcomd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) = ({F ↾}_{(X, V (i + 1))}) (X + s)$
241	240	oveq1d	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) - Y = ({F ↾}_{(X, V (i + 1))}) (X + s) - Y$
242	241	oveq1d	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to \frac{F (X + s) - Y}{s} = \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s}$
243	201 211 242	3eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) = X) \land s \in (Q (i), Q (i + 1))) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) = \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s}$
244	176 243	mpteq12dva	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to (s \in (Q (i), Q (i + 1)) ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) = (s \in (0, V (i + 1) - X) ⟼ \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s})$
245	105 152 244	3eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (0, V (i + 1) - X) ⟼ \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s})$
246	245 163	oveq12d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to ({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (0, V (i + 1) - X) ⟼ \frac{({F ↾}_{(X, V (i + 1))}) (X + s) - Y}{s}) {lim}_{ℂ} 0$
247	100 103 246	3eltr4d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) = X) \to A \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
248		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W))$
249		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ s) = (s \in (Q (i), Q (i + 1)) ⟼ s)$
250		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s}) = (s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s})$
251	3	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to F : ℝ ⟶ ℝ$
252	1	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to X \in ℝ$
253	216	adantl	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
254	252 253	readdcld	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to X + s \in ℝ$
255	251 254	ffvelcdmd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℝ$
256	255	recnd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℂ$
257	256	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℂ$
258	257	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℂ$
259		limccl	$⊢ ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \subseteq ℂ$
260	259 5	sselid	$⊢ φ \to Y \in ℂ$
261	6	recnd	$⊢ φ \to W \in ℂ$
262	260 261	ifcld	$⊢ φ \to if (0 < s, Y, W) \in ℂ$
263	262	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to if (0 < s, Y, W) \in ℂ$
264	263	3ad2antl1	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to if (0 < s, Y, W) \in ℂ$
265	258 264	subcld	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) - if (0 < s, Y, W) \in ℂ$
266	216	recnd	$⊢ s \in (Q (i), Q (i + 1)) \to s \in ℂ$
267	266	adantl	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to s \in ℂ$
268		velsn	$⊢ s \in \{0\} \leftrightarrow s = 0$
269	199 268	sylnibr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to \neg s \in \{0\}$
270	269	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to \neg s \in \{0\}$
271	267 270	eldifd	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to s \in (ℂ ∖ \{0\})$
272		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s))$
273		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ W) = (s \in (Q (i), Q (i + 1)) ⟼ W)$
274		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - W) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - W)$
275	261	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to W \in ℂ$
276		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
277	276	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
278	153 123	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
279	278	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ^{*}$
280	279	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i) \in ℝ^{*}$
281	45	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i + 1) \in ℝ^{*}$
282	254	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s \in ℝ$
283		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
284	108 107 283	mp2an	$⊢ [- π, π] \subseteq ℝ$
285	284 55	sstri	$⊢ [- π, π] \subseteq ℂ$
286	156 145	eqeltrd	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in [- π, π]$
287	153 286	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [- π, π]$
288	285 287	sselid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
289	230 288	addcomd	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i) = Q (i) + X$
290	153	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
291	153 125	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X \in ℝ$
292	11	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in ℝ) \to Q (i) = V (i) - X$
293	290 291 292	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = V (i) - X$
294	293	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + X = V (i) - X + X$
295	278	recnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℂ$
296	295 230	npcand	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X + X = V (i)$
297	289 294 296	3eqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) = X + Q (i)$
298	297	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i) = X + Q (i)$
299	293 291	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
300	299	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ$
301	206	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i) < s$
302	300 221 225 301	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + Q (i) < X + s$
303	298 302	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i) < X + s$
304	280 281 282 303 235	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s \in (V (i), V (i + 1))$
305		ioossre	$⊢ (V (i), V (i + 1)) \subseteq ℝ$
306	305	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (V (i), V (i + 1)) \subseteq ℝ$
307	300 301	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \neq Q (i)$
308	297	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i) = ({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} (X + Q (i))$
309	10 308	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} (X + Q (i)))$
310	35 172 277 272 304 306 307 309 288	fourierdlem53	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) {lim}_{ℂ} Q (i))$
311		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
312	311	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
313	261	adantr	$⊢ (φ \land i \in (0 ..^M)) \to W \in ℂ$
314	273 312 313 288	constlimc	$⊢ (φ \land i \in (0 ..^M)) \to W \in ((s \in (Q (i), Q (i + 1)) ⟼ W) {lim}_{ℂ} Q (i))$
315	272 273 274 257 275 310 314	sublimc	$⊢ (φ \land i \in (0 ..^M)) \to R - W \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - W) {lim}_{ℂ} Q (i))$
316	315	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to R - W \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - W) {lim}_{ℂ} Q (i))$
317		iftrue	$⊢ V (i) < X \to if (V (i) < X, W, Y) = W$
318	317	oveq2d	$⊢ V (i) < X \to R - if (V (i) < X, W, Y) = R - W$
319	318	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to R - if (V (i) < X, W, Y) = R - W$
320	216	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
321		0red	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to 0 \in ℝ$
322	223	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ$
323	226	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to s < Q (i + 1)$
324	174	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to Q (i + 1) = V (i + 1) - X$
325	279	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to V (i) \in ℝ^{*}$
326	45	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to V (i + 1) \in ℝ^{*}$
327	172	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to X \in ℝ$
328		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to V (i) < X$
329		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i + 1) \leq X) \to \neg V (i + 1) \leq X$
330	1	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i + 1) \leq X) \to X \in ℝ$
331	27	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i + 1) \leq X) \to V (i + 1) \in ℝ$
332	330 331	ltnled	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i + 1) \leq X) \to (X < V (i + 1) \leftrightarrow \neg V (i + 1) \leq X)$
333	329 332	mpbird	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i + 1) \leq X) \to X < V (i + 1)$
334	333	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to X < V (i + 1)$
335	325 326 327 328 334	eliood	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to X \in (V (i), V (i + 1))$
336	2 8 9 4	fourierdlem12	$⊢ (φ \land i \in (0 ..^M)) \to \neg X \in (V (i), V (i + 1))$
337	336	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land \neg V (i + 1) \leq X) \to \neg X \in (V (i), V (i + 1))$
338	335 337	condan	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to V (i + 1) \leq X$
339	27	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to V (i + 1) \in ℝ$
340	1	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to X \in ℝ$
341	339 340	suble0d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to (V (i + 1) - X \leq 0 \leftrightarrow V (i + 1) \leq X)$
342	338 341	mpbird	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to V (i + 1) - X \leq 0$
343	324 342	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to Q (i + 1) \leq 0$
344	343	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to Q (i + 1) \leq 0$
345	320 322 321 323 344	ltletrd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to s < 0$
346	320 321 345	ltnsymd	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to \neg 0 < s$
347	346	iffalsed	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to if (0 < s, Y, W) = W$
348	347	oveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land V (i) < X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) - if (0 < s, Y, W) = F (X + s) - W$
349	348	mpteq2dva	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - W)$
350	349	oveq1d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - W) {lim}_{ℂ} Q (i)$
351	316 319 350	3eltr4d	$⊢ ((φ \land i \in (0 ..^M)) \land V (i) < X) \to R - if (V (i) < X, W, Y) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i))$
352	351	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land V (i) < X) \to R - if (V (i) < X, W, Y) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i))$
353		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ Y) = (s \in (Q (i), Q (i + 1)) ⟼ Y)$
354		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - Y) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - Y)$
355	260	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Y \in ℂ$
356	260	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Y \in ℂ$
357	353 312 356 288	constlimc	$⊢ (φ \land i \in (0 ..^M)) \to Y \in ((s \in (Q (i), Q (i + 1)) ⟼ Y) {lim}_{ℂ} Q (i))$
358	272 353 354 257 355 310 357	sublimc	$⊢ (φ \land i \in (0 ..^M)) \to R - Y \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - Y) {lim}_{ℂ} Q (i))$
359	358	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to R - Y \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - Y) {lim}_{ℂ} Q (i))$
360		iffalse	$⊢ \neg V (i) < X \to if (V (i) < X, W, Y) = Y$
361	360	oveq2d	$⊢ \neg V (i) < X \to R - if (V (i) < X, W, Y) = R - Y$
362	361	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to R - if (V (i) < X, W, Y) = R - Y$
363		0red	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to 0 \in ℝ$
364	299	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ$
365	216	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
366	1	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to X \in ℝ$
367	278	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to V (i) \in ℝ$
368		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to \neg V (i) < X$
369	366 367 368	nltled	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to X \leq V (i)$
370	367 366	subge0d	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to (0 \leq V (i) - X \leftrightarrow X \leq V (i))$
371	369 370	mpbird	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to 0 \leq V (i) - X$
372	293	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X = Q (i)$
373	372	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to V (i) - X = Q (i)$
374	371 373	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to 0 \leq Q (i)$
375	374	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to 0 \leq Q (i)$
376	206	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to Q (i) < s$
377	363 364 365 375 376	lelttrd	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to 0 < s$
378	377	iftrued	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to if (0 < s, Y, W) = Y$
379	378	oveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \land s \in (Q (i), Q (i + 1))) \to F (X + s) - if (0 < s, Y, W) = F (X + s) - Y$
380	379	mpteq2dva	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - Y)$
381	380	oveq1d	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - Y) {lim}_{ℂ} Q (i)$
382	359 362 381	3eltr4d	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) < X) \to R - if (V (i) < X, W, Y) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i))$
383	382	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land \neg V (i) < X) \to R - if (V (i) < X, W, Y) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i))$
384	352 383	pm2.61dan	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to R - if (V (i) < X, W, Y) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) - if (0 < s, Y, W)) {lim}_{ℂ} Q (i))$
385	312 249 288	idlimc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((s \in (Q (i), Q (i + 1)) ⟼ s) {lim}_{ℂ} Q (i))$
386	385	3adant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to Q (i) \in ((s \in (Q (i), Q (i + 1)) ⟼ s) {lim}_{ℂ} Q (i))$
387	293	3adant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to Q (i) = V (i) - X$
388	295	3adant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to V (i) \in ℂ$
389	230	3adant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to X \in ℂ$
390		neqne	$⊢ \neg V (i) = X \to V (i) \neq X$
391	390	3ad2ant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to V (i) \neq X$
392	388 389 391	subne0d	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to V (i) - X \neq 0$
393	387 392	eqnetrd	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to Q (i) \neq 0$
394	199	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to \neg s = 0$
395	394	neqned	$⊢ ((φ \land i \in (0 ..^M) \land \neg V (i) = X) \land s \in (Q (i), Q (i + 1))) \to s \neq 0$
396	248 249 250 265 271 384 386 393 395	divlimc	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to \frac{R - if (V (i) < X, W, Y)}{Q (i)} \in ((s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s}) {lim}_{ℂ} Q (i))$
397		iffalse	$⊢ \neg V (i) = X \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) = \frac{R - if (V (i) < X, W, Y)}{Q (i)}$
398	16 397	eqtrid	$⊢ \neg V (i) = X \to A = \frac{R - if (V (i) < X, W, Y)}{Q (i)}$
399	398	3ad2ant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to A = \frac{R - if (V (i) < X, W, Y)}{Q (i)}$
400		ioossre	$⊢ (X, +∞) \subseteq ℝ$
401	400	a1i	$⊢ φ \to (X, +∞) \subseteq ℝ$
402	3 401	fssresd	$⊢ φ \to ({F ↾}_{(X, +∞)}) : (X, +∞) ⟶ ℝ$
403	400 56	sstrid	$⊢ φ \to (X, +∞) \subseteq ℂ$
404	43	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
405	1	ltpnfd	$⊢ φ \to X < +∞$
406	61 404 1 405	lptioo1cn	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞))$
407	402 403 406 5	limcrecl	$⊢ φ \to Y \in ℝ$
408	3 1 407 6 7	fourierdlem9	$⊢ φ \to H : [- π, π] ⟶ ℝ$
409	408	adantr	$⊢ (φ \land i \in (0 ..^M)) \to H : [- π, π] ⟶ ℝ$
410	409 150	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ H (s))$
411	150	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in [- π, π]$
412		0cnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to 0 \in ℂ$
413	262	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to if (0 < s, Y, W) \in ℂ$
414	257 413	subcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to F (X + s) - if (0 < s, Y, W) \in ℂ$
415	266	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in ℂ$
416	199	neqned	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \neq 0$
417	414 415 416	divcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to \frac{F (X + s) - if (0 < s, Y, W)}{s} \in ℂ$
418	412 417	ifcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) \in ℂ$
419	7	fvmpt2	$⊢ (s \in [- π, π] \land if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) \in ℂ) \to H (s) = if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})$
420	411 418 419	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) = if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})$
421	199	iffalsed	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) = \frac{F (X + s) - if (0 < s, Y, W)}{s}$
422	420 421	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) = \frac{F (X + s) - if (0 < s, Y, W)}{s}$
423	422	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ H (s)) = (s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s})$
424	410 423	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s})$
425	424	3adant3	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s})$
426	425	oveq1d	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to ({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ \frac{F (X + s) - if (0 < s, Y, W)}{s}) {lim}_{ℂ} Q (i)$
427	396 399 426	3eltr4d	$⊢ (φ \land i \in (0 ..^M) \land \neg V (i) = X) \to A \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
428	427	3expa	$⊢ ((φ \land i \in (0 ..^M)) \land \neg V (i) = X) \to A \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
429	247 428	pm2.61dan	$⊢ (φ \land i \in (0 ..^M)) \to A \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$

Metamath Proof Explorer

Theorem fourierdlem75

Proof