fourierdlem93

Description: Integral by substitution (the domain is shifted by X ) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem93.1	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem93.2	$⊢ H = (i \in (0 \dots M) ⟼ Q (i) - X)$
	fourierdlem93.3	$⊢ φ \to M \in ℕ$
	fourierdlem93.4	$⊢ φ \to Q \in P (M)$
	fourierdlem93.5	$⊢ φ \to X \in ℝ$
	fourierdlem93.6	$⊢ φ \to F : [- π, π] ⟶ ℂ$
	fourierdlem93.7	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem93.8	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem93.9	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
Assertion	fourierdlem93	$⊢ φ \to \int_{[- π, π]} F (t) d t = \int_{[- π - X, π - X]} F (X + s) d s$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem93.1	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem93.2	$⊢ H = (i \in (0 \dots M) ⟼ Q (i) - X)$
3		fourierdlem93.3	$⊢ φ \to M \in ℕ$
4		fourierdlem93.4	$⊢ φ \to Q \in P (M)$
5		fourierdlem93.5	$⊢ φ \to X \in ℝ$
6		fourierdlem93.6	$⊢ φ \to F : [- π, π] ⟶ ℂ$
7		fourierdlem93.7	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
8		fourierdlem93.8	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
9		fourierdlem93.9	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
10	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
11	3 10	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
12	4 11	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
13	12	simprd	$⊢ φ \to ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
14	13	simplld	$⊢ φ \to Q (0) = - π$
15	14	eqcomd	$⊢ φ \to - π = Q (0)$
16	13	simplrd	$⊢ φ \to Q (M) = π$
17	16	eqcomd	$⊢ φ \to π = Q (M)$
18	15 17	oveq12d	$⊢ φ \to [- π, π] = [Q (0), Q (M)]$
19	18	itgeq1d	$⊢ φ \to \int_{[- π, π]} F (t) d t = \int_{[Q (0), Q (M)]} F (t) d t$
20		0zd	$⊢ φ \to 0 \in ℤ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22	3 21	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
23		1e0p1	$⊢ 1 = 0 + 1$
24	23	a1i	$⊢ φ \to 1 = 0 + 1$
25	24	fveq2d	$⊢ φ \to ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
26	22 25	eleqtrd	$⊢ φ \to M \in ℤ_{\geq (0 + 1)}$
27	1 3 4	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
28		pire	$⊢ π \in ℝ$
29	28	renegcli	$⊢ - π \in ℝ$
30		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
31	29 28 30	mp2an	$⊢ [- π, π] \subseteq ℝ$
32	31	a1i	$⊢ φ \to [- π, π] \subseteq ℝ$
33	27 32	fssd	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
34	13	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
35	34	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
36	6	adantr	$⊢ (φ \land t \in [Q (0), Q (M)]) \to F : [- π, π] ⟶ ℂ$
37		simpr	$⊢ (φ \land t \in [Q (0), Q (M)]) \to t \in [Q (0), Q (M)]$
38	18	eqcomd	$⊢ φ \to [Q (0), Q (M)] = [- π, π]$
39	38	adantr	$⊢ (φ \land t \in [Q (0), Q (M)]) \to [Q (0), Q (M)] = [- π, π]$
40	37 39	eleqtrd	$⊢ (φ \land t \in [Q (0), Q (M)]) \to t \in [- π, π]$
41	36 40	ffvelrnd	$⊢ (φ \land t \in [Q (0), Q (M)]) \to F (t) \in ℂ$
42	33	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
43		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
44	43	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
45	42 44	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
46		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
47	46	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
48	42 47	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
49	6	feqmptd	$⊢ φ \to F = (t \in [- π, π] ⟼ F (t))$
50	49	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F = (t \in [- π, π] ⟼ F (t))$
51	50	reseq1d	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = {(t \in [- π, π] ⟼ F (t)) ↾}_{(Q (i), Q (i + 1))}$
52		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
53	52	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
54	29	rexri	$⊢ - π \in ℝ^{*}$
55	54	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to - π \in ℝ^{*}$
56	28	rexri	$⊢ π \in ℝ^{*}$
57	56	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to π \in ℝ^{*}$
58	27	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to Q : (0 \dots M) ⟶ [- π, π]$
59		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to i \in (0 ..^M)$
60		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to t \in [Q (i), Q (i + 1)]$
61	55 57 58 59 60	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to t \in [- π, π]$
62	61	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall t \in [Q (i), Q (i + 1)] t \in [- π, π]$
63		dfss3	$⊢ [Q (i), Q (i + 1)] \subseteq [- π, π] \leftrightarrow \forall t \in [Q (i), Q (i + 1)] t \in [- π, π]$
64	62 63	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
65	53 64	sstrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
66	65	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(t \in [- π, π] ⟼ F (t)) ↾}_{(Q (i), Q (i + 1))} = (t \in (Q (i), Q (i + 1)) ⟼ F (t))$
67	51 66	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = (t \in (Q (i), Q (i + 1)) ⟼ F (t))$
68	67	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t)) = {F ↾}_{(Q (i), Q (i + 1))}$
69	68 7	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
70	67	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (t \in (Q (i), Q (i + 1)) ⟼ F (t)) {lim}_{ℂ} Q (i + 1)$
71	9 70	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((t \in (Q (i), Q (i + 1)) ⟼ F (t)) {lim}_{ℂ} Q (i + 1))$
72	67	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (t \in (Q (i), Q (i + 1)) ⟼ F (t)) {lim}_{ℂ} Q (i)$
73	8 72	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((t \in (Q (i), Q (i + 1)) ⟼ F (t)) {lim}_{ℂ} Q (i))$
74	45 48 69 71 73	iblcncfioo	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t)) \in 𝐿^{1}$
75	6	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to F : [- π, π] ⟶ ℂ$
76	75 61	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to F (t) \in ℂ$
77	45 48 74 76	ibliooicc	$⊢ (φ \land i \in (0 ..^M)) \to (t \in [Q (i), Q (i + 1)] ⟼ F (t)) \in 𝐿^{1}$
78	20 26 33 35 41 77	itgspltprt	$⊢ φ \to \int_{[Q (0), Q (M)]} F (t) d t = \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (t) d t$
79		fvres	$⊢ t \in [Q (i), Q (i + 1)] \to ({F ↾}_{[Q (i), Q (i + 1)]}) (t) = F (t)$
80	79	eqcomd	$⊢ t \in [Q (i), Q (i + 1)] \to F (t) = ({F ↾}_{[Q (i), Q (i + 1)]}) (t)$
81	80	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i), Q (i + 1)]) \to F (t) = ({F ↾}_{[Q (i), Q (i + 1)]}) (t)$
82	81	itgeq2dv	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i), Q (i + 1)]} F (t) d t = \int_{[Q (i), Q (i + 1)]} ({F ↾}_{[Q (i), Q (i + 1)]}) (t) d t$
83		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)]}) ↾}_{(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)]}) ↾}_{(Q (i), Q (i + 1))}) (x))))$
84	6	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : [- π, π] ⟶ ℂ$
85	84 64	fssresd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{[Q (i), Q (i + 1)]}) : [Q (i), Q (i + 1)] ⟶ ℂ$
86	53	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (i), Q (i + 1))}$
87	86 7	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
88	86	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
89	45 48 35 85	limcicciooub	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({F ↾}_{[Q (i), Q (i + 1)]}) {lim}_{ℂ} Q (i + 1)$
90	88 89	eqtr3d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({F ↾}_{[Q (i), Q (i + 1)]}) {lim}_{ℂ} Q (i + 1)$
91	9 90	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{[Q (i), Q (i + 1)]}) {lim}_{ℂ} Q (i + 1))$
92	86	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = {({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}$
93	92	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
94	45 48 35 85	limciccioolb	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({F ↾}_{[Q (i), Q (i + 1)]}) {lim}_{ℂ} Q (i)$
95	93 94	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({F ↾}_{[Q (i), Q (i + 1)]}) {lim}_{ℂ} Q (i)$
96	8 95	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{[Q (i), Q (i + 1)]}) {lim}_{ℂ} Q (i))$
97	5	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
98	83 45 48 35 85 87 91 96 97	fourierdlem82	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i), Q (i + 1)]} ({F ↾}_{[Q (i), Q (i + 1)]}) (t) d t = \int_{[Q (i) - X, Q (i + 1) - X]} ({F ↾}_{[Q (i), Q (i + 1)]}) (X + t) d t$
99	45	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to Q (i) \in ℝ$
100	48	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to Q (i + 1) \in ℝ$
101	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to X \in ℝ$
102	99 101	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to Q (i) - X \in ℝ$
103	100 101	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to Q (i + 1) - X \in ℝ$
104		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to t \in [Q (i) - X, Q (i + 1) - X]$
105		eliccre	$⊢ (Q (i) - X \in ℝ \land Q (i + 1) - X \in ℝ \land t \in [Q (i) - X, Q (i + 1) - X]) \to t \in ℝ$
106	102 103 104 105	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to t \in ℝ$
107	101 106	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to X + t \in ℝ$
108		elicc2	$⊢ (Q (i) - X \in ℝ \land Q (i + 1) - X \in ℝ) \to (t \in [Q (i) - X, Q (i + 1) - X] \leftrightarrow (t \in ℝ \land Q (i) - X \leq t \land t \leq Q (i + 1) - X))$
109	102 103 108	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to (t \in [Q (i) - X, Q (i + 1) - X] \leftrightarrow (t \in ℝ \land Q (i) - X \leq t \land t \leq Q (i + 1) - X))$
110	104 109	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to (t \in ℝ \land Q (i) - X \leq t \land t \leq Q (i + 1) - X)$
111	110	simp2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to Q (i) - X \leq t$
112	99 101 106	lesubadd2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to (Q (i) - X \leq t \leftrightarrow Q (i) \leq X + t)$
113	111 112	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to Q (i) \leq X + t$
114	110	simp3d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to t \leq Q (i + 1) - X$
115	101 106 100	leaddsub2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to (X + t \leq Q (i + 1) \leftrightarrow t \leq Q (i + 1) - X)$
116	114 115	mpbird	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to X + t \leq Q (i + 1)$
117	99 100 107 113 116	eliccd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to X + t \in [Q (i), Q (i + 1)]$
118		fvres	$⊢ X + t \in [Q (i), Q (i + 1)] \to ({F ↾}_{[Q (i), Q (i + 1)]}) (X + t) = F (X + t)$
119	117 118	syl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [Q (i) - X, Q (i + 1) - X]) \to ({F ↾}_{[Q (i), Q (i + 1)]}) (X + t) = F (X + t)$
120	119	itgeq2dv	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i) - X, Q (i + 1) - X]} ({F ↾}_{[Q (i), Q (i + 1)]}) (X + t) d t = \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
121	82 98 120	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[Q (i), Q (i + 1)]} F (t) d t = \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
122	121	sumeq2dv	$⊢ φ \to \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (t) d t = \sum_{i \in (0 ..^M)} \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
123		oveq2	$⊢ s = t \to X + s = X + t$
124	123	fveq2d	$⊢ s = t \to F (X + s) = F (X + t)$
125	124	cbvitgv	$⊢ \int_{[- π - X, π - X]} F (X + s) d s = \int_{[- π - X, π - X]} F (X + t) d t$
126	125	a1i	$⊢ φ \to \int_{[- π - X, π - X]} F (X + s) d s = \int_{[- π - X, π - X]} F (X + t) d t$
127	2	a1i	$⊢ φ \to H = (i \in (0 \dots M) ⟼ Q (i) - X)$
128		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
129	128	oveq1d	$⊢ i = 0 \to Q (i) - X = Q (0) - X$
130	129	adantl	$⊢ (φ \land i = 0) \to Q (i) - X = Q (0) - X$
131	3	nnzd	$⊢ φ \to M \in ℤ$
132		0le0	$⊢ 0 \leq 0$
133	132	a1i	$⊢ φ \to 0 \leq 0$
134		0red	$⊢ φ \to 0 \in ℝ$
135	3	nnred	$⊢ φ \to M \in ℝ$
136	3	nngt0d	$⊢ φ \to 0 < M$
137	134 135 136	ltled	$⊢ φ \to 0 \leq M$
138	20 131 20 133 137	elfzd	$⊢ φ \to 0 \in (0 \dots M)$
139	14 29	eqeltrdi	$⊢ φ \to Q (0) \in ℝ$
140	139 5	resubcld	$⊢ φ \to Q (0) - X \in ℝ$
141	127 130 138 140	fvmptd	$⊢ φ \to H (0) = Q (0) - X$
142	14	oveq1d	$⊢ φ \to Q (0) - X = - π - X$
143	141 142	eqtr2d	$⊢ φ \to - π - X = H (0)$
144		fveq2	$⊢ i = M \to Q (i) = Q (M)$
145	144	oveq1d	$⊢ i = M \to Q (i) - X = Q (M) - X$
146	145	adantl	$⊢ (φ \land i = M) \to Q (i) - X = Q (M) - X$
147	135	leidd	$⊢ φ \to M \leq M$
148	20 131 131 137 147	elfzd	$⊢ φ \to M \in (0 \dots M)$
149	16 28	eqeltrdi	$⊢ φ \to Q (M) \in ℝ$
150	149 5	resubcld	$⊢ φ \to Q (M) - X \in ℝ$
151	127 146 148 150	fvmptd	$⊢ φ \to H (M) = Q (M) - X$
152	16	oveq1d	$⊢ φ \to Q (M) - X = π - X$
153	151 152	eqtr2d	$⊢ φ \to π - X = H (M)$
154	143 153	oveq12d	$⊢ φ \to [- π - X, π - X] = [H (0), H (M)]$
155	154	itgeq1d	$⊢ φ \to \int_{[- π - X, π - X]} F (X + t) d t = \int_{[H (0), H (M)]} F (X + t) d t$
156	33	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
157	5	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℝ$
158	156 157	resubcld	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) - X \in ℝ$
159	158 2	fmptd	$⊢ φ \to H : (0 \dots M) ⟶ ℝ$
160	45 48 97 35	ltsub1dd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X < Q (i + 1) - X$
161	44 158	syldan	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X \in ℝ$
162	2	fvmpt2	$⊢ (i \in (0 \dots M) \land Q (i) - X \in ℝ) \to H (i) = Q (i) - X$
163	44 161 162	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to H (i) = Q (i) - X$
164		fveq2	$⊢ i = j \to Q (i) = Q (j)$
165	164	oveq1d	$⊢ i = j \to Q (i) - X = Q (j) - X$
166	165	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ Q (i) - X) = (j \in (0 \dots M) ⟼ Q (j) - X)$
167	2 166	eqtri	$⊢ H = (j \in (0 \dots M) ⟼ Q (j) - X)$
168	167	a1i	$⊢ (φ \land i \in (0 ..^M)) \to H = (j \in (0 \dots M) ⟼ Q (j) - X)$
169		fveq2	$⊢ j = i + 1 \to Q (j) = Q (i + 1)$
170	169	oveq1d	$⊢ j = i + 1 \to Q (j) - X = Q (i + 1) - X$
171	170	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to Q (j) - X = Q (i + 1) - X$
172	48 97	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - X \in ℝ$
173	168 171 47 172	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) = Q (i + 1) - X$
174	160 163 173	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to H (i) < H (i + 1)$
175		frn	$⊢ F : [- π, π] ⟶ ℂ \to ran F \subseteq ℂ$
176	6 175	syl	$⊢ φ \to ran F \subseteq ℂ$
177	176	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to ran F \subseteq ℂ$
178		ffun	$⊢ F : [- π, π] ⟶ ℂ \to Fun F$
179	6 178	syl	$⊢ φ \to Fun F$
180	179	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to Fun F$
181	29	a1i	$⊢ (φ \land t \in [H (0), H (M)]) \to - π \in ℝ$
182	28	a1i	$⊢ (φ \land t \in [H (0), H (M)]) \to π \in ℝ$
183	5	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to X \in ℝ$
184	141 140	eqeltrd	$⊢ φ \to H (0) \in ℝ$
185	184	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to H (0) \in ℝ$
186	151 150	eqeltrd	$⊢ φ \to H (M) \in ℝ$
187	186	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to H (M) \in ℝ$
188		simpr	$⊢ (φ \land t \in [H (0), H (M)]) \to t \in [H (0), H (M)]$
189		eliccre	$⊢ (H (0) \in ℝ \land H (M) \in ℝ \land t \in [H (0), H (M)]) \to t \in ℝ$
190	185 187 188 189	syl3anc	$⊢ (φ \land t \in [H (0), H (M)]) \to t \in ℝ$
191	183 190	readdcld	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \in ℝ$
192	128	adantl	$⊢ (φ \land i = 0) \to Q (i) = Q (0)$
193	192	oveq1d	$⊢ (φ \land i = 0) \to Q (i) - X = Q (0) - X$
194	127 193 138 140	fvmptd	$⊢ φ \to H (0) = Q (0) - X$
195	194	oveq2d	$⊢ φ \to X + H (0) = X + Q (0) - X$
196	5	recnd	$⊢ φ \to X \in ℂ$
197	139	recnd	$⊢ φ \to Q (0) \in ℂ$
198	196 197	pncan3d	$⊢ φ \to X + Q (0) - X = Q (0)$
199	195 198 14	3eqtrrd	$⊢ φ \to - π = X + H (0)$
200	199	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to - π = X + H (0)$
201		elicc2	$⊢ (H (0) \in ℝ \land H (M) \in ℝ) \to (t \in [H (0), H (M)] \leftrightarrow (t \in ℝ \land H (0) \leq t \land t \leq H (M)))$
202	185 187 201	syl2anc	$⊢ (φ \land t \in [H (0), H (M)]) \to (t \in [H (0), H (M)] \leftrightarrow (t \in ℝ \land H (0) \leq t \land t \leq H (M)))$
203	188 202	mpbid	$⊢ (φ \land t \in [H (0), H (M)]) \to (t \in ℝ \land H (0) \leq t \land t \leq H (M))$
204	203	simp2d	$⊢ (φ \land t \in [H (0), H (M)]) \to H (0) \leq t$
205	185 190 183 204	leadd2dd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + H (0) \leq X + t$
206	200 205	eqbrtrd	$⊢ (φ \land t \in [H (0), H (M)]) \to - π \leq X + t$
207	203	simp3d	$⊢ (φ \land t \in [H (0), H (M)]) \to t \leq H (M)$
208	190 187 183 207	leadd2dd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \leq X + H (M)$
209	151	oveq2d	$⊢ φ \to X + H (M) = X + Q (M) - X$
210	149	recnd	$⊢ φ \to Q (M) \in ℂ$
211	196 210	pncan3d	$⊢ φ \to X + Q (M) - X = Q (M)$
212	209 211 16	3eqtrrd	$⊢ φ \to π = X + H (M)$
213	212	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to π = X + H (M)$
214	208 213	breqtrrd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \leq π$
215	181 182 191 206 214	eliccd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \in [- π, π]$
216		fdm	$⊢ F : [- π, π] ⟶ ℂ \to dom F = [- π, π]$
217	6 216	syl	$⊢ φ \to dom F = [- π, π]$
218	217	eqcomd	$⊢ φ \to [- π, π] = dom F$
219	218	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to [- π, π] = dom F$
220	215 219	eleqtrd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \in dom F$
221		fvelrn	$⊢ (Fun F \land X + t \in dom F) \to F (X + t) \in ran F$
222	180 220 221	syl2anc	$⊢ (φ \land t \in [H (0), H (M)]) \to F (X + t) \in ran F$
223	177 222	sseldd	$⊢ (φ \land t \in [H (0), H (M)]) \to F (X + t) \in ℂ$
224	163 161	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in ℝ$
225	173 172	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in ℝ$
226	84 65	fssresd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
227	45	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
228	227	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i) \in ℝ^{*}$
229	48	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
230	229	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i + 1) \in ℝ^{*}$
231	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X \in ℝ$
232		elioore	$⊢ t \in (H (i), H (i + 1)) \to t \in ℝ$
233	232	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to t \in ℝ$
234	231 233	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t \in ℝ$
235	163	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to X + H (i) = X + Q (i) - X$
236	196	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℂ$
237	45	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
238	236 237	pncan3d	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i) - X = Q (i)$
239		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = Q (i)$
240	235 238 239	3eqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = X + H (i)$
241	240	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i) = X + H (i)$
242	224	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i) \in ℝ$
243		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to t \in (H (i), H (i + 1))$
244	242	rexrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i) \in ℝ^{*}$
245	225	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in ℝ^{*}$
246	245	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i + 1) \in ℝ^{*}$
247		elioo2	$⊢ (H (i) \in ℝ^{} \land H (i + 1) \in ℝ^{}) \to (t \in (H (i), H (i + 1)) \leftrightarrow (t \in ℝ \land H (i) < t \land t < H (i + 1)))$
248	244 246 247	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to (t \in (H (i), H (i + 1)) \leftrightarrow (t \in ℝ \land H (i) < t \land t < H (i + 1)))$
249	243 248	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to (t \in ℝ \land H (i) < t \land t < H (i + 1))$
250	249	simp2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i) < t$
251	242 233 231 250	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + H (i) < X + t$
252	241 251	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i) < X + t$
253	225	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i + 1) \in ℝ$
254	249	simp3d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to t < H (i + 1)$
255	233 253 231 254	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t < X + H (i + 1)$
256	173	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to X + H (i + 1) = X + Q (i + 1) - X$
257	48	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
258	236 257	pncan3d	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i + 1) - X = Q (i + 1)$
259	256 258	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to X + H (i + 1) = Q (i + 1)$
260	259	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + H (i + 1) = Q (i + 1)$
261	255 260	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t < Q (i + 1)$
262	228 230 234 252 261	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t \in (Q (i), Q (i + 1))$
263		eqid	$⊢ (t \in (H (i), H (i + 1)) ⟼ X + t) = (t \in (H (i), H (i + 1)) ⟼ X + t)$
264	262 263	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) : (H (i), H (i + 1)) ⟶ (Q (i), Q (i + 1))$
265		fcompt	$⊢ (({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \land (t \in (H (i), H (i + 1)) ⟼ X + t) : (H (i), H (i + 1)) ⟶ (Q (i), Q (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t) = (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((t \in (H (i), H (i + 1)) ⟼ X + t) (s)))$
266	226 264 265	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t) = (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((t \in (H (i), H (i + 1)) ⟼ X + t) (s)))$
267		oveq2	$⊢ t = r \to X + t = X + r$
268	267	cbvmptv	$⊢ (t \in (H (i), H (i + 1)) ⟼ X + t) = (r \in (H (i), H (i + 1)) ⟼ X + r)$
269	268	fveq1i	$⊢ (t \in (H (i), H (i + 1)) ⟼ X + t) (s) = (r \in (H (i), H (i + 1)) ⟼ X + r) (s)$
270	269	fveq2i	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) ((t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (s))$
271	270	mpteq2i	$⊢ (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (s)))$
272	271	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (s)))$
273		fveq2	$⊢ s = t \to (r \in (H (i), H (i + 1)) ⟼ X + r) (s) = (r \in (H (i), H (i + 1)) ⟼ X + r) (t)$
274	273	fveq2d	$⊢ s = t \to ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (s)) = ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (t))$
275	274	cbvmptv	$⊢ (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (s))) = (t \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (t)))$
276	275	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (s))) = (t \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (t)))$
277		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to (r \in (H (i), H (i + 1)) ⟼ X + r) = (r \in (H (i), H (i + 1)) ⟼ X + r)$
278		oveq2	$⊢ r = t \to X + r = X + t$
279	278	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \land r = t) \to X + r = X + t$
280	277 279 243 234	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to (r \in (H (i), H (i + 1)) ⟼ X + r) (t) = X + t$
281	280	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (t)) = ({F ↾}_{(Q (i), Q (i + 1))}) (X + t)$
282		fvres	$⊢ X + t \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (X + t) = F (X + t)$
283	262 282	syl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) (X + t) = F (X + t)$
284	281 283	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (t)) = F (X + t)$
285	284	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((r \in (H (i), H (i + 1)) ⟼ X + r) (t))) = (t \in (H (i), H (i + 1)) ⟼ F (X + t))$
286	272 276 285	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) ((t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (t \in (H (i), H (i + 1)) ⟼ F (X + t))$
287	266 286	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ F (X + t)) = ({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t)$
288		eqid	$⊢ (t \in ℂ ⟼ X + t) = (t \in ℂ ⟼ X + t)$
289		ssid	$⊢ ℂ \subseteq ℂ$
290	289	a1i	$⊢ X \in ℂ \to ℂ \subseteq ℂ$
291		id	$⊢ X \in ℂ \to X \in ℂ$
292	290 291 290	constcncfg	$⊢ X \in ℂ \to (t \in ℂ ⟼ X) : ℂ \underset{cn}{⟶} ℂ$
293		cncfmptid	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
294	289 289 293	mp2an	$⊢ (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
295	294	a1i	$⊢ X \in ℂ \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
296	292 295	addcncf	$⊢ X \in ℂ \to (t \in ℂ ⟼ X + t) : ℂ \underset{cn}{⟶} ℂ$
297	236 296	syl	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ℂ ⟼ X + t) : ℂ \underset{cn}{⟶} ℂ$
298		ioosscn	$⊢ (H (i), H (i + 1)) \subseteq ℂ$
299	298	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)) \subseteq ℂ$
300		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
301	300	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
302	288 297 299 301 262	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) : (H (i), H (i + 1)) \underset{cn}{⟶} (Q (i), Q (i + 1))$
303	302 7	cncfco	$⊢ (φ \land i \in (0 ..^M)) \to (({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t)) : (H (i), H (i + 1)) \underset{cn}{⟶} ℂ$
304	287 303	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ F (X + t)) : (H (i), H (i + 1)) \underset{cn}{⟶} ℂ$
305	227	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i) \in ℝ^{*}$
306	229	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i + 1) \in ℝ^{*}$
307		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)$
308		vex	$⊢ r \in V$
309	263	elrnmpt	$⊢ r \in V \to (r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t) \leftrightarrow \exists t \in (H (i), H (i + 1)) r = X + t)$
310	308 309	ax-mp	$⊢ r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t) \leftrightarrow \exists t \in (H (i), H (i + 1)) r = X + t$
311	307 310	sylib	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to \exists t \in (H (i), H (i + 1)) r = X + t$
312		nfv	$⊢ Ⅎ t (φ \land i \in (0 ..^M))$
313		nfmpt1	$⊢ \underline{Ⅎ} t (t \in (H (i), H (i + 1)) ⟼ X + t)$
314	313	nfrn	$⊢ \underline{Ⅎ} t ran (t \in (H (i), H (i + 1)) ⟼ X + t)$
315	314	nfcri	$⊢ Ⅎ t r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)$
316	312 315	nfan	$⊢ Ⅎ t ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t))$
317		nfv	$⊢ Ⅎ t r \in ℝ$
318		simp3	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to r = X + t$
319	5	3ad2ant1	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to X \in ℝ$
320	232	3ad2ant2	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to t \in ℝ$
321	319 320	readdcld	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to X + t \in ℝ$
322	318 321	eqeltrd	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to r \in ℝ$
323	322	3exp	$⊢ φ \to (t \in (H (i), H (i + 1)) \to (r = X + t \to r \in ℝ))$
324	323	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to r \in ℝ))$
325	316 317 324	rexlimd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to (\exists t \in (H (i), H (i + 1)) r = X + t \to r \in ℝ)$
326	311 325	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in ℝ$
327		nfv	$⊢ Ⅎ t Q (i) < r$
328	252	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to Q (i) < X + t$
329		simp3	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to r = X + t$
330	328 329	breqtrrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to Q (i) < r$
331	330	3exp	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to Q (i) < r))$
332	331	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to Q (i) < r))$
333	316 327 332	rexlimd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to (\exists t \in (H (i), H (i + 1)) r = X + t \to Q (i) < r)$
334	311 333	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i) < r$
335		nfv	$⊢ Ⅎ t r < Q (i + 1)$
336	261	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to X + t < Q (i + 1)$
337	329 336	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to r < Q (i + 1)$
338	337	3exp	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to r < Q (i + 1)))$
339	338	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to r < Q (i + 1)))$
340	316 335 339	rexlimd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to (\exists t \in (H (i), H (i + 1)) r = X + t \to r < Q (i + 1))$
341	311 340	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r < Q (i + 1)$
342	305 306 326 334 341	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in (Q (i), Q (i + 1))$
343	217	ineq2d	$⊢ φ \to (Q (i), Q (i + 1)) \cap dom F = (Q (i), Q (i + 1)) \cap [- π, π]$
344	343	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cap dom F = (Q (i), Q (i + 1)) \cap [- π, π]$
345		dmres	$⊢ dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1)) \cap dom F$
346	345	a1i	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1)) \cap dom F$
347		dfss	$⊢ (Q (i), Q (i + 1)) \subseteq [- π, π] \leftrightarrow (Q (i), Q (i + 1)) = (Q (i), Q (i + 1)) \cap [- π, π]$
348	65 347	sylib	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) = (Q (i), Q (i + 1)) \cap [- π, π]$
349	344 346 348	3eqtr4d	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
350	349	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
351	342 350	eleqtrrd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in dom ({F ↾}_{(Q (i), Q (i + 1))})$
352	326 341	ltned	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \neq Q (i + 1)$
353	352	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to \neg r = Q (i + 1)$
354		velsn	$⊢ r \in \{Q (i + 1)\} \leftrightarrow r = Q (i + 1)$
355	353 354	sylnibr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to \neg r \in \{Q (i + 1)\}$
356	351 355	eldifd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\})$
357	356	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t) r \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\})$
358		dfss3	$⊢ ran (t \in (H (i), H (i + 1)) ⟼ X + t) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\} \leftrightarrow \forall r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t) r \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\})$
359	357 358	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to ran (t \in (H (i), H (i + 1)) ⟼ X + t) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i + 1)\}$
360		eqid	$⊢ (s \in ℂ ⟼ X + s) = (s \in ℂ ⟼ X + s)$
361	196	adantr	$⊢ (φ \land s \in ℂ) \to X \in ℂ$
362		simpr	$⊢ (φ \land s \in ℂ) \to s \in ℂ$
363	361 362	addcomd	$⊢ (φ \land s \in ℂ) \to X + s = s + X$
364	363	mpteq2dva	$⊢ φ \to (s \in ℂ ⟼ X + s) = (s \in ℂ ⟼ s + X)$
365		eqid	$⊢ (s \in ℂ ⟼ s + X) = (s \in ℂ ⟼ s + X)$
366	365	addccncf	$⊢ X \in ℂ \to (s \in ℂ ⟼ s + X) : ℂ \underset{cn}{⟶} ℂ$
367	196 366	syl	$⊢ φ \to (s \in ℂ ⟼ s + X) : ℂ \underset{cn}{⟶} ℂ$
368	364 367	eqeltrd	$⊢ φ \to (s \in ℂ ⟼ X + s) : ℂ \underset{cn}{⟶} ℂ$
369	368	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℂ ⟼ X + s) : ℂ \underset{cn}{⟶} ℂ$
370	224	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in ℝ^{*}$
371		iocssre	$⊢ (H (i) \in ℝ^{*} \land H (i + 1) \in ℝ) \to (H (i), H (i + 1)] \subseteq ℝ$
372	370 225 371	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)] \subseteq ℝ$
373		ax-resscn	$⊢ ℝ \subseteq ℂ$
374	372 373	sstrdi	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)] \subseteq ℂ$
375	289	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℂ \subseteq ℂ$
376	196	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1)]) \to X \in ℂ$
377	374	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1)]) \to s \in ℂ$
378	376 377	addcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1)]) \to X + s \in ℂ$
379	360 369 374 375 378	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)] ⟼ X + s) : (H (i), H (i + 1)] \underset{cn}{⟶} ℂ$
380		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
381		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)] = TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]$
382	380	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
383		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
384	383	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
385	382 384	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
386	385	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
387	380 381 386	cncfcn	$⊢ ((H (i), H (i + 1)] \subseteq ℂ \land ℂ \subseteq ℂ) \to (H (i), H (i + 1)] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) Cn TopOpen (ℂ_{fld})$
388	374 375 387	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) Cn TopOpen (ℂ_{fld})$
389	379 388	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) Cn TopOpen (ℂ_{fld}))$
390	380	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
391	390	a1i	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
392		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (H (i), H (i + 1)] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)] \in TopOn ((H (i), H (i + 1)])$
393	391 374 392	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)] \in TopOn ((H (i), H (i + 1)])$
394		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)] \in TopOn ((H (i), H (i + 1)]) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to ((s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((s \in (H (i), H (i + 1)] ⟼ X + s) : (H (i), H (i + 1)] ⟶ ℂ \land \forall t \in (H (i), H (i + 1)] (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t)))$
395	393 391 394	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to ((s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((s \in (H (i), H (i + 1)] ⟼ X + s) : (H (i), H (i + 1)] ⟶ ℂ \land \forall t \in (H (i), H (i + 1)] (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t)))$
396	389 395	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to ((s \in (H (i), H (i + 1)] ⟼ X + s) : (H (i), H (i + 1)] ⟶ ℂ \land \forall t \in (H (i), H (i + 1)] (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t))$
397	396	simprd	$⊢ (φ \land i \in (0 ..^M)) \to \forall t \in (H (i), H (i + 1)] (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t)$
398		ubioc1	$⊢ (H (i) \in ℝ^{} \land H (i + 1) \in ℝ^{} \land H (i) < H (i + 1)) \to H (i + 1) \in (H (i), H (i + 1)]$
399	370 245 174 398	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in (H (i), H (i + 1)]$
400		fveq2	$⊢ t = H (i + 1) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (H (i + 1))$
401	400	eleq2d	$⊢ t = H (i + 1) \to ((s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t) \leftrightarrow (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (H (i + 1)))$
402	401	rspccva	$⊢ (\forall t \in (H (i), H (i + 1)] (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (t) \land H (i + 1) \in (H (i), H (i + 1)]) \to (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (H (i + 1))$
403	397 399 402	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)] ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (H (i + 1))$
404		ioounsn	$⊢ (H (i) \in ℝ^{} \land H (i + 1) \in ℝ^{} \land H (i) < H (i + 1)) \to (H (i), H (i + 1)) \cup \{H (i + 1)\} = (H (i), H (i + 1)]$
405	370 245 174 404	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)) \cup \{H (i + 1)\} = (H (i), H (i + 1)]$
406	259	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = X + H (i + 1)$
407	406	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land s = H (i + 1)) \to Q (i + 1) = X + H (i + 1)$
408		iftrue	$⊢ s = H (i + 1) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = Q (i + 1)$
409	408	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land s = H (i + 1)) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = Q (i + 1)$
410		oveq2	$⊢ s = H (i + 1) \to X + s = X + H (i + 1)$
411	410	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land s = H (i + 1)) \to X + s = X + H (i + 1)$
412	407 409 411	3eqtr4d	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land s = H (i + 1)) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
413		iffalse	$⊢ \neg s = H (i + 1) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = (t \in (H (i), H (i + 1)) ⟼ X + t) (s)$
414	413	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = (t \in (H (i), H (i + 1)) ⟼ X + t) (s)$
415		eqidd	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) = (t \in (H (i), H (i + 1)) ⟼ X + t)$
416		oveq2	$⊢ t = s \to X + t = X + s$
417	416	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \land t = s) \to X + t = X + s$
418		velsn	$⊢ s \in \{H (i + 1)\} \leftrightarrow s = H (i + 1)$
419	418	notbii	$⊢ \neg s \in \{H (i + 1)\} \leftrightarrow \neg s = H (i + 1)$
420		elun	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) \leftrightarrow (s \in (H (i), H (i + 1)) \lor s \in \{H (i + 1)\})$
421	420	biimpi	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) \to (s \in (H (i), H (i + 1)) \lor s \in \{H (i + 1)\})$
422	421	orcomd	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) \to (s \in \{H (i + 1)\} \lor s \in (H (i), H (i + 1)))$
423	422	ord	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) \to (\neg s \in \{H (i + 1)\} \to s \in (H (i), H (i + 1)))$
424	419 423	syl5bir	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) \to (\neg s = H (i + 1) \to s \in (H (i), H (i + 1)))$
425	424	imp	$⊢ (s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) \land \neg s = H (i + 1)) \to s \in (H (i), H (i + 1))$
426	425	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \to s \in (H (i), H (i + 1))$
427	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to X \in ℝ$
428		elioore	$⊢ s \in (H (i), H (i + 1)) \to s \in ℝ$
429	428	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1))) \to s \in ℝ$
430		elsni	$⊢ s \in \{H (i + 1)\} \to s = H (i + 1)$
431	430	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i + 1)\}) \to s = H (i + 1)$
432	225	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i + 1)\}) \to H (i + 1) \in ℝ$
433	431 432	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i + 1)\}) \to s \in ℝ$
434	429 433	jaodan	$⊢ ((φ \land i \in (0 ..^M)) \land (s \in (H (i), H (i + 1)) \lor s \in \{H (i + 1)\})) \to s \in ℝ$
435	420 434	sylan2b	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to s \in ℝ$
436	427 435	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to X + s \in ℝ$
437	436	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \to X + s \in ℝ$
438	415 417 426 437	fvmptd	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) (s) = X + s$
439	414 438	eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \land \neg s = H (i + 1)) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
440	412 439	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
441	405 440	mpteq12dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) ⟼ if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (s \in (H (i), H (i + 1)] ⟼ X + s)$
442	405	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]$
443	442	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\})) CnP TopOpen (ℂ_{fld}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})$
444	443	fveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\})) CnP TopOpen (ℂ_{fld})) (H (i + 1)) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) CnP TopOpen (ℂ_{fld})) (H (i + 1))$
445	403 441 444	3eltr4d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) ⟼ if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\})) CnP TopOpen (ℂ_{fld})) (H (i + 1))$
446		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\})$
447		eqid	$⊢ (s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) ⟼ if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) ⟼ if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)))$
448	264 301	fssd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) : (H (i), H (i + 1)) ⟶ ℂ$
449	225	recnd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in ℂ$
450	446 380 447 448 299 449	ellimc	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i + 1) \in ((t \in (H (i), H (i + 1)) ⟼ X + t) {lim}_{ℂ} H (i + 1)) \leftrightarrow (s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\}) ⟼ if (s = H (i + 1), Q (i + 1), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\})) CnP TopOpen (ℂ_{fld})) (H (i + 1)))$
451	445 450	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ((t \in (H (i), H (i + 1)) ⟼ X + t) {lim}_{ℂ} H (i + 1))$
452	359 451 9	limccog	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t)) {lim}_{ℂ} H (i + 1))$
453	266 286	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t) = (t \in (H (i), H (i + 1)) ⟼ F (X + t))$
454	453	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t)) {lim}_{ℂ} H (i + 1) = (t \in (H (i), H (i + 1)) ⟼ F (X + t)) {lim}_{ℂ} H (i + 1)$
455	452 454	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((t \in (H (i), H (i + 1)) ⟼ F (X + t)) {lim}_{ℂ} H (i + 1))$
456	45	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i) \in ℝ$
457	456 334	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \neq Q (i)$
458	457	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to \neg r = Q (i)$
459		velsn	$⊢ r \in \{Q (i)\} \leftrightarrow r = Q (i)$
460	458 459	sylnibr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to \neg r \in \{Q (i)\}$
461	351 460	eldifd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\})$
462	461	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t) r \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\})$
463		dfss3	$⊢ ran (t \in (H (i), H (i + 1)) ⟼ X + t) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\} \leftrightarrow \forall r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t) r \in (dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\})$
464	462 463	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to ran (t \in (H (i), H (i + 1)) ⟼ X + t) \subseteq dom ({F ↾}_{(Q (i), Q (i + 1))}) ∖ \{Q (i)\}$
465		icossre	$⊢ (H (i) \in ℝ \land H (i + 1) \in ℝ^{*}) \to [H (i), H (i + 1)) \subseteq ℝ$
466	224 245 465	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)) \subseteq ℝ$
467	466 373	sstrdi	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)) \subseteq ℂ$
468	196	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in [H (i), H (i + 1))) \to X \in ℂ$
469	467	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land s \in [H (i), H (i + 1))) \to s \in ℂ$
470	468 469	addcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in [H (i), H (i + 1))) \to X + s \in ℂ$
471	360 369 467 375 470	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (s \in [H (i), H (i + 1)) ⟼ X + s) : [H (i), H (i + 1)) \underset{cn}{⟶} ℂ$
472		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1)) = TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))$
473	380 472 386	cncfcn	$⊢ ([H (i), H (i + 1)) \subseteq ℂ \land ℂ \subseteq ℂ) \to [H (i), H (i + 1)) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) Cn TopOpen (ℂ_{fld})$
474	467 375 473	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) Cn TopOpen (ℂ_{fld})$
475	471 474	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) Cn TopOpen (ℂ_{fld}))$
476		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [H (i), H (i + 1)) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1)) \in TopOn ([H (i), H (i + 1)))$
477	391 467 476	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1)) \in TopOn ([H (i), H (i + 1)))$
478		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1)) \in TopOn ([H (i), H (i + 1))) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to ((s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((s \in [H (i), H (i + 1)) ⟼ X + s) : [H (i), H (i + 1)) ⟶ ℂ \land \forall t \in [H (i), H (i + 1)) (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t)))$
479	477 391 478	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to ((s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((s \in [H (i), H (i + 1)) ⟼ X + s) : [H (i), H (i + 1)) ⟶ ℂ \land \forall t \in [H (i), H (i + 1)) (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t)))$
480	475 479	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to ((s \in [H (i), H (i + 1)) ⟼ X + s) : [H (i), H (i + 1)) ⟶ ℂ \land \forall t \in [H (i), H (i + 1)) (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t))$
481	480	simprd	$⊢ (φ \land i \in (0 ..^M)) \to \forall t \in [H (i), H (i + 1)) (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t)$
482		lbico1	$⊢ (H (i) \in ℝ^{} \land H (i + 1) \in ℝ^{} \land H (i) < H (i + 1)) \to H (i) \in [H (i), H (i + 1))$
483	370 245 174 482	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in [H (i), H (i + 1))$
484		fveq2	$⊢ t = H (i) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (H (i))$
485	484	eleq2d	$⊢ t = H (i) \to ((s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t) \leftrightarrow (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (H (i)))$
486	485	rspccva	$⊢ (\forall t \in [H (i), H (i + 1)) (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (t) \land H (i) \in [H (i), H (i + 1))) \to (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (H (i))$
487	481 483 486	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (s \in [H (i), H (i + 1)) ⟼ X + s) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (H (i))$
488		uncom	$⊢ (H (i), H (i + 1)) \cup \{H (i)\} = \{H (i)\} \cup (H (i), H (i + 1))$
489		snunioo	$⊢ (H (i) \in ℝ^{} \land H (i + 1) \in ℝ^{} \land H (i) < H (i + 1)) \to \{H (i)\} \cup (H (i), H (i + 1)) = [H (i), H (i + 1))$
490	370 245 174 489	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to \{H (i)\} \cup (H (i), H (i + 1)) = [H (i), H (i + 1))$
491	488 490	syl5eq	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)) \cup \{H (i)\} = [H (i), H (i + 1))$
492		iftrue	$⊢ s = H (i) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = Q (i)$
493	492	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s = H (i)) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = Q (i)$
494	240	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s = H (i)) \to Q (i) = X + H (i)$
495		oveq2	$⊢ s = H (i) \to X + s = X + H (i)$
496	495	eqcomd	$⊢ s = H (i) \to X + H (i) = X + s$
497	496	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s = H (i)) \to X + H (i) = X + s$
498	493 494 497	3eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s = H (i)) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
499	498	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land s = H (i)) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
500		iffalse	$⊢ \neg s = H (i) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = (t \in (H (i), H (i + 1)) ⟼ X + t) (s)$
501	500	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = (t \in (H (i), H (i + 1)) ⟼ X + t) (s)$
502		eqidd	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) = (t \in (H (i), H (i + 1)) ⟼ X + t)$
503	416	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \land t = s) \to X + t = X + s$
504		velsn	$⊢ s \in \{H (i)\} \leftrightarrow s = H (i)$
505	504	notbii	$⊢ \neg s \in \{H (i)\} \leftrightarrow \neg s = H (i)$
506		elun	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \leftrightarrow (s \in (H (i), H (i + 1)) \lor s \in \{H (i)\})$
507	506	biimpi	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (s \in (H (i), H (i + 1)) \lor s \in \{H (i)\})$
508	507	orcomd	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (s \in \{H (i)\} \lor s \in (H (i), H (i + 1)))$
509	508	ord	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (\neg s \in \{H (i)\} \to s \in (H (i), H (i + 1)))$
510	505 509	syl5bir	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (\neg s = H (i) \to s \in (H (i), H (i + 1)))$
511	510	imp	$⊢ (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \land \neg s = H (i)) \to s \in (H (i), H (i + 1))$
512	511	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \to s \in (H (i), H (i + 1))$
513	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to X \in ℝ$
514		elsni	$⊢ s \in \{H (i)\} \to s = H (i)$
515	514	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i)\}) \to s = H (i)$
516	224	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i)\}) \to H (i) \in ℝ$
517	515 516	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i)\}) \to s \in ℝ$
518	429 517	jaodan	$⊢ ((φ \land i \in (0 ..^M)) \land (s \in (H (i), H (i + 1)) \lor s \in \{H (i)\})) \to s \in ℝ$
519	506 518	sylan2b	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to s \in ℝ$
520	513 519	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to X + s \in ℝ$
521	520	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \to X + s \in ℝ$
522	502 503 512 521	fvmptd	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) (s) = X + s$
523	501 522	eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \land \neg s = H (i)) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
524	499 523	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = X + s$
525	491 524	mpteq12dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) ⟼ if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (s \in [H (i), H (i + 1)) ⟼ X + s)$
526	491	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))$
527	526	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\})) CnP TopOpen (ℂ_{fld}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})$
528	527	fveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\})) CnP TopOpen (ℂ_{fld})) (H (i)) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) CnP TopOpen (ℂ_{fld})) (H (i))$
529	487 525 528	3eltr4d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) ⟼ if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\})) CnP TopOpen (ℂ_{fld})) (H (i))$
530		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\})$
531		eqid	$⊢ (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) ⟼ if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) = (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) ⟼ if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)))$
532	224	recnd	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in ℂ$
533	530 380 531 448 299 532	ellimc	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) \in ((t \in (H (i), H (i + 1)) ⟼ X + t) {lim}_{ℂ} H (i)) \leftrightarrow (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) ⟼ if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\})) CnP TopOpen (ℂ_{fld})) (H (i)))$
534	529 533	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((t \in (H (i), H (i + 1)) ⟼ X + t) {lim}_{ℂ} H (i))$
535	464 534 8	limccog	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t)) {lim}_{ℂ} H (i))$
536	453	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (({F ↾}_{(Q (i), Q (i + 1))}) \circ (t \in (H (i), H (i + 1)) ⟼ X + t)) {lim}_{ℂ} H (i) = (t \in (H (i), H (i + 1)) ⟼ F (X + t)) {lim}_{ℂ} H (i)$
537	535 536	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((t \in (H (i), H (i + 1)) ⟼ F (X + t)) {lim}_{ℂ} H (i))$
538	224 225 304 455 537	iblcncfioo	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ F (X + t)) \in 𝐿^{1}$
539	6	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to F : [- π, π] ⟶ ℂ$
540	54	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to - π \in ℝ^{*}$
541	56	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to π \in ℝ^{*}$
542	27	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to Q : (0 \dots M) ⟶ [- π, π]$
543		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to i \in (0 ..^M)$
544		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to t \in [H (i), H (i + 1)]$
545	163 173	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)] = [Q (i) - X, Q (i + 1) - X]$
546	545	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to [H (i), H (i + 1)] = [Q (i) - X, Q (i + 1) - X]$
547	544 546	eleqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to t \in [Q (i) - X, Q (i + 1) - X]$
548	547 117	syldan	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to X + t \in [Q (i), Q (i + 1)]$
549	540 541 542 543 548	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to X + t \in [- π, π]$
550	539 549	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to F (X + t) \in ℂ$
551	224 225 538 550	ibliooicc	$⊢ (φ \land i \in (0 ..^M)) \to (t \in [H (i), H (i + 1)] ⟼ F (X + t)) \in 𝐿^{1}$
552	20 26 159 174 223 551	itgspltprt	$⊢ φ \to \int_{[H (0), H (M)]} F (X + t) d t = \sum_{i \in (0 ..^M)} \int_{[H (i), H (i + 1)]} F (X + t) d t$
553	545	itgeq1d	$⊢ (φ \land i \in (0 ..^M)) \to \int_{[H (i), H (i + 1)]} F (X + t) d t = \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
554	553	sumeq2dv	$⊢ φ \to \sum_{i \in (0 ..^M)} \int_{[H (i), H (i + 1)]} F (X + t) d t = \sum_{i \in (0 ..^M)} \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
555	552 554	eqtrd	$⊢ φ \to \int_{[H (0), H (M)]} F (X + t) d t = \sum_{i \in (0 ..^M)} \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
556	126 155 555	3eqtrd	$⊢ φ \to \int_{[- π - X, π - X]} F (X + s) d s = \sum_{i \in (0 ..^M)} \int_{[Q (i) - X, Q (i + 1) - X]} F (X + t) d t$
557	122 556	eqtr4d	$⊢ φ \to \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (t) d t = \int_{[- π - X, π - X]} F (X + s) d s$
558	19 78 557	3eqtrd	$⊢ φ \to \int_{[- π, π]} F (t) d t = \int_{[- π - X, π - X]} F (X + s) d s$

Metamath Proof Explorer

Theorem fourierdlem93

Proof