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	bilanri	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to Q (i + 1) = x$
324	321 323	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to Q (i) < x$
325	320 324	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to x \neq Q (i)$
326	325	neneqd	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to \neg x = Q (i)$
327	326	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))$
328		iftrue	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = L$
329	328	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land x = Q (i + 1)) \to if (x = Q (i + 1), L, F (x)) = L$
330	327 329	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$
331	29	leidd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \leq Q (i + 1)$
332	26 29 29 143 331	eliccd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [Q (i), Q (i + 1)]$
333	319 330 332 10	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) = L$
334	333 35	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) \in ℂ$
335	334	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to D (Q (i + 1)) \in ℂ$
336		eqid	$⊢ \|D (Q (i + 1))\| = \|D (Q (i + 1))\|$
337		iftrue	$⊢ x = Q (i) \to if (x = Q (i), R, if (x = Q (i + 1), L, F (x))) = R$
338	337	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$
339	26	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
340	29	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
341		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)]$
342	339 340 143 341	syl3anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [Q (i), Q (i + 1)]$
343	319 338 342 11	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) = R$
344	343 32	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) \in ℂ$
345	344	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to D (Q (i)) \in ℂ$
346		eqid	$⊢ \|D (Q (i))\| = \|D (Q (i))\|$
347		eqid	$⊢ \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x = \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x$
348		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
349	4	nnrpd	$⊢ φ \to M \in ℝ^{+}$
350	349	adantr	$⊢ (φ \land e \in ℝ^{+}) \to M \in ℝ^{+}$
351	348 350	rpdivcld	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{M} \in ℝ^{+}$
352	351	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \to \frac{e}{M} \in ℝ^{+}$
353		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to r \in ℂ$
354	29	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
355	354	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to Q (i + 1) \in ℂ$
356	353 355	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to r Q (i + 1) \in ℂ$
357	356	coscld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to \cos r Q (i + 1) \in ℂ$
358	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to Q (i + 1) \in ℝ$
359	187 358	remulcld	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to r Q (i + 1) \in ℝ$
360		abscosbd	$⊢ r Q (i + 1) \in ℝ \to \|\cos r Q (i + 1)\| \leq 1$
361	359 360	syl	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \|\cos r Q (i + 1)\| \leq 1$
362	361	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℝ) \to \|\cos r Q (i + 1)\| \leq 1$
363	26	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
364	363	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to Q (i) \in ℂ$
365	353 364	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to r Q (i) \in ℂ$
366	365	coscld	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℂ) \to \cos r Q (i) \in ℂ$
367	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to Q (i) \in ℝ$
368	187 367	remulcld	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to r Q (i) \in ℝ$
369		abscosbd	$⊢ r Q (i) \in ℝ \to \|\cos r Q (i)\| \leq 1$
370	368 369	syl	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ) \to \|\cos r Q (i)\| \leq 1$
371	370	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land e \in ℝ^{+}) \land r \in ℝ) \to \|\cos r Q (i)\| \leq 1$
372		fveq2	$⊢ z = x \to D_{ℝ}^{'} (z) = D_{ℝ}^{'} (x)$
373	372	fveq2d	$⊢ z = x \to \|D_{ℝ}^{'} (z)\| = \|D_{ℝ}^{'} (x)\|$
374	373	cbvitgv	$⊢ \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (z)\| d z = \int_{(Q (i), Q (i + 1))} \|D_{ℝ}^{'} (x)\| d x$
375	374	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$
376	375	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}}$
377	376	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$
378	377	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⌋$
379	378	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$
380	178 308 309 314 318 335 336 345 346 347 352 357 362 366 371 379	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}$
381		simplll	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to φ$
382		simpllr	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to i \in (0 ..^M)$
383		elioore	$⊢ r \in (m, +∞) \to r \in ℝ$
384	383	adantl	$⊢ (m \in ℕ \land r \in (m, +∞)) \to r \in ℝ$
385		0red	$⊢ (m \in ℕ \land r \in (m, +∞)) \to 0 \in ℝ$
386		nnre	$⊢ m \in ℕ \to m \in ℝ$
387	386	adantr	$⊢ (m \in ℕ \land r \in (m, +∞)) \to m \in ℝ$
388		nngt0	$⊢ m \in ℕ \to 0 < m$
389	388	adantr	$⊢ (m \in ℕ \land r \in (m, +∞)) \to 0 < m$
390	387	rexrd	$⊢ (m \in ℕ \land r \in (m, +∞)) \to m \in ℝ^{*}$
391		pnfxr	$⊢ +∞ \in ℝ^{*}$
392	391	a1i	$⊢ (m \in ℕ \land r \in (m, +∞)) \to +∞ \in ℝ^{*}$
393		simpr	$⊢ (m \in ℕ \land r \in (m, +∞)) \to r \in (m, +∞)$
394		ioogtlb	$⊢ (m \in ℝ^{} \land +∞ \in ℝ^{} \land r \in (m, +∞)) \to m < r$
395	390 392 393 394	syl3anc	$⊢ (m \in ℕ \land r \in (m, +∞)) \to m < r$
396	385 387 384 389 395	lttrd	$⊢ (m \in ℕ \land r \in (m, +∞)) \to 0 < r$
397	384 396	elrpd	$⊢ (m \in ℕ \land r \in (m, +∞)) \to r \in ℝ^{+}$
398	397	adantll	$⊢ (((φ \land i \in (0 ..^M)) \land m \in ℕ) \land r \in (m, +∞)) \to r \in ℝ^{+}$
399	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to Q (i) \in ℝ$
400	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to Q (i + 1) \in ℝ$
401	72	ffvelcdmda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to D (x) \in ℂ$
402	401	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to D (x) \in ℂ$
403		rpcn	$⊢ r \in ℝ^{+} \to r \in ℂ$
404	403	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to r \in ℂ$
405	44	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
406	405	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
407	404 406	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to r x \in ℂ$
408	407	sincld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to \sin r x \in ℂ$
409	402 408	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \land x \in [Q (i), Q (i + 1)]) \to D (x) \sin r x \in ℂ$
410	399 400 409	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$
411	143	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to Q (i) \leq Q (i + 1)$
412	72	feqmptd	$⊢ (φ \land i \in (0 ..^M)) \to D = (x \in [Q (i), Q (i + 1)] ⟼ D (x))$
413		iftrue	$⊢ x = Q (i + 1) \to if (x = Q (i + 1), L, ({F ↾}_{(Q (i), Q (i + 1))}) (x)) = L$
414	328 413	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))$
415	414	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))$
416		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)$
417	416	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)$
418	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 ℝ^{*}$
419	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 ℝ^{*}$
420	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 ℝ$
421	26	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) \in ℝ$
422	44	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \in ℝ$
423	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$
424		neqne	$⊢ \neg x = Q (i) \to x \neq Q (i)$
425	424	adantl	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to x \neq Q (i)$
426	421 422 423 425	leneltd	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i)) \to Q (i) < x$
427	426	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$
428	44	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \land \neg x = Q (i + 1)) \to x \in ℝ$
429	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 ℝ$
430	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)$
431	322	biimpi	$⊢ Q (i + 1) = x \to x = Q (i + 1)$
432	431	necon3bi	$⊢ \neg x = Q (i + 1) \to Q (i + 1) \neq x$
433	432	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$
434	428 429 430 433	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)$
435	434	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)$
436	418 419 420 427 435	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))$
437		fvres	$⊢ x \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (x) = F (x)$
438	436 437	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)$
439		iffalse	$⊢ \neg x = Q (i + 1) \to if (x = Q (i + 1), L, F (x)) = F (x)$
440	439	eqcomd	$⊢ \neg x = Q (i + 1) \to F (x) = if (x = Q (i + 1), L, F (x))$
441	440	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))$
442	417 438 441	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))$
443	415 442	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))$
444	443	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)))$
445	444	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))))$
446	319 412 445	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))))$
447		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))))$
448	200 447 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}{⟶} ℂ$
449	446 448	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ D (x)) : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
450	412 449	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
451	450	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to D : [Q (i), Q (i + 1)] \underset{cn}{⟶} ℂ$
452		eqid	$⊢ ℝ D D = ℝ D D$
453	136 13	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to D_{ℝ}^{'} : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
454	453	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to D_{ℝ}^{'} : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
455	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$
456		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
457	399 400 411 451 452 454 455 456	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$
458	410 457	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$
459	381 382 398 458	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$
460	459	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\|$
461	460	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})$
462	461	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})$
463	462	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})$
464	463	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})$
465	380 464	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}$
466	465	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}$
467	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$
468	467	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$
469	468	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$
470	469	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$
471	26	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to Q (i) \in ℝ$
472	29	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \to Q (i + 1) \in ℝ$
473	401	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to D (x) \in ℂ$
474	383	recnd	$⊢ r \in (m, +∞) \to r \in ℂ$
475	474	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to r \in ℂ$
476	405	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
477	475 476	mulcld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to r x \in ℂ$
478	477	sincld	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to \sin r x \in ℂ$
479	473 478	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 ℂ$
480	471 472 479	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$
481	69	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land r \in (m, +∞)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
482	481 478	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 ℂ$
483	471 472 482	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$
484	470 480 483	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$
485	484	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\|$
486	485	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})$
487	486	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})$
488	487	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})$
489	488	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})$
490	466 489	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}$
491	490	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}$
492	491	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}$
493		nfv	$⊢ Ⅎ i (φ \land e \in ℝ^{+})$
494		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}$
495	493 494	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})$
496		nfv	$⊢ Ⅎ r (φ \land e \in ℝ^{+})$
497		nfcv	$⊢ \underline{Ⅎ} r (0 ..^M)$
498		nfcv	$⊢ \underline{Ⅎ} r ℕ$
499		nfra1	$⊢ Ⅎ r \forall r \in (m, +∞) \|\int_{[Q (i), Q (i + 1)]} F (x) \sin r x d x\| < \frac{e}{M}$
500	498 499	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}$
501	497 500	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}$
502	496 501	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})$
503		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}\} ℝ <))$
504		fzofi	$⊢ (0 ..^M) \in Fin$
505	504	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$
506		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}$
507		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}\}$
508		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}\} ℝ <))$
509		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}\} ℝ <)) ℝ <)$
510	495 502 503 505 506 507 508 509	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}$
511		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}$
512		nfv	$⊢ Ⅎ n (φ \land e \in ℝ^{+})$
513		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}$
514	512 513	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})$
515		nfv	$⊢ Ⅎ r n \in ℕ$
516		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}$
517	496 515 516	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})$
518		simpll	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to φ$
519		elioore	$⊢ r \in (n, +∞) \to r \in ℝ$
520	519	adantl	$⊢ (n \in ℕ \land r \in (n, +∞)) \to r \in ℝ$
521		0red	$⊢ (n \in ℕ \land r \in (n, +∞)) \to 0 \in ℝ$
522		nnre	$⊢ n \in ℕ \to n \in ℝ$
523	522	adantr	$⊢ (n \in ℕ \land r \in (n, +∞)) \to n \in ℝ$
524		nngt0	$⊢ n \in ℕ \to 0 < n$
525	524	adantr	$⊢ (n \in ℕ \land r \in (n, +∞)) \to 0 < n$
526	523	rexrd	$⊢ (n \in ℕ \land r \in (n, +∞)) \to n \in ℝ^{*}$
527	391	a1i	$⊢ (n \in ℕ \land r \in (n, +∞)) \to +∞ \in ℝ^{*}$
528		simpr	$⊢ (n \in ℕ \land r \in (n, +∞)) \to r \in (n, +∞)$
529		ioogtlb	$⊢ (n \in ℝ^{} \land +∞ \in ℝ^{} \land r \in (n, +∞)) \to n < r$
530	526 527 528 529	syl3anc	$⊢ (n \in ℕ \land r \in (n, +∞)) \to n < r$
531	521 523 520 525 530	lttrd	$⊢ (n \in ℕ \land r \in (n, +∞)) \to 0 < r$
532	520 531	elrpd	$⊢ (n \in ℕ \land r \in (n, +∞)) \to r \in ℝ^{+}$
533	532	adantll	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to r \in ℝ^{+}$
534	1	adantr	$⊢ (φ \land r \in ℝ^{+}) \to A \in ℝ$
535	2	adantr	$⊢ (φ \land r \in ℝ^{+}) \to B \in ℝ$
536	3	ffvelcdmda	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
537	536	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to F (x) \in ℂ$
538	403	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to r \in ℂ$
539	21	sselda	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
540	539	recnd	$⊢ (φ \land x \in [A, B]) \to x \in ℂ$
541	540	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to x \in ℂ$
542	538 541	mulcld	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to r x \in ℂ$
543	542	sincld	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to \sin r x \in ℂ$
544	537 543	mulcld	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [A, B]) \to F (x) \sin r x \in ℂ$
545	534 535 544	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$
546	6	eqcomd	$⊢ φ \to A = Q (0)$
547	7	eqcomd	$⊢ φ \to B = Q (M)$
548	546 547	oveq12d	$⊢ φ \to [A, B] = [Q (0), Q (M)]$
549	548	adantr	$⊢ (φ \land r \in ℝ^{+}) \to [A, B] = [Q (0), Q (M)]$
550	549	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$
551		0zd	$⊢ (φ \land r \in ℝ^{+}) \to 0 \in ℤ$
552		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
553		0p1e1	$⊢ 0 + 1 = 1$
554	553	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
555	552 554	eqtr4i	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
556	4 555	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq (0 + 1)}$
557	556	adantr	$⊢ (φ \land r \in ℝ^{+}) \to M \in ℤ_{\geq (0 + 1)}$
558	22	adantr	$⊢ (φ \land r \in ℝ^{+}) \to Q : (0 \dots M) ⟶ ℝ$
559	8	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
560		simpr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in [Q (0), Q (M)]$
561	548	eqcomd	$⊢ φ \to [Q (0), Q (M)] = [A, B]$
562	561	adantr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to [Q (0), Q (M)] = [A, B]$
563	560 562	eleqtrd	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in [A, B]$
564	563	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [Q (0), Q (M)]) \to x \in [A, B]$
565	564 544	syldan	$⊢ ((φ \land r \in ℝ^{+}) \land x \in [Q (0), Q (M)]) \to F (x) \sin r x \in ℂ$
566	26	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) \in ℝ$
567	29	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
568	114 111	sstrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [A, B]$
569	121 568	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
570	569 9	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
571	570	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}{⟶} ℂ$
572		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
573	572	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin : ℂ \underset{cn}{⟶} ℂ$
574	185	a1i	$⊢ (φ \land r \in ℝ^{+}) \to (Q (i), Q (i + 1)) \subseteq ℂ$
575	403	adantl	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℂ$
576	189	a1i	$⊢ (φ \land r \in ℝ^{+}) \to ℂ \subseteq ℂ$
577	574 575 576	constcncfg	$⊢ (φ \land r \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ r) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
578	194	adantr	$⊢ (φ \land r \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
579	577 578	mulcncf	$⊢ (φ \land r \in ℝ^{+}) \to (x \in (Q (i), Q (i + 1)) ⟼ r x) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
580	579	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}{⟶} ℂ$
581	573 580	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}{⟶} ℂ$
582	571 581	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}{⟶} ℂ$
583		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ F (x)) = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
584		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ \sin r x) = (x \in (Q (i), Q (i + 1)) ⟼ \sin r x)$
585		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)$
586	3	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F : [A, B] ⟶ ℂ$
587	45	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to A \in ℝ^{*}$
588	47	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to B \in ℝ^{*}$
589	5	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [A, B]$
590		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
591	587 588 589 590 80	fourierdlem1	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in [A, B]$
592	586 591	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x) \in ℂ$
593	592	adantllr	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to F (x) \in ℂ$
594	575	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to r \in ℂ$
595	311	adantl	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in ℂ$
596	594 595	mulcld	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to r x \in ℂ$
597	596	sincld	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to \sin r x \in ℂ$
598	569	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)$
599	10 598	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i + 1))$
600	599	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))$
601		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
602	601	adantr	$⊢ (r \in ℝ^{+} \land x \in (Q (i), Q (i + 1))) \to r \in ℝ$
603	95	adantl	$⊢ (r \in ℝ^{+} \land x \in (Q (i), Q (i + 1))) \to x \in ℝ$
604	602 603	remulcld	$⊢ (r \in ℝ^{+} \land x \in (Q (i), Q (i + 1))) \to r x \in ℝ$
605	604	adantll	$⊢ ((φ \land r \in ℝ^{+}) \land x \in (Q (i), Q (i + 1))) \to r x \in ℝ$
606	605	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 ℝ$
607		recn	$⊢ y \in ℝ \to y \in ℂ$
608	607	sincld	$⊢ y \in ℝ \to \sin y \in ℂ$
609	608	adantl	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land y \in ℝ) \to \sin y \in ℂ$
610		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ r) = (x \in (Q (i), Q (i + 1)) ⟼ r)$
611		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ x) = (x \in (Q (i), Q (i + 1)) ⟼ x)$
612		eqid	$⊢ (x \in (Q (i), Q (i + 1)) ⟼ r x) = (x \in (Q (i), Q (i + 1)) ⟼ r x)$
613	185	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
614	575	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ℂ$
615	567	recnd	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
616	610 613 614 615	constlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ((x \in (Q (i), Q (i + 1)) ⟼ r) {lim}_{ℂ} Q (i + 1))$
617	613 611 615	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))$
618	610 611 612 594 595 616 617	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))$
619		eqid	$⊢ (y \in ℂ ⟼ \sin y) = (y \in ℂ ⟼ \sin y)$
620		sinf	$⊢ \sin : ℂ ⟶ ℂ$
621	620	a1i	$⊢ ⊤ \to \sin : ℂ ⟶ ℂ$
622	621	feqmptd	$⊢ ⊤ \to \sin = (y \in ℂ ⟼ \sin y)$
623	622 572	eqeltrrdi	$⊢ ⊤ \to (y \in ℂ ⟼ \sin y) : ℂ \underset{cn}{⟶} ℂ$
624	19	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
625		resincl	$⊢ y \in ℝ \to \sin y \in ℝ$
626	625	adantl	$⊢ (⊤ \land y \in ℝ) \to \sin y \in ℝ$
627	619 623 624 624 626	cncfmptssg	$⊢ ⊤ \to (y \in ℝ ⟼ \sin y) : ℝ \underset{cn}{⟶} ℝ$
628	627	mptru	$⊢ (y \in ℝ ⟼ \sin y) : ℝ \underset{cn}{⟶} ℝ$
629	628	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (y \in ℝ ⟼ \sin y) : ℝ \underset{cn}{⟶} ℝ$
630	601	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ℝ$
631	630 567	remulcld	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r Q (i + 1) \in ℝ$
632		fveq2	$⊢ y = r Q (i + 1) \to \sin y = \sin r Q (i + 1)$
633	629 631 632	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))$
634		fveq2	$⊢ y = r x \to \sin y = \sin r x$
635		fveq2	$⊢ r x = r Q (i + 1) \to \sin r x = \sin r Q (i + 1)$
636	635	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)$
637	606 609 618 633 634 636	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))$
638	583 584 585 593 597 600 637	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))$
639	569	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)$
640	11 639	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i))$
641	640	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to R \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i))$
642	605	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 ℝ$
643	566	recnd	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) \in ℂ$
644	610 613 614 643	constlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r \in ((x \in (Q (i), Q (i + 1)) ⟼ r) {lim}_{ℂ} Q (i))$
645	613 611 643	idlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to Q (i) \in ((x \in (Q (i), Q (i + 1)) ⟼ x) {lim}_{ℂ} Q (i))$
646	610 611 612 594 595 644 645	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))$
647	630 566	remulcld	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to r Q (i) \in ℝ$
648		fveq2	$⊢ y = r Q (i) \to \sin y = \sin r Q (i)$
649	629 647 648	cnmptlimc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to \sin r Q (i) \in ((y \in ℝ ⟼ \sin y) {lim}_{ℂ} r Q (i))$
650		fveq2	$⊢ r x = r Q (i) \to \sin r x = \sin r Q (i)$
651	650	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)$
652	642 609 646 649 634 651	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))$
653	583 584 585 593 597 641 652	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))$
654	566 567 582 638 653	iblcncfioo	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x) \sin r x) \in 𝐿^{1}$
655		simpll	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to (φ \land r \in ℝ^{+})$
656	68	adantllr	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in [A, B]$
657	655 656 544	syl2anc	$⊢ (((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \sin r x \in ℂ$
658	566 567 654 657	ibliooicc	$⊢ ((φ \land r \in ℝ^{+}) \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ F (x) \sin r x) \in 𝐿^{1}$
659	551 557 558 559 565 658	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$
660	545 550 659	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$
661	518 533 660	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$
662	504	a1i	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to (0 ..^M) \in Fin$
663	69	adantllr	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
664	519	recnd	$⊢ r \in (n, +∞) \to r \in ℂ$
665	664	adantl	$⊢ (φ \land r \in (n, +∞)) \to r \in ℂ$
666	665	ad2antrr	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to r \in ℂ$
667	405	adantllr	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in ℂ$
668	666 667	mulcld	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to r x \in ℂ$
669	668	sincld	$⊢ (((φ \land r \in (n, +∞)) \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to \sin r x \in ℂ$
670	663 669	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 ℂ$
671	670	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 ℂ$
672		simplll	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to φ$
673	533	adantr	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to r \in ℝ^{+}$
674		simpr	$⊢ (((φ \land n \in ℕ) \land r \in (n, +∞)) \land i \in (0 ..^M)) \to i \in (0 ..^M)$
675	672 673 674 658	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}$
676	671 675	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 ℂ$
677	662 676	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 ℂ$
678	661 677	eqeltrd	$⊢ ((φ \land n \in ℕ) \land r \in (n, +∞)) \to \int_{(A, B)} F (x) \sin r x d x \in ℂ$
679	678	adantllr	$⊢ (((φ \land e \in ℝ^{+}) \land n \in ℕ) \land r \in (n, +∞)) \to \int_{(A, B)} F (x) \sin r x d x \in ℂ$
680	679	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 ℂ$
681	680	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 ℝ$
682	676	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 ℝ$
683	662 682	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 ℝ$
684	683	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 ℝ$
685	684	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 ℝ$
686		rpre	$⊢ e \in ℝ^{+} \to e \in ℝ$
687	686	ad2antlr	$⊢ ((φ \land e \in ℝ^{+}) \land r \in (n, +∞)) \to e \in ℝ$
688	687	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 ℝ$
689	661	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\|$
690	662 676	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\|$
691	689 690	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\|$
692	691	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\|$
693	692	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\|$
694	504	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$
695		0zd	$⊢ φ \to 0 \in ℤ$
696	4	nnzd	$⊢ φ \to M \in ℤ$
697	4	nngt0d	$⊢ φ \to 0 < M$
698		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
699	695 696 697 698	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
700		ne0i	$⊢ 0 \in (0 ..^M) \to (0 ..^M) \neq \emptyset$
701	699 700	syl	$⊢ φ \to (0 ..^M) \neq \emptyset$
702	701	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land r \in (n, +∞)) \to (0 ..^M) \neq \emptyset$
703	702	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$
704		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 φ$
705	704	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 φ$
706		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 ℕ$
707	705 706	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 ℕ)$
708		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, +∞)$
709		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)$
710		eleq1w	$⊢ i = j \to (i \in (0 ..^M) \leftrightarrow j \in (0 ..^M))$
711	710	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)))$
712		fveq2	$⊢ i = j \to Q (i) = Q (j)$
713		oveq1	$⊢ i = j \to i + 1 = j + 1$
714	713	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
715	712 714	oveq12d	$⊢ i = j \to [Q (i), Q (i + 1)] = [Q (j), Q (j + 1)]$
716	715	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$
717	716	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 ℂ)$
718	711 717	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 ℂ))$
719	718 676	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 ℂ$
720	707 708 709 719	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 ℂ$
721	720	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 ℝ$
722	351	rpred	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{M} \in ℝ$
723	722	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 ℝ$
724	723	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 ℝ$
725		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}$
726		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}$
727	726	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}$
728	716	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\|$
729	728	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})$
730	729	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}$
731	727 730	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}$
732		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}$
733	731 732	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}$
734	725 708 709 733	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}$
735	694 703 721 724 734	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})$
736		fveq2	$⊢ j = i \to Q (j) = Q (i)$
737		oveq1	$⊢ j = i \to j + 1 = i + 1$
738	737	fveq2d	$⊢ j = i \to Q (j + 1) = Q (i + 1)$
739	736 738	oveq12d	$⊢ j = i \to [Q (j), Q (j + 1)] = [Q (i), Q (i + 1)]$
740	739	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$
741	740	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\|$
742	741	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\|$
743	742	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\|$
744	351	rpcnd	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{M} \in ℂ$
745		fsumconst	$⊢ ((0 ..^M) \in Fin \land \frac{e}{M} \in ℂ) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = \|(0 ..^M)\| (\frac{e}{M})$
746	504 744 745	sylancr	$⊢ (φ \land e \in ℝ^{+}) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = \|(0 ..^M)\| (\frac{e}{M})$
747	4	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
748		hashfzo0	$⊢ M \in ℕ_{0} \to \|(0 ..^M)\| = M$
749	747 748	syl	$⊢ φ \to \|(0 ..^M)\| = M$
750	749	oveq1d	$⊢ φ \to \|(0 ..^M)\| (\frac{e}{M}) = M (\frac{e}{M})$
751	750	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \|(0 ..^M)\| (\frac{e}{M}) = M (\frac{e}{M})$
752	348	rpcnd	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℂ$
753	350	rpcnd	$⊢ (φ \land e \in ℝ^{+}) \to M \in ℂ$
754	350	rpne0d	$⊢ (φ \land e \in ℝ^{+}) \to M \neq 0$
755	752 753 754	divcan2d	$⊢ (φ \land e \in ℝ^{+}) \to M (\frac{e}{M}) = e$
756	746 751 755	3eqtrd	$⊢ (φ \land e \in ℝ^{+}) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = e$
757	756	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land r \in (n, +∞)) \to \sum_{j \in (0 ..^M)} (\frac{e}{M}) = e$
758	757	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$
759	735 743 758	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$
760	681 685 688 693 759	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$
761	760	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)$
762	517 761	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$
763	762	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))$
764	763	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))$
765	514 764	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)$
766	511 765	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$
767	510 766	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$
768	767	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)$
769	768	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)$
770	492 769	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