Theorem fourierdlem22

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

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem22.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem22.c	⊢ 𝐶 = ( - π (,) π )
3		fourierdlem22.fibl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ 𝐿1 )
4		fourierdlem22.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
5		fourierdlem22.b	⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐹 : ℝ ⟶ ℝ )
7		ioossre	⊢ ( - π (,) π ) ⊆ ℝ
8		id	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶 )
9	8 2	eleqtrdi	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ( - π (,) π ) )
10	7 9	sselid	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℝ )
12	6 11	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
13	12	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
14		nn0re	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
15	14	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → 𝑛 ∈ ℝ )
16	10	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℝ )
17	15 16	remulcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑛 · 𝑥 ) ∈ ℝ )
18	17	recoscld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
19	18	adantll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
20	13 19	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ℝ )
21		ioombl	⊢ ( - π (,) π ) ∈ dom vol
22	2 21	eqeltri	⊢ 𝐶 ∈ dom vol
23	22	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ dom vol )
24		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
25		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
26	23 19 13 24 25	offval2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( cos ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) )
27	19	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℂ )
28	13	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
29	27 28	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( cos ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
30	29	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( cos ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) )
31	26 30	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) = ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
32		coscn	⊢ cos ∈ ( ℂ –cn→ ℂ )
33	32	a1i	⊢ ( 𝑛 ∈ ℕ0 → cos ∈ ( ℂ –cn→ ℂ ) )
34	2 7	eqsstri	⊢ 𝐶 ⊆ ℝ
35		ax-resscn	⊢ ℝ ⊆ ℂ
36	34 35	sstri	⊢ 𝐶 ⊆ ℂ
37	36	a1i	⊢ ( 𝑛 ∈ ℕ0 → 𝐶 ⊆ ℂ )
38	14	recnd	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
39		ssid	⊢ ℂ ⊆ ℂ
40	39	a1i	⊢ ( 𝑛 ∈ ℕ0 → ℂ ⊆ ℂ )
41	37 38 40	constcncfg	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ 𝑛 ) ∈ ( 𝐶 –cn→ ℂ ) )
42		cncfmptid	⊢ ( ( 𝐶 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ ) )
43	36 39 42	mp2an	⊢ ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ )
44	43	a1i	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ ) )
45	41 44	mulcncf	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐶 –cn→ ℂ ) )
46	33 45	cncfmpt1f	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) )
47		cnmbf	⊢ ( ( 𝐶 ∈ dom vol ∧ ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
48	22 46 47	sylancr	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
49	48	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
50	1	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
51	50	reseq1d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) )
52		resmpt	⊢ ( 𝐶 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
53	34 52	mp1i	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
54	51 53	eqtr2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ↾ 𝐶 ) )
55	54 3	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
57		1re	⊢ 1 ∈ ℝ
58		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
59		nfv	⊢ Ⅎ 𝑥 𝑛 ∈ ℕ0
60		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) )
61	60	nfdm	⊢ Ⅎ 𝑥 dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) )
62	61	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) )
63	59 62	nfan	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
64	18	ex	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
65	64	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝐶 → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
66	63 65	ralrimi	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐶 ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
67		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐶 ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ → dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
68	66 67	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
69	58 68	eleqtrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ 𝐶 )
70		eqidd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
71		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑦 ) )
72	71	fveq2d	⊢ ( 𝑥 = 𝑦 → ( cos ‘ ( 𝑛 · 𝑥 ) ) = ( cos ‘ ( 𝑛 · 𝑦 ) ) )
73	72	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 = 𝑦 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) = ( cos ‘ ( 𝑛 · 𝑦 ) ) )
74		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
75	14	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑛 ∈ ℝ )
76	34 74	sselid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ℝ )
77	75 76	remulcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑛 · 𝑦 ) ∈ ℝ )
78	77	recoscld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑦 ) ) ∈ ℝ )
79	70 73 74 78	fvmptd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) = ( cos ‘ ( 𝑛 · 𝑦 ) ) )
80	79	fveq2d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( cos ‘ ( 𝑛 · 𝑦 ) ) ) )
81		abscosbd	⊢ ( ( 𝑛 · 𝑦 ) ∈ ℝ → ( abs ‘ ( cos ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
82	77 81	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( cos ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
83	80 82	eqbrtrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
84	69 83	syldan	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
85	84	ralrimiva	⊢ ( 𝑛 ∈ ℕ0 → ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
86		breq2	⊢ ( 𝑏 = 1 → ( ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
87	86	ralbidv	⊢ ( 𝑏 = 1 → ( ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
88	87	rspcev	⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
89	57 85 88	sylancr	⊢ ( 𝑛 ∈ ℕ0 → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
90	89	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
91		bddmulibl	⊢ ( ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
92	49 56 90 91	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
93	31 92	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) ∈ 𝐿1 )
94	20 93	itgrecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
95		pire	⊢ π ∈ ℝ
96	95	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → π ∈ ℝ )
97		0re	⊢ 0 ∈ ℝ
98		pipos	⊢ 0 < π
99	97 98	gtneii	⊢ π ≠ 0
100	99	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → π ≠ 0 )
101	94 96 100	redivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ∈ ℝ )
102	101 4	fmptd	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℝ )
103	102	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℝ )
104	103	ex	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 → ( 𝐴 ‘ 𝑛 ) ∈ ℝ ) )
105		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
106	17	resincld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
107	106	adantll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
108	13 107	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ℝ )
109		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
110	23 107 13 109 25	offval2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( sin ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) )
111	107	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℂ )
112	111 28	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( sin ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
113	112	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( sin ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) )
114	110 113	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) = ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
115		sincn	⊢ sin ∈ ( ℂ –cn→ ℂ )
116	115	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → sin ∈ ( ℂ –cn→ ℂ ) )
117	45	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐶 –cn→ ℂ ) )
118	116 117	cncfmpt1f	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) )
119		cnmbf	⊢ ( ( 𝐶 ∈ dom vol ∧ ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
120	22 118 119	sylancr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
121		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
122		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) )
123	122	nfdm	⊢ Ⅎ 𝑥 dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) )
124	123	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) )
125	59 124	nfan	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
126	106	ex	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
127	126	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝐶 → ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
128	125 127	ralrimi	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐶 ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
129		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐶 ( sin ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ → dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
130	128 129	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
131	121 130	eleqtrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ 𝐶 )
132		eqidd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) )
133	71	fveq2d	⊢ ( 𝑥 = 𝑦 → ( sin ‘ ( 𝑛 · 𝑥 ) ) = ( sin ‘ ( 𝑛 · 𝑦 ) ) )
134	133	adantl	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 = 𝑦 ) → ( sin ‘ ( 𝑛 · 𝑥 ) ) = ( sin ‘ ( 𝑛 · 𝑦 ) ) )
135	77	resincld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( sin ‘ ( 𝑛 · 𝑦 ) ) ∈ ℝ )
136	132 134 74 135	fvmptd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) = ( sin ‘ ( 𝑛 · 𝑦 ) ) )
137	136	fveq2d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( sin ‘ ( 𝑛 · 𝑦 ) ) ) )
138		abssinbd	⊢ ( ( 𝑛 · 𝑦 ) ∈ ℝ → ( abs ‘ ( sin ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
139	77 138	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( sin ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
140	137 139	eqbrtrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
141	131 140	syldan	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
142	141	ralrimiva	⊢ ( 𝑛 ∈ ℕ0 → ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
143		breq2	⊢ ( 𝑏 = 1 → ( ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
144	143	ralbidv	⊢ ( 𝑏 = 1 → ( ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
145	144	rspcev	⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
146	57 142 145	sylancr	⊢ ( 𝑛 ∈ ℕ0 → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
147	146	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
148		bddmulibl	⊢ ( ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
149	120 56 147 148	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
150	114 149	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) ) ∈ 𝐿1 )
151	108 150	itgrecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
152	105 151	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
153	95	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℝ )
154	99	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ≠ 0 )
155	152 153 154	redivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ∈ ℝ )
156	155 5	fmptd	⊢ ( 𝜑 → 𝐵 : ℕ ⟶ ℝ )
157	156	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 ‘ 𝑛 ) ∈ ℝ )
158	157	ex	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ → ( 𝐵 ‘ 𝑛 ) ∈ ℝ ) )
159	104 158	jca	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 → ( 𝐴 ‘ 𝑛 ) ∈ ℝ ) ∧ ( 𝑛 ∈ ℕ → ( 𝐵 ‘ 𝑛 ) ∈ ℝ ) ) )