Theorem fourierdlem68 38150

Description: The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem68.f	|- ( ph -> F : RR --> RR )
fourierdlem68.xre	|- ( ph -> X e. RR )
fourierdlem68.a	|- ( ph -> A e. RR )
fourierdlem68.b	|- ( ph -> B e. RR )
fourierdlem68.altb	|- ( ph -> A < B )
fourierdlem68.ab	|- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )
fourierdlem68.n0	|- ( ph -> -. 0 e. ( A [,] B ) )
fourierdlem68.fdv	|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
fourierdlem68.d	|- ( ph -> D e. RR )
fourierdlem68.fbd	|- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D )
fourierdlem68.e	|- ( ph -> E e. RR )
fourierdlem68.fdvbd	|- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E )
fourierdlem68.c	|- ( ph -> C e. RR )
fourierdlem68.o	|- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )

Assertion

Ref	Expression
fourierdlem68	|- ( ph -> ( dom ( RR _D O ) = ( A (,) B ) /\ E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) )

Distinct variable groups:   A, b, s   t, A, s   B, b, s   t, B   C, b, s   D, b, s   t, D   E, b, s   t, E   F, b, s   t, F   X, b, s   t, X   ph, b, s   ph, t

Allowed substitution hints:   C( t)   O( t, s, b)

Proof of Theorem fourierdlem68

Dummy variable c is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem68.f	. . . . . 6 |- ( ph -> F : RR --> RR )
2		fourierdlem68.xre	. . . . . 6 |- ( ph -> X e. RR )
3		fourierdlem68.a	. . . . . 6 |- ( ph -> A e. RR )
4		fourierdlem68.b	. . . . . 6 |- ( ph -> B e. RR )
5		fourierdlem68.fdv	. . . . . 6 |- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
6		ioossicc 11745	. . . . . . 7 |- ( A (,) B ) C_ ( A [,] B )
7		fourierdlem68.ab	. . . . . . 7 |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )
8	6, 7	syl5ss 3429	. . . . . 6 |- ( ph -> ( A (,) B ) C_ ( -u pi [,] pi ) )
9		fourierdlem68.n0	. . . . . . 7 |- ( ph -> -. 0 e. ( A [,] B ) )
10	6	sseli 3414	. . . . . . 7 |- ( 0 e. ( A (,) B ) -> 0 e. ( A [,] B ) )
11	9, 10	nsyl 125	. . . . . 6 |- ( ph -> -. 0 e. ( A (,) B ) )
12		fourierdlem68.c	. . . . . 6 |- ( ph -> C e. RR )
13		fourierdlem68.o	. . . . . 6 |- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
14	1, 2, 3, 4, 5, 8, 11, 12, 13	fourierdlem57 38139	. . . . 5 |- ( ( ph -> ( ( RR _D O ) : ( A (,) B ) --> RR /\ ( RR _D O ) = ( s e. ( A (,) B ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) ) /\ ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
15	14	simpli 465	. . . 4 |- ( ph -> ( ( RR _D O ) : ( A (,) B ) --> RR /\ ( RR _D O ) = ( s e. ( A (,) B ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) )
16	15	simpld 466	. . 3 |- ( ph -> ( RR _D O ) : ( A (,) B ) --> RR )
17		fdm 5745	. . 3 |- ( ( RR _D O ) : ( A (,) B ) --> RR -> dom ( RR _D O ) = ( A (,) B ) )
18	16, 17	syl 17	. 2 |- ( ph -> dom ( RR _D O ) = ( A (,) B ) )
19		eqid 2471	. . . . . 6 |- ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) = ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) )
20		fourierdlem68.altb	. . . . . . 7 |- ( ph -> A < B )
21	3, 4, 20	ltled 9800	. . . . . 6 |- ( ph -> A <_ B )
22		2re 10701	. . . . . . . . . . 11 |- 2 e. RR
23	22	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ t e. ( A [,] B ) ) -> 2 e. RR )
24	3, 4	iccssred 37698	. . . . . . . . . . . . 13 |- ( ph -> ( A [,] B ) C_ RR )
25	24	sselda 3418	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( A [,] B ) ) -> t e. RR )
26	25	rehalfcld 10882	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( t / 2 ) e. RR )
27	26	resincld 14274	. . . . . . . . . 10 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( sin ` ( t / 2 ) ) e. RR )
28	23, 27	remulcld 9689	. . . . . . . . 9 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( t / 2 ) ) ) e. RR )
29		2cnd 10704	. . . . . . . . . 10 |- ( ( ph /\ t e. ( A [,] B ) ) -> 2 e. CC )
30	27	recnd 9687	. . . . . . . . . 10 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( sin ` ( t / 2 ) ) e. CC )
31		2ne0 10724	. . . . . . . . . . 11 |- 2 =/= 0
32	31	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ t e. ( A [,] B ) ) -> 2 =/= 0 )
33	7	sselda 3418	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( A [,] B ) ) -> t e. ( -u pi [,] pi ) )
34		eqcom 2478	. . . . . . . . . . . . . . . . 17 |- ( t = 0 <-> 0 = t )
35	34	biimpi 199	. . . . . . . . . . . . . . . 16 |- ( t = 0 -> 0 = t )
36	35	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( t e. ( A [,] B ) /\ t = 0 ) -> 0 = t )
37		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( t e. ( A [,] B ) /\ t = 0 ) -> t e. ( A [,] B ) )
38	36, 37	eqeltrd 2549	. . . . . . . . . . . . . 14 |- ( ( t e. ( A [,] B ) /\ t = 0 ) -> 0 e. ( A [,] B ) )
39	38	adantll 728	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. ( A [,] B ) ) /\ t = 0 ) -> 0 e. ( A [,] B ) )
40	9	ad2antrr 740	. . . . . . . . . . . . 13 |- ( ( ( ph /\ t e. ( A [,] B ) ) /\ t = 0 ) -> -. 0 e. ( A [,] B ) )
41	39, 40	pm2.65da 586	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( A [,] B ) ) -> -. t = 0 )
42	41	neqned 2650	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( A [,] B ) ) -> t =/= 0 )
43		fourierdlem44 38127	. . . . . . . . . . 11 |- ( ( t e. ( -u pi [,] pi ) /\ t =/= 0 ) -> ( sin ` ( t / 2 ) ) =/= 0 )
44	33, 42, 43	syl2anc 673	. . . . . . . . . 10 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( sin ` ( t / 2 ) ) =/= 0 )
45	29, 30, 32, 44	mulne0d 10286	. . . . . . . . 9 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( t / 2 ) ) ) =/= 0 )
46		eldifsn 4088	. . . . . . . . 9 |- ( ( 2 x. ( sin ` ( t / 2 ) ) ) e. ( RR \ { 0 } ) <-> ( ( 2 x. ( sin ` ( t / 2 ) ) ) e. RR /\ ( 2 x. ( sin ` ( t / 2 ) ) ) =/= 0 ) )
47	28, 45, 46	sylanbrc 677	. . . . . . . 8 |- ( ( ph /\ t e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( t / 2 ) ) ) e. ( RR \ { 0 } ) )
48	47, 19	fmptd 6061	. . . . . . 7 |- ( ph -> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) : ( A [,] B ) --> ( RR \ { 0 } ) )
49		difss 3549	. . . . . . . . . 10 |- ( RR \ { 0 } ) C_ RR
50		ax-resscn 9614	. . . . . . . . . 10 |- RR C_ CC
51	49, 50	sstri 3427	. . . . . . . . 9 |- ( RR \ { 0 } ) C_ CC
52	51	a1i 11	. . . . . . . 8 |- ( ph -> ( RR \ { 0 } ) C_ CC )
53	24, 50	syl6ss 3430	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) C_ CC )
54		2cnd 10704	. . . . . . . . . 10 |- ( ph -> 2 e. CC )
55		ssid 3437	. . . . . . . . . . 11 |- CC C_ CC
56	55	a1i 11	. . . . . . . . . 10 |- ( ph -> CC C_ CC )
57	53, 54, 56	constcncfg 37845	. . . . . . . . 9 |- ( ph -> ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> CC ) )
58		sincn 23478	. . . . . . . . . . 11 |- sin e. ( CC -cn-> CC )
59	58	a1i 11	. . . . . . . . . 10 |- ( ph -> sin e. ( CC -cn-> CC ) )
60	53, 56	idcncfg 37846	. . . . . . . . . . 11 |- ( ph -> ( t e. ( A [,] B ) |-> t ) e. ( ( A [,] B ) -cn-> CC ) )
61		eldifsn 4088	. . . . . . . . . . . . . 14 |- ( 2 e. ( CC \ { 0 } ) <-> ( 2 e. CC /\ 2 =/= 0 ) )
62	29, 32, 61	sylanbrc 677	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( A [,] B ) ) -> 2 e. ( CC \ { 0 } ) )
63		eqid 2471	. . . . . . . . . . . . 13 |- ( t e. ( A [,] B ) |-> 2 ) = ( t e. ( A [,] B ) |-> 2 )
64	62, 63	fmptd 6061	. . . . . . . . . . . 12 |- ( ph -> ( t e. ( A [,] B ) |-> 2 ) : ( A [,] B ) --> ( CC \ { 0 } ) )
65		difssd 3550	. . . . . . . . . . . . 13 |- ( ph -> ( CC \ { 0 } ) C_ CC )
66		cncffvrn 22008	. . . . . . . . . . . . 13 |- ( ( ( CC \ { 0 } ) C_ CC /\ ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> 2 ) : ( A [,] B ) --> ( CC \ { 0 } ) ) )
67	65, 57, 66	syl2anc 673	. . . . . . . . . . . 12 |- ( ph -> ( ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> 2 ) : ( A [,] B ) --> ( CC \ { 0 } ) ) )
68	64, 67	mpbird 240	. . . . . . . . . . 11 |- ( ph -> ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) )
69	60, 68	divcncf 37858	. . . . . . . . . 10 |- ( ph -> ( t e. ( A [,] B ) |-> ( t / 2 ) ) e. ( ( A [,] B ) -cn-> CC ) )
70	59, 69	cncfmpt1f 22023	. . . . . . . . 9 |- ( ph -> ( t e. ( A [,] B ) |-> ( sin ` ( t / 2 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
71	57, 70	mulcncf 22476	. . . . . . . 8 |- ( ph -> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
72		cncffvrn 22008	. . . . . . . 8 |- ( ( ( RR \ { 0 } ) C_ CC /\ ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) : ( A [,] B ) --> ( RR \ { 0 } ) ) )
73	52, 71, 72	syl2anc 673	. . . . . . 7 |- ( ph -> ( ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) : ( A [,] B ) --> ( RR \ { 0 } ) ) )
74	48, 73	mpbird 240	. . . . . 6 |- ( ph -> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) )
75	19, 3, 4, 21, 74	cncficcgt0 37863	. . . . 5 |- ( ph -> E. c e. RR+ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) )
76		reelprrecn 9649	. . . . . . . 8 |- RR e. { RR , CC }
77	76	a1i 11	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> RR e. { RR , CC } )
78	1	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
79	2	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
80		elioore 11691	. . . . . . . . . . . . 13 |- ( s e. ( A (,) B ) -> s e. RR )
81	80	adantl 473	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
82	79, 81	readdcld 9688	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
83	78, 82	ffvelrnd 6038	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
84	12	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> C e. RR )
85	83, 84	resubcld 10068	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. RR )
86	85	recnd 9687	. . . . . . . 8 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
87	86	3ad2antl1 1192	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
88	76	a1i 11	. . . . . . . . . 10 |- ( ph -> RR e. { RR , CC } )
89	83	recnd 9687	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
90	5	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
91	2, 3	readdcld 9688	. . . . . . . . . . . . . 14 |- ( ph -> ( X + A ) e. RR )
92	91	rexrd 9708	. . . . . . . . . . . . 13 |- ( ph -> ( X + A ) e. RR* )
93	92	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) e. RR* )
94	2, 4	readdcld 9688	. . . . . . . . . . . . . 14 |- ( ph -> ( X + B ) e. RR )
95	94	rexrd 9708	. . . . . . . . . . . . 13 |- ( ph -> ( X + B ) e. RR* )
96	95	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) e. RR* )
97	3	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
98	97	rexrd 9708	. . . . . . . . . . . . . 14 |- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
99	4	rexrd 9708	. . . . . . . . . . . . . . 15 |- ( ph -> B e. RR* )
100	99	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
101		simpr 468	. . . . . . . . . . . . . 14 |- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
102		ioogtlb 37688	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
103	98, 100, 101, 102	syl3anc 1292	. . . . . . . . . . . . 13 |- ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
104	97, 81, 79, 103	ltadd2dd 9811	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
105	4	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
106		iooltub 37706	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
107	98, 100, 101, 106	syl3anc 1292	. . . . . . . . . . . . 13 |- ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
108	81, 105, 79, 107	ltadd2dd 9811	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
109	93, 96, 82, 104, 108	eliood 37691	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) )
110	90, 109	ffvelrnd 6038	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. RR )
111		eqid 2471	. . . . . . . . . . 11 |- ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
112	1, 2, 3, 4, 111, 5	fourierdlem28 38109	. . . . . . . . . 10 |- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
113	84	recnd 9687	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
114		0red 9662	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR )
115		iooretop 21864	. . . . . . . . . . . . 13 |- ( A (,) B ) e. ( topGen ` ran (,) )
116		eqid 2471	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
117	116	tgioo2 21899	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
118	115, 117	eleqtri 2547	. . . . . . . . . . . 12 |- ( A (,) B ) e. ( ( TopOpen ` ℂfld ) ↾t RR )
119	118	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( A (,) B ) e. ( ( TopOpen ` ℂfld ) ↾t RR ) )
120	12	recnd 9687	. . . . . . . . . . 11 |- ( ph -> C e. CC )
121	88, 119, 120	dvmptconst 37882	. . . . . . . . . 10 |- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
122	88, 89, 110, 112, 113, 114, 121	dvmptsub 23000	. . . . . . . . 9 |- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) ) )
123	110	recnd 9687	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
124	123	subid1d 9994	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) = ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) )
125	124	mpteq2dva 4482	. . . . . . . . 9 |- ( ph -> ( s e. ( A (,) B ) |-> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
126	122, 125	eqtrd 2505	. . . . . . . 8 |- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
127	126	3ad2ant1 1051	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
128	123	3ad2antl1 1192	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
129		2cnd 10704	. . . . . . . . 9 |- ( s e. ( A (,) B ) -> 2 e. CC )
130	80	recnd 9687	. . . . . . . . . . 11 |- ( s e. ( A (,) B ) -> s e. CC )
131	130	halfcld 10880	. . . . . . . . . 10 |- ( s e. ( A (,) B ) -> ( s / 2 ) e. CC )
132	131	sincld 14261	. . . . . . . . 9 |- ( s e. ( A (,) B ) -> ( sin ` ( s / 2 ) ) e. CC )
133	129, 132	mulcld 9681	. . . . . . . 8 |- ( s e. ( A (,) B ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
134	133	adantl 473	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
135		fourierdlem68.e	. . . . . . . 8 |- ( ph -> E e. RR )
136	135	3ad2ant1 1051	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> E e. RR )
137		1re 9660	. . . . . . . . 9 |- 1 e. RR
138	22, 137	remulcli 9675	. . . . . . . 8 |- ( 2 x. 1 ) e. RR
139	138	a1i 11	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( 2 x. 1 ) e. RR )
140		1red 9676	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> 1 e. RR )
141		fourierdlem68.d	. . . . . . . . 9 |- ( ph -> D e. RR )
142	120	abscld 13575	. . . . . . . . 9 |- ( ph -> ( abs ` C ) e. RR )
143	141, 142	readdcld 9688	. . . . . . . 8 |- ( ph -> ( D + ( abs ` C ) ) e. RR )
144	143	3ad2ant1 1051	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( D + ( abs ` C ) ) e. RR )
145		simpl 464	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ph )
146	145, 109	jca 541	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) )
147		eleq1 2537	. . . . . . . . . . . 12 |- ( t = ( X + s ) -> ( t e. ( ( X + A ) (,) ( X + B ) ) <-> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) )
148	147	anbi2d 718	. . . . . . . . . . 11 |- ( t = ( X + s ) -> ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) <-> ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) ) )
149		fveq2 5879	. . . . . . . . . . . . 13 |- ( t = ( X + s ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) = ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) )
150	149	fveq2d 5883	. . . . . . . . . . . 12 |- ( t = ( X + s ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
151	150	breq1d 4405	. . . . . . . . . . 11 |- ( t = ( X + s ) -> ( ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E <-> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E ) )
152	148, 151	imbi12d 327	. . . . . . . . . 10 |- ( t = ( X + s ) -> ( ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E ) <-> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E ) ) )
153		fourierdlem68.fdvbd	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E )
154	152, 153	vtoclg 3093	. . . . . . . . 9 |- ( ( X + s ) e. RR -> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E ) )
155	82, 146, 154	sylc 61	. . . . . . . 8 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E )
156	155	3ad2antl1 1192	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E )
157	129, 132	absmuld 13593	. . . . . . . . 9 |- ( s e. ( A (,) B ) -> ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( abs ` 2 ) x. ( abs ` ( sin ` ( s / 2 ) ) ) ) )
158		0le2 10722	. . . . . . . . . . . 12 |- 0 <_ 2
159		absid 13436	. . . . . . . . . . . 12 |- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
160	22, 158, 159	mp2an 686	. . . . . . . . . . 11 |- ( abs ` 2 ) = 2
161	160	oveq1i 6318	. . . . . . . . . 10 |- ( ( abs ` 2 ) x. ( abs ` ( sin ` ( s / 2 ) ) ) ) = ( 2 x. ( abs ` ( sin ` ( s / 2 ) ) ) )
162	132	abscld 13575	. . . . . . . . . . 11 |- ( s e. ( A (,) B ) -> ( abs ` ( sin ` ( s / 2 ) ) ) e. RR )
163		1red 9676	. . . . . . . . . . 11 |- ( s e. ( A (,) B ) -> 1 e. RR )
164	22	a1i 11	. . . . . . . . . . 11 |- ( s e. ( A (,) B ) -> 2 e. RR )
165	158	a1i 11	. . . . . . . . . . 11 |- ( s e. ( A (,) B ) -> 0 <_ 2 )
166	80	rehalfcld 10882	. . . . . . . . . . . 12 |- ( s e. ( A (,) B ) -> ( s / 2 ) e. RR )
167		abssinbd 37600	. . . . . . . . . . . 12 |- ( ( s / 2 ) e. RR -> ( abs ` ( sin ` ( s / 2 ) ) ) <_ 1 )
168	166, 167	syl 17	. . . . . . . . . . 11 |- ( s e. ( A (,) B ) -> ( abs ` ( sin ` ( s / 2 ) ) ) <_ 1 )
169	162, 163, 164, 165, 168	lemul2ad 10569	. . . . . . . . . 10 |- ( s e. ( A (,) B ) -> ( 2 x. ( abs ` ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
170	161, 169	syl5eqbr 4429	. . . . . . . . 9 |- ( s e. ( A (,) B ) -> ( ( abs ` 2 ) x. ( abs ` ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
171	157, 170	eqbrtrd 4416	. . . . . . . 8 |- ( s e. ( A (,) B ) -> ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
172	171	adantl 473	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
173		abscosbd 37578	. . . . . . . . 9 |- ( ( s / 2 ) e. RR -> ( abs ` ( cos ` ( s / 2 ) ) ) <_ 1 )
174	101, 166, 173	3syl 18	. . . . . . . 8 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( cos ` ( s / 2 ) ) ) <_ 1 )
175	174	3ad2antl1 1192	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( cos ` ( s / 2 ) ) ) <_ 1 )
176	86	abscld 13575	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) e. RR )
177	89	abscld 13575	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( F ` ( X + s ) ) ) e. RR )
178	113	abscld 13575	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` C ) e. RR )
179	177, 178	readdcld 9688	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( abs ` ( F ` ( X + s ) ) ) + ( abs ` C ) ) e. RR )
180	141	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> D e. RR )
181	180, 178	readdcld 9688	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( D + ( abs ` C ) ) e. RR )
182	89, 113	abs2dif2d 13597	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) <_ ( ( abs ` ( F ` ( X + s ) ) ) + ( abs ` C ) ) )
183		fveq2 5879	. . . . . . . . . . . . . . 15 |- ( t = ( X + s ) -> ( F ` t ) = ( F ` ( X + s ) ) )
184	183	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( t = ( X + s ) -> ( abs ` ( F ` t ) ) = ( abs ` ( F ` ( X + s ) ) ) )
185	184	breq1d 4405	. . . . . . . . . . . . 13 |- ( t = ( X + s ) -> ( ( abs ` ( F ` t ) ) <_ D <-> ( abs ` ( F ` ( X + s ) ) ) <_ D ) )
186	148, 185	imbi12d 327	. . . . . . . . . . . 12 |- ( t = ( X + s ) -> ( ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D ) <-> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` ( X + s ) ) ) <_ D ) ) )
187		fourierdlem68.fbd	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D )
188	186, 187	vtoclg 3093	. . . . . . . . . . 11 |- ( ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) -> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` ( X + s ) ) ) <_ D ) )
189	109, 146, 188	sylc 61	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( F ` ( X + s ) ) ) <_ D )
190	177, 180, 178, 189	leadd1dd 10248	. . . . . . . . 9 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( abs ` ( F ` ( X + s ) ) ) + ( abs ` C ) ) <_ ( D + ( abs ` C ) ) )
191	176, 179, 181, 182, 190	letrd 9809	. . . . . . . 8 |- ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) <_ ( D + ( abs ` C ) ) )
192	191	3ad2antl1 1192	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) <_ ( D + ( abs ` C ) ) )
193	14	simpri 469	. . . . . . . 8 |- ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
194	193	a1i 11	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
195	131	coscld 14262	. . . . . . . 8 |- ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC )
196	195	adantl 473	. . . . . . 7 |- ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC )
197		simp2 1031	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> c e. RR+ )
198		oveq1 6315	. . . . . . . . . . . . . 14 |- ( t = s -> ( t / 2 ) = ( s / 2 ) )
199	198	fveq2d 5883	. . . . . . . . . . . . 13 |- ( t = s -> ( sin ` ( t / 2 ) ) = ( sin ` ( s / 2 ) ) )
200	199	oveq2d 6324	. . . . . . . . . . . 12 |- ( t = s -> ( 2 x. ( sin ` ( t / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
201	200	fveq2d 5883	. . . . . . . . . . 11 |- ( t = s -> ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) = ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
202	201	breq2d 4407	. . . . . . . . . 10 |- ( t = s -> ( c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) <-> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
203	202	cbvralv 3005	. . . . . . . . 9 |- ( A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) <-> A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
204		nfv 1769	. . . . . . . . . . 11 |- F/ s ph
205		nfra1 2785	. . . . . . . . . . 11 |- F/ s A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) )
206	204, 205	nfan 2031	. . . . . . . . . 10 |- F/ s ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
207		simplr 770	. . . . . . . . . . . 12 |- ( ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
208	6, 101	sseldi 3416	. . . . . . . . . . . . 13 |- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A [,] B ) )
209	208	adantlr 729	. . . . . . . . . . . 12 |- ( ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> s e. ( A [,] B ) )
210		rspa 2774	. . . . . . . . . . . 12 |- ( ( A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) /\ s e. ( A [,] B ) ) -> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
211	207, 209, 210	syl2anc 673	. . . . . . . . . . 11 |- ( ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
212	211	ex 441	. . . . . . . . . 10 |- ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) -> ( s e. ( A (,) B ) -> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
213	206, 212	ralrimi 2800	. . . . . . . . 9 |- ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) -> A. s e. ( A (,) B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
214	203, 213	sylan2b 483	. . . . . . . 8 |- ( ( ph /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> A. s e. ( A (,) B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
215	214	3adant2 1049	. . . . . . 7 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> A. s e. ( A (,) B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
216		eqid 2471	. . . . . . 7 |- ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
217	77, 87, 127, 128, 134, 136, 139, 140, 144, 156, 172, 175, 192, 194, 196, 197, 215, 216	dvdivbd 37892	. . . . . 6 |- ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b )
218	217	rexlimdv3a 2873	. . . . 5 |- ( ph -> ( E. c e. RR+ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) -> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
219	75, 218	mpd 15	. . . 4 |- ( ph -> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b )
220		nfcv 2612	. . . . . . . . 9 |- F/_ s RR
221		nfcv 2612	. . . . . . . . 9 |- F/_ s _D
222		nfmpt1 4485	. . . . . . . . . 10 |- F/_ s ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
223	13, 222	nfcxfr 2610	. . . . . . . . 9 |- F/_ s O
224	220, 221, 223	nfov 6334	. . . . . . . 8 |- F/_ s ( RR _D O )
225	224	nfdm 5082	. . . . . . 7 |- F/_ s dom ( RR _D O )
226		nfcv 2612	. . . . . . 7 |- F/_ s ( A (,) B )
227	225, 226	raleqf 2969	. . . . . 6 |- ( dom ( RR _D O ) = ( A (,) B ) -> ( A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b <-> A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
228	18, 227	syl 17	. . . . 5 |- ( ph -> ( A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b <-> A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
229	228	rexbidv 2892	. . . 4 |- ( ph -> ( E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b <-> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
230	219, 229	mpbird 240	. . 3 |- ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b )
231	13	a1i 11	. . . . . . . 8 |- ( ph -> O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
232	231	oveq2d 6324	. . . . . . 7 |- ( ph -> ( RR _D O ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
233	232	fveq1d 5881	. . . . . 6 |- ( ph -> ( ( RR _D O ) ` s ) = ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) )
234	233	fveq2d 5883	. . . . 5 |- ( ph -> ( abs ` ( ( RR _D O ) ` s ) ) = ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) )
235	234	breq1d 4405	. . . 4 |- ( ph -> ( ( abs ` ( ( RR _D O ) ` s ) ) <_ b <-> ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
236	235	rexralbidv 2898	. . 3 |- ( ph -> ( E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b <-> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
237	230, 236	mpbird 240	. 2 |- ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b )
238	18, 237	jca 541	1 |- ( ph -> ( dom ( RR _D O ) = ( A (,) B ) /\ E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   \ cdif 3387   C_ wss 3390   {csn 3959   {cpr 3961   class class class wbr 4395   |-> cmpt 4454   dom cdm 4839   ran crn 4840   |` cres 4841   -->wf 5585   ` cfv 5589  (class class class)co 6308   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   x. cmul 9562   RR*cxr 9692   < clt 9693   <_ cle 9694   - cmin 9880   -ucneg 9881   / cdiv 10291   2c2 10681   RR+crp 11325   (,)cioo 11660   [,]cicc 11663   ^cexp 12310   abscabs 13374   sincsin 14193   cosccos 14194   picpi 14196   ↾_t crest 15397   TopOpenctopn 15398   topGenctg 15414  ℂ_fldccnfld 19047   -cn->ccncf 21986   _D cdv 22897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13207  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-ef 14198  df-sin 14200  df-cos 14201  df-pi 14203  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-t1 20407  df-haus 20408  df-cmp 20479  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-limc 22900  df-dv 22901

This theorem is referenced by:  fourierdlem80  38162