fourierdlem81

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T . In this lemma, T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem81.a	$⊢ φ \to A \in ℝ$
	fourierdlem81.b	$⊢ φ \to B \in ℝ$
	fourierdlem81.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem81.m	$⊢ φ \to M \in ℕ$
	fourierdlem81.t	$⊢ φ \to T \in ℝ^{+}$
	fourierdlem81.q	$⊢ φ \to Q \in P (M)$
	fourierdlem81.fper	$⊢ (φ \land x \in [A, B]) \to F (x + T) = F (x)$
	fourierdlem81.s	$⊢ S = (i \in (0 \dots M) ⟼ Q (i) + T)$
	fourierdlem81.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem81.cncf	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem81.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem81.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem81.g	$⊢ G = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x))))$
	fourierdlem81.h	$⊢ H = (x \in [S (i), S (i + 1)] ⟼ G (x - T))$
Assertion	fourierdlem81	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem81.a	$⊢ φ \to A \in ℝ$
2		fourierdlem81.b	$⊢ φ \to B \in ℝ$
3		fourierdlem81.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
4		fourierdlem81.m	$⊢ φ \to M \in ℕ$
5		fourierdlem81.t	$⊢ φ \to T \in ℝ^{+}$
6		fourierdlem81.q	$⊢ φ \to Q \in P (M)$
7		fourierdlem81.fper	$⊢ (φ \land x \in [A, B]) \to F (x + T) = F (x)$
8		fourierdlem81.s	$⊢ S = (i \in (0 \dots M) ⟼ Q (i) + T)$
9		fourierdlem81.f	$⊢ φ \to F : ℝ ⟶ ℂ$
10		fourierdlem81.cncf	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem81.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
12		fourierdlem81.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
13		fourierdlem81.g	$⊢ G = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x))))$
14		fourierdlem81.h	$⊢ H = (x \in [S (i), S (i + 1)] ⟼ G (x - T))$
15	3	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
16	4 15	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
17	6 16	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
18	17	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
19	18	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
20	19	simpld	$⊢ φ \to Q (0) = A$
21	20	eqcomd	$⊢ φ \to A = Q (0)$
22	19	simprd	$⊢ φ \to Q (M) = B$
23	22	eqcomd	$⊢ φ \to B = Q (M)$
24	21 23	oveq12d	$⊢ φ \to [A, B] = [Q (0), Q (M)]$
25	24	itgeq1d	$⊢ φ \to \int_{[A, B]} F (x) d x = \int_{[Q (0), Q (M)]} F (x) d x$
26		0zd	$⊢ φ \to 0 \in ℤ$
27		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
28		0p1e1	$⊢ 0 + 1 = 1$
29	28	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
30	27 29	eqtr4i	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
31	4 30	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq (0 + 1)}$
32	17	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
33		reex	$⊢ ℝ \in V$
34	33	a1i	$⊢ φ \to ℝ \in V$
35		ovex	$⊢ (0 \dots M) \in V$
36	35	a1i	$⊢ φ \to (0 \dots M) \in V$
37	34 36	elmapd	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \leftrightarrow Q : (0 \dots M) ⟶ ℝ)$
38	32 37	mpbid	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
39	18	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
40	39	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
41	9	adantr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to F : ℝ ⟶ ℂ$
42	20 1	eqeltrd	$⊢ φ \to Q (0) \in ℝ$
43	22 2	eqeltrd	$⊢ φ \to Q (M) \in ℝ$
44	42 43	iccssred	$⊢ φ \to [Q (0), Q (M)] \subseteq ℝ$
45	44	sselda	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in ℝ$
46	41 45	ffvelrnd	$⊢ (φ \land x \in [Q (0), Q (M)]) \to F (x) \in ℂ$
47	38	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
48		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
49	48	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
50	47 49	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
51		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
52	51	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
53	47 52	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
54	9	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
55	54	reseq1d	$⊢ φ \to {F ↾}_{(Q (i), Q (i + 1))} = {(x \in ℝ ⟼ F (x)) ↾}_{(Q (i), Q (i + 1))}$
56	55	adantr	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = {(x \in ℝ ⟼ F (x)) ↾}_{(Q (i), Q (i + 1))}$
57		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
58	57	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
59	58	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(x \in ℝ ⟼ F (x)) ↾}_{(Q (i), Q (i + 1))} = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
60	56 59	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) = {F ↾}_{(Q (i), Q (i + 1))}$
61	50 53 10 12 11	iblcncfioo	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} \in 𝐿^{1}$
62	60 61	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) \in 𝐿^{1}$
63	9	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F : ℝ ⟶ ℂ$
64	50 53	iccssred	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq ℝ$
65	64	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℝ$
66	63 65	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
67	50 53 62 66	ibliooicc	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ F (x)) \in 𝐿^{1}$
68	26 31 38 40 46 67	itgspltprt	$⊢ φ \to \int_{[Q (0), Q (M)]} F (x) d x = \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) d x$
69	8	a1i	$⊢ φ \to S = (i \in (0 \dots M) ⟼ Q (i) + T)$
70		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
71	70	oveq1d	$⊢ i = 0 \to Q (i) + T = Q (0) + T$
72	71	adantl	$⊢ (φ \land i = 0) \to Q (i) + T = Q (0) + T$
73	4	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
74		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
75	73 74	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
76		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
77	75 76	syl	$⊢ φ \to 0 \in (0 \dots M)$
78	5	rpred	$⊢ φ \to T \in ℝ$
79	42 78	readdcld	$⊢ φ \to Q (0) + T \in ℝ$
80	69 72 77 79	fvmptd	$⊢ φ \to S (0) = Q (0) + T$
81	20	oveq1d	$⊢ φ \to Q (0) + T = A + T$
82	80 81	eqtr2d	$⊢ φ \to A + T = S (0)$
83		fveq2	$⊢ i = M \to Q (i) = Q (M)$
84	83	oveq1d	$⊢ i = M \to Q (i) + T = Q (M) + T$
85	84	adantl	$⊢ (φ \land i = M) \to Q (i) + T = Q (M) + T$
86		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
87	75 86	syl	$⊢ φ \to M \in (0 \dots M)$
88	43 78	readdcld	$⊢ φ \to Q (M) + T \in ℝ$
89	69 85 87 88	fvmptd	$⊢ φ \to S (M) = Q (M) + T$
90	22	oveq1d	$⊢ φ \to Q (M) + T = B + T$
91	89 90	eqtr2d	$⊢ φ \to B + T = S (M)$
92	82 91	oveq12d	$⊢ φ \to [A + T, B + T] = [S (0), S (M)]$
93	92	itgeq1d	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[S (0), S (M)]} F (x) d x$
94	38	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
95	78	adantr	$⊢ (φ \land i \in (0 \dots M)) \to T \in ℝ$
96	94 95	readdcld	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) + T \in ℝ$
97	96 8	fmptd	$⊢ φ \to S : (0 \dots M) ⟶ ℝ$
98	78	adantr	$⊢ (φ \land i \in (0 ..^M)) \to T \in ℝ$
99	50 53 98 40	ltadd1dd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T < Q (i + 1) + T$
100	48 96	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T \in ℝ$
101	8	fvmpt2	$⊢ (i \in (0 \dots M) \land Q (i) + T \in ℝ) \to S (i) = Q (i) + T$
102	49 100 101	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to S (i) = Q (i) + T$
103		fveq2	$⊢ i = j \to Q (i) = Q (j)$
104	103	oveq1d	$⊢ i = j \to Q (i) + T = Q (j) + T$
105	104	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ Q (i) + T) = (j \in (0 \dots M) ⟼ Q (j) + T)$
106	8 105	eqtri	$⊢ S = (j \in (0 \dots M) ⟼ Q (j) + T)$
107	106	a1i	$⊢ (φ \land i \in (0 ..^M)) \to S = (j \in (0 \dots M) ⟼ Q (j) + T)$
108		fveq2	$⊢ j = i + 1 \to Q (j) = Q (i + 1)$
109	108	oveq1d	$⊢ j = i + 1 \to Q (j) + T = Q (i + 1) + T$
110	109	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to Q (j) + T = Q (i + 1) + T$
111	53 98	readdcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T \in ℝ$
112	107 110 52 111	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) = Q (i + 1) + T$
113	99 102 112	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to S (i) < S (i + 1)$
114	9	adantr	$⊢ (φ \land x \in [S (0), S (M)]) \to F : ℝ ⟶ ℂ$
115	80 79	eqeltrd	$⊢ φ \to S (0) \in ℝ$
116	115	adantr	$⊢ (φ \land x \in [S (0), S (M)]) \to S (0) \in ℝ$
117	89 88	eqeltrd	$⊢ φ \to S (M) \in ℝ$
118	117	adantr	$⊢ (φ \land x \in [S (0), S (M)]) \to S (M) \in ℝ$
119	116 118	iccssred	$⊢ (φ \land x \in [S (0), S (M)]) \to [S (0), S (M)] \subseteq ℝ$
120		simpr	$⊢ (φ \land x \in [S (0), S (M)]) \to x \in [S (0), S (M)]$
121	119 120	sseldd	$⊢ (φ \land x \in [S (0), S (M)]) \to x \in ℝ$
122	114 121	ffvelrnd	$⊢ (φ \land x \in [S (0), S (M)]) \to F (x) \in ℂ$
123	102 100	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i) \in ℝ$
124	112 111	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) \in ℝ$
125		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
126	125	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
127		eqeq1	$⊢ w = x \to (w = z + T \leftrightarrow x = z + T)$
128	127	rexbidv	$⊢ w = x \to (\exists z \in (Q (i), Q (i + 1)) w = z + T \leftrightarrow \exists z \in (Q (i), Q (i + 1)) x = z + T)$
129		oveq1	$⊢ z = y \to z + T = y + T$
130	129	eqeq2d	$⊢ z = y \to (x = z + T \leftrightarrow x = y + T)$
131	130	cbvrexvw	$⊢ \exists z \in (Q (i), Q (i + 1)) x = z + T \leftrightarrow \exists y \in (Q (i), Q (i + 1)) x = y + T$
132	128 131	bitrdi	$⊢ w = x \to (\exists z \in (Q (i), Q (i + 1)) w = z + T \leftrightarrow \exists y \in (Q (i), Q (i + 1)) x = y + T)$
133	132	cbvrabv	$⊢ \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} = \{x \in ℂ \| \exists y \in (Q (i), Q (i + 1)) x = y + T\}$
134		fdm	$⊢ F : ℝ ⟶ ℂ \to dom F = ℝ$
135	9 134	syl	$⊢ φ \to dom F = ℝ$
136	135	feq2d	$⊢ φ \to (F : dom F ⟶ ℂ \leftrightarrow F : ℝ ⟶ ℂ)$
137	9 136	mpbird	$⊢ φ \to F : dom F ⟶ ℂ$
138	137	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : dom F ⟶ ℂ$
139		elioore	$⊢ z \in (Q (i), Q (i + 1)) \to z \in ℝ$
140	139	adantl	$⊢ (φ \land z \in (Q (i), Q (i + 1))) \to z \in ℝ$
141	78	adantr	$⊢ (φ \land z \in (Q (i), Q (i + 1))) \to T \in ℝ$
142	140 141	readdcld	$⊢ (φ \land z \in (Q (i), Q (i + 1))) \to z + T \in ℝ$
143	142	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z + T \in ℝ$
144	143	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land w = z + T) \to z + T \in ℝ$
145		simp3	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land w = z + T) \to w = z + T$
146	135	3ad2ant1	$⊢ (φ \land z \in (Q (i), Q (i + 1)) \land w = z + T) \to dom F = ℝ$
147	146	3adant1r	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land w = z + T) \to dom F = ℝ$
148	144 145 147	3eltr4d	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land w = z + T) \to w \in dom F$
149	148	3exp	$⊢ (φ \land i \in (0 ..^M)) \to (z \in (Q (i), Q (i + 1)) \to (w = z + T \to w \in dom F))$
150	149	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land w \in ℂ) \to (z \in (Q (i), Q (i + 1)) \to (w = z + T \to w \in dom F))$
151	150	rexlimdv	$⊢ ((φ \land i \in (0 ..^M)) \land w \in ℂ) \to (\exists z \in (Q (i), Q (i + 1)) w = z + T \to w \in dom F)$
152	151	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall w \in ℂ (\exists z \in (Q (i), Q (i + 1)) w = z + T \to w \in dom F)$
153		rabss	$⊢ \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \subseteq dom F \leftrightarrow \forall w \in ℂ (\exists z \in (Q (i), Q (i + 1)) w = z + T \to w \in dom F)$
154	152 153	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \subseteq dom F$
155		simpll	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to φ$
156	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
157	156	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to A \in ℝ^{*}$
158	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
159	158	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to B \in ℝ^{*}$
160	3 4 6	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
161	160	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [A, B]$
162		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
163		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
164	163	sseli	$⊢ x \in (Q (i), Q (i + 1)) \to x \in [Q (i), Q (i + 1)]$
165	164	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in [Q (i), Q (i + 1)]$
166	157 159 161 162 165	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in [A, B]$
167	155 166 7	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x + T) = F (x)$
168	126 98 133 138 154 167 10	cncfperiod	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}}) : \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \underset{cn}{⟶} ℂ$
169	128	elrab	$⊢ x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \leftrightarrow (x \in ℂ \land \exists z \in (Q (i), Q (i + 1)) x = z + T)$
170	169	simprbi	$⊢ x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \to \exists z \in (Q (i), Q (i + 1)) x = z + T$
171		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to \exists z \in (Q (i), Q (i + 1)) x = z + T$
172		nfv	$⊢ Ⅎ z (φ \land i \in (0 ..^M))$
173		nfre1	$⊢ Ⅎ z \exists z \in (Q (i), Q (i + 1)) x = z + T$
174	172 173	nfan	$⊢ Ⅎ z ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T)$
175		nfv	$⊢ Ⅎ z (x \in ℝ \land S (i) < x \land x < S (i + 1))$
176		simp3	$⊢ (φ \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to x = z + T$
177	142	3adant3	$⊢ (φ \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to z + T \in ℝ$
178	176 177	eqeltrd	$⊢ (φ \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to x \in ℝ$
179	178	3adant1r	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to x \in ℝ$
180	50	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ$
181	139	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z \in ℝ$
182	78	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to T \in ℝ$
183		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z \in (Q (i), Q (i + 1))$
184	50	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
185	184	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ^{*}$
186	53	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
187	186	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ^{*}$
188		elioo2	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{}) \to (z \in (Q (i), Q (i + 1)) \leftrightarrow (z \in ℝ \land Q (i) < z \land z < Q (i + 1)))$
189	185 187 188	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to (z \in (Q (i), Q (i + 1)) \leftrightarrow (z \in ℝ \land Q (i) < z \land z < Q (i + 1)))$
190	183 189	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to (z \in ℝ \land Q (i) < z \land z < Q (i + 1))$
191	190	simp2d	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q (i) < z$
192	180 181 182 191	ltadd1dd	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q (i) + T < z + T$
193	192	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to Q (i) + T < z + T$
194	102	3ad2ant1	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to S (i) = Q (i) + T$
195		simp3	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to x = z + T$
196	193 194 195	3brtr4d	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to S (i) < x$
197	53	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ$
198	190	simp3d	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z < Q (i + 1)$
199	181 197 182 198	ltadd1dd	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z + T < Q (i + 1) + T$
200	199	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to z + T < Q (i + 1) + T$
201	112	3ad2ant1	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to S (i + 1) = Q (i + 1) + T$
202	200 195 201	3brtr4d	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to x < S (i + 1)$
203	179 196 202	3jca	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1)) \land x = z + T) \to (x \in ℝ \land S (i) < x \land x < S (i + 1))$
204	203	3exp	$⊢ (φ \land i \in (0 ..^M)) \to (z \in (Q (i), Q (i + 1)) \to (x = z + T \to (x \in ℝ \land S (i) < x \land x < S (i + 1))))$
205	204	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to (z \in (Q (i), Q (i + 1)) \to (x = z + T \to (x \in ℝ \land S (i) < x \land x < S (i + 1))))$
206	174 175 205	rexlimd	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to (\exists z \in (Q (i), Q (i + 1)) x = z + T \to (x \in ℝ \land S (i) < x \land x < S (i + 1)))$
207	171 206	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to (x \in ℝ \land S (i) < x \land x < S (i + 1))$
208	123	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i) \in ℝ^{*}$
209	208	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to S (i) \in ℝ^{*}$
210	124	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) \in ℝ^{*}$
211	210	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to S (i + 1) \in ℝ^{*}$
212		elioo2	$⊢ (S (i) \in ℝ^{} \land S (i + 1) \in ℝ^{}) \to (x \in (S (i), S (i + 1)) \leftrightarrow (x \in ℝ \land S (i) < x \land x < S (i + 1)))$
213	209 211 212	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to (x \in (S (i), S (i + 1)) \leftrightarrow (x \in ℝ \land S (i) < x \land x < S (i + 1)))$
214	207 213	mpbird	$⊢ ((φ \land i \in (0 ..^M)) \land \exists z \in (Q (i), Q (i + 1)) x = z + T) \to x \in (S (i), S (i + 1))$
215	170 214	sylan2	$⊢ ((φ \land i \in (0 ..^M)) \land x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}) \to x \in (S (i), S (i + 1))$
216		elioore	$⊢ x \in (S (i), S (i + 1)) \to x \in ℝ$
217	216	recnd	$⊢ x \in (S (i), S (i + 1)) \to x \in ℂ$
218	217	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \in ℂ$
219	184	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to Q (i) \in ℝ^{*}$
220	186	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to Q (i + 1) \in ℝ^{*}$
221	216	adantl	$⊢ (φ \land x \in (S (i), S (i + 1))) \to x \in ℝ$
222	78	adantr	$⊢ (φ \land x \in (S (i), S (i + 1))) \to T \in ℝ$
223	221 222	resubcld	$⊢ (φ \land x \in (S (i), S (i + 1))) \to x - T \in ℝ$
224	223	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x - T \in ℝ$
225	102	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to S (i) - T = Q (i) + T - T$
226	50	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
227	98	recnd	$⊢ (φ \land i \in (0 ..^M)) \to T \in ℂ$
228	226 227	pncand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T - T = Q (i)$
229	225 228	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = S (i) - T$
230	229	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to Q (i) = S (i) - T$
231	123	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i) \in ℝ$
232	216	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \in ℝ$
233	78	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to T \in ℝ$
234		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \in (S (i), S (i + 1))$
235	208	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i) \in ℝ^{*}$
236	210	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i + 1) \in ℝ^{*}$
237	235 236 212	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to (x \in (S (i), S (i + 1)) \leftrightarrow (x \in ℝ \land S (i) < x \land x < S (i + 1)))$
238	234 237	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to (x \in ℝ \land S (i) < x \land x < S (i + 1))$
239	238	simp2d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i) < x$
240	231 232 233 239	ltsub1dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i) - T < x - T$
241	230 240	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to Q (i) < x - T$
242	124	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i + 1) \in ℝ$
243	238	simp3d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x < S (i + 1)$
244	232 242 233 243	ltsub1dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x - T < S (i + 1) - T$
245	112	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) - T = Q (i + 1) + T - T$
246	53	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
247	246 227	pncand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T - T = Q (i + 1)$
248	245 247	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) - T = Q (i + 1)$
249	248	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to S (i + 1) - T = Q (i + 1)$
250	244 249	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x - T < Q (i + 1)$
251	219 220 224 241 250	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x - T \in (Q (i), Q (i + 1))$
252	221	recnd	$⊢ (φ \land x \in (S (i), S (i + 1))) \to x \in ℂ$
253	222	recnd	$⊢ (φ \land x \in (S (i), S (i + 1))) \to T \in ℂ$
254	252 253	npcand	$⊢ (φ \land x \in (S (i), S (i + 1))) \to x - T + T = x$
255	254	eqcomd	$⊢ (φ \land x \in (S (i), S (i + 1))) \to x = x - T + T$
256	255	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x = x - T + T$
257		oveq1	$⊢ z = x - T \to z + T = x - T + T$
258	257	eqeq2d	$⊢ z = x - T \to (x = z + T \leftrightarrow x = x - T + T)$
259	258	rspcev	$⊢ (x - T \in (Q (i), Q (i + 1)) \land x = x - T + T) \to \exists z \in (Q (i), Q (i + 1)) x = z + T$
260	251 256 259	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to \exists z \in (Q (i), Q (i + 1)) x = z + T$
261	218 260 169	sylanbrc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}$
262	215 261	impbida	$⊢ (φ \land i \in (0 ..^M)) \to (x \in \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \leftrightarrow x \in (S (i), S (i + 1)))$
263	262	eqrdv	$⊢ (φ \land i \in (0 ..^M)) \to \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} = (S (i), S (i + 1))$
264	263	reseq2d	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}} = {F ↾}_{(S (i), S (i + 1))}$
265	9	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℂ$
266		ioossre	$⊢ (S (i), S (i + 1)) \subseteq ℝ$
267	266	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (S (i), S (i + 1)) \subseteq ℝ$
268	265 267	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(S (i), S (i + 1))} = (x \in (S (i), S (i + 1)) ⟼ F (x))$
269	264 268	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}} = (x \in (S (i), S (i + 1)) ⟼ F (x))$
270	263	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} \underset{cn}{⟶} ℂ = (S (i), S (i + 1)) \underset{cn}{⟶} ℂ$
271	168 269 270	3eltr3d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (S (i), S (i + 1)) ⟼ F (x)) : (S (i), S (i + 1)) \underset{cn}{⟶} ℂ$
272	57 135	sseqtrrid	$⊢ φ \to (Q (i), Q (i + 1)) \subseteq dom F$
273	272	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom F$
274		eqid	$⊢ \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\} = \{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}$
275		simpll	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to φ$
276	156	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to A \in ℝ^{*}$
277	158	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to B \in ℝ^{*}$
278	160	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [A, B]$
279		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
280	163 183	sselid	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z \in [Q (i), Q (i + 1)]$
281	276 277 278 279 280	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to z \in [A, B]$
282		eleq1	$⊢ x = z \to (x \in [A, B] \leftrightarrow z \in [A, B])$
283	282	anbi2d	$⊢ x = z \to ((φ \land x \in [A, B]) \leftrightarrow (φ \land z \in [A, B]))$
284		oveq1	$⊢ x = z \to x + T = z + T$
285	284	fveq2d	$⊢ x = z \to F (x + T) = F (z + T)$
286		fveq2	$⊢ x = z \to F (x) = F (z)$
287	285 286	eqeq12d	$⊢ x = z \to (F (x + T) = F (x) \leftrightarrow F (z + T) = F (z))$
288	283 287	imbi12d	$⊢ x = z \to (((φ \land x \in [A, B]) \to F (x + T) = F (x)) \leftrightarrow ((φ \land z \in [A, B]) \to F (z + T) = F (z)))$
289	288 7	chvarvv	$⊢ (φ \land z \in [A, B]) \to F (z + T) = F (z)$
290	275 281 289	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to F (z + T) = F (z)$
291	138 126 273 227 274 154 290 12	limcperiod	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}}) {lim}_{ℂ} (Q (i + 1) + T))$
292	112	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + T = S (i + 1)$
293	269 292	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}}) {lim}_{ℂ} (Q (i + 1) + T) = (x \in (S (i), S (i + 1)) ⟼ F (x)) {lim}_{ℂ} S (i + 1)$
294	291 293	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((x \in (S (i), S (i + 1)) ⟼ F (x)) {lim}_{ℂ} S (i + 1))$
295	138 126 273 227 274 154 290 11	limcperiod	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}}) {lim}_{ℂ} (Q (i) + T))$
296	102	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + T = S (i)$
297	269 296	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{\{w \in ℂ \| \exists z \in (Q (i), Q (i + 1)) w = z + T\}}) {lim}_{ℂ} (Q (i) + T) = (x \in (S (i), S (i + 1)) ⟼ F (x)) {lim}_{ℂ} S (i)$
298	295 297	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((x \in (S (i), S (i + 1)) ⟼ F (x)) {lim}_{ℂ} S (i))$
299	123 124 271 294 298	iblcncfioo	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (S (i), S (i + 1)) ⟼ F (x)) \in 𝐿^{1}$
300	9	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to F : ℝ ⟶ ℂ$
301	123	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i) \in ℝ$
302	124	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i + 1) \in ℝ$
303		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x \in [S (i), S (i + 1)]$
304		eliccre	$⊢ (S (i) \in ℝ \land S (i + 1) \in ℝ \land x \in [S (i), S (i + 1)]) \to x \in ℝ$
305	301 302 303 304	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x \in ℝ$
306	300 305	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to F (x) \in ℂ$
307	123 124 299 306	ibliooicc	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [S (i), S (i + 1)] ⟼ F (x)) \in 𝐿^{1}$
308	26 31 97 113 122 307	itgspltprt	$⊢ φ \to \int_{[S (0), S (M)]} F (x) d x = \sum_{i \in (0 ..^M)} \int_{[S (i), S (i + 1)]} F (x) d x$
309		iftrue	$⊢ x = S (i) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = R$
310	309	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = R$
311		iftrue	$⊢ x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = R$
312		iftrue	$⊢ x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))) = R$
313	311 312	eqtr4d	$⊢ x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
314	313	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land x = Q (i)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
315		iffalse	$⊢ \neg x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i + 1), L, F (x))$
316	315	adantr	$⊢ (\neg x = Q (i) \land x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i + 1), L, F (x))$
317		iftrue	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = L$
318	317	adantl	$⊢ (\neg x = Q (i) \land x = Q (i + 1)) \to if (x = Q (i + 1), L, F (x)) = L$
319		iffalse	$⊢ \neg x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
320	319	adantr	$⊢ (\neg x = Q (i) \land x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
321		iftrue	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = L$
322	321	adantl	$⊢ (\neg x = Q (i) \land x = Q (i + 1)) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = L$
323	320 322	eqtr2d	$⊢ (\neg x = Q (i) \land x = Q (i + 1)) \to L = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
324	316 318 323	3eqtrd	$⊢ (\neg x = Q (i) \land x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
325	324	adantll	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
326	315	ad2antlr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i + 1), L, F (x))$
327		iffalse	$⊢ \neg x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = F (x)$
328	327	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i + 1), L, F (x)) = F (x)$
329	319	ad2antlr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
330		iffalse	$⊢ \neg x = Q (i + 1) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x)$
331	330	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x)$
332	184	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i) \in ℝ^{*}$
333	186	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i + 1) \in ℝ^{*}$
334	65	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x \in ℝ$
335	50	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) \in ℝ$
336	65	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \in ℝ$
337	184	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) \in ℝ^{*}$
338	186	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i + 1) \in ℝ^{*}$
339		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \in [Q (i), Q (i + 1)]$
340		iccgelb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land x \in [Q (i), Q (i + 1)]) \to Q (i) \leq x$
341	337 338 339 340	syl3anc	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) \leq x$
342		neqne	$⊢ \neg x = Q (i) \to x \neq Q (i)$
343	342	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \neq Q (i)$
344	335 336 341 343	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) < x$
345	344	adantr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i) < x$
346	53	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i + 1) \in ℝ$
347	184	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i) \in ℝ^{*}$
348	186	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i + 1) \in ℝ^{*}$
349		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in [Q (i), Q (i + 1)]$
350		iccleub	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land x \in [Q (i), Q (i + 1)]) \to x \leq Q (i + 1)$
351	347 348 349 350	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \leq Q (i + 1)$
352	351	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x \leq Q (i + 1)$
353		neqne	$⊢ \neg x = Q (i + 1) \to x \neq Q (i + 1)$
354	353	necomd	$⊢ \neg x = Q (i + 1) \to Q (i + 1) \neq x$
355	354	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i + 1) \neq x$
356	334 346 352 355	leneltd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x < Q (i + 1)$
357	332 333 334 345 356	eliood	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x \in (Q (i), Q (i + 1))$
358		fvres	$⊢ x \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x) = F (x)$
359	357 358	syl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x) = F (x)$
360	329 331 359	3eqtrrd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to F (x) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
361	326 328 360	3eqtrd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
362	325 361	pm2.61dan	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
363	314 362	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
364	363	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x)))) = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))))$
365	13 364	eqtrid	$⊢ (φ \land i \in (0 ..^M)) \to G = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))))$
366		eqeq1	$⊢ x = w \to (x = Q (i) \leftrightarrow w = Q (i))$
367		eqeq1	$⊢ x = w \to (x = Q (i + 1) \leftrightarrow w = Q (i + 1))$
368		fveq2	$⊢ x = w \to ({F ↾}_{(Q (i), Q (i + 1))}) (x) = ({F ↾}_{(Q (i), Q (i + 1))}) (w)$
369	367 368	ifbieq2d	$⊢ x = w \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))$
370	366 369	ifbieq2d	$⊢ x = w \to if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))) = if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w)))$
371	370	cbvmptv	$⊢ (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))) = (w \in [Q (i), Q (i + 1)] ⟼ if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))))$
372	365 371	eqtrdi	$⊢ (φ \land i \in (0 ..^M)) \to G = (w \in [Q (i), Q (i + 1)] ⟼ if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))))$
373	372	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to G = (w \in [Q (i), Q (i + 1)] ⟼ if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))))$
374		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land x = S (i)) \land w = x - T) \to w = x - T$
375		oveq1	$⊢ x = S (i) \to x - T = S (i) - T$
376	375	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land x = S (i)) \land w = x - T) \to x - T = S (i) - T$
377	229	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to S (i) - T = Q (i)$
378	377	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x = S (i)) \land w = x - T) \to S (i) - T = Q (i)$
379	374 376 378	3eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land x = S (i)) \land w = x - T) \to w = Q (i)$
380	379	iftrued	$⊢ (((φ \land i \in (0 ..^M)) \land x = S (i)) \land w = x - T) \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = R$
381	375	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to x - T = S (i) - T$
382	50 53 40	ltled	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \leq Q (i + 1)$
383		lbicc2	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land Q (i) \leq Q (i + 1)) \to Q (i) \in [Q (i), Q (i + 1)]$
384	184 186 382 383	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [Q (i), Q (i + 1)]$
385	377 384	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i) - T \in [Q (i), Q (i + 1)]$
386	385	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to S (i) - T \in [Q (i), Q (i + 1)]$
387	381 386	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to x - T \in [Q (i), Q (i + 1)]$
388		limccl	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \subseteq ℂ$
389	388 11	sselid	$⊢ (φ \land i \in (0 ..^M)) \to R \in ℂ$
390	389	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to R \in ℂ$
391	373 380 387 390	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to G (x - T) = R$
392	310 391	eqtr4d	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = G (x - T)$
393	392	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = G (x - T)$
394		iffalse	$⊢ \neg x = S (i) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))$
395	394	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))$
396	372	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to G = (w \in [Q (i), Q (i + 1)] ⟼ if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))))$
397		eqeq1	$⊢ w = S (i + 1) - T \to (w = Q (i) \leftrightarrow S (i + 1) - T = Q (i))$
398		eqeq1	$⊢ w = S (i + 1) - T \to (w = Q (i + 1) \leftrightarrow S (i + 1) - T = Q (i + 1))$
399		fveq2	$⊢ w = S (i + 1) - T \to ({F ↾}_{(Q (i), Q (i + 1))}) (w) = ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T)$
400	398 399	ifbieq2d	$⊢ w = S (i + 1) - T \to if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w)) = if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T))$
401	397 400	ifbieq2d	$⊢ w = S (i + 1) - T \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = if (S (i + 1) - T = Q (i), R, if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T)))$
402	401	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land w = S (i + 1) - T) \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = if (S (i + 1) - T = Q (i), R, if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T)))$
403		eqeq1	$⊢ S (i + 1) - T = Q (i + 1) \to (S (i + 1) - T = Q (i) \leftrightarrow Q (i + 1) = Q (i))$
404		iftrue	$⊢ S (i + 1) - T = Q (i + 1) \to if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T)) = L$
405	403 404	ifbieq2d	$⊢ S (i + 1) - T = Q (i + 1) \to if (S (i + 1) - T = Q (i), R, if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T))) = if (Q (i + 1) = Q (i), R, L)$
406	248 405	syl	$⊢ (φ \land i \in (0 ..^M)) \to if (S (i + 1) - T = Q (i), R, if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T))) = if (Q (i + 1) = Q (i), R, L)$
407	406	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land w = S (i + 1) - T) \to if (S (i + 1) - T = Q (i), R, if (S (i + 1) - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (S (i + 1) - T))) = if (Q (i + 1) = Q (i), R, L)$
408	50 40	gtned	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \neq Q (i)$
409	408	neneqd	$⊢ (φ \land i \in (0 ..^M)) \to \neg Q (i + 1) = Q (i)$
410	409	iffalsed	$⊢ (φ \land i \in (0 ..^M)) \to if (Q (i + 1) = Q (i), R, L) = L$
411	410	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land w = S (i + 1) - T) \to if (Q (i + 1) = Q (i), R, L) = L$
412	402 407 411	3eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land w = S (i + 1) - T) \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = L$
413	412	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \land w = S (i + 1) - T) \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = L$
414		ubicc2	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land Q (i) \leq Q (i + 1)) \to Q (i + 1) \in [Q (i), Q (i + 1)]$
415	184 186 382 414	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [Q (i), Q (i + 1)]$
416	248 415	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to S (i + 1) - T \in [Q (i), Q (i + 1)]$
417	416	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to S (i + 1) - T \in [Q (i), Q (i + 1)]$
418		limccl	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \subseteq ℂ$
419	418 12	sselid	$⊢ (φ \land i \in (0 ..^M)) \to L \in ℂ$
420	419	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to L \in ℂ$
421	396 413 417 420	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to G (S (i + 1) - T) = L$
422		oveq1	$⊢ x = S (i + 1) \to x - T = S (i + 1) - T$
423	422	fveq2d	$⊢ x = S (i + 1) \to G (x - T) = G (S (i + 1) - T)$
424	423	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to G (x - T) = G (S (i + 1) - T)$
425		iftrue	$⊢ x = S (i + 1) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = L$
426	425	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = L$
427	421 424 426	3eqtr4rd	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = G (x - T)$
428	427	ad4ant14	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = G (x - T)$
429		iffalse	$⊢ \neg x = S (i + 1) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = ({F ↾}_{(S (i), S (i + 1))}) (x)$
430	429	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = ({F ↾}_{(S (i), S (i + 1))}) (x)$
431	372	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to G = (w \in [Q (i), Q (i + 1)] ⟼ if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))))$
432	431	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to G = (w \in [Q (i), Q (i + 1)] ⟼ if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))))$
433		eqeq1	$⊢ w = x - T \to (w = Q (i) \leftrightarrow x - T = Q (i))$
434		eqeq1	$⊢ w = x - T \to (w = Q (i + 1) \leftrightarrow x - T = Q (i + 1))$
435		fveq2	$⊢ w = x - T \to ({F ↾}_{(Q (i), Q (i + 1))}) (w) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
436	434 435	ifbieq2d	$⊢ w = x - T \to if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w)) = if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))$
437	433 436	ifbieq2d	$⊢ w = x - T \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = if (x - T = Q (i), R, if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)))$
438	437	adantl	$⊢ (((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \land w = x - T) \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = if (x - T = Q (i), R, if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)))$
439	305	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x \in ℂ$
440	227	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to T \in ℂ$
441	439 440	npcand	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T + T = x$
442	441	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x = x - T + T$
443	442	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i)) \to x = x - T + T$
444		oveq1	$⊢ x - T = Q (i) \to x - T + T = Q (i) + T$
445	444	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i)) \to x - T + T = Q (i) + T$
446	296	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i)) \to Q (i) + T = S (i)$
447	443 445 446	3eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i)) \to x = S (i)$
448	447	stoic1a	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to \neg x - T = Q (i)$
449	448	iffalsed	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to if (x - T = Q (i), R, if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))) = if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))$
450	449	ad2antrr	$⊢ (((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \land w = x - T) \to if (x - T = Q (i), R, if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))) = if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T))$
451	442	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i + 1)) \to x = x - T + T$
452		oveq1	$⊢ x - T = Q (i + 1) \to x - T + T = Q (i + 1) + T$
453	452	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i + 1)) \to x - T + T = Q (i + 1) + T$
454	292	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i + 1)) \to Q (i + 1) + T = S (i + 1)$
455	451 453 454	3eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x - T = Q (i + 1)) \to x = S (i + 1)$
456	455	stoic1a	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to \neg x - T = Q (i + 1)$
457	456	iffalsed	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
458	457	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
459	458	adantr	$⊢ (((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \land w = x - T) \to if (x - T = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
460	438 450 459	3eqtrd	$⊢ (((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \land w = x - T) \to if (w = Q (i), R, if (w = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (w))) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
461	50	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to Q (i) \in ℝ$
462	53	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to Q (i + 1) \in ℝ$
463	78	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to T \in ℝ$
464	305 463	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \in ℝ$
465	229	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to Q (i) = S (i) - T$
466	208	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i) \in ℝ^{*}$
467	210	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i + 1) \in ℝ^{*}$
468		iccgelb	$⊢ (S (i) \in ℝ^{} \land S (i + 1) \in ℝ^{} \land x \in [S (i), S (i + 1)]) \to S (i) \leq x$
469	466 467 303 468	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i) \leq x$
470	301 305 463 469	lesub1dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i) - T \leq x - T$
471	465 470	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to Q (i) \leq x - T$
472		iccleub	$⊢ (S (i) \in ℝ^{} \land S (i + 1) \in ℝ^{} \land x \in [S (i), S (i + 1)]) \to x \leq S (i + 1)$
473	466 467 303 472	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x \leq S (i + 1)$
474	305 302 463 473	lesub1dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \leq S (i + 1) - T$
475	248	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to S (i + 1) - T = Q (i + 1)$
476	474 475	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \leq Q (i + 1)$
477	461 462 464 471 476	eliccd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \in [Q (i), Q (i + 1)]$
478	477	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x - T \in [Q (i), Q (i + 1)]$
479	138 273	fssresd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
480	479	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
481	184	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to Q (i) \in ℝ^{*}$
482	186	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to Q (i + 1) \in ℝ^{*}$
483	305	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x \in ℝ$
484	98	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to T \in ℝ$
485	483 484	resubcld	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x - T \in ℝ$
486	50	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to Q (i) \in ℝ$
487	464	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to x - T \in ℝ$
488	471	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to Q (i) \leq x - T$
489	448	neqned	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to x - T \neq Q (i)$
490	486 487 488 489	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to Q (i) < x - T$
491	490	adantr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to Q (i) < x - T$
492	464	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to x - T \in ℝ$
493	53	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to Q (i + 1) \in ℝ$
494	476	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to x - T \leq Q (i + 1)$
495		eqcom	$⊢ x - T = Q (i + 1) \leftrightarrow Q (i + 1) = x - T$
496	455	ex	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to (x - T = Q (i + 1) \to x = S (i + 1))$
497	495 496	syl5bir	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to (Q (i + 1) = x - T \to x = S (i + 1))$
498	497	con3dimp	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to \neg Q (i + 1) = x - T$
499	498	neqned	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to Q (i + 1) \neq x - T$
500	492 493 494 499	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i + 1)) \to x - T < Q (i + 1)$
501	500	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x - T < Q (i + 1)$
502	481 482 485 491 501	eliood	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x - T \in (Q (i), Q (i + 1))$
503	480 502	ffvelrnd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x - T) \in ℂ$
504	432 460 478 503	fvmptd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to G (x - T) = ({F ↾}_{(Q (i), Q (i + 1))}) (x - T)$
505		fvres	$⊢ x - T \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x - T) = F (x - T)$
506	502 505	syl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x - T) = F (x - T)$
507	504 506	eqtrd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to G (x - T) = F (x - T)$
508	466	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to S (i) \in ℝ^{*}$
509	467	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to S (i + 1) \in ℝ^{*}$
510	123	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to S (i) \in ℝ$
511	305	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to x \in ℝ$
512	469	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to S (i) \leq x$
513		neqne	$⊢ \neg x = S (i) \to x \neq S (i)$
514	513	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to x \neq S (i)$
515	510 511 512 514	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to S (i) < x$
516	515	adantr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to S (i) < x$
517	302	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to S (i + 1) \in ℝ$
518	473	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x \leq S (i + 1)$
519		neqne	$⊢ \neg x = S (i + 1) \to x \neq S (i + 1)$
520	519	necomd	$⊢ \neg x = S (i + 1) \to S (i + 1) \neq x$
521	520	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to S (i + 1) \neq x$
522	483 517 518 521	leneltd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x < S (i + 1)$
523	508 509 483 516 522	eliood	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x \in (S (i), S (i + 1))$
524		fvres	$⊢ x \in (S (i), S (i + 1)) \to ({F ↾}_{(S (i), S (i + 1))}) (x) = F (x)$
525	523 524	syl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(S (i), S (i + 1))}) (x) = F (x)$
526	441	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to F (x - T + T) = F (x)$
527	526	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to F (x) = F (x - T + T)$
528	527	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to F (x) = F (x - T + T)$
529	439 440	subcld	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \in ℂ$
530		elex	$⊢ x - T \in ℂ \to x - T \in V$
531	529 530	syl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \in V$
532	531	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x - T \in V$
533		simp-4l	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to φ$
534	156	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ^{*}$
535	158	adantr	$⊢ (φ \land i \in (0 ..^M)) \to B \in ℝ^{*}$
536	160	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [A, B]$
537		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
538	534 535 536 537	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
539	538	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
540	539 477	sseldd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to x - T \in [A, B]$
541	540	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to x - T \in [A, B]$
542	533 541	jca	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to (φ \land x - T \in [A, B])$
543		eleq1	$⊢ y = x - T \to (y \in [A, B] \leftrightarrow x - T \in [A, B])$
544	543	anbi2d	$⊢ y = x - T \to ((φ \land y \in [A, B]) \leftrightarrow (φ \land x - T \in [A, B]))$
545		oveq1	$⊢ y = x - T \to y + T = x - T + T$
546	545	fveq2d	$⊢ y = x - T \to F (y + T) = F (x - T + T)$
547		fveq2	$⊢ y = x - T \to F (y) = F (x - T)$
548	546 547	eqeq12d	$⊢ y = x - T \to (F (y + T) = F (y) \leftrightarrow F (x - T + T) = F (x - T))$
549	544 548	imbi12d	$⊢ y = x - T \to (((φ \land y \in [A, B]) \to F (y + T) = F (y)) \leftrightarrow ((φ \land x - T \in [A, B]) \to F (x - T + T) = F (x - T)))$
550		eleq1	$⊢ x = y \to (x \in [A, B] \leftrightarrow y \in [A, B])$
551	550	anbi2d	$⊢ x = y \to ((φ \land x \in [A, B]) \leftrightarrow (φ \land y \in [A, B]))$
552		oveq1	$⊢ x = y \to x + T = y + T$
553	552	fveq2d	$⊢ x = y \to F (x + T) = F (y + T)$
554		fveq2	$⊢ x = y \to F (x) = F (y)$
555	553 554	eqeq12d	$⊢ x = y \to (F (x + T) = F (x) \leftrightarrow F (y + T) = F (y))$
556	551 555	imbi12d	$⊢ x = y \to (((φ \land x \in [A, B]) \to F (x + T) = F (x)) \leftrightarrow ((φ \land y \in [A, B]) \to F (y + T) = F (y)))$
557	556 7	chvarvv	$⊢ (φ \land y \in [A, B]) \to F (y + T) = F (y)$
558	549 557	vtoclg	$⊢ x - T \in V \to ((φ \land x - T \in [A, B]) \to F (x - T + T) = F (x - T))$
559	532 542 558	sylc	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to F (x - T + T) = F (x - T)$
560	525 528 559	3eqtrd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(S (i), S (i + 1))}) (x) = F (x - T)$
561	507 560	eqtr4d	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to G (x - T) = ({F ↾}_{(S (i), S (i + 1))}) (x)$
562	430 561	eqtr4d	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = G (x - T)$
563	428 562	pm2.61dan	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = G (x - T)$
564	395 563	eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = G (x - T)$
565	393 564	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = G (x - T)$
566	310 390	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) \in ℂ$
567	566	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) \in ℂ$
568	426 420	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) \in ℂ$
569	568	ad4ant14	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) \in ℂ$
570	265 267	fssresd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(S (i), S (i + 1))}) : (S (i), S (i + 1)) ⟶ ℂ$
571	570	ad3antrrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(S (i), S (i + 1))}) : (S (i), S (i + 1)) ⟶ ℂ$
572	571 523	ffvelrnd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to ({F ↾}_{(S (i), S (i + 1))}) (x) \in ℂ$
573	430 572	eqeltrd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \land \neg x = S (i + 1)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) \in ℂ$
574	569 573	pm2.61dan	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) \in ℂ$
575	395 574	eqeltrd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \land \neg x = S (i)) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) \in ℂ$
576	567 575	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) \in ℂ$
577		eqid	$⊢ (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) = (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))))$
578	577	fvmpt2	$⊢ (x \in [S (i), S (i + 1)] \land if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) \in ℂ) \to (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) = if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))$
579	303 576 578	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) = if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))$
580		nfv	$⊢ Ⅎ x (φ \land i \in (0 ..^M))$
581		eqid	$⊢ (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))) = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))))$
582	580 581 50 53 10 12 11	cncfiooicc	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))) : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
583	365 582	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to G : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
584		cncff	$⊢ G : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ \to G : [Q (i), Q (i + 1)] ⟶ ℂ$
585	583 584	syl	$⊢ (φ \land i \in (0 ..^M)) \to G : [Q (i), Q (i + 1)] ⟶ ℂ$
586	585	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to G : [Q (i), Q (i + 1)] ⟶ ℂ$
587	586 477	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to G (x - T) \in ℂ$
588	14	fvmpt2	$⊢ (x \in [S (i), S (i + 1)] \land G (x - T) \in ℂ) \to H (x) = G (x - T)$
589	303 587 588	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to H (x) = G (x - T)$
590	565 579 589	3eqtr4rd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to H (x) = (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x)$
591	590	itgeq2dv	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[S (i), S (i + 1)]} H (x) d x = \int_{[S (i), S (i + 1)]} (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) d x$
592		ioossicc	$⊢ (S (i), S (i + 1)) \subseteq [S (i), S (i + 1)]$
593	592	sseli	$⊢ x \in (S (i), S (i + 1)) \to x \in [S (i), S (i + 1)]$
594	593	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \in [S (i), S (i + 1)]$
595	593 576	sylan2	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) \in ℂ$
596	594 595 578	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) = if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))$
597	231 239	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \neq S (i)$
598	597	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to \neg x = S (i)$
599	598	iffalsed	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))) = if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x))$
600	232 243	ltned	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to x \neq S (i + 1)$
601	600	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to \neg x = S (i + 1)$
602	601	iffalsed	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = ({F ↾}_{(S (i), S (i + 1))}) (x)$
603	524	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to ({F ↾}_{(S (i), S (i + 1))}) (x) = F (x)$
604	602 603	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)) = F (x)$
605	596 599 604	3eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (S (i), S (i + 1))) \to (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) = F (x)$
606	605	itgeq2dv	$⊢ (φ \land i \in (0 ..^M)) \to \int_{(S (i), S (i + 1))} (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) d x = \int_{(S (i), S (i + 1))} F (x) d x$
607	579 576	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [S (i), S (i + 1)]) \to (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) \in ℂ$
608	123 124 607	itgioo	$⊢ (φ \land i \in (0 ..^M)) \to \int_{(S (i), S (i + 1))} (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) d x = \int_{[S (i), S (i + 1)]} (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) d x$
609	123 124 306	itgioo	$⊢ (φ \land i \in (0 ..^M)) \to \int_{(S (i), S (i + 1))} F (x) d x = \int_{[S (i), S (i + 1)]} F (x) d x$
610	606 608 609	3eqtr3d	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[S (i), S (i + 1)]} (x \in [S (i), S (i + 1)] ⟼ if (x = S (i), R, if (x = S (i + 1), L, ({F ↾}_{(S (i), S (i + 1))}) (x)))) (x) d x = \int_{[S (i), S (i + 1)]} F (x) d x$
611	591 610	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[S (i), S (i + 1)]} F (x) d x = \int_{[S (i), S (i + 1)]} H (x) d x$
612	102 112	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to [S (i), S (i + 1)] = [Q (i) + T, Q (i + 1) + T]$
613	612	itgeq1d	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[S (i), S (i + 1)]} H (x) d x = \int_{[Q (i) + T, Q (i + 1) + T]} H (x) d x$
614		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x \in [Q (i) + T, Q (i + 1) + T]$
615	612	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i) + T, Q (i + 1) + T] = [S (i), S (i + 1)]$
616	615	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to [Q (i) + T, Q (i + 1) + T] = [S (i), S (i + 1)]$
617	614 616	eleqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x \in [S (i), S (i + 1)]$
618	585	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to G : [Q (i), Q (i + 1)] ⟶ ℂ$
619	50	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) \in ℝ$
620	53	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i + 1) \in ℝ$
621	100	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) + T \in ℝ$
622	111	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i + 1) + T \in ℝ$
623		eliccre	$⊢ (Q (i) + T \in ℝ \land Q (i + 1) + T \in ℝ \land x \in [Q (i) + T, Q (i + 1) + T]) \to x \in ℝ$
624	621 622 614 623	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x \in ℝ$
625	78	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to T \in ℝ$
626	624 625	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x - T \in ℝ$
627	228	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = Q (i) + T - T$
628	627	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) = Q (i) + T - T$
629	621	rexrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) + T \in ℝ^{*}$
630	622	rexrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i + 1) + T \in ℝ^{*}$
631		iccgelb	$⊢ (Q (i) + T \in ℝ^{} \land Q (i + 1) + T \in ℝ^{} \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) + T \leq x$
632	629 630 614 631	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) + T \leq x$
633	621 624 625 632	lesub1dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) + T - T \leq x - T$
634	628 633	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i) \leq x - T$
635		iccleub	$⊢ (Q (i) + T \in ℝ^{} \land Q (i + 1) + T \in ℝ^{} \land x \in [Q (i) + T, Q (i + 1) + T]) \to x \leq Q (i + 1) + T$
636	629 630 614 635	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x \leq Q (i + 1) + T$
637	624 622 625 636	lesub1dd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x - T \leq Q (i + 1) + T - T$
638	247	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to Q (i + 1) + T - T = Q (i + 1)$
639	637 638	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x - T \leq Q (i + 1)$
640	619 620 626 634 639	eliccd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to x - T \in [Q (i), Q (i + 1)]$
641	618 640	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to G (x - T) \in ℂ$
642	617 641 588	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to H (x) = G (x - T)$
643		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T)) = (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T))$
644		oveq1	$⊢ y = x \to y - T = x - T$
645	644	fveq2d	$⊢ y = x \to G (y - T) = G (x - T)$
646	645	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \land y = x) \to G (y - T) = G (x - T)$
647	643 646 614 641	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T)) (x) = G (x - T)$
648	642 647	eqtr4d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i) + T, Q (i + 1) + T]) \to H (x) = (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T)) (x)$
649	648	itgeq2dv	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i) + T, Q (i + 1) + T]} H (x) d x = \int_{[Q (i) + T, Q (i + 1) + T]} (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T)) (x) d x$
650	5	adantr	$⊢ (φ \land i \in (0 ..^M)) \to T \in ℝ^{+}$
651	645	cbvmptv	$⊢ (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T)) = (x \in [Q (i) + T, Q (i + 1) + T] ⟼ G (x - T))$
652	50 53 382 583 650 651	itgiccshift	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i) + T, Q (i + 1) + T]} (y \in [Q (i) + T, Q (i + 1) + T] ⟼ G (y - T)) (x) d x = \int_{[Q (i), Q (i + 1)]} G (x) d x$
653	613 649 652	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[S (i), S (i + 1)]} H (x) d x = \int_{[Q (i), Q (i + 1)]} G (x) d x$
654	135	adantr	$⊢ (φ \land i \in (0 ..^M)) \to dom F = ℝ$
655	64 654	sseqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq dom F$
656	50 53 138 10 655 11 12 13	itgioocnicc	$⊢ (φ \land i \in (0 ..^M)) \to (G \in 𝐿^{1} \land \int_{[Q (i), Q (i + 1)]} G (x) d x = \int_{[Q (i), Q (i + 1)]} F (x) d x)$
657	656	simprd	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i), Q (i + 1)]} G (x) d x = \int_{[Q (i), Q (i + 1)]} F (x) d x$
658	611 653 657	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[S (i), S (i + 1)]} F (x) d x = \int_{[Q (i), Q (i + 1)]} F (x) d x$
659	658	sumeq2dv	$⊢ φ \to \sum_{i \in (0 ..^M)} \int_{[S (i), S (i + 1)]} F (x) d x = \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) d x$
660	93 308 659	3eqtrrd	$⊢ φ \to \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) d x = \int_{[A + T, B + T]} F (x) d x$
661	25 68 660	3eqtrrd	$⊢ φ \to \int_{[A + T, B + T]} F (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem fourierdlem81

Proof