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