fourierdlem74

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

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

Proof

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

Metamath Proof Explorer

Theorem fourierdlem74

Proof