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