fourierdlem101

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

	Ref	Expression
Hypotheses	fourierdlem101.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
	fourierdlem101.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem101.g	$⊢ G = (t \in [- π, π] ⟼ F (t) D (N) (t - X))$
	fourierdlem101.q	$⊢ φ \to Q \in P (M)$
	fourierdlem101.6	$⊢ φ \to M \in ℕ$
	fourierdlem101.n	$⊢ φ \to N \in ℕ$
	fourierdlem101.x	$⊢ φ \to X \in ℝ$
	fourierdlem101.f	$⊢ φ \to F : [- π, π] ⟶ ℂ$
	fourierdlem101.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem101.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem101.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
Assertion	fourierdlem101	$⊢ φ \to \int_{[- π, π]} F (t) D (N) (t - X) d t = \int_{[- π - X, π - X]} F (X + s) D (N) (s) d s$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem101.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
2		fourierdlem101.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
3		fourierdlem101.g	$⊢ G = (t \in [- π, π] ⟼ F (t) D (N) (t - X))$
4		fourierdlem101.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem101.6	$⊢ φ \to M \in ℕ$
6		fourierdlem101.n	$⊢ φ \to N \in ℕ$
7		fourierdlem101.x	$⊢ φ \to X \in ℝ$
8		fourierdlem101.f	$⊢ φ \to F : [- π, π] ⟶ ℂ$
9		fourierdlem101.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
10		fourierdlem101.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
11		fourierdlem101.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
12		simpr	$⊢ (φ \land t \in [- π, π]) \to t \in [- π, π]$
13	8	ffvelcdmda	$⊢ (φ \land t \in [- π, π]) \to F (t) \in ℂ$
14	6	adantr	$⊢ (φ \land t \in [- π, π]) \to N \in ℕ$
15		pire	$⊢ π \in ℝ$
16	15	renegcli	$⊢ - π \in ℝ$
17		eliccre	$⊢ (- π \in ℝ \land π \in ℝ \land t \in [- π, π]) \to t \in ℝ$
18	16 15 17	mp3an12	$⊢ t \in [- π, π] \to t \in ℝ$
19	18	adantl	$⊢ (φ \land t \in [- π, π]) \to t \in ℝ$
20	7	adantr	$⊢ (φ \land t \in [- π, π]) \to X \in ℝ$
21	19 20	resubcld	$⊢ (φ \land t \in [- π, π]) \to t - X \in ℝ$
22	1	dirkerre	$⊢ (N \in ℕ \land t - X \in ℝ) \to D (N) (t - X) \in ℝ$
23	14 21 22	syl2anc	$⊢ (φ \land t \in [- π, π]) \to D (N) (t - X) \in ℝ$
24	23	recnd	$⊢ (φ \land t \in [- π, π]) \to D (N) (t - X) \in ℂ$
25	13 24	mulcld	$⊢ (φ \land t \in [- π, π]) \to F (t) D (N) (t - X) \in ℂ$
26	3	fvmpt2	$⊢ (t \in [- π, π] \land F (t) D (N) (t - X) \in ℂ) \to G (t) = F (t) D (N) (t - X)$
27	12 25 26	syl2anc	$⊢ (φ \land t \in [- π, π]) \to G (t) = F (t) D (N) (t - X)$
28	27	eqcomd	$⊢ (φ \land t \in [- π, π]) \to F (t) D (N) (t - X) = G (t)$
29	28	itgeq2dv	$⊢ φ \to \int_{[- π, π]} F (t) D (N) (t - X) d t = \int_{[- π, π]} G (t) d t$
30		fveq2	$⊢ j = i \to Q (j) = Q (i)$
31	30	oveq1d	$⊢ j = i \to Q (j) - X = Q (i) - X$
32	31	cbvmptv	$⊢ (j \in (0 \dots M) ⟼ Q (j) - X) = (i \in (0 \dots M) ⟼ Q (i) - X)$
33	25 3	fmptd	$⊢ φ \to G : [- π, π] ⟶ ℂ$
34	3	reseq1i	$⊢ {G ↾}_{(Q (i), Q (i + 1))} = {(t \in [- π, π] ⟼ F (t) D (N) (t - X)) ↾}_{(Q (i), Q (i + 1))}$
35		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
36	16	a1i	$⊢ φ \to - π \in ℝ$
37	36	rexrd	$⊢ φ \to - π \in ℝ^{*}$
38	37	adantr	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
39	15	a1i	$⊢ φ \to π \in ℝ$
40	39	rexrd	$⊢ φ \to π \in ℝ^{*}$
41	40	adantr	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
42	2 5 4	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
43	42	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
44		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
45	38 41 43 44	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
46	35 45	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
47	46	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(t \in [- π, π] ⟼ F (t) D (N) (t - X)) ↾}_{(Q (i), Q (i + 1))} = (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X))$
48	34 47	eqtrid	$⊢ (φ \land i \in (0 ..^M)) \to {G ↾}_{(Q (i), Q (i + 1))} = (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X))$
49	8	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : [- π, π] ⟶ ℂ$
50	49 46	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = (t \in (Q (i), Q (i + 1)) ⟼ F (t))$
51	50 9	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
52		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to (s \in ℝ ⟼ D (N) (s)) = (s \in ℝ ⟼ D (N) (s))$
53		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \land s = (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)) \to s = (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)$
54		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to (t \in (Q (i), Q (i + 1)) ⟼ t - X) = (t \in (Q (i), Q (i + 1)) ⟼ t - X)$
55		oveq1	$⊢ t = r \to t - X = r - X$
56	55	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \land t = r) \to t - X = r - X$
57		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to r \in (Q (i), Q (i + 1))$
58		elioore	$⊢ r \in (Q (i), Q (i + 1)) \to r \in ℝ$
59	58	adantl	$⊢ (φ \land r \in (Q (i), Q (i + 1))) \to r \in ℝ$
60	7	adantr	$⊢ (φ \land r \in (Q (i), Q (i + 1))) \to X \in ℝ$
61	59 60	resubcld	$⊢ (φ \land r \in (Q (i), Q (i + 1))) \to r - X \in ℝ$
62	61	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to r - X \in ℝ$
63	54 56 57 62	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r) = r - X$
64	63	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \land s = (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)) \to (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r) = r - X$
65	53 64	eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \land s = (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)) \to s = r - X$
66	65	fveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \land s = (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)) \to D (N) (s) = D (N) (r - X)$
67		elioore	$⊢ t \in (Q (i), Q (i + 1)) \to t \in ℝ$
68	67	adantl	$⊢ (φ \land t \in (Q (i), Q (i + 1))) \to t \in ℝ$
69	7	adantr	$⊢ (φ \land t \in (Q (i), Q (i + 1))) \to X \in ℝ$
70	68 69	resubcld	$⊢ (φ \land t \in (Q (i), Q (i + 1))) \to t - X \in ℝ$
71	70	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to t - X \in ℝ$
72		eqid	$⊢ (t \in (Q (i), Q (i + 1)) ⟼ t - X) = (t \in (Q (i), Q (i + 1)) ⟼ t - X)$
73	71 72	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ t - X) : (Q (i), Q (i + 1)) ⟶ ℝ$
74	73	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to (t \in (Q (i), Q (i + 1)) ⟼ t - X) (r) \in ℝ$
75	6	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to N \in ℕ$
76	1	dirkerre	$⊢ (N \in ℕ \land r - X \in ℝ) \to D (N) (r - X) \in ℝ$
77	75 62 76	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to D (N) (r - X) \in ℝ$
78	52 66 74 77	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to (s \in ℝ ⟼ D (N) (s)) ((t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)) = D (N) (r - X)$
79	78	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (Q (i), Q (i + 1))) \to D (N) (r - X) = (s \in ℝ ⟼ D (N) (s)) ((t \in (Q (i), Q (i + 1)) ⟼ t - X) (r))$
80	79	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (r \in (Q (i), Q (i + 1)) ⟼ D (N) (r - X)) = (r \in (Q (i), Q (i + 1)) ⟼ (s \in ℝ ⟼ D (N) (s)) ((t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)))$
81	55	fveq2d	$⊢ t = r \to D (N) (t - X) = D (N) (r - X)$
82	81	cbvmptv	$⊢ (t \in (Q (i), Q (i + 1)) ⟼ D (N) (t - X)) = (r \in (Q (i), Q (i + 1)) ⟼ D (N) (r - X))$
83	82	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ D (N) (t - X)) = (r \in (Q (i), Q (i + 1)) ⟼ D (N) (r - X))$
84	1	dirkerre	$⊢ (N \in ℕ \land s \in ℝ) \to D (N) (s) \in ℝ$
85	6 84	sylan	$⊢ (φ \land s \in ℝ) \to D (N) (s) \in ℝ$
86		eqid	$⊢ (s \in ℝ ⟼ D (N) (s)) = (s \in ℝ ⟼ D (N) (s))$
87	85 86	fmptd	$⊢ φ \to (s \in ℝ ⟼ D (N) (s)) : ℝ ⟶ ℝ$
88	87	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℝ ⟼ D (N) (s)) : ℝ ⟶ ℝ$
89		fcompt	$⊢ ((s \in ℝ ⟼ D (N) (s)) : ℝ ⟶ ℝ \land (t \in (Q (i), Q (i + 1)) ⟼ t - X) : (Q (i), Q (i + 1)) ⟶ ℝ) \to (s \in ℝ ⟼ D (N) (s)) \circ (t \in (Q (i), Q (i + 1)) ⟼ t - X) = (r \in (Q (i), Q (i + 1)) ⟼ (s \in ℝ ⟼ D (N) (s)) ((t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)))$
90	88 73 89	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℝ ⟼ D (N) (s)) \circ (t \in (Q (i), Q (i + 1)) ⟼ t - X) = (r \in (Q (i), Q (i + 1)) ⟼ (s \in ℝ ⟼ D (N) (s)) ((t \in (Q (i), Q (i + 1)) ⟼ t - X) (r)))$
91	80 83 90	3eqtr4d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ D (N) (t - X)) = (s \in ℝ ⟼ D (N) (s)) \circ (t \in (Q (i), Q (i + 1)) ⟼ t - X)$
92		eqid	$⊢ (t \in ℂ ⟼ t - X) = (t \in ℂ ⟼ t - X)$
93		simpr	$⊢ (φ \land t \in ℂ) \to t \in ℂ$
94	7	recnd	$⊢ φ \to X \in ℂ$
95	94	adantr	$⊢ (φ \land t \in ℂ) \to X \in ℂ$
96	93 95	negsubd	$⊢ (φ \land t \in ℂ) \to t + (- X) = t - X$
97	96	eqcomd	$⊢ (φ \land t \in ℂ) \to t - X = t + (- X)$
98	97	mpteq2dva	$⊢ φ \to (t \in ℂ ⟼ t - X) = (t \in ℂ ⟼ t + (- X))$
99	94	negcld	$⊢ φ \to - X \in ℂ$
100		eqid	$⊢ (t \in ℂ ⟼ t + (- X)) = (t \in ℂ ⟼ t + (- X))$
101	100	addccncf	$⊢ - X \in ℂ \to (t \in ℂ ⟼ t + (- X)) : ℂ \underset{cn}{⟶} ℂ$
102	99 101	syl	$⊢ φ \to (t \in ℂ ⟼ t + (- X)) : ℂ \underset{cn}{⟶} ℂ$
103	98 102	eqeltrd	$⊢ φ \to (t \in ℂ ⟼ t - X) : ℂ \underset{cn}{⟶} ℂ$
104	103	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ℂ ⟼ t - X) : ℂ \underset{cn}{⟶} ℂ$
105		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
106		ax-resscn	$⊢ ℝ \subseteq ℂ$
107	105 106	sstri	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
108	107	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
109	106	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℂ$
110	92 104 108 109 71	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ t - X) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℝ$
111	85	recnd	$⊢ (φ \land s \in ℝ) \to D (N) (s) \in ℂ$
112	111 86	fmptd	$⊢ φ \to (s \in ℝ ⟼ D (N) (s)) : ℝ ⟶ ℂ$
113		ssid	$⊢ ℂ \subseteq ℂ$
114	1	dirkerf	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℝ$
115	6 114	syl	$⊢ φ \to D (N) : ℝ ⟶ ℝ$
116	115	feqmptd	$⊢ φ \to D (N) = (s \in ℝ ⟼ D (N) (s))$
117	1	dirkercncf	$⊢ N \in ℕ \to D (N) : ℝ \underset{cn}{⟶} ℝ$
118	6 117	syl	$⊢ φ \to D (N) : ℝ \underset{cn}{⟶} ℝ$
119	116 118	eqeltrrd	$⊢ φ \to (s \in ℝ ⟼ D (N) (s)) : ℝ \underset{cn}{⟶} ℝ$
120		cncfcdm	$⊢ (ℂ \subseteq ℂ \land (s \in ℝ ⟼ D (N) (s)) : ℝ \underset{cn}{⟶} ℝ) \to ((s \in ℝ ⟼ D (N) (s)) : ℝ \underset{cn}{⟶} ℂ \leftrightarrow (s \in ℝ ⟼ D (N) (s)) : ℝ ⟶ ℂ)$
121	113 119 120	sylancr	$⊢ φ \to ((s \in ℝ ⟼ D (N) (s)) : ℝ \underset{cn}{⟶} ℂ \leftrightarrow (s \in ℝ ⟼ D (N) (s)) : ℝ ⟶ ℂ)$
122	112 121	mpbird	$⊢ φ \to (s \in ℝ ⟼ D (N) (s)) : ℝ \underset{cn}{⟶} ℂ$
123	122	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℝ ⟼ D (N) (s)) : ℝ \underset{cn}{⟶} ℂ$
124	110 123	cncfco	$⊢ (φ \land i \in (0 ..^M)) \to ((s \in ℝ ⟼ D (N) (s)) \circ (t \in (Q (i), Q (i + 1)) ⟼ t - X)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
125	91 124	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
126	51 125	mulcncf	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
127	48 126	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
128		cncff	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
129	9 128	syl	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
130	115	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to D (N) : ℝ ⟶ ℝ$
131		elioore	$⊢ s \in (Q (i), Q (i + 1)) \to s \in ℝ$
132	131	adantl	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
133	7	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to X \in ℝ$
134	132 133	resubcld	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to s - X \in ℝ$
135	130 134	ffvelcdmd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to D (N) (s - X) \in ℝ$
136	135	recnd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to D (N) (s - X) \in ℂ$
137		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) = (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X))$
138	136 137	fmptd	$⊢ φ \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) : (Q (i), Q (i + 1)) ⟶ ℂ$
139	138	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) : (Q (i), Q (i + 1)) ⟶ ℂ$
140		eqid	$⊢ (t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = (t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))$
141		oveq1	$⊢ t = Q (i) \to t - X = Q (i) - X$
142	141	fveq2d	$⊢ t = Q (i) \to D (N) (t - X) = D (N) (Q (i) - X)$
143	142	eqcomd	$⊢ t = Q (i) \to D (N) (Q (i) - X) = D (N) (t - X)$
144	143	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land t = Q (i)) \to D (N) (Q (i) - X) = D (N) (t - X)$
145		eqidd	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land \neg t = Q (i)) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) = (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X))$
146		oveq1	$⊢ s = t \to s - X = t - X$
147	146	fveq2d	$⊢ s = t \to D (N) (s - X) = D (N) (t - X)$
148	147	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land \neg t = Q (i)) \land s = t) \to D (N) (s - X) = D (N) (t - X)$
149		velsn	$⊢ t \in \{Q (i)\} \leftrightarrow t = Q (i)$
150	149	notbii	$⊢ \neg t \in \{Q (i)\} \leftrightarrow \neg t = Q (i)$
151		elunnel2	$⊢ (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \land \neg t \in \{Q (i)\}) \to t \in (Q (i), Q (i + 1))$
152	150 151	sylan2br	$⊢ (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \land \neg t = Q (i)) \to t \in (Q (i), Q (i + 1))$
153	152	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land \neg t = Q (i)) \to t \in (Q (i), Q (i + 1))$
154	115	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to D (N) : ℝ ⟶ ℝ$
155		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t = Q (i)) \to t = Q (i)$
156	18	ssriv	$⊢ [- π, π] \subseteq ℝ$
157		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
158	157 44	sselid	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
159	43 158	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [- π, π]$
160	156 159	sselid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
161	160	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t = Q (i)) \to Q (i) \in ℝ$
162	155 161	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land t = Q (i)) \to t \in ℝ$
163	162	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land t = Q (i)) \to t \in ℝ$
164	153 67	syl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land \neg t = Q (i)) \to t \in ℝ$
165	163 164	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to t \in ℝ$
166	7	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to X \in ℝ$
167	165 166	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to t - X \in ℝ$
168	154 167	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to D (N) (t - X) \in ℝ$
169	168	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land \neg t = Q (i)) \to D (N) (t - X) \in ℝ$
170	145 148 153 169	fvmptd	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land \neg t = Q (i)) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t) = D (N) (t - X)$
171	144 170	ifeqda	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to if (t = Q (i), D (N) (Q (i) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = D (N) (t - X)$
172	171	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ if (t = Q (i), D (N) (Q (i) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X))$
173	115	adantr	$⊢ (φ \land i \in (0 ..^M)) \to D (N) : ℝ ⟶ ℝ$
174		elun	$⊢ s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \leftrightarrow (s \in (Q (i), Q (i + 1)) \lor s \in \{Q (i)\})$
175	174	bilani	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to (s \in (Q (i), Q (i + 1)) \lor s \in \{Q (i)\})$
176		elsni	$⊢ s \in \{Q (i)\} \to s = Q (i)$
177	176	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{Q (i)\}) \to s = Q (i)$
178	160	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{Q (i)\}) \to Q (i) \in ℝ$
179	177 178	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{Q (i)\}) \to s \in ℝ$
180	179	ex	$⊢ (φ \land i \in (0 ..^M)) \to (s \in \{Q (i)\} \to s \in ℝ)$
181	180	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to (s \in \{Q (i)\} \to s \in ℝ)$
182		pm3.44	$⊢ ((s \in (Q (i), Q (i + 1)) \to s \in ℝ) \land (s \in \{Q (i)\} \to s \in ℝ)) \to ((s \in (Q (i), Q (i + 1)) \lor s \in \{Q (i)\}) \to s \in ℝ)$
183	131 181 182	sylancr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to ((s \in (Q (i), Q (i + 1)) \lor s \in \{Q (i)\}) \to s \in ℝ)$
184	175 183	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to s \in ℝ$
185	7	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to X \in ℝ$
186	184 185	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to s - X \in ℝ$
187		eqid	$⊢ (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) = (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X)$
188	186 187	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) : (Q (i), Q (i + 1)) \cup \{Q (i)\} ⟶ ℝ$
189		fcompt	$⊢ (D (N) : ℝ ⟶ ℝ \land (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) : (Q (i), Q (i + 1)) \cup \{Q (i)\} ⟶ ℝ) \to D (N) \circ (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) ((s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) (t)))$
190	173 188 189	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to D (N) \circ (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) ((s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) (t)))$
191		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) = (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X)$
192	146	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \land s = t) \to s - X = t - X$
193		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
194	191 192 193 167	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) (t) = t - X$
195	194	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to D (N) ((s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) (t)) = D (N) (t - X)$
196	195	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) ((s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) (t))) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X))$
197	190 196	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) = D (N) \circ (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X)$
198		eqid	$⊢ (s \in ℂ ⟼ s - X) = (s \in ℂ ⟼ s - X)$
199		simpr	$⊢ (φ \land s \in ℂ) \to s \in ℂ$
200	94	adantr	$⊢ (φ \land s \in ℂ) \to X \in ℂ$
201	199 200	negsubd	$⊢ (φ \land s \in ℂ) \to s + (- X) = s - X$
202	201	eqcomd	$⊢ (φ \land s \in ℂ) \to s - X = s + (- X)$
203	202	mpteq2dva	$⊢ φ \to (s \in ℂ ⟼ s - X) = (s \in ℂ ⟼ s + (- X))$
204		eqid	$⊢ (s \in ℂ ⟼ s + (- X)) = (s \in ℂ ⟼ s + (- X))$
205	204	addccncf	$⊢ - X \in ℂ \to (s \in ℂ ⟼ s + (- X)) : ℂ \underset{cn}{⟶} ℂ$
206	99 205	syl	$⊢ φ \to (s \in ℂ ⟼ s + (- X)) : ℂ \underset{cn}{⟶} ℂ$
207	203 206	eqeltrd	$⊢ φ \to (s \in ℂ ⟼ s - X) : ℂ \underset{cn}{⟶} ℂ$
208	207	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℂ ⟼ s - X) : ℂ \underset{cn}{⟶} ℂ$
209	160	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
210	209	snssd	$⊢ (φ \land i \in (0 ..^M)) \to \{Q (i)\} \subseteq ℂ$
211	108 210	unssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cup \{Q (i)\} \subseteq ℂ$
212	198 208 211 109 186	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) : ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \underset{cn}{⟶} ℝ$
213	116 122	eqeltrd	$⊢ φ \to D (N) : ℝ \underset{cn}{⟶} ℂ$
214	213	adantr	$⊢ (φ \land i \in (0 ..^M)) \to D (N) : ℝ \underset{cn}{⟶} ℂ$
215	212 214	cncfco	$⊢ (φ \land i \in (0 ..^M)) \to (D (N) \circ (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X)) : ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \underset{cn}{⟶} ℂ$
216		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
217		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
218	216	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
219		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
220	219	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
221	218 220	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
222	221	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
223	216 217 222	cncfcn	$⊢ ((Q (i), Q (i + 1)) \cup \{Q (i)\} \subseteq ℂ \land ℂ \subseteq ℂ) \to ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) Cn TopOpen (ℂ_{fld})$
224	211 113 223	sylancl	$⊢ (φ \land i \in (0 ..^M)) \to ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) Cn TopOpen (ℂ_{fld})$
225	215 224	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to D (N) \circ (s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ s - X) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) Cn TopOpen (ℂ_{fld}))$
226	197 225	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) Cn TopOpen (ℂ_{fld}))$
227	216	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
228		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (Q (i), Q (i + 1)) \cup \{Q (i)\} \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \in TopOn ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
229	227 211 228	sylancr	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \in TopOn ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
230		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \in TopOn ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \cup \{Q (i)\} ⟶ ℂ \land \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s)))$
231	229 227 230	sylancl	$⊢ (φ \land i \in (0 ..^M)) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \cup \{Q (i)\} ⟶ ℂ \land \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s)))$
232	226 231	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \cup \{Q (i)\} ⟶ ℂ \land \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s))$
233	232	simprd	$⊢ (φ \land i \in (0 ..^M)) \to \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s)$
234		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = Q (i)$
235		elsng	$⊢ Q (i) \in ℝ \to (Q (i) \in \{Q (i)\} \leftrightarrow Q (i) = Q (i))$
236	160 235	syl	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) \in \{Q (i)\} \leftrightarrow Q (i) = Q (i))$
237	234 236	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in \{Q (i)\}$
238	237	olcd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) \in (Q (i), Q (i + 1)) \lor Q (i) \in \{Q (i)\})$
239		elun	$⊢ Q (i) \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \leftrightarrow (Q (i) \in (Q (i), Q (i + 1)) \lor Q (i) \in \{Q (i)\})$
240	238 239	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
241		fveq2	$⊢ s = Q (i) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (Q (i))$
242	241	eleq2d	$⊢ s = Q (i) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s) \leftrightarrow (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (Q (i)))$
243	242	rspccva	$⊢ (\forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (s) \land Q (i) \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (Q (i))$
244	233 240 243	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (Q (i))$
245	172 244	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ if (t = Q (i), D (N) (Q (i) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (Q (i))$
246		eqid	$⊢ (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ if (t = Q (i), D (N) (Q (i) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ if (t = Q (i), D (N) (Q (i) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)))$
247	217 216 246 139 108 209	ellimc	$⊢ (φ \land i \in (0 ..^M)) \to (D (N) (Q (i) - X) \in ((s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) {lim}_{ℂ} Q (i)) \leftrightarrow (t \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) ⟼ if (t = Q (i), D (N) (Q (i) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})) CnP TopOpen (ℂ_{fld})) (Q (i)))$
248	245 247	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to D (N) (Q (i) - X) \in ((s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) {lim}_{ℂ} Q (i))$
249	129 139 140 10 248	mullimcf	$⊢ (φ \land i \in (0 ..^M)) \to R D (N) (Q (i) - X) \in ((t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i))$
250		fvres	$⊢ t \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (t) = F (t)$
251	250	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) (t) = F (t)$
252	251	oveq1d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t) = F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)$
253	252	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = (t \in (Q (i), Q (i + 1)) ⟼ F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))$
254	253	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i) = (t \in (Q (i), Q (i + 1)) ⟼ F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i)$
255	249 254	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R D (N) (Q (i) - X) \in ((t \in (Q (i), Q (i + 1)) ⟼ F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i))$
256		eqidd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) = (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X))$
257		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \land s = t) \to s = t$
258	257	oveq1d	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \land s = t) \to s - X = t - X$
259	258	fveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \land s = t) \to D (N) (s - X) = D (N) (t - X)$
260		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to t \in (Q (i), Q (i + 1))$
261	115	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to D (N) : ℝ ⟶ ℝ$
262	261 71	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to D (N) (t - X) \in ℝ$
263	256 259 260 262	fvmptd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t) = D (N) (t - X)$
264	263	oveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t) = F (t) D (N) (t - X)$
265	264	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X))$
266	265	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i) = (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X)) {lim}_{ℂ} Q (i)$
267	255 266	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R D (N) (Q (i) - X) \in ((t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X)) {lim}_{ℂ} Q (i))$
268	48	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X)) = {G ↾}_{(Q (i), Q (i + 1))}$
269	268	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ F (t) D (N) (t - X)) {lim}_{ℂ} Q (i) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
270	267 269	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R D (N) (Q (i) - X) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
271		iftrue	$⊢ t = Q (i + 1) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = D (N) (Q (i + 1) - X)$
272		oveq1	$⊢ t = Q (i + 1) \to t - X = Q (i + 1) - X$
273	272	eqcomd	$⊢ t = Q (i + 1) \to Q (i + 1) - X = t - X$
274	273	fveq2d	$⊢ t = Q (i + 1) \to D (N) (Q (i + 1) - X) = D (N) (t - X)$
275	271 274	eqtrd	$⊢ t = Q (i + 1) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = D (N) (t - X)$
276	275	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land t = Q (i + 1)) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = D (N) (t - X)$
277		iffalse	$⊢ \neg t = Q (i + 1) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)$
278	277	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)$
279		eqidd	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) = (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X))$
280	147	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \land s = t) \to D (N) (s - X) = D (N) (t - X)$
281		elun	$⊢ t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \leftrightarrow (t \in (Q (i), Q (i + 1)) \lor t \in \{Q (i + 1)\})$
282	281	biimpi	$⊢ t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \to (t \in (Q (i), Q (i + 1)) \lor t \in \{Q (i + 1)\})$
283	282	orcomd	$⊢ t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \to (t \in \{Q (i + 1)\} \lor t \in (Q (i), Q (i + 1)))$
284	283	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to (t \in \{Q (i + 1)\} \lor t \in (Q (i), Q (i + 1)))$
285		velsn	$⊢ t \in \{Q (i + 1)\} \leftrightarrow t = Q (i + 1)$
286	285	notbii	$⊢ \neg t \in \{Q (i + 1)\} \leftrightarrow \neg t = Q (i + 1)$
287	286	bilanri	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to \neg t \in \{Q (i + 1)\}$
288		pm2.53	$⊢ (t \in \{Q (i + 1)\} \lor t \in (Q (i), Q (i + 1))) \to (\neg t \in \{Q (i + 1)\} \to t \in (Q (i), Q (i + 1)))$
289	284 287 288	sylc	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to t \in (Q (i), Q (i + 1))$
290	173	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to D (N) : ℝ ⟶ ℝ$
291	289 67	syl	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to t \in ℝ$
292	7	ad3antrrr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to X \in ℝ$
293	291 292	resubcld	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to t - X \in ℝ$
294	290 293	ffvelcdmd	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to D (N) (t - X) \in ℝ$
295	279 280 289 294	fvmptd	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t) = D (N) (t - X)$
296	278 295	eqtrd	$⊢ (((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \land \neg t = Q (i + 1)) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = D (N) (t - X)$
297	276 296	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = D (N) (t - X)$
298	297	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X))$
299		eqid	$⊢ (t \in ℝ ⟼ D (N) (t - X)) = (t \in ℝ ⟼ D (N) (t - X))$
300	106	a1i	$⊢ φ \to ℝ \subseteq ℂ$
301		simpr	$⊢ (φ \land t \in ℝ) \to t \in ℝ$
302	7	adantr	$⊢ (φ \land t \in ℝ) \to X \in ℝ$
303	301 302	resubcld	$⊢ (φ \land t \in ℝ) \to t - X \in ℝ$
304	92 103 300 300 303	cncfmptssg	$⊢ φ \to (t \in ℝ ⟼ t - X) : ℝ \underset{cn}{⟶} ℝ$
305	304 213	cncfcompt	$⊢ φ \to (t \in ℝ ⟼ D (N) (t - X)) : ℝ \underset{cn}{⟶} ℂ$
306	305	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ℝ ⟼ D (N) (t - X)) : ℝ \underset{cn}{⟶} ℂ$
307	105	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
308		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
309	308	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
310	43 309	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [- π, π]$
311	156 310	sselid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
312	311	snssd	$⊢ (φ \land i \in (0 ..^M)) \to \{Q (i + 1)\} \subseteq ℝ$
313	307 312	unssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} \subseteq ℝ$
314	113	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℂ \subseteq ℂ$
315	173	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to D (N) : ℝ ⟶ ℝ$
316	313	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to t \in ℝ$
317	7	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to X \in ℝ$
318	316 317	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to t - X \in ℝ$
319	315 318	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to D (N) (t - X) \in ℝ$
320	319	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to D (N) (t - X) \in ℂ$
321	299 306 313 314 320	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) : ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \underset{cn}{⟶} ℂ$
322	156 106	sstri	$⊢ [- π, π] \subseteq ℂ$
323	322 310	sselid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
324	323	snssd	$⊢ (φ \land i \in (0 ..^M)) \to \{Q (i + 1)\} \subseteq ℂ$
325	108 324	unssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} \subseteq ℂ$
326		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})$
327	216 326 222	cncfcn	$⊢ ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\} \subseteq ℂ \land ℂ \subseteq ℂ) \to ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) Cn TopOpen (ℂ_{fld})$
328	325 113 327	sylancl	$⊢ (φ \land i \in (0 ..^M)) \to ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) Cn TopOpen (ℂ_{fld})$
329	321 328	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) Cn TopOpen (ℂ_{fld}))$
330		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \in TopOn ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})$
331	227 325 330	sylancr	$⊢ (φ \land i \in (0 ..^M)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \in TopOn ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})$
332		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \in TopOn ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} ⟶ ℂ \land \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s)))$
333	331 227 332	sylancl	$⊢ (φ \land i \in (0 ..^M)) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} ⟶ ℂ \land \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s)))$
334	329 333	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) : (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} ⟶ ℂ \land \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s))$
335	334	simprd	$⊢ (φ \land i \in (0 ..^M)) \to \forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s)$
336		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = Q (i + 1)$
337		elsng	$⊢ Q (i + 1) \in ℝ \to (Q (i + 1) \in \{Q (i + 1)\} \leftrightarrow Q (i + 1) = Q (i + 1))$
338	311 337	syl	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i + 1) \in \{Q (i + 1)\} \leftrightarrow Q (i + 1) = Q (i + 1))$
339	336 338	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in \{Q (i + 1)\}$
340	339	olcd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i + 1) \in (Q (i), Q (i + 1)) \lor Q (i + 1) \in \{Q (i + 1)\})$
341		elun	$⊢ Q (i + 1) \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) \leftrightarrow (Q (i + 1) \in (Q (i), Q (i + 1)) \lor Q (i + 1) \in \{Q (i + 1)\})$
342	340 341	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})$
343		fveq2	$⊢ s = Q (i + 1) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (Q (i + 1))$
344	343	eleq2d	$⊢ s = Q (i + 1) \to ((t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s) \leftrightarrow (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (Q (i + 1)))$
345	344	rspccva	$⊢ (\forall s \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (s) \land Q (i + 1) \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (Q (i + 1))$
346	335 342 345	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ D (N) (t - X)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (Q (i + 1))$
347	298 346	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (Q (i + 1))$
348		eqid	$⊢ (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) = (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)))$
349	326 216 348 139 108 323	ellimc	$⊢ (φ \land i \in (0 ..^M)) \to (D (N) (Q (i + 1) - X) \in ((s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) {lim}_{ℂ} Q (i + 1)) \leftrightarrow (t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) ⟼ if (t = Q (i + 1), D (N) (Q (i + 1) - X), (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) CnP TopOpen (ℂ_{fld})) (Q (i + 1)))$
350	347 349	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to D (N) (Q (i + 1) - X) \in ((s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) {lim}_{ℂ} Q (i + 1))$
351	129 139 140 11 350	mullimcf	$⊢ (φ \land i \in (0 ..^M)) \to L D (N) (Q (i + 1) - X) \in ((t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i + 1))$
352	265 253 48	3eqtr4d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) = {G ↾}_{(Q (i), Q (i + 1))}$
353	352	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (t \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(Q (i), Q (i + 1))}) (t) (s \in (Q (i), Q (i + 1)) ⟼ D (N) (s - X)) (t)) {lim}_{ℂ} Q (i + 1) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
354	351 353	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L D (N) (Q (i + 1) - X) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
355	2 32 5 4 7 33 127 270 354	fourierdlem93	$⊢ φ \to \int_{[- π, π]} G (t) d t = \int_{[- π - X, π - X]} G (X + s) d s$
356	3	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to G = (t \in [- π, π] ⟼ F (t) D (N) (t - X))$
357		fveq2	$⊢ t = X + s \to F (t) = F (X + s)$
358	357	oveq1d	$⊢ t = X + s \to F (t) D (N) (t - X) = F (X + s) D (N) (t - X)$
359	358	adantl	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to F (t) D (N) (t - X) = F (X + s) D (N) (t - X)$
360		oveq1	$⊢ t = X + s \to t - X = X + s - X$
361	94	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to X \in ℂ$
362	36 7	resubcld	$⊢ φ \to - π - X \in ℝ$
363	362	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to - π - X \in ℝ$
364	39 7	resubcld	$⊢ φ \to π - X \in ℝ$
365	364	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to π - X \in ℝ$
366		simpr	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in [- π - X, π - X]$
367		eliccre	$⊢ (- π - X \in ℝ \land π - X \in ℝ \land s \in [- π - X, π - X]) \to s \in ℝ$
368	363 365 366 367	syl3anc	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in ℝ$
369	368	recnd	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in ℂ$
370	361 369	pncan2d	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s - X = s$
371	360 370	sylan9eqr	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to t - X = s$
372	371	fveq2d	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to D (N) (t - X) = D (N) (s)$
373	372	oveq2d	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to F (X + s) D (N) (t - X) = F (X + s) D (N) (s)$
374	359 373	eqtrd	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to F (t) D (N) (t - X) = F (X + s) D (N) (s)$
375	16	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to - π \in ℝ$
376	15	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to π \in ℝ$
377	7	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to X \in ℝ$
378	377 368	readdcld	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \in ℝ$
379	36	recnd	$⊢ φ \to - π \in ℂ$
380	94 379	pncan3d	$⊢ φ \to X + (- π) - X = - π$
381	380	eqcomd	$⊢ φ \to - π = X + (- π) - X$
382	381	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to - π = X + (- π) - X$
383		elicc2	$⊢ (- π - X \in ℝ \land π - X \in ℝ) \to (s \in [- π - X, π - X] \leftrightarrow (s \in ℝ \land - π - X \leq s \land s \leq π - X))$
384	363 365 383	syl2anc	$⊢ (φ \land s \in [- π - X, π - X]) \to (s \in [- π - X, π - X] \leftrightarrow (s \in ℝ \land - π - X \leq s \land s \leq π - X))$
385	366 384	mpbid	$⊢ (φ \land s \in [- π - X, π - X]) \to (s \in ℝ \land - π - X \leq s \land s \leq π - X)$
386	385	simp2d	$⊢ (φ \land s \in [- π - X, π - X]) \to - π - X \leq s$
387	363 368 377 386	leadd2dd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + (- π) - X \leq X + s$
388	382 387	eqbrtrd	$⊢ (φ \land s \in [- π - X, π - X]) \to - π \leq X + s$
389	385	simp3d	$⊢ (φ \land s \in [- π - X, π - X]) \to s \leq π - X$
390	368 365 377 389	leadd2dd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \leq X + π - X$
391		picn	$⊢ π \in ℂ$
392	391	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to π \in ℂ$
393	361 392	pncan3d	$⊢ (φ \land s \in [- π - X, π - X]) \to X + π - X = π$
394	390 393	breqtrd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \leq π$
395	375 376 378 388 394	eliccd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \in [- π, π]$
396	8	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to F : [- π, π] ⟶ ℂ$
397	396 395	ffvelcdmd	$⊢ (φ \land s \in [- π - X, π - X]) \to F (X + s) \in ℂ$
398	368 111	syldan	$⊢ (φ \land s \in [- π - X, π - X]) \to D (N) (s) \in ℂ$
399	397 398	mulcld	$⊢ (φ \land s \in [- π - X, π - X]) \to F (X + s) D (N) (s) \in ℂ$
400	356 374 395 399	fvmptd	$⊢ (φ \land s \in [- π - X, π - X]) \to G (X + s) = F (X + s) D (N) (s)$
401	400	itgeq2dv	$⊢ φ \to \int_{[- π - X, π - X]} G (X + s) d s = \int_{[- π - X, π - X]} F (X + s) D (N) (s) d s$
402	29 355 401	3eqtrd	$⊢ φ \to \int_{[- π, π]} F (t) D (N) (t - X) d t = \int_{[- π - X, π - X]} F (X + s) D (N) (s) d s$

Metamath Proof Explorer

Theorem fourierdlem101

Proof