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		simpr	$⊢ (φ \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
175		elun	$⊢ s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\}) \leftrightarrow (s \in (Q (i), Q (i + 1)) \lor s \in \{Q (i)\})$
176	174 175	sylib	$⊢ (φ \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to (s \in (Q (i), Q (i + 1)) \lor s \in \{Q (i)\})$
177	176	adantlr	$⊢ ((φ \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)\})$
178		elsni	$⊢ s \in \{Q (i)\} \to s = Q (i)$
179	178	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{Q (i)\}) \to s = Q (i)$
180	160	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{Q (i)\}) \to Q (i) \in ℝ$
181	179 180	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in \{Q (i)\}) \to s \in ℝ$
182	181	ex	$⊢ (φ \land i \in (0 ..^M)) \to (s \in \{Q (i)\} \to s \in ℝ)$
183	182	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 ℝ)$
184		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 ℝ)$
185	131 183 184	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 ℝ)$
186	177 185	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to s \in ℝ$
187	7	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to X \in ℝ$
188	186 187	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})) \to s - X \in ℝ$
189		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)$
190	188 189	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)\} ⟶ ℝ$
191		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)))$
192	173 190 191	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)))$
193		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)$
194	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$
195		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)\})$
196	193 194 195 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$
197	196	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)$
198	197	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))$
199	192 198	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)$
200		eqid	$⊢ (s \in ℂ ⟼ s - X) = (s \in ℂ ⟼ s - X)$
201		simpr	$⊢ (φ \land s \in ℂ) \to s \in ℂ$
202	94	adantr	$⊢ (φ \land s \in ℂ) \to X \in ℂ$
203	201 202	negsubd	$⊢ (φ \land s \in ℂ) \to s + (- X) = s - X$
204	203	eqcomd	$⊢ (φ \land s \in ℂ) \to s - X = s + (- X)$
205	204	mpteq2dva	$⊢ φ \to (s \in ℂ ⟼ s - X) = (s \in ℂ ⟼ s + (- X))$
206		eqid	$⊢ (s \in ℂ ⟼ s + (- X)) = (s \in ℂ ⟼ s + (- X))$
207	206	addccncf	$⊢ - X \in ℂ \to (s \in ℂ ⟼ s + (- X)) : ℂ \underset{cn}{⟶} ℂ$
208	99 207	syl	$⊢ φ \to (s \in ℂ ⟼ s + (- X)) : ℂ \underset{cn}{⟶} ℂ$
209	205 208	eqeltrd	$⊢ φ \to (s \in ℂ ⟼ s - X) : ℂ \underset{cn}{⟶} ℂ$
210	209	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℂ ⟼ s - X) : ℂ \underset{cn}{⟶} ℂ$
211	160	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
212	211	snssd	$⊢ (φ \land i \in (0 ..^M)) \to \{Q (i)\} \subseteq ℂ$
213	108 212	unssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cup \{Q (i)\} \subseteq ℂ$
214	200 210 213 109 188	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}{⟶} ℝ$
215	116 122	eqeltrd	$⊢ φ \to D (N) : ℝ \underset{cn}{⟶} ℂ$
216	215	adantr	$⊢ (φ \land i \in (0 ..^M)) \to D (N) : ℝ \underset{cn}{⟶} ℂ$
217	214 216	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}{⟶} ℂ$
218		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
219		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
220	218	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
221		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
222	221	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
223	220 222	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
224	223	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
225	218 219 224	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})$
226	213 113 225	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})$
227	217 226	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}))$
228	199 227	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}))$
229	218	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
230		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)\})$
231	229 213 230	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)\})$
232		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)))$
233	231 229 232	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)))$
234	228 233	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))$
235	234	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)$
236		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = Q (i)$
237		elsng	$⊢ Q (i) \in ℝ \to (Q (i) \in \{Q (i)\} \leftrightarrow Q (i) = Q (i))$
238	160 237	syl	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) \in \{Q (i)\} \leftrightarrow Q (i) = Q (i))$
239	236 238	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in \{Q (i)\}$
240	239	olcd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) \in (Q (i), Q (i + 1)) \lor Q (i) \in \{Q (i)\})$
241		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)\})$
242	240 241	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ((Q (i), Q (i + 1)) \cup \{Q (i)\})$
243		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))$
244	243	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)))$
245	244	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))$
246	235 242 245	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))$
247	172 246	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))$
248		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)))$
249	219 218 248 139 108 211	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)))$
250	247 249	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))$
251	129 139 140 10 250	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))$
252		fvres	$⊢ t \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (t) = F (t)$
253	252	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) (t) = F (t)$
254	253	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)$
255	254	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))$
256	255	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)$
257	251 256	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))$
258		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))$
259		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \land s = t) \to s = t$
260	259	oveq1d	$⊢ (((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \land s = t) \to s - X = t - X$
261	260	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)$
262		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to t \in (Q (i), Q (i + 1))$
263	115	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to D (N) : ℝ ⟶ ℝ$
264	263 71	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to D (N) (t - X) \in ℝ$
265	258 261 262 264	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)$
266	265	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)$
267	266	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))$
268	267	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)$
269	257 268	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))$
270	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))}$
271	270	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)$
272	269 271	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R D (N) (Q (i) - X) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
273		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)$
274		oveq1	$⊢ t = Q (i + 1) \to t - X = Q (i + 1) - X$
275	274	eqcomd	$⊢ t = Q (i + 1) \to Q (i + 1) - X = t - X$
276	275	fveq2d	$⊢ t = Q (i + 1) \to D (N) (Q (i + 1) - X) = D (N) (t - X)$
277	273 276	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)$
278	277	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)$
279		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)$
280	279	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)$
281		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))$
282	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)$
283		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)\})$
284	283	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)\})$
285	284	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)))$
286	285	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)))$
287		velsn	$⊢ t \in \{Q (i + 1)\} \leftrightarrow t = Q (i + 1)$
288	287	notbii	$⊢ \neg t \in \{Q (i + 1)\} \leftrightarrow \neg t = Q (i + 1)$
289	288	biimpri	$⊢ \neg t = Q (i + 1) \to \neg t \in \{Q (i + 1)\}$
290	289	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 \neg t \in \{Q (i + 1)\}$
291		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)))$
292	286 290 291	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))$
293	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) : ℝ ⟶ ℝ$
294	292 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 ℝ$
295	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 ℝ$
296	294 295	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 ℝ$
297	293 296	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 ℝ$
298	281 282 292 297	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)$
299	280 298	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)$
300	278 299	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)$
301	300	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))$
302		eqid	$⊢ (t \in ℝ ⟼ D (N) (t - X)) = (t \in ℝ ⟼ D (N) (t - X))$
303	106	a1i	$⊢ φ \to ℝ \subseteq ℂ$
304		simpr	$⊢ (φ \land t \in ℝ) \to t \in ℝ$
305	7	adantr	$⊢ (φ \land t \in ℝ) \to X \in ℝ$
306	304 305	resubcld	$⊢ (φ \land t \in ℝ) \to t - X \in ℝ$
307	92 103 303 303 306	cncfmptssg	$⊢ φ \to (t \in ℝ ⟼ t - X) : ℝ \underset{cn}{⟶} ℝ$
308	307 215	cncfcompt	$⊢ φ \to (t \in ℝ ⟼ D (N) (t - X)) : ℝ \underset{cn}{⟶} ℂ$
309	308	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (t \in ℝ ⟼ D (N) (t - X)) : ℝ \underset{cn}{⟶} ℂ$
310	105	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
311		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
312	311	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
313	43 312	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [- π, π]$
314	156 313	sselid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
315	314	snssd	$⊢ (φ \land i \in (0 ..^M)) \to \{Q (i + 1)\} \subseteq ℝ$
316	310 315	unssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} \subseteq ℝ$
317	113	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℂ \subseteq ℂ$
318	173	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to D (N) : ℝ ⟶ ℝ$
319	316	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to t \in ℝ$
320	7	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to X \in ℝ$
321	319 320	resubcld	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to t - X \in ℝ$
322	318 321	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to D (N) (t - X) \in ℝ$
323	322	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land t \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})) \to D (N) (t - X) \in ℂ$
324	302 309 316 317 323	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}{⟶} ℂ$
325	156 106	sstri	$⊢ [- π, π] \subseteq ℂ$
326	325 313	sselid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
327	326	snssd	$⊢ (φ \land i \in (0 ..^M)) \to \{Q (i + 1)\} \subseteq ℂ$
328	108 327	unssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \cup \{Q (i + 1)\} \subseteq ℂ$
329		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})$
330	218 329 224	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})$
331	328 113 330	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})$
332	324 331	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}))$
333		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)\})$
334	229 328 333	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)\})$
335		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)))$
336	334 229 335	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)))$
337	332 336	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))$
338	337	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)$
339		eqidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = Q (i + 1)$
340		elsng	$⊢ Q (i + 1) \in ℝ \to (Q (i + 1) \in \{Q (i + 1)\} \leftrightarrow Q (i + 1) = Q (i + 1))$
341	314 340	syl	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i + 1) \in \{Q (i + 1)\} \leftrightarrow Q (i + 1) = Q (i + 1))$
342	339 341	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in \{Q (i + 1)\}$
343	342	olcd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i + 1) \in (Q (i), Q (i + 1)) \lor Q (i + 1) \in \{Q (i + 1)\})$
344		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)\})$
345	343 344	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ((Q (i), Q (i + 1)) \cup \{Q (i + 1)\})$
346		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))$
347	346	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)))$
348	347	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))$
349	338 345 348	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))$
350	301 349	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))$
351		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)))$
352	329 218 351 139 108 326	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)))$
353	350 352	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))$
354	129 139 140 11 353	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))$
355	267 255 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))}$
356	355	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)$
357	354 356	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))$
358	2 32 5 4 7 33 127 272 357	fourierdlem93	$⊢ φ \to \int_{[- π, π]} G (t) d t = \int_{[- π - X, π - X]} G (X + s) d s$
359	3	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to G = (t \in [- π, π] ⟼ F (t) D (N) (t - X))$
360		fveq2	$⊢ t = X + s \to F (t) = F (X + s)$
361	360	oveq1d	$⊢ t = X + s \to F (t) D (N) (t - X) = F (X + s) D (N) (t - X)$
362	361	adantl	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to F (t) D (N) (t - X) = F (X + s) D (N) (t - X)$
363		oveq1	$⊢ t = X + s \to t - X = X + s - X$
364	94	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to X \in ℂ$
365	36 7	resubcld	$⊢ φ \to - π - X \in ℝ$
366	365	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to - π - X \in ℝ$
367	39 7	resubcld	$⊢ φ \to π - X \in ℝ$
368	367	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to π - X \in ℝ$
369		simpr	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in [- π - X, π - X]$
370		eliccre	$⊢ (- π - X \in ℝ \land π - X \in ℝ \land s \in [- π - X, π - X]) \to s \in ℝ$
371	366 368 369 370	syl3anc	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in ℝ$
372	371	recnd	$⊢ (φ \land s \in [- π - X, π - X]) \to s \in ℂ$
373	364 372	pncan2d	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s - X = s$
374	363 373	sylan9eqr	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to t - X = s$
375	374	fveq2d	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to D (N) (t - X) = D (N) (s)$
376	375	oveq2d	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to F (X + s) D (N) (t - X) = F (X + s) D (N) (s)$
377	362 376	eqtrd	$⊢ ((φ \land s \in [- π - X, π - X]) \land t = X + s) \to F (t) D (N) (t - X) = F (X + s) D (N) (s)$
378	16	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to - π \in ℝ$
379	15	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to π \in ℝ$
380	7	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to X \in ℝ$
381	380 371	readdcld	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \in ℝ$
382	36	recnd	$⊢ φ \to - π \in ℂ$
383	94 382	pncan3d	$⊢ φ \to X + (- π) - X = - π$
384	383	eqcomd	$⊢ φ \to - π = X + (- π) - X$
385	384	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to - π = X + (- π) - X$
386		elicc2	$⊢ (- π - X \in ℝ \land π - X \in ℝ) \to (s \in [- π - X, π - X] \leftrightarrow (s \in ℝ \land - π - X \leq s \land s \leq π - X))$
387	366 368 386	syl2anc	$⊢ (φ \land s \in [- π - X, π - X]) \to (s \in [- π - X, π - X] \leftrightarrow (s \in ℝ \land - π - X \leq s \land s \leq π - X))$
388	369 387	mpbid	$⊢ (φ \land s \in [- π - X, π - X]) \to (s \in ℝ \land - π - X \leq s \land s \leq π - X)$
389	388	simp2d	$⊢ (φ \land s \in [- π - X, π - X]) \to - π - X \leq s$
390	366 371 380 389	leadd2dd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + (- π) - X \leq X + s$
391	385 390	eqbrtrd	$⊢ (φ \land s \in [- π - X, π - X]) \to - π \leq X + s$
392	388	simp3d	$⊢ (φ \land s \in [- π - X, π - X]) \to s \leq π - X$
393	371 368 380 392	leadd2dd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \leq X + π - X$
394		picn	$⊢ π \in ℂ$
395	394	a1i	$⊢ (φ \land s \in [- π - X, π - X]) \to π \in ℂ$
396	364 395	pncan3d	$⊢ (φ \land s \in [- π - X, π - X]) \to X + π - X = π$
397	393 396	breqtrd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \leq π$
398	378 379 381 391 397	eliccd	$⊢ (φ \land s \in [- π - X, π - X]) \to X + s \in [- π, π]$
399	8	adantr	$⊢ (φ \land s \in [- π - X, π - X]) \to F : [- π, π] ⟶ ℂ$
400	399 398	ffvelcdmd	$⊢ (φ \land s \in [- π - X, π - X]) \to F (X + s) \in ℂ$
401	371 111	syldan	$⊢ (φ \land s \in [- π - X, π - X]) \to D (N) (s) \in ℂ$
402	400 401	mulcld	$⊢ (φ \land s \in [- π - X, π - X]) \to F (X + s) D (N) (s) \in ℂ$
403	359 377 398 402	fvmptd	$⊢ (φ \land s \in [- π - X, π - X]) \to G (X + s) = F (X + s) D (N) (s)$
404	403	itgeq2dv	$⊢ φ \to \int_{[- π - X, π - X]} G (X + s) d s = \int_{[- π - X, π - X]} F (X + s) D (N) (s) d s$
405	29 358 404	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