Theorem fourierdlem16

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

	Ref	Expression
Hypotheses	fourierdlem16.f	|- ( ph -> F : RR --> RR )
	fourierdlem16.c	|- C = ( -u _pi (,) _pi )
	fourierdlem16.fibl	|- ( ph -> ( F |` C ) e. L^1 )
	fourierdlem16.a	|- A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
	fourierdlem16.n	|- ( ph -> N e. NN0 )
Assertion	fourierdlem16	|- ( ph -> ( ( ( A ` N ) e. RR /\ ( x e. C |-> ( F ` x ) ) e. L^1 ) /\ S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem16.f	|- ( ph -> F : RR --> RR )
2		fourierdlem16.c	|- C = ( -u _pi (,) _pi )
3		fourierdlem16.fibl	|- ( ph -> ( F |` C ) e. L^1 )
4		fourierdlem16.a	|- A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
5		fourierdlem16.n	|- ( ph -> N e. NN0 )
6	1	adantr	|- ( ( ph /\ x e. C ) -> F : RR --> RR )
7		ioossre	|- ( -u _pi (,) _pi ) C_ RR
8		id	|- ( x e. C -> x e. C )
9	8 2	eleqtrdi	|- ( x e. C -> x e. ( -u _pi (,) _pi ) )
10	7 9	sselid	|- ( x e. C -> x e. RR )
11	10	adantl	|- ( ( ph /\ x e. C ) -> x e. RR )
12	6 11	ffvelrnd	|- ( ( ph /\ x e. C ) -> ( F ` x ) e. RR )
13	12	adantlr	|- ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( F ` x ) e. RR )
14		nn0re	|- ( n e. NN0 -> n e. RR )
15	14	adantr	|- ( ( n e. NN0 /\ x e. C ) -> n e. RR )
16	10	adantl	|- ( ( n e. NN0 /\ x e. C ) -> x e. RR )
17	15 16	remulcld	|- ( ( n e. NN0 /\ x e. C ) -> ( n x. x ) e. RR )
18	17	recoscld	|- ( ( n e. NN0 /\ x e. C ) -> ( cos ` ( n x. x ) ) e. RR )
19	18	adantll	|- ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( cos ` ( n x. x ) ) e. RR )
20	13 19	remulcld	|- ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) e. RR )
21		ioombl	|- ( -u _pi (,) _pi ) e. dom vol
22	2 21	eqeltri	|- C e. dom vol
23	22	a1i	|- ( ( ph /\ n e. NN0 ) -> C e. dom vol )
24		eqidd	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) = ( x e. C |-> ( cos ` ( n x. x ) ) ) )
25		eqidd	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> ( F ` x ) ) )
26	23 19 13 24 25	offval2	|- ( ( ph /\ n e. NN0 ) -> ( ( x e. C |-> ( cos ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) = ( x e. C |-> ( ( cos ` ( n x. x ) ) x. ( F ` x ) ) ) )
27	19	recnd	|- ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( cos ` ( n x. x ) ) e. CC )
28	13	recnd	|- ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( F ` x ) e. CC )
29	27 28	mulcomd	|- ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( ( cos ` ( n x. x ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) )
30	29	mpteq2dva	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( ( cos ` ( n x. x ) ) x. ( F ` x ) ) ) = ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) )
31	26 30	eqtr2d	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) = ( ( x e. C |-> ( cos ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) )
32		coscn	|- cos e. ( CC -cn-> CC )
33	32	a1i	|- ( n e. NN0 -> cos e. ( CC -cn-> CC ) )
34	2 7	eqsstri	|- C C_ RR
35		ax-resscn	|- RR C_ CC
36	34 35	sstri	|- C C_ CC
37	36	a1i	|- ( n e. NN0 -> C C_ CC )
38	14	recnd	|- ( n e. NN0 -> n e. CC )
39		ssid	|- CC C_ CC
40	39	a1i	|- ( n e. NN0 -> CC C_ CC )
41	37 38 40	constcncfg	|- ( n e. NN0 -> ( x e. C |-> n ) e. ( C -cn-> CC ) )
42		cncfmptid	|- ( ( C C_ CC /\ CC C_ CC ) -> ( x e. C |-> x ) e. ( C -cn-> CC ) )
43	36 39 42	mp2an	|- ( x e. C |-> x ) e. ( C -cn-> CC )
44	43	a1i	|- ( n e. NN0 -> ( x e. C |-> x ) e. ( C -cn-> CC ) )
45	41 44	mulcncf	|- ( n e. NN0 -> ( x e. C |-> ( n x. x ) ) e. ( C -cn-> CC ) )
46	33 45	cncfmpt1f	|- ( n e. NN0 -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. ( C -cn-> CC ) )
47		cnmbf	|- ( ( C e. dom vol /\ ( x e. C |-> ( cos ` ( n x. x ) ) ) e. ( C -cn-> CC ) ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. MblFn )
48	22 46 47	sylancr	|- ( n e. NN0 -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. MblFn )
49	48	adantl	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. MblFn )
50	1	feqmptd	|- ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
51	50	reseq1d	|- ( ph -> ( F |` C ) = ( ( x e. RR |-> ( F ` x ) ) |` C ) )
52		resmpt	|- ( C C_ RR -> ( ( x e. RR |-> ( F ` x ) ) |` C ) = ( x e. C |-> ( F ` x ) ) )
53	34 52	mp1i	|- ( ph -> ( ( x e. RR |-> ( F ` x ) ) |` C ) = ( x e. C |-> ( F ` x ) ) )
54	51 53	eqtr2d	|- ( ph -> ( x e. C |-> ( F ` x ) ) = ( F |` C ) )
55	54 3	eqeltrd	|- ( ph -> ( x e. C |-> ( F ` x ) ) e. L^1 )
56	55	adantr	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( F ` x ) ) e. L^1 )
57		1re	|- 1 e. RR
58		simpr	|- ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) )
59		nfv	|- F/ x n e. NN0
60		nfmpt1	|- F/_ x ( x e. C |-> ( cos ` ( n x. x ) ) )
61	60	nfdm	|- F/_ x dom ( x e. C |-> ( cos ` ( n x. x ) ) )
62	61	nfcri	|- F/ x y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) )
63	59 62	nfan	|- F/ x ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) )
64	18	ex	|- ( n e. NN0 -> ( x e. C -> ( cos ` ( n x. x ) ) e. RR ) )
65	64	adantr	|- ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> ( x e. C -> ( cos ` ( n x. x ) ) e. RR ) )
66	63 65	ralrimi	|- ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> A. x e. C ( cos ` ( n x. x ) ) e. RR )
67		dmmptg	|- ( A. x e. C ( cos ` ( n x. x ) ) e. RR -> dom ( x e. C |-> ( cos ` ( n x. x ) ) ) = C )
68	66 67	syl	|- ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> dom ( x e. C |-> ( cos ` ( n x. x ) ) ) = C )
69	58 68	eleqtrd	|- ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> y e. C )
70		eqidd	|- ( ( n e. NN0 /\ y e. C ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) = ( x e. C |-> ( cos ` ( n x. x ) ) ) )
71		oveq2	|- ( x = y -> ( n x. x ) = ( n x. y ) )
72	71	fveq2d	|- ( x = y -> ( cos ` ( n x. x ) ) = ( cos ` ( n x. y ) ) )
73	72	adantl	|- ( ( ( n e. NN0 /\ y e. C ) /\ x = y ) -> ( cos ` ( n x. x ) ) = ( cos ` ( n x. y ) ) )
74		simpr	|- ( ( n e. NN0 /\ y e. C ) -> y e. C )
75	14	adantr	|- ( ( n e. NN0 /\ y e. C ) -> n e. RR )
76	34 74	sselid	|- ( ( n e. NN0 /\ y e. C ) -> y e. RR )
77	75 76	remulcld	|- ( ( n e. NN0 /\ y e. C ) -> ( n x. y ) e. RR )
78	77	recoscld	|- ( ( n e. NN0 /\ y e. C ) -> ( cos ` ( n x. y ) ) e. RR )
79	70 73 74 78	fvmptd	|- ( ( n e. NN0 /\ y e. C ) -> ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) = ( cos ` ( n x. y ) ) )
80	79	fveq2d	|- ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) = ( abs ` ( cos ` ( n x. y ) ) ) )
81		abscosbd	|- ( ( n x. y ) e. RR -> ( abs ` ( cos ` ( n x. y ) ) ) <_ 1 )
82	77 81	syl	|- ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( cos ` ( n x. y ) ) ) <_ 1 )
83	80 82	eqbrtrd	|- ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 )
84	69 83	syldan	|- ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 )
85	84	ralrimiva	|- ( n e. NN0 -> A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 )
86		breq2	|- ( b = 1 -> ( ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b <-> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 ) )
87	86	ralbidv	|- ( b = 1 -> ( A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b <-> A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 ) )
88	87	rspcev	|- ( ( 1 e. RR /\ A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 ) -> E. b e. RR A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b )
89	57 85 88	sylancr	|- ( n e. NN0 -> E. b e. RR A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b )
90	89	adantl	|- ( ( ph /\ n e. NN0 ) -> E. b e. RR A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b )
91		bddmulibl	|- ( ( ( x e. C |-> ( cos ` ( n x. x ) ) ) e. MblFn /\ ( x e. C |-> ( F ` x ) ) e. L^1 /\ E. b e. RR A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b ) -> ( ( x e. C |-> ( cos ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
92	49 56 90 91	syl3anc	|- ( ( ph /\ n e. NN0 ) -> ( ( x e. C |-> ( cos ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
93	31 92	eqeltrd	|- ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) e. L^1 )
94	20 93	itgrecl	|- ( ( ph /\ n e. NN0 ) -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x e. RR )
95		pire	|- _pi e. RR
96	95	a1i	|- ( ( ph /\ n e. NN0 ) -> _pi e. RR )
97		0re	|- 0 e. RR
98		pipos	|- 0 < _pi
99	97 98	gtneii	|- _pi =/= 0
100	99	a1i	|- ( ( ph /\ n e. NN0 ) -> _pi =/= 0 )
101	94 96 100	redivcld	|- ( ( ph /\ n e. NN0 ) -> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) e. RR )
102	101 4	fmptd	|- ( ph -> A : NN0 --> RR )
103	102 5	ffvelrnd	|- ( ph -> ( A ` N ) e. RR )
104	5	ancli	|- ( ph -> ( ph /\ N e. NN0 ) )
105		eleq1	|- ( n = N -> ( n e. NN0 <-> N e. NN0 ) )
106	105	anbi2d	|- ( n = N -> ( ( ph /\ n e. NN0 ) <-> ( ph /\ N e. NN0 ) ) )
107		simpl	|- ( ( n = N /\ x e. C ) -> n = N )
108	107	oveq1d	|- ( ( n = N /\ x e. C ) -> ( n x. x ) = ( N x. x ) )
109	108	fveq2d	|- ( ( n = N /\ x e. C ) -> ( cos ` ( n x. x ) ) = ( cos ` ( N x. x ) ) )
110	109	oveq2d	|- ( ( n = N /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) )
111	110	itgeq2dv	|- ( n = N -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x = S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x )
112	111	eleq1d	|- ( n = N -> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x e. RR <-> S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR ) )
113	106 112	imbi12d	|- ( n = N -> ( ( ( ph /\ n e. NN0 ) -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x e. RR ) <-> ( ( ph /\ N e. NN0 ) -> S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR ) ) )
114	113 94	vtoclg	|- ( N e. NN0 -> ( ( ph /\ N e. NN0 ) -> S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR ) )
115	5 104 114	sylc	|- ( ph -> S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR )
116	103 55 115	jca31	|- ( ph -> ( ( ( A ` N ) e. RR /\ ( x e. C |-> ( F ` x ) ) e. L^1 ) /\ S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR ) )