Theorem fourierdlem57

Description: The derivative of O . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem57.f	|- ( ph -> F : RR --> RR )
	fourierdlem57.xre	|- ( ph -> X e. RR )
	fourierdlem57.a	|- ( ph -> A e. RR )
	fourierdlem57.b	|- ( ph -> B e. RR )
	fourierdlem57.fdv	|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
	fourierdlem57.ab	|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
	fourierdlem57.n0	|- ( ph -> -. 0 e. ( A (,) B ) )
	fourierdlem57.c	|- ( ph -> C e. RR )
	fourierdlem57.o	|- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
Assertion	fourierdlem57	|- ( ( 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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem57.f	|- ( ph -> F : RR --> RR )
2		fourierdlem57.xre	|- ( ph -> X e. RR )
3		fourierdlem57.a	|- ( ph -> A e. RR )
4		fourierdlem57.b	|- ( ph -> B e. RR )
5		fourierdlem57.fdv	|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
6		fourierdlem57.ab	|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
7		fourierdlem57.n0	|- ( ph -> -. 0 e. ( A (,) B ) )
8		fourierdlem57.c	|- ( ph -> C e. RR )
9		fourierdlem57.o	|- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
10	5	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
11	2 3	readdcld	|- ( ph -> ( X + A ) e. RR )
12	11	rexrd	|- ( ph -> ( X + A ) e. RR* )
13	12	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) e. RR* )
14	2 4	readdcld	|- ( ph -> ( X + B ) e. RR )
15	14	rexrd	|- ( ph -> ( X + B ) e. RR* )
16	15	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) e. RR* )
17	2	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
18		elioore	|- ( s e. ( A (,) B ) -> s e. RR )
19	18	adantl	|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
20	17 19	readdcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
21	3	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
22	21	rexrd	|- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
23	4	rexrd	|- ( ph -> B e. RR* )
24	23	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
25		simpr	|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
26		ioogtlb	|- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
27	22 24 25 26	syl3anc	|- ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
28	21 19 17 27	ltadd2dd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
29	4	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
30		iooltub	|- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
31	22 24 25 30	syl3anc	|- ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
32	19 29 17 31	ltadd2dd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
33	13 16 20 28 32	eliood	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) )
34	10 33	ffvelrnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. RR )
35		2re	|- 2 e. RR
36	35	a1i	|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. RR )
37		rehalfcl	|- ( s e. RR -> ( s / 2 ) e. RR )
38	19 37	syl	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. RR )
39	38	resincld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. RR )
40	36 39	remulcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
41	34 40	remulcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR )
42	38	recoscld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. RR )
43	1	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
44	43 20	ffvelrnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
45	8	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> C e. RR )
46	44 45	resubcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. RR )
47	42 46	remulcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) e. RR )
48	41 47	resubcld	|- ( ( ph /\ 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 ) ) ) e. RR )
49	40	resqcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) e. RR )
50		2cnd	|- ( s e. RR -> 2 e. CC )
51	37	recnd	|- ( s e. RR -> ( s / 2 ) e. CC )
52	51	sincld	|- ( s e. RR -> ( sin ` ( s / 2 ) ) e. CC )
53	50 52	mulcld	|- ( s e. RR -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
54	19 53	syl	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
55		2cnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. CC )
56	19 52	syl	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC )
57		2ne0	|- 2 =/= 0
58	57	a1i	|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 =/= 0 )
59	6	sselda	|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) )
60		eqcom	|- ( s = 0 <-> 0 = s )
61	60	biimpi	|- ( s = 0 -> 0 = s )
62	61	adantl	|- ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 = s )
63		simpl	|- ( ( s e. ( A (,) B ) /\ s = 0 ) -> s e. ( A (,) B ) )
64	62 63	eqeltrd	|- ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
65	64	adantll	|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
66	7	ad2antrr	|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> -. 0 e. ( A (,) B ) )
67	65 66	pm2.65da	|- ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 )
68	67	neqned	|- ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
69		fourierdlem44	|- ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
70	59 68 69	syl2anc	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
71	55 56 58 70	mulne0d	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
72		2z	|- 2 e. ZZ
73	72	a1i	|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. ZZ )
74	54 71 73	expne0d	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) =/= 0 )
75	48 49 74	redivcld	|- ( ( ph /\ 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 ) ) e. RR )
76		eqid	|- ( 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 ) ) ) = ( 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 ) ) )
77	75 76	fmptd	|- ( ph -> ( 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 ) ) ) : ( A (,) B ) --> RR )
78	9	a1i	|- ( ph -> O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
79	78	oveq2d	|- ( ph -> ( RR _D O ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
80		reelprrecn	|- RR e. { RR , CC }
81	80	a1i	|- ( ph -> RR e. { RR , CC } )
82	46	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
83	44	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
84		eqid	|- ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
85	1 2 3 4 84 5	fourierdlem28	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
86	45	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
87		0red	|- ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR )
88		iooretop	|- ( A (,) B ) e. ( topGen ` ran (,) )
89		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
90	89	tgioo2	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
91	88 90	eleqtri	|- ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
92	91	a1i	|- ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
93	8	recnd	|- ( ph -> C e. CC )
94	81 92 93	dvmptconst	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
95	81 83 34 85 86 87 94	dvmptsub	|- ( 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 ) ) )
96	34	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
97	96	subid1d	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) = ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) )
98	97	mpteq2dva	|- ( 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 ) ) ) )
99	95 98	eqtrd	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
100		eldifsn	|- ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) <-> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC /\ ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 ) )
101	54 71 100	sylanbrc	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
102		recn	|- ( s e. RR -> s e. CC )
103	57	a1i	|- ( s e. RR -> 2 =/= 0 )
104	102 50 103	divrec2d	|- ( s e. RR -> ( s / 2 ) = ( ( 1 / 2 ) x. s ) )
105	104	eqcomd	|- ( s e. RR -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
106	18 105	syl	|- ( s e. ( A (,) B ) -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
107	106	fveq2d	|- ( s e. ( A (,) B ) -> ( cos ` ( ( 1 / 2 ) x. s ) ) = ( cos ` ( s / 2 ) ) )
108		halfcn	|- ( 1 / 2 ) e. CC
109	108	a1i	|- ( s e. CC -> ( 1 / 2 ) e. CC )
110		id	|- ( s e. CC -> s e. CC )
111	109 110	mulcld	|- ( s e. CC -> ( ( 1 / 2 ) x. s ) e. CC )
112	111	coscld	|- ( s e. CC -> ( cos ` ( ( 1 / 2 ) x. s ) ) e. CC )
113	18 102 112	3syl	|- ( s e. ( A (,) B ) -> ( cos ` ( ( 1 / 2 ) x. s ) ) e. CC )
114	107 113	eqeltrrd	|- ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC )
115	114	adantl	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC )
116		ioossre	|- ( A (,) B ) C_ RR
117		resmpt	|- ( ( A (,) B ) C_ RR -> ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
118	116 117	ax-mp	|- ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
119	118	eqcomi	|- ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) )
120	119	oveq2i	|- ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) )
121		ax-resscn	|- RR C_ CC
122		eqid	|- ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
123	122 53	fmpti	|- ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC
124		ssid	|- RR C_ RR
125	89 90	dvres	|- ( ( ( RR C_ CC /\ ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC ) /\ ( RR C_ RR /\ ( A (,) B ) C_ RR ) ) -> ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) ) )
126	121 123 124 116 125	mp4an	|- ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
127		resmpt	|- ( RR C_ CC -> ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
128	121 127	ax-mp	|- ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
129	105	fveq2d	|- ( s e. RR -> ( sin ` ( ( 1 / 2 ) x. s ) ) = ( sin ` ( s / 2 ) ) )
130	129	oveq2d	|- ( s e. RR -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
131	130	mpteq2ia	|- ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
132	128 131	eqtr2i	|- ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR )
133	132	oveq2i	|- ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) )
134		ioontr	|- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
135	133 134	reseq12i	|- ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) ) = ( ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) |` ( A (,) B ) )
136		eqid	|- ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
137		2cnd	|- ( s e. CC -> 2 e. CC )
138	111	sincld	|- ( s e. CC -> ( sin ` ( ( 1 / 2 ) x. s ) ) e. CC )
139	137 138	mulcld	|- ( s e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
140	136 139	fmpti	|- ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC
141		ssid	|- CC C_ CC
142		dmmptg	|- ( A. s e. CC ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) e. CC -> dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = CC )
143		2cn	|- 2 e. CC
144	143 108	mulcli	|- ( 2 x. ( 1 / 2 ) ) e. CC
145	144	a1i	|- ( s e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
146	145 112	mulcld	|- ( s e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
147	142 146	mprg	|- dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = CC
148	121 147	sseqtrri	|- RR C_ dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
149		dvasinbx	|- ( ( 2 e. CC /\ ( 1 / 2 ) e. CC ) -> ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) )
150	143 108 149	mp2an	|- ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
151	150	dmeqi	|- dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
152	148 151	sseqtrri	|- RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
153		dvres3	|- ( ( ( RR e. { RR , CC } /\ ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) ) ) -> ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) )
154	80 140 141 152 153	mp4an	|- ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR )
155	154	reseq1i	|- ( ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) |` ( A (,) B ) ) = ( ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) |` ( A (,) B ) )
156	150	reseq1i	|- ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) = ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR )
157	156	reseq1i	|- ( ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) |` ( A (,) B ) )
158		resabs1	|- ( ( A (,) B ) C_ RR -> ( ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) ) )
159	116 158	ax-mp	|- ( ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) )
160		ioosscn	|- ( A (,) B ) C_ CC
161		resmpt	|- ( ( A (,) B ) C_ CC -> ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) )
162	160 161	ax-mp	|- ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
163	157 159 162	3eqtri	|- ( ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
164	135 155 163	3eqtri	|- ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
165	120 126 164	3eqtri	|- ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
166	143 57	recidi	|- ( 2 x. ( 1 / 2 ) ) = 1
167	166	oveq1i	|- ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) )
168	167	a1i	|- ( s e. ( A (,) B ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
169	113	mulid2d	|- ( s e. ( A (,) B ) -> ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( ( 1 / 2 ) x. s ) ) )
170	168 169 107	3eqtrd	|- ( s e. ( A (,) B ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( s / 2 ) ) )
171	170	mpteq2ia	|- ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
172	165 171	eqtri	|- ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
173	172	a1i	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
174	81 82 34 99 101 115 173	dvmptdiv	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( 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 ) ) ) )
175	79 174	eqtrd	|- ( ph -> ( 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 ) ) ) )
176	175	feq1d	|- ( ph -> ( ( RR _D O ) : ( A (,) B ) --> RR <-> ( 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 ) ) ) : ( A (,) B ) --> RR ) )
177	77 176	mpbird	|- ( ph -> ( RR _D O ) : ( A (,) B ) --> RR )
178	177 175	jca	|- ( 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 ) ) ) ) )
179	178 172	pm3.2i	|- ( ( 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 ) ) ) )