fourierdlem73

Description: A version of the Riemann Lebesgue lemma: as r increases, the integral in S goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem73.a	$⊢ φ \to A \in ℝ$
	fourierdlem73.b	$⊢ φ \to B \in ℝ$
	fourierdlem73.f	$⊢ φ \to F : [A, B] ⟶ ℂ$
	fourierdlem73.m	$⊢ φ \to M \in ℕ$
	fourierdlem73.qf	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
	fourierdlem73.q0	$⊢ φ \to Q (0) = A$
	fourierdlem73.qm	$⊢ φ \to Q (M) = B$
	fourierdlem73.qilt	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
	fourierdlem73.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem73.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem73.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem73.g	$⊢ G = ℝ D F$
	fourierdlem73.gcn	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem73.gbd	$⊢ φ \to \exists y \in ℝ \forall x \in dom G \|G (x)\| \leq y$
	fourierdlem73.s	$⊢ S = (r \in ℝ^{+} ⟼ \int_{(A, B)} F (x) \sin r x d x)$
	fourierdlem73.d	$⊢ D = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x))))$
Assertion	fourierdlem73	$⊢ φ \to \forall e \in ℝ^{+} \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem73.a	$⊢ φ \to A \in ℝ$
2		fourierdlem73.b	$⊢ φ \to B \in ℝ$
3		fourierdlem73.f	$⊢ φ \to F : [A, B] ⟶ ℂ$
4		fourierdlem73.m	$⊢ φ \to M \in ℕ$
5		fourierdlem73.qf	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
6		fourierdlem73.q0	$⊢ φ \to Q (0) = A$
7		fourierdlem73.qm	$⊢ φ \to Q (M) = B$
8		fourierdlem73.qilt	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
9		fourierdlem73.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
10		fourierdlem73.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
11		fourierdlem73.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
12		fourierdlem73.g	$⊢ G = ℝ D F$
13		fourierdlem73.gcn	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
14		fourierdlem73.gbd	$⊢ φ \to \exists y \in ℝ \forall x \in dom G \|G (x)\| \leq y$
15		fourierdlem73.s	$⊢ S = (r \in ℝ^{+} ⟼ \int_{(A, B)} F (x) \sin r x d x)$
16		fourierdlem73.d	$⊢ D = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x))))$
17		cncff	$⊢ ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
18	13 17	syl	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
19		ax-resscn	$⊢ ℝ \subseteq ℂ$
20	19	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℂ$
21	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
22	5 21	fssd	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
23	22	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
24		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
25	24	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
26	23 25	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
27		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
28	27	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
29	23 28	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
30	26 29	iccssred	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq ℝ$
31		limccl	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \subseteq ℂ$
32	31 11	sselid	$⊢ (φ \land i \in (0 ..^M)) \to R \in ℂ$
33	32	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to R \in ℂ$
34		limccl	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \subseteq ℂ$
35	34 10	sselid	$⊢ (φ \land i \in (0 ..^M)) \to L \in ℂ$
36	35	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to L \in ℂ$
37	3	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F : [A, B] ⟶ ℂ$
38	1	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to A \in ℝ$
39	2	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to B \in ℝ$
40	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i) \in ℝ$
41	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i + 1) \in ℝ$
42		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in [Q (i), Q (i + 1)]$
43		eliccre	$⊢ (Q (i) \in ℝ \land Q (i + 1) \in ℝ \land x \in [Q (i), Q (i + 1)]) \to x \in ℝ$
44	40 41 42 43	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℝ$
45	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
46	45	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ^{*}$
47	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
48	47	adantr	$⊢ (φ \land i \in (0 ..^M)) \to B \in ℝ^{*}$
49	5	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [A, B]$
50	49 25	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [A, B]$
51		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (i) \in [A, B]) \to A \leq Q (i)$
52	46 48 50 51	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to A \leq Q (i)$
53	52	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to A \leq Q (i)$
54	40	rexrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i) \in ℝ^{*}$
55	41	rexrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i + 1) \in ℝ^{*}$
56		iccgelb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land x \in [Q (i), Q (i + 1)]) \to Q (i) \leq x$
57	54 55 42 56	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i) \leq x$
58	38 40 44 53 57	letrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to A \leq x$
59		iccleub	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land x \in [Q (i), Q (i + 1)]) \to x \leq Q (i + 1)$
60	54 55 42 59	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \leq Q (i + 1)$
61	45	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to A \in ℝ^{*}$
62	47	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to B \in ℝ^{*}$
63	49 28	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [A, B]$
64	63	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i + 1) \in [A, B]$
65		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (i + 1) \in [A, B]) \to Q (i + 1) \leq B$
66	61 62 64 65	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to Q (i + 1) \leq B$
67	44 41 39 60 66	letrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \leq B$
68	38 39 44 58 67	eliccd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in [A, B]$
69	37 68	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
70	36 69	ifcld	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to if (x = Q (i + 1), L, F (x)) \in ℂ$
71	33 70	ifcld	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) \in ℂ$
72	71 16	fmptd	$⊢ (φ \land i \in (0 ..^M)) \to D : [Q (i), Q (i + 1)] ⟶ ℂ$
73		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
74		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
75		iccntr	$⊢ (Q (i) \in ℝ \land Q (i + 1) \in ℝ) \to int (topGen (ran (.))) ([Q (i), Q (i + 1)]) = (Q (i), Q (i + 1))$
76	26 29 75	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to int (topGen (ran (.))) ([Q (i), Q (i + 1)]) = (Q (i), Q (i + 1))$
77	20 30 72 73 74 76	dvresntr	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D D = ℝ D ({D ↾}_{(Q (i), Q (i + 1))})$
78		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
79	78	sseli	$⊢ x \in (Q (i), Q (i + 1)) \to x \in [Q (i), Q (i + 1)]$
80	79	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in [Q (i), Q (i + 1)]$
81		fvres	$⊢ x \in [Q (i), Q (i + 1)] \to ({F ↾}_{[Q (i), Q (i + 1)]}) (x) = F (x)$
82	80 81	syl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to ({F ↾}_{[Q (i), Q (i + 1)]}) (x) = F (x)$
83	80 71	syldan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) \in ℂ$
84	16	fvmpt2	$⊢ (x \in [Q (i), Q (i + 1)] \land if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) \in ℂ) \to D (x) = if (x = Q (i), R, if (x = Q (i + 1), L, F (x)))$
85	80 83 84	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to D (x) = if (x = Q (i), R, if (x = Q (i + 1), L, F (x)))$
86	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ$
87	80 54	syldan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ^{*}$
88	80 55	syldan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ^{*}$
89		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in (Q (i), Q (i + 1))$
90		ioogtlb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land x \in (Q (i), Q (i + 1))) \to Q (i) < x$
91	87 88 89 90	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q (i) < x$
92	86 91	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \neq Q (i)$
93	92	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to \neg x = Q (i)$
94	93	iffalsed	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i + 1), L, F (x))$
95		elioore	$⊢ x \in (Q (i), Q (i + 1)) \to x \in ℝ$
96	95	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in ℝ$
97		iooltub	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land x \in (Q (i), Q (i + 1))) \to x < Q (i + 1)$
98	87 88 89 97	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x < Q (i + 1)$
99	96 98	ltned	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \neq Q (i + 1)$
100	99	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to \neg x = Q (i + 1)$
101	100	iffalsed	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to if (x = Q (i + 1), L, F (x)) = F (x)$
102	85 94 101	3eqtrrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x) = D (x)$
103	82 102	eqtr2d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to D (x) = ({F ↾}_{[Q (i), Q (i + 1)]}) (x)$
104	103	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall x \in (Q (i), Q (i + 1)) D (x) = ({F ↾}_{[Q (i), Q (i + 1)]}) (x)$
105		ffn	$⊢ D : [Q (i), Q (i + 1)] ⟶ ℂ \to D Fn [Q (i), Q (i + 1)]$
106	72 105	syl	$⊢ (φ \land i \in (0 ..^M)) \to D Fn [Q (i), Q (i + 1)]$
107		ffn	$⊢ F : [A, B] ⟶ ℂ \to F Fn [A, B]$
108	3 107	syl	$⊢ φ \to F Fn [A, B]$
109	108	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F Fn [A, B]$
110		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
111	46 48 49 110	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
112		fnssres	$⊢ (F Fn [A, B] \land [Q (i), Q (i + 1)] \subseteq [A, B]) \to ({F ↾}_{[Q (i), Q (i + 1)]}) Fn [Q (i), Q (i + 1)]$
113	109 111 112	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{[Q (i), Q (i + 1)]}) Fn [Q (i), Q (i + 1)]$
114	78	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
115		fvreseq	$⊢ ((D Fn [Q (i), Q (i + 1)] \land ({F ↾}_{[Q (i), Q (i + 1)]}) Fn [Q (i), Q (i + 1)]) \land (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]) \to ({D ↾}_{(Q (i), Q (i + 1))} = {({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))} \leftrightarrow \forall x \in (Q (i), Q (i + 1)) D (x) = ({F ↾}_{[Q (i), Q (i + 1)]}) (x))$
116	106 113 114 115	syl21anc	$⊢ (φ \land i \in (0 ..^M)) \to ({D ↾}_{(Q (i), Q (i + 1))} = {({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))} \leftrightarrow \forall x \in (Q (i), Q (i + 1)) D (x) = ({F ↾}_{[Q (i), Q (i + 1)]}) (x))$
117	104 116	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to {D ↾}_{(Q (i), Q (i + 1))} = {({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))}$
118	114	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{[Q (i), Q (i + 1)]}) ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (i), Q (i + 1))}$
119	117 118	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to {D ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (i), Q (i + 1))}$
120	119	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({D ↾}_{(Q (i), Q (i + 1))}) = ℝ D ({F ↾}_{(Q (i), Q (i + 1))})$
121	3	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : [A, B] ⟶ ℂ$
122	21	adantr	$⊢ (φ \land i \in (0 ..^M)) \to [A, B] \subseteq ℝ$
123	114 30	sstrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
124	74 73	dvres	$⊢ ((ℝ \subseteq ℂ \land F : [A, B] ⟶ ℂ) \land ([A, B] \subseteq ℝ \land (Q (i), Q (i + 1)) \subseteq ℝ)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}$
125	20 121 122 123 124	syl22anc	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}$
126	12	eqcomi	$⊢ ℝ D F = G$
127	126	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D F = G$
128		iooretop	$⊢ (Q (i), Q (i + 1)) \in topGen (ran (.))$
129		retop	$⊢ topGen (ran (.)) \in Top$
130		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
131	130	isopn3	$⊢ (topGen (ran (.)) \in Top \land (Q (i), Q (i + 1)) \subseteq ℝ) \to ((Q (i), Q (i + 1)) \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) ((Q (i), Q (i + 1))) = (Q (i), Q (i + 1)))$
132	129 123 131	sylancr	$⊢ (φ \land i \in (0 ..^M)) \to ((Q (i), Q (i + 1)) \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) ((Q (i), Q (i + 1))) = (Q (i), Q (i + 1)))$
133	128 132	mpbii	$⊢ (φ \land i \in (0 ..^M)) \to int (topGen (ran (.))) ((Q (i), Q (i + 1))) = (Q (i), Q (i + 1))$
134	127 133	reseq12d	$⊢ (φ \land i \in (0 ..^M)) \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))} = {G ↾}_{(Q (i), Q (i + 1))}$
135	125 134	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {G ↾}_{(Q (i), Q (i + 1))}$
136	77 120 135	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D D = {G ↾}_{(Q (i), Q (i + 1))}$
137	136	feq1d	$⊢ (φ \land i \in (0 ..^M)) \to (D_{ℝ}^{'} : (Q (i), Q (i + 1)) ⟶ ℂ \leftrightarrow ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ)$
138	18 137	mpbird	$⊢ (φ \land i \in (0 ..^M)) \to D_{ℝ}^{'} : (Q (i), Q (i + 1)) ⟶ ℂ$
139	138	feqmptd	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D D = (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x))$
140	139 136	eqtr3d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x)) = {G ↾}_{(Q (i), Q (i + 1))}$
141		ioombl	$⊢ (Q (i), Q (i + 1)) \in dom vol$
142	141	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \in dom vol$
143	26 29 8	ltled	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \leq Q (i + 1)$
144		volioo	$⊢ (Q (i) \in ℝ \land Q (i + 1) \in ℝ \land Q (i) \leq Q (i + 1)) \to vol ((Q (i), Q (i + 1))) = Q (i + 1) - Q (i)$
145	26 29 143 144	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to vol ((Q (i), Q (i + 1))) = Q (i + 1) - Q (i)$
146	29 26	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - Q (i) \in ℝ$
147	145 146	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to vol ((Q (i), Q (i + 1))) \in ℝ$
148	14	adantr	$⊢ (φ \land i \in (0 ..^M)) \to \exists y \in ℝ \forall x \in dom G \|G (x)\| \leq y$
149		nfv	$⊢ Ⅎ x ((φ \land i \in (0 ..^M)) \land y \in ℝ)$
150		nfra1	$⊢ Ⅎ x \forall x \in dom G \|G (x)\| \leq y$
151	149 150	nfan	$⊢ Ⅎ x (((φ \land i \in (0 ..^M)) \land y \in ℝ) \land \forall x \in dom G \|G (x)\| \leq y)$
152		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to x \in dom ({G ↾}_{(Q (i), Q (i + 1))})$
153		fdm	$⊢ ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \to dom ({G ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
154	18 153	syl	$⊢ (φ \land i \in (0 ..^M)) \to dom ({G ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
155	154	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to dom ({G ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
156	152 155	eleqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to x \in (Q (i), Q (i + 1))$
157		fvres	$⊢ x \in (Q (i), Q (i + 1)) \to ({G ↾}_{(Q (i), Q (i + 1))}) (x) = G (x)$
158	156 157	syl	$⊢ ((φ \land i \in (0 ..^M)) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to ({G ↾}_{(Q (i), Q (i + 1))}) (x) = G (x)$
159	158	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| = \|G (x)\|$
160	159	ad4ant14	$⊢ ((((φ \land i \in (0 ..^M)) \land y \in ℝ) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| = \|G (x)\|$
161		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to \forall x \in dom G \|G (x)\| \leq y$
162		ssdmres	$⊢ (Q (i), Q (i + 1)) \subseteq dom G \leftrightarrow dom ({G ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
163	154 162	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom G$
164	163	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in dom G$
165	156 164	syldan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to x \in dom G$
166	165	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to x \in dom G$
167		rsp	$⊢ \forall x \in dom G \|G (x)\| \leq y \to (x \in dom G \to \|G (x)\| \leq y)$
168	161 166 167	sylc	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to \|G (x)\| \leq y$
169	168	adantllr	$⊢ ((((φ \land i \in (0 ..^M)) \land y \in ℝ) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to \|G (x)\| \leq y$
170	160 169	eqbrtrd	$⊢ ((((φ \land i \in (0 ..^M)) \land y \in ℝ) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in dom ({G ↾}_{(Q (i), Q (i + 1))})) \to \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| \leq y$
171	170	ex	$⊢ (((φ \land i \in (0 ..^M)) \land y \in ℝ) \land \forall x \in dom G \|G (x)\| \leq y) \to (x \in dom ({G ↾}_{(Q (i), Q (i + 1))}) \to \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| \leq y)$
172	151 171	ralrimi	$⊢ (((φ \land i \in (0 ..^M)) \land y \in ℝ) \land \forall x \in dom G \|G (x)\| \leq y) \to \forall x \in dom ({G ↾}_{(Q (i), Q (i + 1))}) \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| \leq y$
173	172	ex	$⊢ ((φ \land i \in (0 ..^M)) \land y \in ℝ) \to (\forall x \in dom G \|G (x)\| \leq y \to \forall x \in dom ({G ↾}_{(Q (i), Q (i + 1))}) \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| \leq y)$
174	173	reximdva	$⊢ (φ \land i \in (0 ..^M)) \to (\exists y \in ℝ \forall x \in dom G \|G (x)\| \leq y \to \exists y \in ℝ \forall x \in dom ({G ↾}_{(Q (i), Q (i + 1))}) \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| \leq y)$
175	148 174	mpd	$⊢ (φ \land i \in (0 ..^M)) \to \exists y \in ℝ \forall x \in dom ({G ↾}_{(Q (i), Q (i + 1))}) \|({G ↾}_{(Q (i), Q (i + 1))}) (x)\| \leq y$
176	142 147 13 175	cnbdibl	$⊢ (φ \land i \in (0 ..^M)) \to {G ↾}_{(Q (i), Q (i + 1))} \in 𝐿^{1}$
177	140 176	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x)) \in 𝐿^{1}$
178	177	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x)) \in 𝐿^{1}$
179	141	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (Q (i), Q (i + 1)) \in dom vol$
180	147	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to vol ((Q (i), Q (i + 1))) \in ℝ$
181	140 13	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
182	181	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
183		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
184	183	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \cos : ℂ \underset{cn}{⟶} ℂ$
185		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
186	185	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (Q (i), Q (i + 1)) \subseteq ℂ$
187		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to r \in ℝ$
188	187	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to r \in ℂ$
189		ssid	$⊢ ℂ \subseteq ℂ$
190	189	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to ℂ \subseteq ℂ$
191	186 188 190	constcncfg	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ r) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
192	185	a1i	$⊢ φ \to (Q (i), Q (i + 1)) \subseteq ℂ$
193	189	a1i	$⊢ φ \to ℂ \subseteq ℂ$
194	192 193	idcncfg	$⊢ φ \to (x \in (Q (i), Q (i + 1)) ⟼ x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
195	194	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
196	191 195	mulcncf	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
197	184 196	cncfmpt1f	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ \cos r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
198	197	negcncfg	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ - \cos r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
199	182 198	mulcncf	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
200		nfv	$⊢ Ⅎ x (φ \land i \in (0 ..^M))$
201	200 150	nfan	$⊢ Ⅎ x ((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y)$
202	136	fveq1d	$⊢ (φ \land i \in (0 ..^M)) \to D_{ℝ}^{'} (x) = ({G ↾}_{(Q (i), Q (i + 1))}) (x)$
203	202 157	sylan9eq	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (x) = G (x)$
204	203	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to \|D_{ℝ}^{'} (x)\| = \|G (x)\|$
205	204	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in (Q (i), Q (i + 1))) \to \|D_{ℝ}^{'} (x)\| = \|G (x)\|$
206		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in (Q (i), Q (i + 1))) \to \forall x \in dom G \|G (x)\| \leq y$
207	164	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in (Q (i), Q (i + 1))) \to x \in dom G$
208	206 207 167	sylc	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in (Q (i), Q (i + 1))) \to \|G (x)\| \leq y$
209	205 208	eqbrtrd	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \land x \in (Q (i), Q (i + 1))) \to \|D_{ℝ}^{'} (x)\| \leq y$
210	209	ex	$⊢ ((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \to (x \in (Q (i), Q (i + 1)) \to \|D_{ℝ}^{'} (x)\| \leq y)$
211	201 210	ralrimi	$⊢ ((φ \land i \in (0 ..^M)) \land \forall x \in dom G \|G (x)\| \leq y) \to \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y$
212	211	ex	$⊢ (φ \land i \in (0 ..^M)) \to (\forall x \in dom G \|G (x)\| \leq y \to \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y)$
213	212	reximdv	$⊢ (φ \land i \in (0 ..^M)) \to (\exists y \in ℝ \forall x \in dom G \|G (x)\| \leq y \to \exists y \in ℝ \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y)$
214	148 213	mpd	$⊢ (φ \land i \in (0 ..^M)) \to \exists y \in ℝ \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y$
215	214	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \exists y \in ℝ \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y$
216		eqidd	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) = (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x))$
217		fveq2	$⊢ x = z \to D_{ℝ}^{'} (x) = D_{ℝ}^{'} (z)$
218		eleq1w	$⊢ x = z \to (x \in (Q (i), Q (i + 1)) \leftrightarrow z \in (Q (i), Q (i + 1)))$
219	218	anbi2d	$⊢ x = z \to (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \leftrightarrow ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))))$
220		fveq2	$⊢ x = z \to G (x) = G (z)$
221	217 220	eqeq12d	$⊢ x = z \to (D_{ℝ}^{'} (x) = G (x) \leftrightarrow D_{ℝ}^{'} (z) = G (z))$
222	219 221	imbi12d	$⊢ x = z \to ((((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (x) = G (x)) \leftrightarrow (((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (z) = G (z)))$
223	222 203	chvarvv	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (z) = G (z)$
224	217 223	sylan9eqr	$⊢ (((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \land x = z) \to D_{ℝ}^{'} (x) = G (z)$
225		oveq2	$⊢ x = z \to r x = r z$
226	225	fveq2d	$⊢ x = z \to \cos r x = \cos r z$
227	226	negeqd	$⊢ x = z \to - \cos r x = - \cos r z$
228	227	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \land x = z) \to - \cos r x = - \cos r z$
229	224 228	oveq12d	$⊢ (((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \land x = z) \to D_{ℝ}^{'} (x) (- \cos r x) = G (z) (- \cos r z)$
230	229	adantllr	$⊢ ((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \land x = z) \to D_{ℝ}^{'} (x) (- \cos r x) = G (z) (- \cos r z)$
231		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to z \in (Q (i), Q (i + 1))$
232		fvres	$⊢ z \in (Q (i), Q (i + 1)) \to ({G ↾}_{(Q (i), Q (i + 1))}) (z) = G (z)$
233	232	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to ({G ↾}_{(Q (i), Q (i + 1))}) (z) = G (z)$
234	18	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to ({G ↾}_{(Q (i), Q (i + 1))}) (z) \in ℂ$
235	233 234	eqeltrrd	$⊢ ((φ \land i \in (0 ..^M)) \land z \in (Q (i), Q (i + 1))) \to G (z) \in ℂ$
236	235	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to G (z) \in ℂ$
237		simpl	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to r \in ℝ$
238		elioore	$⊢ z \in (Q (i), Q (i + 1)) \to z \in ℝ$
239	238	adantl	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to z \in ℝ$
240	237 239	remulcld	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to r z \in ℝ$
241	240	recnd	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to r z \in ℂ$
242	241	coscld	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to \cos r z \in ℂ$
243	242	negcld	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to - \cos r z \in ℂ$
244	243	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to - \cos r z \in ℂ$
245	236 244	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to G (z) (- \cos r z) \in ℂ$
246	216 230 231 245	fvmptd	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z) = G (z) (- \cos r z)$
247	246	fveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| = \|G (z) (- \cos r z)\|$
248	247	ad4ant14	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| = \|G (z) (- \cos r z)\|$
249	245	abscld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z) (- \cos r z)\| \in ℝ$
250	249	ad4ant14	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|G (z) (- \cos r z)\| \in ℝ$
251	236	abscld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| \in ℝ$
252	251	ad4ant14	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| \in ℝ$
253		simpllr	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to y \in ℝ$
254	244	abscld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|- \cos r z\| \in ℝ$
255		1red	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to 1 \in ℝ$
256	236	absge0d	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to 0 \leq \|G (z)\|$
257	242	absnegd	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to \|- \cos r z\| = \|\cos r z\|$
258		abscosbd	$⊢ r z \in ℝ \to \|\cos r z\| \leq 1$
259	240 258	syl	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to \|\cos r z\| \leq 1$
260	257 259	eqbrtrd	$⊢ (r \in ℝ \land z \in (Q (i), Q (i + 1))) \to \|- \cos r z\| \leq 1$
261	260	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|- \cos r z\| \leq 1$
262	254 255 251 256 261	lemul2ad	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| \|- \cos r z\| \leq \|G (z)\| \cdot 1$
263	236 244	absmuld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z) (- \cos r z)\| = \|G (z)\| \|- \cos r z\|$
264	251	recnd	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| \in ℂ$
265	264	mulridd	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| \cdot 1 = \|G (z)\|$
266	265	eqcomd	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| = \|G (z)\| \cdot 1$
267	262 263 266	3brtr4d	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land z \in (Q (i), Q (i + 1))) \to \|G (z) (- \cos r z)\| \leq \|G (z)\|$
268	267	ad4ant14	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|G (z) (- \cos r z)\| \leq \|G (z)\|$
269		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y$
270		nfra1	$⊢ Ⅎ x \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y$
271	200 270	nfan	$⊢ Ⅎ x ((φ \land i \in (0 ..^M)) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y)$
272	204	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to \|G (x)\| = \|D_{ℝ}^{'} (x)\|$
273	272	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \|D_{ℝ}^{'} (x)\| \leq y) \to \|G (x)\| = \|D_{ℝ}^{'} (x)\|$
274		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \|D_{ℝ}^{'} (x)\| \leq y) \to \|D_{ℝ}^{'} (x)\| \leq y$
275	273 274	eqbrtrd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \|D_{ℝ}^{'} (x)\| \leq y) \to \|G (x)\| \leq y$
276	275	ex	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to (\|D_{ℝ}^{'} (x)\| \leq y \to \|G (x)\| \leq y)$
277	276	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land x \in (Q (i), Q (i + 1))) \to (\|D_{ℝ}^{'} (x)\| \leq y \to \|G (x)\| \leq y)$
278	271 277	ralimdaa	$⊢ ((φ \land i \in (0 ..^M)) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to (\forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y \to \forall x \in (Q (i), Q (i + 1)) \|G (x)\| \leq y)$
279	269 278	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to \forall x \in (Q (i), Q (i + 1)) \|G (x)\| \leq y$
280	220	fveq2d	$⊢ x = z \to \|G (x)\| = \|G (z)\|$
281	280	breq1d	$⊢ x = z \to (\|G (x)\| \leq y \leftrightarrow \|G (z)\| \leq y)$
282	281	cbvralvw	$⊢ \forall x \in (Q (i), Q (i + 1)) \|G (x)\| \leq y \leftrightarrow \forall z \in (Q (i), Q (i + 1)) \|G (z)\| \leq y$
283	279 282	sylib	$⊢ ((φ \land i \in (0 ..^M)) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to \forall z \in (Q (i), Q (i + 1)) \|G (z)\| \leq y$
284	283	ad4ant14	$⊢ ((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to \forall z \in (Q (i), Q (i + 1)) \|G (z)\| \leq y$
285	284	r19.21bi	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|G (z)\| \leq y$
286	250 252 253 268 285	letrd	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|G (z) (- \cos r z)\| \leq y$
287	248 286	eqbrtrd	$⊢ (((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \land z \in (Q (i), Q (i + 1))) \to \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| \leq y$
288	287	ralrimiva	$⊢ ((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to \forall z \in (Q (i), Q (i + 1)) \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| \leq y$
289	138	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (x) \in ℂ$
290	289	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land x \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (x) \in ℂ$
291		simpl	$⊢ (r \in ℝ \land x \in (Q (i), Q (i + 1))) \to r \in ℝ$
292	95	adantl	$⊢ (r \in ℝ \land x \in (Q (i), Q (i + 1))) \to x \in ℝ$
293	291 292	remulcld	$⊢ (r \in ℝ \land x \in (Q (i), Q (i + 1))) \to r x \in ℝ$
294	293	recnd	$⊢ (r \in ℝ \land x \in (Q (i), Q (i + 1))) \to r x \in ℂ$
295	294	coscld	$⊢ (r \in ℝ \land x \in (Q (i), Q (i + 1))) \to \cos r x \in ℂ$
296	295	negcld	$⊢ (r \in ℝ \land x \in (Q (i), Q (i + 1))) \to - \cos r x \in ℂ$
297	296	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land x \in (Q (i), Q (i + 1))) \to - \cos r x \in ℂ$
298	290 297	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land x \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (x) (- \cos r x) \in ℂ$
299	298	ralrimiva	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \forall x \in (Q (i), Q (i + 1)) D_{ℝ}^{'} (x) (- \cos r x) \in ℂ$
300		dmmptg	$⊢ \forall x \in (Q (i), Q (i + 1)) D_{ℝ}^{'} (x) (- \cos r x) \in ℂ \to dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) = (Q (i), Q (i + 1))$
301	299 300	syl	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) = (Q (i), Q (i + 1))$
302	301	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) = (Q (i), Q (i + 1))$
303	288 302	raleqtrrdv	$⊢ ((((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \land \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y) \to \forall z \in dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| \leq y$
304	303	ex	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ) \land y \in ℝ) \to (\forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y \to \forall z \in dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| \leq y)$
305	304	reximdva	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (\exists y \in ℝ \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y \to \exists y \in ℝ \forall z \in dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| \leq y)$
306	215 305	mpd	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \exists y \in ℝ \forall z \in dom (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) \|(x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) (z)\| \leq y$
307	179 180 199 306	cnbdibl	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) \in 𝐿^{1}$
308	307	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℝ) \to (x \in (Q (i), Q (i + 1)) ⟼ D_{ℝ}^{'} (x) (- \cos r x)) \in 𝐿^{1}$
309	289	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \to D_{ℝ}^{'} (x) \in ℂ$
310		simpr	$⊢ ((((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \land r \in ℂ) \to r \in ℂ$
311	185	sseli	$⊢ x \in (Q (i), Q (i + 1)) \to x \in ℂ$
312	311	ad2antlr	$⊢ ((((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \land r \in ℂ) \to x \in ℂ$
313	310 312	mulcld	$⊢ ((((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \land r \in ℂ) \to r x \in ℂ$
314	313	coscld	$⊢ ((((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \land r \in ℂ) \to \cos r x \in ℂ$
315	293	ancoms	$⊢ (x \in (Q (i), Q (i + 1)) \land r \in ℝ) \to r x \in ℝ$
316		abscosbd	$⊢ r x \in ℝ \to \|\cos r x\| \leq 1$
317	315 316	syl	$⊢ (x \in (Q (i), Q (i + 1)) \land r \in ℝ) \to \|\cos r x\| \leq 1$
318	317	adantll	$⊢ ((((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \land r \in ℝ) \to \|\cos r x\| \leq 1$
319	16	a1i	$⊢ (φ \land i \in (0 ..^M)) \to D = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x))))$
320	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to Q (i) \in ℝ$
321	8	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to Q (i) < Q (i + 1)$
322		eqcom	$⊢ Q (i + 1) = x \leftrightarrow x = Q (i + 1)$
323	322	biimpri	$⊢ x = Q (i + 1) \to Q (i + 1) = x$
324	323	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to Q (i + 1) = x$
325	321 324	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to Q (i) < x$
326	320 325	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to x \neq Q (i)$
327	326	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to \neg x = Q (i)$
328	327	iffalsed	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i + 1), L, F (x))$
329		iftrue	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = L$
330	329	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to if (x = Q (i + 1), L, F (x)) = L$
331	328 330	eqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = L$
332	29	leidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \leq Q (i + 1)$
333	26 29 29 143 332	eliccd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [Q (i), Q (i + 1)]$
334	319 331 333 10	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) = L$
335	334 35	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) \in ℂ$
336	335	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to D (Q (i + 1)) \in ℂ$
337		eqid	$⊢ \|D (Q (i + 1))\| = \|D (Q (i + 1))\|$
338		iftrue	$⊢ x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = R$
339	338	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i)) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = R$
340	26	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
341	29	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
342		lbicc2	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land Q (i) \leq Q (i + 1)) \to Q (i) \in [Q (i), Q (i + 1)]$
343	340 341 143 342	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [Q (i), Q (i + 1)]$
344	319 339 343 11	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) = R$
345	344 32	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) \in ℂ$
346	345	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to D (Q (i)) \in ℂ$
347		eqid	$⊢ \|D (Q (i))\| = \|D (Q (i))\|$
348		eqid	$⊢ \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x = \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x$
349		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
350	4	nnrpd	$⊢ φ \to M \in ℝ^{+}$
351	350	adantr	$⊢ (φ \land e \in ℝ^{+}) \to M \in ℝ^{+}$
352	349 351	rpdivcld	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{M} \in ℝ^{+}$
353	352	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to \frac{e}{M} \in ℝ^{+}$
354		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to r \in ℂ$
355	29	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
356	355	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to Q (i + 1) \in ℂ$
357	354 356	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to r Q (i + 1) \in ℂ$
358	357	coscld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to \cos r Q (i + 1) \in ℂ$
359	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to Q (i + 1) \in ℝ$
360	187 359	remulcld	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to r Q (i + 1) \in ℝ$
361		abscosbd	$⊢ r Q (i + 1) \in ℝ \to \|\cos r Q (i + 1)\| \leq 1$
362	360 361	syl	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \|\cos r Q (i + 1)\| \leq 1$
363	362	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℝ) \to \|\cos r Q (i + 1)\| \leq 1$
364	26	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
365	364	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to Q (i) \in ℂ$
366	354 365	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to r Q (i) \in ℂ$
367	366	coscld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to \cos r Q (i) \in ℂ$
368	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to Q (i) \in ℝ$
369	187 368	remulcld	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to r Q (i) \in ℝ$
370		abscosbd	$⊢ r Q (i) \in ℝ \to \|\cos r Q (i)\| \leq 1$
371	369 370	syl	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \|\cos r Q (i)\| \leq 1$
372	371	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℝ) \to \|\cos r Q (i)\| \leq 1$
373		fveq2	$⊢ z = x \to D_{ℝ}^{'} (z) = D_{ℝ}^{'} (x)$
374	373	fveq2d	$⊢ z = x \to \|D_{ℝ}^{'} (z)\| = \|D_{ℝ}^{'} (x)\|$
375	374	cbvitgv	$⊢ \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z = \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x$
376	375	oveq2i	$⊢ \|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z = \|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x$
377	376	oveq1i	$⊢ \frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z}{\frac{e}{M}} = \frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x}{\frac{e}{M}}$
378	377	oveq1i	$⊢ (\frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z}{\frac{e}{M}}) + 1 = (\frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x}{\frac{e}{M}}) + 1$
379	378	fveq2i	$⊢ ⌊(\frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z}{\frac{e}{M}}) + 1⌋ = ⌊(\frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x}{\frac{e}{M}}) + 1⌋$
380	379	oveq1i	$⊢ ⌊(\frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z}{\frac{e}{M}}) + 1⌋ + 1 = ⌊(\frac{\|D (Q (i + 1))\| + \|D (Q (i))\| + \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x}{\frac{e}{M}}) + 1⌋ + 1$
381	178 308 309 314 318 336 337 346 347 348 353 358 363 367 372 380	fourierdlem47	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to \exists m \in ℕ \forall r \in (m, +∞) \|D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x\| < \frac{e}{M}$
382		simplll	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to φ$
383		simpllr	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to i \in (0 ..^M)$
384		elioore	$⊢ r \in (m, +∞) \to r \in ℝ$
385	384	adantl	$⊢ (m \in ℕ \land r \in (m, +∞)) \to r \in ℝ$
386		0red	$⊢ (m \in ℕ \land r \in (m, +∞)) \to 0 \in ℝ$
387		nnre	$⊢ m \in ℕ \to m \in ℝ$
388	387	adantr	$⊢ (m \in ℕ \land r \in (m, +∞)) \to m \in ℝ$
389		nngt0	$⊢ m \in ℕ \to 0 < m$
390	389	adantr	$⊢ (m \in ℕ \land r \in (m, +∞)) \to 0 < m$
391	388	rexrd	$⊢ (m \in ℕ \land r \in (m, +∞)) \to m \in ℝ^{*}$
392		pnfxr	$⊢ +∞ \in ℝ^{*}$
393	392	a1i	$⊢ (m \in ℕ \land r \in (m, +∞)) \to +∞ \in ℝ^{*}$
394		simpr	$⊢ (m \in ℕ \land r \in (m, +∞)) \to r \in (m, +∞)$
395		ioogtlb	$⊢ (m \in ℝ^{} \land +∞ \in ℝ^{} \land r \in (m, +∞)) \to m < r$
396	391 393 394 395	syl3anc	$⊢ (m \in ℕ \land r \in (m, +∞)) \to m < r$
397	386 388 385 390 396	lttrd	$⊢ (m \in ℕ \land r \in (m, +∞)) \to 0 < r$
398	385 397	elrpd	$⊢ (m \in ℕ \land r \in (m, +∞)) \to r \in ℝ^{+}$
399	398	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to r \in ℝ^{+}$
400	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to Q (i) \in ℝ$
401	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to Q (i + 1) \in ℝ$
402	72	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to D (x) \in ℂ$
403	402	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to D (x) \in ℂ$
404		rpcn	$⊢ r \in ℝ^{+} \to r \in ℂ$
405	404	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to r \in ℂ$
406	44	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
407	406	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
408	405 407	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to r x \in ℂ$
409	408	sincld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to \sin r x \in ℂ$
410	403 409	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to D (x) \sin r x \in ℂ$
411	400 401 410	itgioo	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to \int_{(Q (i), Q (i + 1))} D (x) \sin r x d x = \int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x$
412	143	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to Q (i) \leq Q (i + 1)$
413	72	feqmptd	$⊢ (φ \land i \in (0 ..^M)) \to D = (x \in [Q (i), Q (i + 1)] ⟼ D (x))$
414		iftrue	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = L$
415	329 414	eqtr4d	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
416	415	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land x = Q (i + 1)) \to if (x = Q (i + 1), L, F (x)) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
417		iffalse	$⊢ \neg x = Q (i + 1) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x)$
418	417	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = ({F ↾}_{(Q (i), Q (i + 1))}) (x)$
419	54	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i) \in ℝ^{*}$
420	55	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i + 1) \in ℝ^{*}$
421	44	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x \in ℝ$
422	26	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) \in ℝ$
423	44	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \in ℝ$
424	57	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) \leq x$
425		neqne	$⊢ \neg x = Q (i) \to x \neq Q (i)$
426	425	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \neq Q (i)$
427	422 423 424 426	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) < x$
428	427	adantr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to Q (i) < x$
429	44	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i + 1)) \to x \in ℝ$
430	29	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i + 1)) \to Q (i + 1) \in ℝ$
431	60	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i + 1)) \to x \leq Q (i + 1)$
432	322	biimpi	$⊢ Q (i + 1) = x \to x = Q (i + 1)$
433	432	necon3bi	$⊢ \neg x = Q (i + 1) \to Q (i + 1) \neq x$
434	433	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i + 1)) \to Q (i + 1) \neq x$
435	429 430 431 434	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i + 1)) \to x < Q (i + 1)$
436	435	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x < Q (i + 1)$
437	419 420 421 428 436	eliood	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to x \in (Q (i), Q (i + 1))$
438		fvres	$⊢ x \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x) = F (x)$
439	437 438	syl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x) = F (x)$
440		iffalse	$⊢ \neg x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = F (x)$
441	440	eqcomd	$⊢ \neg x = Q (i + 1) \to F (x) = if (x = Q (i + 1), L, F (x))$
442	441	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to F (x) = if (x = Q (i + 1), L, F (x))$
443	418 439 442	3eqtrrd	$⊢ ((((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \land \neg x = Q (i + 1)) \to if (x = Q (i + 1), L, F (x)) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
444	416 443	pm2.61dan	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to if (x = Q (i + 1), L, F (x)) = if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))$
445	444	ifeq2da	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))$
446	445	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, F (x)))) = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))))$
447	319 413 446	3eqtr3d	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ D (x)) = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))))$
448		eqid	$⊢ (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))) = (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x))))$
449	200 448 26 29 9 10 11	cncfiooicc	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ if (x = Q (i), R, if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)))) : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
450	447 449	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ D (x)) : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
451	413 450	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
452	451	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to D : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
453		eqid	$⊢ ℝ D D = ℝ D D$
454	136 13	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D_{ℝ}^{'} : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
455	454	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to D_{ℝ}^{'} : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
456	214	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to \exists y \in ℝ \forall x \in (Q (i), Q (i + 1)) \|D_{ℝ}^{'} (x)\| \leq y$
457		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
458	400 401 412 452 453 455 456 457	fourierdlem39	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to \int_{(Q (i), Q (i + 1))} D (x) \sin r x d x = D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x$
459	411 458	eqtr3d	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to \int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x = D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x$
460	382 383 399 459	syl21anc	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to \int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x = D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x$
461	460	fveq2d	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| = \|D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x\|$
462	461	breq1d	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to (\|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \|D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x\| < \frac{e}{M})$
463	462	ralbidva	$⊢ ((φ \land i \in (0 ..^M)) \land m \in ℕ) \to (\forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \forall r \in (m, +∞) \|D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x\| < \frac{e}{M})$
464	463	rexbidva	$⊢ (φ \land i \in (0 ..^M)) \to (\exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \exists m \in ℕ \forall r \in (m, +∞) \|D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x\| < \frac{e}{M})$
465	464	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to (\exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \exists m \in ℕ \forall r \in (m, +∞) \|D (Q (i + 1)) (- \frac{\cos r Q (i + 1)}{r}) - D (Q (i)) (- \frac{\cos r Q (i)}{r}) - \int_{(Q (i), Q (i + 1))} D_{ℝ}^{'} (x) (- \frac{\cos r x}{r}) d x\| < \frac{e}{M})$
466	381 465	mpbird	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M}$
467	466	an32s	$⊢ ((φ \land e \in ℝ^{+}) \land i \in (0 ..^M)) \to \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M}$
468	102	oveq1d	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x) \sin r x = D (x) \sin r x$
469	468	itgeq2dv	$⊢ (φ \land i \in (0 ..^M)) \to \int_{(Q (i), Q (i + 1))} F (x) \sin r x d x = \int_{(Q (i), Q (i + 1))} D (x) \sin r x d x$
470	469	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to \int_{(Q (i), Q (i + 1))} D (x) \sin r x d x = \int_{(Q (i), Q (i + 1))} F (x) \sin r x d x$
471	470	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to \int_{(Q (i), Q (i + 1))} D (x) \sin r x d x = \int_{(Q (i), Q (i + 1))} F (x) \sin r x d x$
472	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to Q (i) \in ℝ$
473	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to Q (i + 1) \in ℝ$
474	402	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to D (x) \in ℂ$
475	384	recnd	$⊢ r \in (m, +∞) \to r \in ℂ$
476	475	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to r \in ℂ$
477	406	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
478	476 477	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to r x \in ℂ$
479	478	sincld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to \sin r x \in ℂ$
480	474 479	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to D (x) \sin r x \in ℂ$
481	472 473 480	itgioo	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to \int_{(Q (i), Q (i + 1))} D (x) \sin r x d x = \int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x$
482	69	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
483	482 479	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \sin r x \in ℂ$
484	472 473 483	itgioo	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to \int_{(Q (i), Q (i + 1))} F (x) \sin r x d x = \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x$
485	471 481 484	3eqtr3d	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to \int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x = \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x$
486	485	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| = \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
487	486	breq1d	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to (\|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
488	487	ralbidva	$⊢ (φ \land i \in (0 ..^M)) \to (\forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
489	488	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in (0 ..^M)) \to (\forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
490	489	rexbidv	$⊢ ((φ \land e \in ℝ^{+}) \land i \in (0 ..^M)) \to (\exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} D (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
491	467 490	mpbid	$⊢ ((φ \land e \in ℝ^{+}) \land i \in (0 ..^M)) \to \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
492	491	ralrimiva	$⊢ (φ \land e \in ℝ^{+}) \to \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
493	492	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
494		nfv	$⊢ Ⅎ i (φ \land e \in ℝ^{+})$
495		nfra1	$⊢ Ⅎ i \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
496	494 495	nfan	$⊢ Ⅎ i ((φ \land e \in ℝ^{+}) \land \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
497		nfv	$⊢ Ⅎ r (φ \land e \in ℝ^{+})$
498		nfcv	$⊢ \underline{Ⅎ} r (0 ..^M)$
499		nfcv	$⊢ \underline{Ⅎ} r ℕ$
500		nfra1	$⊢ Ⅎ r \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
501	499 500	nfrexw	$⊢ Ⅎ r \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
502	498 501	nfralw	$⊢ Ⅎ r \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
503	497 502	nfan	$⊢ Ⅎ r ((φ \land e \in ℝ^{+}) \land \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
504		nfmpt1	$⊢ \underline{Ⅎ} i (i \in (0 ..^M) ⟼ inf (\{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\} ℝ <))$
505		fzofi	$⊢ (0 ..^M) \in Fin$
506	505	a1i	$⊢ ((φ \land e \in ℝ^{+}) \land \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to (0 ..^M) \in Fin$
507		simpr	$⊢ ((φ \land e \in ℝ^{+}) \land \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
508		eqid	$⊢ \{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\} = \{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\}$
509		eqid	$⊢ (i \in (0 ..^M) ⟼ inf (\{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\} ℝ <)) = (i \in (0 ..^M) ⟼ inf (\{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\} ℝ <))$
510		eqid	$⊢ sup (ran (i \in (0 ..^M) ⟼ inf (\{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\} ℝ <)) ℝ <) = sup (ran (i \in (0 ..^M) ⟼ inf (\{m \in ℕ \| \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}\} ℝ <)) ℝ <)$
511	496 503 504 506 507 508 509 510	fourierdlem31	$⊢ ((φ \land e \in ℝ^{+}) \land \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
512		simpr	$⊢ ((φ \land e \in ℝ^{+}) \land \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
513		nfv	$⊢ Ⅎ n (φ \land e \in ℝ^{+})$
514		nfre1	$⊢ Ⅎ n \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
515	513 514	nfan	$⊢ Ⅎ n ((φ \land e \in ℝ^{+}) \land \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
516		nfv	$⊢ Ⅎ r n \in ℕ$
517		nfra1	$⊢ Ⅎ r \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
518	497 516 517	nf3an	$⊢ Ⅎ r ((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
519		simpll	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to φ$
520		elioore	$⊢ r \in (n, +∞) \to r \in ℝ$
521	520	adantl	$⊢ (n \in ℕ \land r \in (n, +∞)) \to r \in ℝ$
522		0red	$⊢ (n \in ℕ \land r \in (n, +∞)) \to 0 \in ℝ$
523		nnre	$⊢ n \in ℕ \to n \in ℝ$
524	523	adantr	$⊢ (n \in ℕ \land r \in (n, +∞)) \to n \in ℝ$
525		nngt0	$⊢ n \in ℕ \to 0 < n$
526	525	adantr	$⊢ (n \in ℕ \land r \in (n, +∞)) \to 0 < n$
527	524	rexrd	$⊢ (n \in ℕ \land r \in (n, +∞)) \to n \in ℝ^{*}$
528	392	a1i	$⊢ (n \in ℕ \land r \in (n, +∞)) \to +∞ \in ℝ^{*}$
529		simpr	$⊢ (n \in ℕ \land r \in (n, +∞)) \to r \in (n, +∞)$
530		ioogtlb	$⊢ (n \in ℝ^{} \land +∞ \in ℝ^{} \land r \in (n, +∞)) \to n < r$
531	527 528 529 530	syl3anc	$⊢ (n \in ℕ \land r \in (n, +∞)) \to n < r$
532	522 524 521 526 531	lttrd	$⊢ (n \in ℕ \land r \in (n, +∞)) \to 0 < r$
533	521 532	elrpd	$⊢ (n \in ℕ \land r \in (n, +∞)) \to r \in ℝ^{+}$
534	533	adantll	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to r \in ℝ^{+}$
535	1	adantr	$⊢ (φ \land r \in ℝ^{+}) \to A \in ℝ$
536	2	adantr	$⊢ (φ \land r \in ℝ^{+}) \to B \in ℝ$
537	3	ffvelcdmda	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
538	537	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to F (x) \in ℂ$
539	404	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to r \in ℂ$
540	21	sselda	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
541	540	recnd	$⊢ (φ \land x \in [A, B]) \to x \in ℂ$
542	541	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to x \in ℂ$
543	539 542	mulcld	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to r x \in ℂ$
544	543	sincld	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to \sin r x \in ℂ$
545	538 544	mulcld	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to F (x) \sin r x \in ℂ$
546	535 536 545	itgioo	$⊢ (φ \land r \in ℝ^{+}) \to \int_{(A, B)} F (x) \sin r x d x = \int_{[A, B]} F (x) \sin r x d x$
547	6	eqcomd	$⊢ φ \to A = Q (0)$
548	7	eqcomd	$⊢ φ \to B = Q (M)$
549	547 548	oveq12d	$⊢ φ \to [A, B] = [Q (0), Q (M)]$
550	549	adantr	$⊢ (φ \land r \in ℝ^{+}) \to [A, B] = [Q (0), Q (M)]$
551	550	itgeq1d	$⊢ (φ \land r \in ℝ^{+}) \to \int_{[A, B]} F (x) \sin r x d x = \int_{[Q (0), Q (M)]} F (x) \sin r x d x$
552		0zd	$⊢ (φ \land r \in ℝ^{+}) \to 0 \in ℤ$
553		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
554		0p1e1	$⊢ 0 + 1 = 1$
555	554	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
556	553 555	eqtr4i	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
557	4 556	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq (0 + 1)}$
558	557	adantr	$⊢ (φ \land r \in ℝ^{+}) \to M \in ℤ_{\geq (0 + 1)}$
559	22	adantr	$⊢ (φ \land r \in ℝ^{+}) \to Q : (0 \dots M) ⟶ ℝ$
560	8	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
561		simpr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in [Q (0), Q (M)]$
562	549	eqcomd	$⊢ φ \to [Q (0), Q (M)] = [A, B]$
563	562	adantr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to [Q (0), Q (M)] = [A, B]$
564	561 563	eleqtrd	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in [A, B]$
565	564	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [Q (0), Q (M)]) \to x \in [A, B]$
566	565 545	syldan	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [Q (0), Q (M)]) \to F (x) \sin r x \in ℂ$
567	26	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) \in ℝ$
568	29	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
569	114 111	sstrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [A, B]$
570	121 569	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
571	570 9	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
572	571	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
573		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
574	573	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin : ℂ \underset{cn}{⟶} ℂ$
575	185	a1i	$⊢ (φ \land r \in ℝ^{+}) \to (Q (i), Q (i + 1)) \subseteq ℂ$
576	404	adantl	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℂ$
577	189	a1i	$⊢ (φ \land r \in ℝ^{+}) \to ℂ \subseteq ℂ$
578	575 576 577	constcncfg	$⊢ (φ \land r \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ r) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
579	194	adantr	$⊢ (φ \land r \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
580	578 579	mulcncf	$⊢ (φ \land r \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
581	580	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
582	574 581	cncfmpt1f	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ \sin r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
583	572 582	mulcncf	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
584		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ F (x)) = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
585		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ \sin r x) = (x \in (Q (i), Q (i + 1)) ⟼ \sin r x)$
586		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x) = (x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x)$
587	3	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F : [A, B] ⟶ ℂ$
588	45	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to A \in ℝ^{*}$
589	47	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to B \in ℝ^{*}$
590	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [A, B]$
591		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
592	588 589 590 591 80	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in [A, B]$
593	587 592	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x) \in ℂ$
594	593	adantllr	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x) \in ℂ$
595	576	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to r \in ℂ$
596	311	adantl	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in ℂ$
597	595 596	mulcld	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to r x \in ℂ$
598	597	sincld	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to \sin r x \in ℂ$
599	570	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i + 1)$
600	10 599	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i + 1))$
601	600	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to L \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i + 1))$
602		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
603	602	adantr	$⊢ (r \in ℝ^{+} \land x \in (Q (i), Q (i + 1))) \to r \in ℝ$
604	95	adantl	$⊢ (r \in ℝ^{+} \land x \in (Q (i), Q (i + 1))) \to x \in ℝ$
605	603 604	remulcld	$⊢ (r \in ℝ^{+} \land x \in (Q (i), Q (i + 1))) \to r x \in ℝ$
606	605	adantll	$⊢ ((φ \land r \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \to r x \in ℝ$
607	606	ad2ant2r	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land (x \in (Q (i), Q (i + 1)) \land r x \neq r Q (i + 1))) \to r x \in ℝ$
608		recn	$⊢ y \in ℝ \to y \in ℂ$
609	608	sincld	$⊢ y \in ℝ \to \sin y \in ℂ$
610	609	adantl	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land y \in ℝ) \to \sin y \in ℂ$
611		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ r) = (x \in (Q (i), Q (i + 1)) ⟼ r)$
612		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ x) = (x \in (Q (i), Q (i + 1)) ⟼ x)$
613		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ r x) = (x \in (Q (i), Q (i + 1)) ⟼ r x)$
614	185	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
615	576	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ℂ$
616	568	recnd	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
617	611 614 615 616	constlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ((x \in (Q (i), Q (i + 1)) ⟼ r) {lim}_{ℂ} Q (i + 1))$
618	614 612 616	idlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i + 1) \in ((x \in (Q (i), Q (i + 1)) ⟼ x) {lim}_{ℂ} Q (i + 1))$
619	611 612 613 595 596 617 618	mullimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r Q (i + 1) \in ((x \in (Q (i), Q (i + 1)) ⟼ r x) {lim}_{ℂ} Q (i + 1))$
620		eqid	$⊢ (y \in ℂ ⟼ \sin y) = (y \in ℂ ⟼ \sin y)$
621		sinf	$⊢ \sin : ℂ ⟶ ℂ$
622	621	a1i	$⊢ ⊤ \to \sin : ℂ ⟶ ℂ$
623	622	feqmptd	$⊢ ⊤ \to \sin = (y \in ℂ ⟼ \sin y)$
624	623 573	eqeltrrdi	$⊢ ⊤ \to (y \in ℂ ⟼ \sin y) : ℂ \underset{cn}{⟶} ℂ$
625	19	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
626		resincl	$⊢ y \in ℝ \to \sin y \in ℝ$
627	626	adantl	$⊢ (⊤ \land y \in ℝ) \to \sin y \in ℝ$
628	620 624 625 625 627	cncfmptssg	$⊢ ⊤ \to (y \in ℝ ⟼ \sin y) : ℝ \underset{cn}{⟶} ℝ$
629	628	mptru	$⊢ (y \in ℝ ⟼ \sin y) : ℝ \underset{cn}{⟶} ℝ$
630	629	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (y \in ℝ ⟼ \sin y) : ℝ \underset{cn}{⟶} ℝ$
631	602	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ℝ$
632	631 568	remulcld	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r Q (i + 1) \in ℝ$
633		fveq2	$⊢ y = r Q (i + 1) \to \sin y = \sin r Q (i + 1)$
634	630 632 633	cnmptlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin r Q (i + 1) \in ((y \in ℝ ⟼ \sin y) {lim}_{ℂ} r Q (i + 1))$
635		fveq2	$⊢ y = r x \to \sin y = \sin r x$
636		fveq2	$⊢ r x = r Q (i + 1) \to \sin r x = \sin r Q (i + 1)$
637	636	ad2antll	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land (x \in (Q (i), Q (i + 1)) \land r x = r Q (i + 1))) \to \sin r x = \sin r Q (i + 1)$
638	607 610 619 634 635 637	limcco	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin r Q (i + 1) \in ((x \in (Q (i), Q (i + 1)) ⟼ \sin r x) {lim}_{ℂ} Q (i + 1))$
639	584 585 586 594 598 601 638	mullimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to L \sin r Q (i + 1) \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x) {lim}_{ℂ} Q (i + 1))$
640	570	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i)$
641	11 640	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i))$
642	641	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to R \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i))$
643	606	ad2ant2r	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land (x \in (Q (i), Q (i + 1)) \land r x \neq r Q (i))) \to r x \in ℝ$
644	567	recnd	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) \in ℂ$
645	611 614 615 644	constlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ((x \in (Q (i), Q (i + 1)) ⟼ r) {lim}_{ℂ} Q (i))$
646	614 612 644	idlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) \in ((x \in (Q (i), Q (i + 1)) ⟼ x) {lim}_{ℂ} Q (i))$
647	611 612 613 595 596 645 646	mullimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r Q (i) \in ((x \in (Q (i), Q (i + 1)) ⟼ r x) {lim}_{ℂ} Q (i))$
648	631 567	remulcld	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r Q (i) \in ℝ$
649		fveq2	$⊢ y = r Q (i) \to \sin y = \sin r Q (i)$
650	630 648 649	cnmptlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin r Q (i) \in ((y \in ℝ ⟼ \sin y) {lim}_{ℂ} r Q (i))$
651		fveq2	$⊢ r x = r Q (i) \to \sin r x = \sin r Q (i)$
652	651	ad2antll	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land (x \in (Q (i), Q (i + 1)) \land r x = r Q (i))) \to \sin r x = \sin r Q (i)$
653	643 610 647 650 635 652	limcco	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin r Q (i) \in ((x \in (Q (i), Q (i + 1)) ⟼ \sin r x) {lim}_{ℂ} Q (i))$
654	584 585 586 594 598 642 653	mullimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to R \sin r Q (i) \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x) {lim}_{ℂ} Q (i))$
655	567 568 583 639 654	iblcncfioo	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x) \in 𝐿^{1}$
656		simpll	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to (φ \land r \in ℝ^{+})$
657	68	adantllr	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in [A, B]$
658	656 657 545	syl2anc	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \sin r x \in ℂ$
659	567 568 655 658	ibliooicc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ F (x) \sin r x) \in 𝐿^{1}$
660	552 558 559 560 566 659	itgspltprt	$⊢ (φ \land r \in ℝ^{+}) \to \int_{[Q (0), Q (M)]} F (x) \sin r x d x = \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x$
661	546 551 660	3eqtrd	$⊢ (φ \land r \in ℝ^{+}) \to \int_{(A, B)} F (x) \sin r x d x = \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x$
662	519 534 661	syl2anc	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \int_{(A, B)} F (x) \sin r x d x = \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x$
663	505	a1i	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to (0 ..^M) \in Fin$
664	69	adantllr	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
665	520	recnd	$⊢ r \in (n, +∞) \to r \in ℂ$
666	665	adantl	$⊢ (φ \land r \in (n, +∞)) \to r \in ℂ$
667	666	ad2antrr	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to r \in ℂ$
668	406	adantllr	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
669	667 668	mulcld	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to r x \in ℂ$
670	669	sincld	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to \sin r x \in ℂ$
671	664 670	mulcld	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \sin r x \in ℂ$
672	671	adantl3r	$⊢ ((((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \sin r x \in ℂ$
673		simplll	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to φ$
674	534	adantr	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to r \in ℝ^{+}$
675		simpr	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to i \in (0 ..^M)$
676	673 674 675 659	syl21anc	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ F (x) \sin r x) \in 𝐿^{1}$
677	672 676	itgcl	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x \in ℂ$
678	663 677	fsumcl	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x \in ℂ$
679	662 678	eqeltrd	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \int_{(A, B)} F (x) \sin r x d x \in ℂ$
680	679	adantllr	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ) \land r \in (n, +∞)) \to \int_{(A, B)} F (x) \sin r x d x \in ℂ$
681	680	3adantl3	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \int_{(A, B)} F (x) \sin r x d x \in ℂ$
682	681	abscld	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \|\int_{(A, B)} F (x) \sin r x d x\| \in ℝ$
683	677	abscld	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| \in ℝ$
684	663 683	fsumrecl	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| \in ℝ$
685	684	adantllr	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ) \land r \in (n, +∞)) \to \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| \in ℝ$
686	685	3adantl3	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| \in ℝ$
687		rpre	$⊢ e \in ℝ^{+} \to e \in ℝ$
688	687	ad2antlr	$⊢ ((φ \land e \in ℝ^{+}) \land r \in (n, +∞)) \to e \in ℝ$
689	688	3ad2antl1	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to e \in ℝ$
690	662	fveq2d	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \|\int_{(A, B)} F (x) \sin r x d x\| = \|\sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
691	663 677	fsumabs	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \|\sum_{i \in (0 ..^M)} \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| \leq \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
692	690 691	eqbrtrd	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \|\int_{(A, B)} F (x) \sin r x d x\| \leq \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
693	692	adantllr	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ) \land r \in (n, +∞)) \to \|\int_{(A, B)} F (x) \sin r x d x\| \leq \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
694	693	3adantl3	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \|\int_{(A, B)} F (x) \sin r x d x\| \leq \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
695	505	a1i	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to (0 ..^M) \in Fin$
696		0zd	$⊢ φ \to 0 \in ℤ$
697	4	nnzd	$⊢ φ \to M \in ℤ$
698	4	nngt0d	$⊢ φ \to 0 < M$
699		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
700	696 697 698 699	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
701		ne0i	$⊢ 0 \in (0 ..^M) \to (0 ..^M) \neq \emptyset$
702	700 701	syl	$⊢ φ \to (0 ..^M) \neq \emptyset$
703	702	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land r \in (n, +∞)) \to (0 ..^M) \neq \emptyset$
704	703	3ad2antl1	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to (0 ..^M) \neq \emptyset$
705		simp1l	$⊢ ((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to φ$
706	705	ad2antrr	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to φ$
707		simpll2	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to n \in ℕ$
708	706 707	jca	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to (φ \land n \in ℕ)$
709		simplr	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to r \in (n, +∞)$
710		simpr	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to j \in (0 ..^M)$
711		eleq1w	$⊢ i = j \to (i \in (0 ..^M) \leftrightarrow j \in (0 ..^M))$
712	711	anbi2d	$⊢ i = j \to ((((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \leftrightarrow (((φ \land n \in ℕ) \land r \in (n, +∞)) \land j \in (0 ..^M)))$
713		fveq2	$⊢ i = j \to Q (i) = Q (j)$
714		oveq1	$⊢ i = j \to i + 1 = j + 1$
715	714	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
716	713 715	oveq12d	$⊢ i = j \to [Q (i), Q (i + 1)] = [Q (j), Q (j + 1)]$
717	716	itgeq1d	$⊢ i = j \to \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x = \int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x$
718	717	eleq1d	$⊢ i = j \to (\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x \in ℂ \leftrightarrow \int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x \in ℂ)$
719	712 718	imbi12d	$⊢ i = j \to (((((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x \in ℂ) \leftrightarrow ((((φ \land n \in ℕ) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x \in ℂ))$
720	719 677	chvarvv	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x \in ℂ$
721	708 709 710 720	syl21anc	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x \in ℂ$
722	721	abscld	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| \in ℝ$
723	352	rpred	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{M} \in ℝ$
724	723	3ad2ant1	$⊢ ((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \frac{e}{M} \in ℝ$
725	724	ad2antrr	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \frac{e}{M} \in ℝ$
726		simpll3	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
727		rspa	$⊢ (\forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \land r \in (n, +∞)) \to \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
728	727	adantr	$⊢ ((\forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
729	717	fveq2d	$⊢ i = j \to \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| = \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\|$
730	729	breq1d	$⊢ i = j \to (\|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M})$
731	730	cbvralvw	$⊢ \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \leftrightarrow \forall j \in (0 ..^M) \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
732	728 731	sylib	$⊢ ((\forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \forall j \in (0 ..^M) \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
733		rspa	$⊢ (\forall j \in (0 ..^M) \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \land j \in (0 ..^M)) \to \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
734	732 733	sylancom	$⊢ ((\forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
735	726 709 710 734	syl21anc	$⊢ ((((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \land j \in (0 ..^M)) \to \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
736	695 704 722 725 735	fsumlt	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \sum_{j \in (0 ..^M)} \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| < \sum_{j \in (0 ..^M)} (\frac{e}{M})$
737		fveq2	$⊢ j = i \to Q (j) = Q (i)$
738		oveq1	$⊢ j = i \to j + 1 = i + 1$
739	738	fveq2d	$⊢ j = i \to Q (j + 1) = Q (i + 1)$
740	737 739	oveq12d	$⊢ j = i \to [Q (j), Q (j + 1)] = [Q (i), Q (i + 1)]$
741	740	itgeq1d	$⊢ j = i \to \int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x = \int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x$
742	741	fveq2d	$⊢ j = i \to \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| = \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
743	742	cbvsumv	$⊢ \sum_{j \in (0 ..^M)} \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| = \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
744	743	a1i	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \sum_{j \in (0 ..^M)} \|\int_{[Q (j), Q (j + 1)]} F (x) \sin r x d x\| = \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\|$
745	352	rpcnd	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{M} \in ℂ$
746		fsumconst	$⊢ ((0 ..^M) \in Fin \land \frac{e}{M} \in ℂ) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = \|(0 ..^M)\| (\frac{e}{M})$
747	505 745 746	sylancr	$⊢ (φ \land e \in ℝ^{+}) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = \|(0 ..^M)\| (\frac{e}{M})$
748	4	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
749		hashfzo0	$⊢ M \in ℕ_{0} \to \|(0 ..^M)\| = M$
750	748 749	syl	$⊢ φ \to \|(0 ..^M)\| = M$
751	750	oveq1d	$⊢ φ \to \|(0 ..^M)\| (\frac{e}{M}) = M (\frac{e}{M})$
752	751	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \|(0 ..^M)\| (\frac{e}{M}) = M (\frac{e}{M})$
753	349	rpcnd	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℂ$
754	351	rpcnd	$⊢ (φ \land e \in ℝ^{+}) \to M \in ℂ$
755	351	rpne0d	$⊢ (φ \land e \in ℝ^{+}) \to M \neq 0$
756	753 754 755	divcan2d	$⊢ (φ \land e \in ℝ^{+}) \to M (\frac{e}{M}) = e$
757	747 752 756	3eqtrd	$⊢ (φ \land e \in ℝ^{+}) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = e$
758	757	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land r \in (n, +∞)) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = e$
759	758	3ad2antl1	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = e$
760	736 744 759	3brtr3d	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \sum_{i \in (0 ..^M)} \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < e$
761	682 686 689 694 760	lelttrd	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \land r \in (n, +∞)) \to \|\int_{(A, B)} F (x) \sin r x d x\| < e$
762	761	ex	$⊢ ((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to (r \in (n, +∞) \to \|\int_{(A, B)} F (x) \sin r x d x\| < e)$
763	518 762	ralrimi	$⊢ ((φ \land e \in ℝ^{+}) \land n \in ℕ \land \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e$
764	763	3exp	$⊢ (φ \land e \in ℝ^{+}) \to (n \in ℕ \to (\forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \to \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e))$
765	764	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to (n \in ℕ \to (\forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \to \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e))$
766	515 765	reximdai	$⊢ ((φ \land e \in ℝ^{+}) \land \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to (\exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \to \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e)$
767	512 766	mpd	$⊢ ((φ \land e \in ℝ^{+}) \land \exists n \in ℕ \forall r \in (n, +∞) \forall i \in (0 ..^M) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e$
768	511 767	syldan	$⊢ ((φ \land e \in ℝ^{+}) \land \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}) \to \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e$
769	768	ex	$⊢ (φ \land e \in ℝ^{+}) \to (\forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \to \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e)$
770	769	ralimdva	$⊢ φ \to (\forall e \in ℝ^{+} \forall i \in (0 ..^M) \exists m \in ℕ \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M} \to \forall e \in ℝ^{+} \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e)$
771	493 770	mpd	$⊢ φ \to \forall e \in ℝ^{+} \exists n \in ℕ \forall r \in (n, +∞) \|\int_{(A, B)} F (x) \sin r x d x\| < e$

Metamath Proof Explorer

Theorem fourierdlem73

Proof