Theorem fourierdlem21

Description: The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem21.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem21.c	⊢ 𝐶 = ( - π (,) π )
	fourierdlem21.fibl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ 𝐿1 )
	fourierdlem21.b	⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
	fourierdlem21.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	fourierdlem21	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 ) ∧ ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem21.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem21.c	⊢ 𝐶 = ( - π (,) π )
3		fourierdlem21.fibl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ 𝐿1 )
4		fourierdlem21.b	⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
5		fourierdlem21.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐹 : ℝ ⟶ ℝ )
8		ioossre	⊢ ( - π (,) π ) ⊆ ℝ
9		id	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶 )
10	9 2	eleqtrdi	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ( - π (,) π ) )
11	8 10	sselid	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℝ )
13	7 12	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
14	13	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
15		nn0re	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
16	15	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → 𝑛 ∈ ℝ )
17	11	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℝ )
18	16 17	remulcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑛 · 𝑥 ) ∈ ℝ )
19	18	resincld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
20	19	adantll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
21	14 20	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ℝ )
22		ioombl	⊢ ( - π (,) π ) ∈ dom vol
23	2 22	eqeltri	⊢ 𝐶 ∈ dom vol
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ dom vol )
25		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
26		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
27	24 20 14 25 26	offval2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( sin ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) )
28	20	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℂ )
29	14	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
30	28 29	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( sin ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
31	30	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( sin ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) )
32	27 31	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) = ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
33		sincn	⊢ sin ∈ ( ℂ –cn→ ℂ )
34	33	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → sin ∈ ( ℂ –cn→ ℂ ) )
35	2 8	eqsstri	⊢ 𝐶 ⊆ ℝ
36		ax-resscn	⊢ ℝ ⊆ ℂ
37	35 36	sstri	⊢ 𝐶 ⊆ ℂ
38	37	a1i	⊢ ( 𝑛 ∈ ℕ0 → 𝐶 ⊆ ℂ )
39	15	recnd	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
40		ssid	⊢ ℂ ⊆ ℂ
41	40	a1i	⊢ ( 𝑛 ∈ ℕ0 → ℂ ⊆ ℂ )
42	38 39 41	constcncfg	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ 𝑛 ) ∈ ( 𝐶 –cn→ ℂ ) )
43	38 41	idcncfg	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ ) )
44	42 43	mulcncf	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐶 –cn→ ℂ ) )
45	44	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐶 –cn→ ℂ ) )
46	34 45	cncfmpt1f	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) )
47		cnmbf	⊢ ( ( 𝐶 ∈ dom vol ∧ ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
48	23 46 47	sylancr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
49	1	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
50	49	reseq1d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) )
51		resmpt	⊢ ( 𝐶 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
52	35 51	mp1i	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
53	50 52	eqtr2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ↾ 𝐶 ) )
54	53 3	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
55	54	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
56		1re	⊢ 1 ∈ ℝ
57		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
58		nfv	⊢ Ⅎ 𝑥 𝑛 ∈ ℕ0
59		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) )
60	59	nfdm	⊢ Ⅎ 𝑥 dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) )
61	60	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) )
62	58 61	nfan	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
63	19	ex	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
64	63	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝐶 → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
65	62 64	ralrimi	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐶 ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
66		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐶 ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ → dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
67	65 66	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
68	57 67	eleqtrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ 𝐶 )
69		eqidd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
70		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑦 ) )
71	70	fveq2d	⊢ ( 𝑥 = 𝑦 → ( sin ‘ ( 𝑛 · 𝑥 ) ) = ( sin ‘ ( 𝑛 · 𝑦 ) ) )
72	71	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 = 𝑦 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) = ( sin ‘ ( 𝑛 · 𝑦 ) ) )
73		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
74	15	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑛 ∈ ℝ )
75	35 73	sselid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ℝ )
76	74 75	remulcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑛 · 𝑦 ) ∈ ℝ )
77	76	resincld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑦 ) ) ∈ ℝ )
78	69 72 73 77	fvmptd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) = ( sin ‘ ( 𝑛 · 𝑦 ) ) )
79	78	fveq2d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( sin ‘ ( 𝑛 · 𝑦 ) ) ) )
80		abssinbd	⊢ ( ( 𝑛 · 𝑦 ) ∈ ℝ → ( abs ‘ ( sin ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
81	76 80	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( sin ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
82	79 81	eqbrtrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
83	68 82	syldan	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
84	83	ralrimiva	⊢ ( 𝑛 ∈ ℕ0 → ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
85		breq2	⊢ ( 𝑏 = 1 → ( ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
86	85	ralbidv	⊢ ( 𝑏 = 1 → ( ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
87	86	rspcev	⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
88	56 84 87	sylancr	⊢ ( 𝑛 ∈ ℕ0 → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
89	88	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
90		bddmulibl	⊢ ( ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
91	48 55 89 90	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
92	32 91	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) ∈ 𝐿1 )
93	21 92	itgrecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
94	6 93	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
95		pire	⊢ π ∈ ℝ
96	95	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℝ )
97		0re	⊢ 0 ∈ ℝ
98		pipos	⊢ 0 < π
99	97 98	gtneii	⊢ π ≠ 0
100	99	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ≠ 0 )
101	94 96 100	redivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ∈ ℝ )
102	101 4	fmptd	⊢ ( 𝜑 → 𝐵 : ℕ ⟶ ℝ )
103	102 5	ffvelcdmd	⊢ ( 𝜑 → ( 𝐵 ‘ 𝑁 ) ∈ ℝ )
104	5	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
105		eleq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
106	105	anbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ↔ ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) ) )
107		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → 𝑛 = 𝑁 )
108	107	oveq1d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑛 · 𝑥 ) = ( 𝑁 · 𝑥 ) )
109	108	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) = ( sin ‘ ( 𝑁 · 𝑥 ) ) )
110	109	oveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
111	110	mpteq2dva	⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) )
112	111	eleq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 ) )
113	106 112	imbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) ∈ 𝐿1 ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 ) ) )
114	113 92	vtoclg	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 ) )
115	114	anabsi7	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
116	104 115	mpdan	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
117	5	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝑁 ∈ ℕ ) )
118		eleq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ℕ ↔ 𝑁 ∈ ℕ ) )
119	118	anbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑁 ∈ ℕ ) ) )
120	110	itgeq2dv	⊢ ( 𝑛 = 𝑁 → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 = ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
121	120	eleq1d	⊢ ( 𝑛 = 𝑁 → ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ↔ ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )
122	119 121	imbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) ) )
123	122 94	vtoclg	⊢ ( 𝑁 ∈ ℕ → ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )
124	5 117 123	sylc	⊢ ( 𝜑 → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
125	103 116 124	jca31	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 ) ∧ ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )