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	20 131 20	3jca	$⊢ φ \to (0 \in ℤ \land M \in ℤ \land 0 \in ℤ)$
133		0le0	$⊢ 0 \leq 0$
134	133	a1i	$⊢ φ \to 0 \leq 0$
135		0red	$⊢ φ \to 0 \in ℝ$
136	3	nnred	$⊢ φ \to M \in ℝ$
137	3	nngt0d	$⊢ φ \to 0 < M$
138	135 136 137	ltled	$⊢ φ \to 0 \leq M$
139	134 138	jca	$⊢ φ \to (0 \leq 0 \land 0 \leq M)$
140		elfz2	$⊢ 0 \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land 0 \in ℤ) \land (0 \leq 0 \land 0 \leq M))$
141	132 139 140	sylanbrc	$⊢ φ \to 0 \in (0 \dots M)$
142	14 29	eqeltrdi	$⊢ φ \to Q (0) \in ℝ$
143	142 5	resubcld	$⊢ φ \to Q (0) - X \in ℝ$
144	127 130 141 143	fvmptd	$⊢ φ \to H (0) = Q (0) - X$
145	14	oveq1d	$⊢ φ \to Q (0) - X = - π - X$
146	144 145	eqtr2d	$⊢ φ \to - π - X = H (0)$
147		fveq2	$⊢ i = M \to Q (i) = Q (M)$
148	147	oveq1d	$⊢ i = M \to Q (i) - X = Q (M) - X$
149	148	adantl	$⊢ (φ \land i = M) \to Q (i) - X = Q (M) - X$
150	20 131 131	3jca	$⊢ φ \to (0 \in ℤ \land M \in ℤ \land M \in ℤ)$
151	136	leidd	$⊢ φ \to M \leq M$
152	138 151	jca	$⊢ φ \to (0 \leq M \land M \leq M)$
153		elfz2	$⊢ M \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land M \in ℤ) \land (0 \leq M \land M \leq M))$
154	150 152 153	sylanbrc	$⊢ φ \to M \in (0 \dots M)$
155	16 28	eqeltrdi	$⊢ φ \to Q (M) \in ℝ$
156	155 5	resubcld	$⊢ φ \to Q (M) - X \in ℝ$
157	127 149 154 156	fvmptd	$⊢ φ \to H (M) = Q (M) - X$
158	16	oveq1d	$⊢ φ \to Q (M) - X = π - X$
159	157 158	eqtr2d	$⊢ φ \to π - X = H (M)$
160	146 159	oveq12d	$⊢ φ \to [- π - X, π - X] = [H (0), H (M)]$
161	160	itgeq1d	$⊢ φ \to \int_{[- π - X, π - X]} F (X + t) d t = \int_{[H (0), H (M)]} F (X + t) d t$
162	33	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
163	5	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℝ$
164	162 163	resubcld	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) - X \in ℝ$
165	164 2	fmptd	$⊢ φ \to H : (0 \dots M) ⟶ ℝ$
166	45 48 97 35	ltsub1dd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X < Q (i + 1) - X$
167	44 164	syldan	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - X \in ℝ$
168	2	fvmpt2	$⊢ (i \in (0 \dots M) \land Q (i) - X \in ℝ) \to H (i) = Q (i) - X$
169	44 167 168	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to H (i) = Q (i) - X$
170		fveq2	$⊢ i = j \to Q (i) = Q (j)$
171	170	oveq1d	$⊢ i = j \to Q (i) - X = Q (j) - X$
172	171	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ Q (i) - X) = (j \in (0 \dots M) ⟼ Q (j) - X)$
173	2 172	eqtri	$⊢ H = (j \in (0 \dots M) ⟼ Q (j) - X)$
174	173	a1i	$⊢ (φ \land i \in (0 ..^M)) \to H = (j \in (0 \dots M) ⟼ Q (j) - X)$
175		fveq2	$⊢ j = i + 1 \to Q (j) = Q (i + 1)$
176	175	oveq1d	$⊢ j = i + 1 \to Q (j) - X = Q (i + 1) - X$
177	176	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to Q (j) - X = Q (i + 1) - X$
178	48 97	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - X \in ℝ$
179	174 177 47 178	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) = Q (i + 1) - X$
180	166 169 179	3brtr4d	$⊢ (φ \land i \in (0 ..^M)) \to H (i) < H (i + 1)$
181		frn	$⊢ F : [- π, π] ⟶ ℂ \to ran F \subseteq ℂ$
182	6 181	syl	$⊢ φ \to ran F \subseteq ℂ$
183	182	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to ran F \subseteq ℂ$
184		ffun	$⊢ F : [- π, π] ⟶ ℂ \to Fun F$
185	6 184	syl	$⊢ φ \to Fun F$
186	185	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to Fun F$
187	29	a1i	$⊢ (φ \land t \in [H (0), H (M)]) \to - π \in ℝ$
188	28	a1i	$⊢ (φ \land t \in [H (0), H (M)]) \to π \in ℝ$
189	5	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to X \in ℝ$
190	144 143	eqeltrd	$⊢ φ \to H (0) \in ℝ$
191	190	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to H (0) \in ℝ$
192	157 156	eqeltrd	$⊢ φ \to H (M) \in ℝ$
193	192	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to H (M) \in ℝ$
194		simpr	$⊢ (φ \land t \in [H (0), H (M)]) \to t \in [H (0), H (M)]$
195		eliccre	$⊢ (H (0) \in ℝ \land H (M) \in ℝ \land t \in [H (0), H (M)]) \to t \in ℝ$
196	191 193 194 195	syl3anc	$⊢ (φ \land t \in [H (0), H (M)]) \to t \in ℝ$
197	189 196	readdcld	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \in ℝ$
198	128	adantl	$⊢ (φ \land i = 0) \to Q (i) = Q (0)$
199	198	oveq1d	$⊢ (φ \land i = 0) \to Q (i) - X = Q (0) - X$
200	127 199 141 143	fvmptd	$⊢ φ \to H (0) = Q (0) - X$
201	200	oveq2d	$⊢ φ \to X + H (0) = X + Q (0) - X$
202	5	recnd	$⊢ φ \to X \in ℂ$
203	142	recnd	$⊢ φ \to Q (0) \in ℂ$
204	202 203	pncan3d	$⊢ φ \to X + Q (0) - X = Q (0)$
205	201 204 14	3eqtrrd	$⊢ φ \to - π = X + H (0)$
206	205	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to - π = X + H (0)$
207		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)))$
208	191 193 207	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)))$
209	194 208	mpbid	$⊢ (φ \land t \in [H (0), H (M)]) \to (t \in ℝ \land H (0) \leq t \land t \leq H (M))$
210	209	simp2d	$⊢ (φ \land t \in [H (0), H (M)]) \to H (0) \leq t$
211	191 196 189 210	leadd2dd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + H (0) \leq X + t$
212	206 211	eqbrtrd	$⊢ (φ \land t \in [H (0), H (M)]) \to - π \leq X + t$
213	209	simp3d	$⊢ (φ \land t \in [H (0), H (M)]) \to t \leq H (M)$
214	196 193 189 213	leadd2dd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \leq X + H (M)$
215	157	oveq2d	$⊢ φ \to X + H (M) = X + Q (M) - X$
216	155	recnd	$⊢ φ \to Q (M) \in ℂ$
217	202 216	pncan3d	$⊢ φ \to X + Q (M) - X = Q (M)$
218	215 217 16	3eqtrrd	$⊢ φ \to π = X + H (M)$
219	218	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to π = X + H (M)$
220	214 219	breqtrrd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \leq π$
221	187 188 197 212 220	eliccd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \in [- π, π]$
222		fdm	$⊢ F : [- π, π] ⟶ ℂ \to dom F = [- π, π]$
223	6 222	syl	$⊢ φ \to dom F = [- π, π]$
224	223	eqcomd	$⊢ φ \to [- π, π] = dom F$
225	224	adantr	$⊢ (φ \land t \in [H (0), H (M)]) \to [- π, π] = dom F$
226	221 225	eleqtrd	$⊢ (φ \land t \in [H (0), H (M)]) \to X + t \in dom F$
227		fvelrn	$⊢ (Fun F \land X + t \in dom F) \to F (X + t) \in ran F$
228	186 226 227	syl2anc	$⊢ (φ \land t \in [H (0), H (M)]) \to F (X + t) \in ran F$
229	183 228	sseldd	$⊢ (φ \land t \in [H (0), H (M)]) \to F (X + t) \in ℂ$
230	169 167	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in ℝ$
231	179 178	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in ℝ$
232	84 65	fssresd	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
233	45	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
234	233	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i) \in ℝ^{*}$
235	48	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
236	235	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i + 1) \in ℝ^{*}$
237	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X \in ℝ$
238		elioore	$⊢ t \in (H (i), H (i + 1)) \to t \in ℝ$
239	238	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to t \in ℝ$
240	237 239	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t \in ℝ$
241	169	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to X + H (i) = X + Q (i) - X$
242	202	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℂ$
243	45	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
244	242 243	pncan3d	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i) - X = Q (i)$
245		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = Q (i)$
246	241 244 245	3eqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = X + H (i)$
247	246	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i) = X + H (i)$
248	230	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i) \in ℝ$
249		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to t \in (H (i), H (i + 1))$
250	248	rexrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i) \in ℝ^{*}$
251	231	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in ℝ^{*}$
252	251	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i + 1) \in ℝ^{*}$
253		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)))$
254	250 252 253	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)))$
255	249 254	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))$
256	255	simp2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i) < t$
257	248 239 237 256	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + H (i) < X + t$
258	247 257	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to Q (i) < X + t$
259	231	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to H (i + 1) \in ℝ$
260	255	simp3d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to t < H (i + 1)$
261	239 259 237 260	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t < X + H (i + 1)$
262	179	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to X + H (i + 1) = X + Q (i + 1) - X$
263	48	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
264	242 263	pncan3d	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i + 1) - X = Q (i + 1)$
265	262 264	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to X + H (i + 1) = Q (i + 1)$
266	265	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + H (i + 1) = Q (i + 1)$
267	261 266	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t < Q (i + 1)$
268	234 236 240 258 267	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \to X + t \in (Q (i), Q (i + 1))$
269		eqid	$⊢ (t \in (H (i), H (i + 1)) ⟼ X + t) = (t \in (H (i), H (i + 1)) ⟼ X + t)$
270	268 269	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))$
271		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)))$
272	232 270 271	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)))$
273		oveq2	$⊢ t = r \to X + t = X + r$
274	273	cbvmptv	$⊢ (t \in (H (i), H (i + 1)) ⟼ X + t) = (r \in (H (i), H (i + 1)) ⟼ X + r)$
275	274	fveq1i	$⊢ (t \in (H (i), H (i + 1)) ⟼ X + t) (s) = (r \in (H (i), H (i + 1)) ⟼ X + r) (s)$
276	275	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))$
277	276	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)))$
278	277	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)))$
279		fveq2	$⊢ s = t \to (r \in (H (i), H (i + 1)) ⟼ X + r) (s) = (r \in (H (i), H (i + 1)) ⟼ X + r) (t)$
280	279	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))$
281	280	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)))$
282	281	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)))$
283		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)$
284		oveq2	$⊢ r = t \to X + r = X + t$
285	284	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1))) \land r = t) \to X + r = X + t$
286	283 285 249 240	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$
287	286	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)$
288		fvres	$⊢ X + t \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (X + t) = F (X + t)$
289	268 288	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)$
290	287 289	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)$
291	290	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))$
292	278 282 291	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))$
293	272 292	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)$
294		eqid	$⊢ (t \in ℂ ⟼ X + t) = (t \in ℂ ⟼ X + t)$
295		ssid	$⊢ ℂ \subseteq ℂ$
296	295	a1i	$⊢ X \in ℂ \to ℂ \subseteq ℂ$
297		id	$⊢ X \in ℂ \to X \in ℂ$
298	296 297 296	constcncfg	$⊢ X \in ℂ \to (t \in ℂ ⟼ X) : ℂ \underset{cn}{⟶} ℂ$
299		cncfmptid	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
300	295 295 299	mp2an	$⊢ (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
301	300	a1i	$⊢ X \in ℂ \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
302	298 301	addcncf	$⊢ X \in ℂ \to (t \in ℂ ⟼ X + t) : ℂ \underset{cn}{⟶} ℂ$
303	242 302	syl	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ℂ ⟼ X + t) : ℂ \underset{cn}{⟶} ℂ$
304		ioosscn	$⊢ (H (i), H (i + 1)) \subseteq ℂ$
305	304	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)) \subseteq ℂ$
306		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
307	306	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
308	294 303 305 307 268	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))$
309	308 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}{⟶} ℂ$
310	293 309	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ F (X + t)) : (H (i), H (i + 1)) \underset{cn}{⟶} ℂ$
311	233	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i) \in ℝ^{*}$
312	235	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i + 1) \in ℝ^{*}$
313		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)$
314		vex	$⊢ r \in V$
315	269	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)$
316	314 315	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$
317	313 316	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$
318		nfv	$⊢ Ⅎ t (φ \land i \in (0 ..^M))$
319		nfmpt1	$⊢ \underline{Ⅎ} t (t \in (H (i), H (i + 1)) ⟼ X + t)$
320	319	nfrn	$⊢ \underline{Ⅎ} t ran (t \in (H (i), H (i + 1)) ⟼ X + t)$
321	320	nfcri	$⊢ Ⅎ t r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)$
322	318 321	nfan	$⊢ Ⅎ t ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t))$
323		nfv	$⊢ Ⅎ t r \in ℝ$
324		simp3	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to r = X + t$
325	5	3ad2ant1	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to X \in ℝ$
326	238	3ad2ant2	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to t \in ℝ$
327	325 326	readdcld	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to X + t \in ℝ$
328	324 327	eqeltrd	$⊢ (φ \land t \in (H (i), H (i + 1)) \land r = X + t) \to r \in ℝ$
329	328	3exp	$⊢ φ \to (t \in (H (i), H (i + 1)) \to (r = X + t \to r \in ℝ))$
330	329	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 ℝ))$
331	322 323 330	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 ℝ)$
332	317 331	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \in ℝ$
333		nfv	$⊢ Ⅎ t Q (i) < r$
334	258	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to Q (i) < X + t$
335		simp3	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to r = X + t$
336	334 335	breqtrrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to Q (i) < r$
337	336	3exp	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to Q (i) < r))$
338	337	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))$
339	322 333 338	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)$
340	317 339	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i) < r$
341		nfv	$⊢ Ⅎ t r < Q (i + 1)$
342	267	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to X + t < Q (i + 1)$
343	335 342	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (H (i), H (i + 1)) \land r = X + t) \to r < Q (i + 1)$
344	343	3exp	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) \to (r = X + t \to r < Q (i + 1)))$
345	344	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)))$
346	322 341 345	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))$
347	317 346	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r < Q (i + 1)$
348	311 312 332 340 347	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))$
349	223	ineq2d	$⊢ φ \to (Q (i), Q (i + 1)) \cap dom F = (Q (i), Q (i + 1)) \cap [- π, π]$
350	349	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cap dom F = (Q (i), Q (i + 1)) \cap [- π, π]$
351		dmres	$⊢ dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1)) \cap dom F$
352	351	a1i	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1)) \cap dom F$
353		dfss	$⊢ (Q (i), Q (i + 1)) \subseteq [- π, π] \leftrightarrow (Q (i), Q (i + 1)) = (Q (i), Q (i + 1)) \cap [- π, π]$
354	65 353	sylib	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) = (Q (i), Q (i + 1)) \cap [- π, π]$
355	350 352 354	3eqtr4d	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
356	355	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))$
357	348 356	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))})$
358	332 347	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)$
359	358	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)$
360		velsn	$⊢ r \in \{Q (i + 1)\} \leftrightarrow r = Q (i + 1)$
361	359 360	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)\}$
362	357 361	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)\})$
363	362	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)\})$
364		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)\})$
365	363 364	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)\}$
366		eqid	$⊢ (s \in ℂ ⟼ X + s) = (s \in ℂ ⟼ X + s)$
367	202	adantr	$⊢ (φ \land s \in ℂ) \to X \in ℂ$
368		simpr	$⊢ (φ \land s \in ℂ) \to s \in ℂ$
369	367 368	addcomd	$⊢ (φ \land s \in ℂ) \to X + s = s + X$
370	369	mpteq2dva	$⊢ φ \to (s \in ℂ ⟼ X + s) = (s \in ℂ ⟼ s + X)$
371		eqid	$⊢ (s \in ℂ ⟼ s + X) = (s \in ℂ ⟼ s + X)$
372	371	addccncf	$⊢ X \in ℂ \to (s \in ℂ ⟼ s + X) : ℂ \underset{cn}{⟶} ℂ$
373	202 372	syl	$⊢ φ \to (s \in ℂ ⟼ s + X) : ℂ \underset{cn}{⟶} ℂ$
374	370 373	eqeltrd	$⊢ φ \to (s \in ℂ ⟼ X + s) : ℂ \underset{cn}{⟶} ℂ$
375	374	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℂ ⟼ X + s) : ℂ \underset{cn}{⟶} ℂ$
376	230	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in ℝ^{*}$
377		iocssre	$⊢ (H (i) \in ℝ^{*} \land H (i + 1) \in ℝ) \to (H (i), H (i + 1)] \subseteq ℝ$
378	376 231 377	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)] \subseteq ℝ$
379		ax-resscn	$⊢ ℝ \subseteq ℂ$
380	378 379	sstrdi	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)] \subseteq ℂ$
381	295	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℂ \subseteq ℂ$
382	202	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1)]) \to X \in ℂ$
383	380	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1)]) \to s \in ℂ$
384	382 383	addcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1)]) \to X + s \in ℂ$
385	366 375 380 381 384	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (H (i), H (i + 1)] ⟼ X + s) : (H (i), H (i + 1)] \underset{cn}{⟶} ℂ$
386		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
387		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)] = TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]$
388	386	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
389		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
390	389	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
391	388 390	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
392	391	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
393	386 387 392	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})$
394	380 381 393	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)]) Cn TopOpen (ℂ_{fld})$
395	385 394	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}))$
396	386	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
397	396	a1i	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
398		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)])$
399	397 380 398	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (H (i), H (i + 1)] \in TopOn ((H (i), H (i + 1)])$
400		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)))$
401	399 397 400	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)))$
402	395 401	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))$
403	402	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)$
404		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)]$
405	376 251 180 404	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in (H (i), H (i + 1)]$
406		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))$
407	406	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)))$
408	407	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))$
409	403 405 408	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))$
410		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)]$
411	376 251 180 410	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)) \cup \{H (i + 1)\} = (H (i), H (i + 1)]$
412	265	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = X + H (i + 1)$
413	412	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)$
414		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)$
415	414	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)$
416		oveq2	$⊢ s = H (i + 1) \to X + s = X + H (i + 1)$
417	416	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)$
418	413 415 417	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$
419		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)$
420	419	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)$
421		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)$
422		oveq2	$⊢ t = s \to X + t = X + s$
423	422	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$
424		velsn	$⊢ s \in \{H (i + 1)\} \leftrightarrow s = H (i + 1)$
425	424	notbii	$⊢ \neg s \in \{H (i + 1)\} \leftrightarrow \neg s = H (i + 1)$
426		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)\})$
427	426	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)\})$
428	427	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)))$
429	428	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)))$
430	425 429	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)))$
431	430	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))$
432	431	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))$
433	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to X \in ℝ$
434		elioore	$⊢ s \in (H (i), H (i + 1)) \to s \in ℝ$
435	434	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (H (i), H (i + 1))) \to s \in ℝ$
436		elsni	$⊢ s \in \{H (i + 1)\} \to s = H (i + 1)$
437	436	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i + 1)\}) \to s = H (i + 1)$
438	231	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i + 1)\}) \to H (i + 1) \in ℝ$
439	437 438	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i + 1)\}) \to s \in ℝ$
440	435 439	jaodan	$⊢ ((φ \land i \in (0 ..^M)) \land (s \in (H (i), H (i + 1)) \lor s \in \{H (i + 1)\})) \to s \in ℝ$
441	426 440	sylan2b	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to s \in ℝ$
442	433 441	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i + 1)\})) \to X + s \in ℝ$
443	442	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 ℝ$
444	421 423 432 443	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$
445	420 444	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$
446	418 445	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$
447	411 446	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)$
448	411	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)]$
449	448	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})$
450	449	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))$
451	409 447 450	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))$
452		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i + 1)\})$
453		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)))$
454	270 307	fssd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ X + t) : (H (i), H (i + 1)) ⟶ ℂ$
455	231	recnd	$⊢ (φ \land i \in (0 ..^M)) \to H (i + 1) \in ℂ$
456	452 386 453 454 305 455	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)))$
457	451 456	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ((t \in (H (i), H (i + 1)) ⟼ X + t) {lim}_{ℂ} H (i + 1))$
458	365 457 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))$
459	272 292	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))$
460	459	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)$
461	458 460	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((t \in (H (i), H (i + 1)) ⟼ F (X + t)) {lim}_{ℂ} H (i + 1))$
462	45	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to Q (i) \in ℝ$
463	462 340	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to r \neq Q (i)$
464	463	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ran (t \in (H (i), H (i + 1)) ⟼ X + t)) \to \neg r = Q (i)$
465		velsn	$⊢ r \in \{Q (i)\} \leftrightarrow r = Q (i)$
466	464 465	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)\}$
467	357 466	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)\})$
468	467	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)\})$
469		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)\})$
470	468 469	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)\}$
471		icossre	$⊢ (H (i) \in ℝ \land H (i + 1) \in ℝ^{*}) \to [H (i), H (i + 1)) \subseteq ℝ$
472	230 251 471	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)) \subseteq ℝ$
473	472 379	sstrdi	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)) \subseteq ℂ$
474	202	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in [H (i), H (i + 1))) \to X \in ℂ$
475	473	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land s \in [H (i), H (i + 1))) \to s \in ℂ$
476	474 475	addcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in [H (i), H (i + 1))) \to X + s \in ℂ$
477	366 375 473 381 476	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (s \in [H (i), H (i + 1)) ⟼ X + s) : [H (i), H (i + 1)) \underset{cn}{⟶} ℂ$
478		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1)) = TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))$
479	386 478 392	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})$
480	473 381 479	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))) Cn TopOpen (ℂ_{fld})$
481	477 480	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}))$
482		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)))$
483	397 473 482	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1)) \in TopOn ([H (i), H (i + 1)))$
484		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)))$
485	483 397 484	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)))$
486	481 485	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))$
487	486	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)$
488		lbico1	$⊢ (H (i) \in ℝ^{} \land H (i + 1) \in ℝ^{} \land H (i) < H (i + 1)) \to H (i) \in [H (i), H (i + 1))$
489	376 251 180 488	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in [H (i), H (i + 1))$
490		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))$
491	490	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)))$
492	491	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))$
493	487 489 492	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))$
494		uncom	$⊢ (H (i), H (i + 1)) \cup \{H (i)\} = \{H (i)\} \cup (H (i), H (i + 1))$
495		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))$
496	376 251 180 495	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to \{H (i)\} \cup (H (i), H (i + 1)) = [H (i), H (i + 1))$
497	494 496	syl5eq	$⊢ (φ \land i \in (0 ..^M)) \to (H (i), H (i + 1)) \cup \{H (i)\} = [H (i), H (i + 1))$
498		iftrue	$⊢ s = H (i) \to if (s = H (i), Q (i), (t \in (H (i), H (i + 1)) ⟼ X + t) (s)) = Q (i)$
499	498	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)$
500	246	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s = H (i)) \to Q (i) = X + H (i)$
501		oveq2	$⊢ s = H (i) \to X + s = X + H (i)$
502	501	eqcomd	$⊢ s = H (i) \to X + H (i) = X + s$
503	502	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s = H (i)) \to X + H (i) = X + s$
504	499 500 503	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$
505	504	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$
506		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)$
507	506	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)$
508		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)$
509	422	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$
510		velsn	$⊢ s \in \{H (i)\} \leftrightarrow s = H (i)$
511	510	notbii	$⊢ \neg s \in \{H (i)\} \leftrightarrow \neg s = H (i)$
512		elun	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \leftrightarrow (s \in (H (i), H (i + 1)) \lor s \in \{H (i)\})$
513	512	biimpi	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (s \in (H (i), H (i + 1)) \lor s \in \{H (i)\})$
514	513	orcomd	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (s \in \{H (i)\} \lor s \in (H (i), H (i + 1)))$
515	514	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)))$
516	511 515	syl5bir	$⊢ s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \to (\neg s = H (i) \to s \in (H (i), H (i + 1)))$
517	516	imp	$⊢ (s \in ((H (i), H (i + 1)) \cup \{H (i)\}) \land \neg s = H (i)) \to s \in (H (i), H (i + 1))$
518	517	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))$
519	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to X \in ℝ$
520		elsni	$⊢ s \in \{H (i)\} \to s = H (i)$
521	520	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i)\}) \to s = H (i)$
522	230	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i)\}) \to H (i) \in ℝ$
523	521 522	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{H (i)\}) \to s \in ℝ$
524	435 523	jaodan	$⊢ ((φ \land i \in (0 ..^M)) \land (s \in (H (i), H (i + 1)) \lor s \in \{H (i)\})) \to s \in ℝ$
525	512 524	sylan2b	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to s \in ℝ$
526	519 525	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((H (i), H (i + 1)) \cup \{H (i)\})) \to X + s \in ℝ$
527	526	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 ℝ$
528	508 509 518 527	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$
529	507 528	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$
530	505 529	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$
531	497 530	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)$
532	497	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} [H (i), H (i + 1))$
533	532	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})$
534	533	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))$
535	493 531 534	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))$
536		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((H (i), H (i + 1)) \cup \{H (i)\})$
537		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)))$
538	230	recnd	$⊢ (φ \land i \in (0 ..^M)) \to H (i) \in ℂ$
539	536 386 537 454 305 538	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)))$
540	535 539	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((t \in (H (i), H (i + 1)) ⟼ X + t) {lim}_{ℂ} H (i))$
541	470 540 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))$
542	459	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)$
543	541 542	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((t \in (H (i), H (i + 1)) ⟼ F (X + t)) {lim}_{ℂ} H (i))$
544	230 231 310 461 543	iblcncfioo	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (H (i), H (i + 1)) ⟼ F (X + t)) \in 𝐿^{1}$
545	6	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to F : [- π, π] ⟶ ℂ$
546	54	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to - π \in ℝ^{*}$
547	56	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to π \in ℝ^{*}$
548	27	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to Q : (0 \dots M) ⟶ [- π, π]$
549		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to i \in (0 ..^M)$
550		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to t \in [H (i), H (i + 1)]$
551	169 179	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to [H (i), H (i + 1)] = [Q (i) - X, Q (i + 1) - X]$
552	551	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]$
553	550 552	eleqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to t \in [Q (i) - X, Q (i + 1) - X]$
554	553 117	syldan	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to X + t \in [Q (i), Q (i + 1)]$
555	546 547 548 549 554	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to X + t \in [- π, π]$
556	545 555	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in [H (i), H (i + 1)]) \to F (X + t) \in ℂ$
557	230 231 544 556	ibliooicc	$⊢ (φ \land i \in (0 ..^M)) \to (t \in [H (i), H (i + 1)] ⟼ F (X + t)) \in 𝐿^{1}$
558	20 26 165 180 229 557	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$
559	551	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$
560	559	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$
561	558 560	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$
562	126 161 561	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$
563	122 562	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$
564	19 78 563	3eqtrd	$⊢ φ \to \int_{[- π, π]} F (t) d t = \int_{[- π - X, π - X]} F (X + s) d s$

Metamath Proof Explorer

Theorem fourierdlem93

Proof