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