Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dirkercncflem2 Structured version   Unicode version

Theorem dirkercncflem2 31727
Description: Lemma used to proof that the Dirichlet Kernel is continuous at  Y points that are multiples of 
( 2  x.  pi ) (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
dirkercncflem2.d  |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
dirkercncflem2.f  |-  F  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )
dirkercncflem2.g  |-  G  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )
dirkercncflem2.yne0  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
y  /  2 ) )  =/=  0 )
dirkercncflem2.h  |-  H  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
dirkercncflem2.i  |-  I  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )
dirkercncflem2.l  |-  L  =  ( w  e.  ( A (,) B ) 
|->  ( ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  w ) ) )  /  (
pi  x.  ( cos `  ( w  /  2
) ) ) ) )
dirkercncflem2.n  |-  ( ph  ->  N  e.  NN )
dirkercncflem2.y  |-  ( ph  ->  Y  e.  ( A (,) B ) )
dirkercncflem2.ymod  |-  ( ph  ->  ( Y  mod  (
2  x.  pi ) )  =  0 )
dirkercncflem2.11  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( cos `  (
y  /  2 ) )  =/=  0 )
Assertion
Ref Expression
dirkercncflem2  |-  ( ph  ->  ( ( D `  N ) `  Y
)  e.  ( ( ( D `  N
)  |`  ( ( A (,) B )  \  { Y } ) ) lim
CC  Y ) )
Distinct variable groups:    w, A, y    w, B, y    y, D    w, F, y    w, G, y    w, H, y   
w, I, y    y, L    w, N, y    w, Y, y    y, n    ph, w, y
Allowed substitution hints:    ph( n)    A( n)    B( n)    D( w, n)    F( n)    G( n)    H( n)    I( n)    L( w, n)    N( n)    Y( n)

Proof of Theorem dirkercncflem2
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 difss 3636 . . . . 5  |-  ( ( A (,) B ) 
\  { Y }
)  C_  ( A (,) B )
2 ioossre 11598 . . . . 5  |-  ( A (,) B )  C_  RR
31, 2sstri 3518 . . . 4  |-  ( ( A (,) B ) 
\  { Y }
)  C_  RR
43a1i 11 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  RR )
5 dirkercncflem2.n . . . . . . . . 9  |-  ( ph  ->  N  e.  NN )
65adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  NN )
76nnred 10563 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  RR )
8 1re 9607 . . . . . . . . 9  |-  1  e.  RR
98rehalfcli 10799 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
109a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 1  /  2
)  e.  RR )
117, 10readdcld 9635 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( N  +  ( 1  /  2 ) )  e.  RR )
124sselda 3509 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
y  e.  RR )
1311, 12remulcld 9636 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  y
)  e.  RR )
1413resincld 13756 . . . 4  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) )  e.  RR )
15 dirkercncflem2.f . . . 4  |-  F  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )
1614, 15fmptd 6056 . . 3  |-  ( ph  ->  F : ( ( A (,) B ) 
\  { Y }
) --> RR )
17 2re 10617 . . . . . . . 8  |-  2  e.  RR
18 pire 22718 . . . . . . . 8  |-  pi  e.  RR
1917, 18remulcli 9622 . . . . . . 7  |-  ( 2  x.  pi )  e.  RR
2019a1i 11 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 2  x.  pi )  e.  RR )
21 rehalfcl 10777 . . . . . . . 8  |-  ( y  e.  RR  ->  (
y  /  2 )  e.  RR )
2212, 21syl 16 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  2
)  e.  RR )
23 resincl 13753 . . . . . . 7  |-  ( ( y  /  2 )  e.  RR  ->  ( sin `  ( y  / 
2 ) )  e.  RR )
2422, 23syl 16 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
y  /  2 ) )  e.  RR )
2520, 24jca 532 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( 2  x.  pi )  e.  RR  /\  ( sin `  (
y  /  2 ) )  e.  RR ) )
26 remulcl 9589 . . . . 5  |-  ( ( ( 2  x.  pi )  e.  RR  /\  ( sin `  ( y  / 
2 ) )  e.  RR )  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  e.  RR )
2725, 26syl 16 . . . 4  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) )  e.  RR )
28 dirkercncflem2.g . . . 4  |-  G  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )
2927, 28fmptd 6056 . . 3  |-  ( ph  ->  G : ( ( A (,) B ) 
\  { Y }
) --> RR )
30 iooretop 21141 . . . 4  |-  ( A (,) B )  e.  ( topGen `  ran  (,) )
3130a1i 11 . . 3  |-  ( ph  ->  ( A (,) B
)  e.  ( topGen ` 
ran  (,) ) )
32 dirkercncflem2.y . . 3  |-  ( ph  ->  Y  e.  ( A (,) B ) )
33 eqid 2467 . . 3  |-  ( ( A (,) B ) 
\  { Y }
)  =  ( ( A (,) B ) 
\  { Y }
)
3415a1i 11 . . . . . . . 8  |-  ( ph  ->  F  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
3534oveq2d 6311 . . . . . . 7  |-  ( ph  ->  ( RR  _D  F
)  =  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
36 resmpt 5329 . . . . . . . . . . . 12  |-  ( ( ( A (,) B
)  \  { Y } )  C_  RR  ->  ( ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  (
( A (,) B
)  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )
373, 36ax-mp 5 . . . . . . . . . . 11  |-  ( ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  ( ( A (,) B )  \  { Y } ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )
3837eqcomi 2480 . . . . . . . . . 10  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  =  ( ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  ( ( A (,) B )  \  { Y } ) )
3938a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  (
( A (,) B
)  \  { Y } ) ) )
4039oveq2d 6311 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  ( RR  _D  (
( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) ) )
41 ax-resscn 9561 . . . . . . . . . . 11  |-  RR  C_  CC
4241a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
435nncnd 10564 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
44 ax-1cn 9562 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
45 halfcl 10776 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  CC  ->  (
1  /  2 )  e.  CC )
4644, 45ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( 1  /  2 )  e.  CC
4746a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  /  2
)  e.  CC )
4843, 47addcld 9627 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  CC )
4948adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
5042sselda 3509 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
5149, 50mulcld 9628 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
5251sincld 13743 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
53 eqid 2467 . . . . . . . . . . 11  |-  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
5452, 53fmptd 6056 . . . . . . . . . 10  |-  ( ph  ->  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : RR --> CC )
5542, 54jca 532 . . . . . . . . 9  |-  ( ph  ->  ( RR  C_  CC  /\  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : RR --> CC ) )
56 ssid 3528 . . . . . . . . . . 11  |-  RR  C_  RR
5756, 3pm3.2i 455 . . . . . . . . . 10  |-  ( RR  C_  RR  /\  ( ( A (,) B ) 
\  { Y }
)  C_  RR )
5857a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( RR  C_  RR  /\  ( ( A (,) B )  \  { Y } )  C_  RR ) )
59 eqid 2467 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6059tgioo2 21176 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
6159, 60dvres 22183 . . . . . . . . 9  |-  ( ( ( RR  C_  CC  /\  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : RR --> CC )  /\  ( RR  C_  RR  /\  ( ( A (,) B )  \  { Y } )  C_  RR ) )  ->  ( RR  _D  ( ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )  =  ( ( RR 
_D  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) ) )
6255, 58, 61syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) ) )
63 retop 21136 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  Top
6463a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( topGen `  ran  (,) )  e.  Top )
65 rehaus 21172 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Haus
6665a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( topGen `  ran  (,) )  e.  Haus )
672, 32sseldi 3507 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
68 uniretop 21137 . . . . . . . . . . . . . 14  |-  RR  =  U. ( topGen `  ran  (,) )
6968sncld 19740 . . . . . . . . . . . . 13  |-  ( ( ( topGen `  ran  (,) )  e.  Haus  /\  Y  e.  RR )  ->  { Y }  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
7066, 67, 69syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  { Y }  e.  ( Clsd `  ( topGen ` 
ran  (,) ) ) )
7168difopn 19403 . . . . . . . . . . . 12  |-  ( ( ( A (,) B
)  e.  ( topGen ` 
ran  (,) )  /\  { Y }  e.  ( Clsd `  ( topGen `  ran  (,) ) ) )  -> 
( ( A (,) B )  \  { Y } )  e.  (
topGen `  ran  (,) )
)
7231, 70, 71syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  e.  (
topGen `  ran  (,) )
)
73 isopn3i 19451 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( A (,) B ) 
\  { Y }
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) )  =  ( ( A (,) B )  \  { Y } ) )
7464, 72, 73syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) )  =  ( ( A (,) B )  \  { Y } ) )
7574reseq2d 5279 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )
76 reex 9595 . . . . . . . . . . . . . . . . 17  |-  RR  e.  _V
7776prid1 4141 . . . . . . . . . . . . . . . 16  |-  RR  e.  { RR ,  CC }
7877a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  e.  { RR ,  CC } )
7948adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
80 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  y  e.  CC )
8179, 80mulcld 9628 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
8281sincld 13743 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  CC )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
83 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
8482, 83fmptd 6056 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : CC --> CC )
8578, 84jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( RR  e.  { RR ,  CC }  /\  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : CC --> CC ) )
86 ssid 3528 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
8786a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  C_  CC )
88 dvsinax 31564 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  +  ( 1  /  2 ) )  e.  CC  ->  ( CC  _D  ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) ) )
8948, 88syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
90 dmeq 5209 . . . . . . . . . . . . . . . . . 18  |-  ( ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  =  ( y  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  ->  dom  ( CC  _D  (
y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  dom  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) ) )
9189, 90syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  dom  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) ) )
92 coscl 13740 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC  ->  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) )  e.  CC )
9381, 92syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
9479, 93jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  e.  CC  /\  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) )  e.  CC ) )
95 mulcl 9588 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  +  ( 1  /  2 ) )  e.  CC  /\  ( cos `  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  e.  CC )  -> 
( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) )  e.  CC )
9694, 95syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  e.  CC )
97 eqid 2467 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) )
9896, 97fmptd 6056 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) ) : CC --> CC )
99 fdm 5741 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) : CC --> CC  ->  dom  ( y  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) )  =  CC )
10098, 99syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( y  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  CC )
10191, 100eqtrd 2508 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  CC )
10242, 101sseqtr4d 3546 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
10387, 102jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  C_  CC  /\  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) ) )
104 dvres3 22185 . . . . . . . . . . . . . 14  |-  ( ( ( RR  e.  { RR ,  CC }  /\  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : CC --> CC )  /\  ( CC  C_  CC  /\  RR  C_  dom  ( CC  _D  (
y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) ) )  ->  ( RR  _D  ( ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR ) )  =  ( ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  RR ) )
10585, 103, 104syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( RR  _D  (
( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )
)  =  ( ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  RR ) )
10689reseq1d 5278 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  RR )  =  ( ( y  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  RR ) )
107 resmpt 5329 . . . . . . . . . . . . . . . 16  |-  ( RR  C_  CC  ->  ( (
y  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
10841, 107ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )
109108a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( y  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  RR )  =  (
y  e.  RR  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
110106, 109eqtrd 2508 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
111105, 110eqtrd 2508 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  _D  (
( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )
)  =  ( y  e.  RR  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
112 resmpt 5329 . . . . . . . . . . . . . . 15  |-  ( RR  C_  CC  ->  ( (
y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
11341, 112ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )
114113a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
115114oveq2d 6311 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  _D  (
( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )
)  =  ( RR 
_D  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
116111, 115eqtr3d 2510 . . . . . . . . . . 11  |-  ( ph  ->  ( y  e.  RR  |->  ( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) ) )  =  ( RR 
_D  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
117116eqcomd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  ( y  e.  RR  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
118117reseq1d 5278 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  (
( A (,) B
)  \  { Y } ) )  =  ( ( y  e.  RR  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )
119 resmpt 5329 . . . . . . . . . . 11  |-  ( ( ( A (,) B
)  \  { Y } )  C_  RR  ->  ( ( y  e.  RR  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
1203, 119ax-mp 5 . . . . . . . . . 10  |-  ( ( y  e.  RR  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) )  |`  ( ( A (,) B )  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
121120a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( ( y  e.  RR  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
12275, 118, 1213eqtrd 2512 . . . . . . . 8  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
12340, 62, 1223eqtrd 2512 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
124 dirkercncflem2.h . . . . . . . . 9  |-  H  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
125124a1i 11 . . . . . . . 8  |-  ( ph  ->  H  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
126125eqcomd 2475 . . . . . . 7  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  H )
12735, 123, 1263eqtrd 2512 . . . . . 6  |-  ( ph  ->  ( RR  _D  F
)  =  H )
128127dmeqd 5211 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  F )  =  dom  H )
129 simpl 457 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  ph )
13012, 50syldan 470 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
y  e.  CC )
131129, 130jca 532 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ph  /\  y  e.  CC ) )
132131, 96syl 16 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) )  e.  CC )
133132, 124fmptd 6056 . . . . . 6  |-  ( ph  ->  H : ( ( A (,) B ) 
\  { Y }
) --> CC )
134 fdm 5741 . . . . . 6  |-  ( H : ( ( A (,) B )  \  { Y } ) --> CC 
->  dom  H  =  ( ( A (,) B
)  \  { Y } ) )
135133, 134syl 16 . . . . 5  |-  ( ph  ->  dom  H  =  ( ( A (,) B
)  \  { Y } ) )
136128, 135eqtr2d 2509 . . . 4  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  =  dom  ( RR  _D  F
) )
137 eqimss 3561 . . . 4  |-  ( ( ( A (,) B
)  \  { Y } )  =  dom  ( RR  _D  F
)  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  F
) )
138136, 137syl 16 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  F
) )
139 dirkercncflem2.i . . . . . . . 8  |-  I  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )
140139a1i 11 . . . . . . 7  |-  ( ph  ->  I  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) )
141 resmpt 5329 . . . . . . . . . . . . 13  |-  ( ( ( A (,) B
)  \  { Y } )  C_  RR  ->  ( ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )
1423, 141ax-mp 5 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) )  |`  ( ( A (,) B )  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )
143142eqcomi 2480 . . . . . . . . . . 11  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) )  =  ( ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) )
144143oveq2i 6306 . . . . . . . . . 10  |-  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  ( RR  _D  ( ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )
145144a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  ( RR  _D  ( ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) ) )
146 2cn 10618 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
14741, 18sselii 3506 . . . . . . . . . . . . . . . 16  |-  pi  e.  CC
148146, 147mulcli 9613 . . . . . . . . . . . . . . 15  |-  ( 2  x.  pi )  e.  CC
149148a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( 2  x.  pi )  e.  CC )
150 id 22 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  ->  y  e.  CC )
151146a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  ->  2  e.  CC )
152 2ne0 10640 . . . . . . . . . . . . . . . . . 18  |-  2  =/=  0
153152a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  ->  2  =/=  0 )
154150, 151, 153divcld 10332 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  ->  (
y  /  2 )  e.  CC )
15550, 154syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  /  2 )  e.  CC )
156 sincl 13739 . . . . . . . . . . . . . . 15  |-  ( ( y  /  2 )  e.  CC  ->  ( sin `  ( y  / 
2 ) )  e.  CC )
157155, 156syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( sin `  ( y  /  2
) )  e.  CC )
158149, 157jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  e.  CC  /\  ( sin `  ( y  / 
2 ) )  e.  CC ) )
159 mulcl 9588 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  pi )  e.  CC  /\  ( sin `  ( y  / 
2 ) )  e.  CC )  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  e.  CC )
160158, 159syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) )  e.  CC )
161 eqid 2467 . . . . . . . . . . . 12  |-  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
162160, 161fmptd 6056 . . . . . . . . . . 11  |-  ( ph  ->  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) : RR --> CC )
16342, 162jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( RR  C_  CC  /\  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) : RR --> CC ) )
16459, 60dvres 22183 . . . . . . . . . 10  |-  ( ( ( RR  C_  CC  /\  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) : RR --> CC )  /\  ( RR  C_  RR  /\  ( ( A (,) B )  \  { Y } )  C_  RR ) )  ->  ( RR  _D  ( ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )  =  ( ( RR 
_D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) ) )
165163, 58, 164syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  (
( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) ) )
16674reseq2d 5279 . . . . . . . . . 10  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  |`  ( ( A (,) B )  \  { Y } ) ) )
16741sseli 3505 . . . . . . . . . . . . . . . 16  |-  ( y  e.  RR  ->  y  e.  CC )
16844a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  1  e.  CC )
169168, 151, 150, 153div13d 10356 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( 1  /  2
)  x.  y )  =  ( ( y  /  2 )  x.  1 ) )
170154mulid1d 9625 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( y  /  2
)  x.  1 )  =  ( y  / 
2 ) )
171169, 170eqtrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  CC  ->  (
( 1  /  2
)  x.  y )  =  ( y  / 
2 ) )
172171fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  CC  ->  ( sin `  ( ( 1  /  2 )  x.  y ) )  =  ( sin `  (
y  /  2 ) ) )
173172oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  ->  (
( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
174173eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
175167, 174syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  RR  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
176175adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) )
177176mpteq2dva 4539 . . . . . . . . . . . . 13  |-  ( ph  ->  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) )
178177oveq2d 6311 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) )  =  ( RR 
_D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) ) )
179 resmpt 5329 . . . . . . . . . . . . . . . . . 18  |-  ( RR  C_  CC  ->  ( (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )
18041, 179ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) )
181180a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) )  |`  RR )  =  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )
182181oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( RR  _D  (
( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )  |`  RR )
)  =  ( RR 
_D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) ) )
183182eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( RR 
_D  ( ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) )  |`  RR ) ) )
184148a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  CC )  ->  ( 2  x.  pi )  e.  CC )
18546a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( 1  /  2 )  e.  CC )
186185, 80jca 532 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 1  /  2 )  e.  CC  /\  y  e.  CC ) )
187 mulcl 9588 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1  /  2
)  e.  CC  /\  y  e.  CC )  ->  ( ( 1  / 
2 )  x.  y
)  e.  CC )
188186, 187syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 1  /  2 )  x.  y )  e.  CC )
189 sincl 13739 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  /  2
)  x.  y )  e.  CC  ->  ( sin `  ( ( 1  /  2 )  x.  y ) )  e.  CC )
190188, 189syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  CC )  ->  ( sin `  ( ( 1  / 
2 )  x.  y
) )  e.  CC )
191184, 190jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  e.  CC  /\  ( sin `  ( ( 1  /  2 )  x.  y ) )  e.  CC ) )
192 mulcl 9588 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 2  x.  pi )  e.  CC  /\  ( sin `  ( ( 1  /  2 )  x.  y ) )  e.  CC )  ->  (
( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) )  e.  CC )
193191, 192syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) )  e.  CC )
194 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
195193, 194fmptd 6056 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) : CC --> CC )
19678, 195jca 532 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( RR  e.  { RR ,  CC }  /\  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) : CC --> CC ) )
197146a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  2  e.  CC )
198147a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  pi  e.  CC )
199197, 198mulcld 9628 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 2  x.  pi )  e.  CC )
200 dvasinbx 31573 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 2  x.  pi )  e.  CC  /\  (
1  /  2 )  e.  CC )  -> 
( CC  _D  (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( y  e.  CC  |->  ( ( ( 2  x.  pi )  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  y ) ) ) ) )
201199, 47, 200syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( y  e.  CC  |->  ( ( ( 2  x.  pi )  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  y ) ) ) ) )
202146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  CC )  ->  2  e.  CC )
203147a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  CC )  ->  pi  e.  CC )
204202, 203, 185mul32d 9801 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( 1  / 
2 ) )  =  ( ( 2  x.  ( 1  /  2
) )  x.  pi ) )
20544a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  CC )  ->  1  e.  CC )
206152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  CC )  ->  2  =/=  0 )
207205, 202, 206divcan2d 10334 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  CC )  ->  ( 2  x.  ( 1  / 
2 ) )  =  1 )
208207oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  ( 1  /  2 ) )  x.  pi )  =  ( 1  x.  pi ) )
209203mulid2d 9626 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  ( 1  x.  pi )  =  pi )
210204, 208, 2093eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( 1  / 
2 ) )  =  pi )
211171fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  CC  ->  ( cos `  ( ( 1  /  2 )  x.  y ) )  =  ( cos `  (
y  /  2 ) ) )
212211adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( ( 1  / 
2 )  x.  y
) )  =  ( cos `  ( y  /  2 ) ) )
213210, 212oveq12d 6313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( 2  x.  pi )  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  y ) ) )  =  ( pi  x.  ( cos `  ( y  /  2
) ) ) )
214213mpteq2dva 4539 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( y  e.  CC  |->  ( ( ( 2  x.  pi )  x.  ( 1  /  2
) )  x.  ( cos `  ( ( 1  /  2 )  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
215201, 214eqtrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
216 dmeq 5209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  ->  dom  ( CC  _D  (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  dom  (
y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) )
217215, 216syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) )  =  dom  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  / 
2 ) ) ) ) )
21880, 154syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  ( y  /  2 )  e.  CC )
219 coscl 13740 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  /  2 )  e.  CC  ->  ( cos `  ( y  / 
2 ) )  e.  CC )
220218, 219syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( y  /  2
) )  e.  CC )
221203, 220jca 532 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( pi  e.  CC  /\  ( cos `  ( y  / 
2 ) )  e.  CC ) )
222 mulcl 9588 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( pi  e.  CC  /\  ( cos `  ( y  /  2 ) )  e.  CC )  -> 
( pi  x.  ( cos `  ( y  / 
2 ) ) )  e.  CC )
223221, 222syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( pi  x.  ( cos `  (
y  /  2 ) ) )  e.  CC )
224 eqid 2467 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  / 
2 ) ) ) )
225223, 224fmptd 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  / 
2 ) ) ) ) : CC --> CC )
226 fdm 5741 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) : CC --> CC  ->  dom  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  / 
2 ) ) ) )  =  CC )
227225, 226syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  =  CC )
228217, 227eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) )  =  CC )
22942, 228sseqtr4d 3546 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) ) )
23087, 229jca 532 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( CC  C_  CC  /\  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) ) ) )
231 dvres3 22185 . . . . . . . . . . . . . . 15  |-  ( ( ( RR  e.  { RR ,  CC }  /\  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) : CC --> CC )  /\  ( CC  C_  CC  /\  RR  C_  dom  ( CC  _D  (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) ) ) )  -> 
( RR  _D  (
( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )  |`  RR )
)  =  ( ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) )  |`  RR ) )
232196, 230, 231syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( RR  _D  (
( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )  |`  RR )
)  =  ( ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) )  |`  RR ) )
233215reseq1d 5278 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) )  |`  RR )  =  ( ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )  |`  RR ) )
234183, 232, 2333eqtrd 2512 . . . . . . . . . . . . 13  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )  |`  RR ) )
235 resmpt 5329 . . . . . . . . . . . . . . 15  |-  ( RR  C_  CC  ->  ( (
y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) )
23641, 235ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )
237236a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) ) )
238234, 237eqtrd 2508 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
239178, 238eqtrd 2508 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
240239reseq1d 5278 . . . . . . . . . 10  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) )  |`  (
( A (,) B
)  \  { Y } ) )  =  ( ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  |`  (
( A (,) B
)  \  { Y } ) ) )
241 resmpt 5329 . . . . . . . . . . 11  |-  ( ( ( A (,) B
)  \  { Y } )  C_  RR  ->  ( ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  |`  (
( A (,) B
)  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
2424, 241syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  |`  (
( A (,) B
)  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
243166, 240, 2423eqtrd 2512 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) )
244145, 165, 2433eqtrd 2512 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
245244eqcomd 2475 . . . . . . 7  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )  =  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
24628a1i 11 . . . . . . . . 9  |-  ( ph  ->  G  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) )
247246oveq2d 6311 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  G
)  =  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
248247eqcomd 2475 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  ( RR  _D  G ) )
249140, 245, 2483eqtrrd 2513 . . . . . 6  |-  ( ph  ->  ( RR  _D  G
)  =  I )
250249dmeqd 5211 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  G )  =  dom  I )
251131, 223syl 16 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( pi  x.  ( cos `  ( y  / 
2 ) ) )  e.  CC )
252251, 139fmptd 6056 . . . . . 6  |-  ( ph  ->  I : ( ( A (,) B ) 
\  { Y }
) --> CC )
253 fdm 5741 . . . . . 6  |-  ( I : ( ( A (,) B )  \  { Y } ) --> CC 
->  dom  I  =  ( ( A (,) B
)  \  { Y } ) )
254252, 253syl 16 . . . . 5  |-  ( ph  ->  dom  I  =  ( ( A (,) B
)  \  { Y } ) )
255250, 254eqtr2d 2509 . . . 4  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  =  dom  ( RR  _D  G
) )
256 eqimss 3561 . . . 4  |-  ( ( ( A (,) B
)  \  { Y } )  =  dom  ( RR  _D  G
)  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  G
) )
257255, 256syl 16 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  G
) )
258131, 81syl 16 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  y
)  e.  CC )
259258ralrimiva 2881 . . . . . . 7  |-  ( ph  ->  A. y  e.  ( ( A (,) B
)  \  { Y } ) ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
260 eqid 2467 . . . . . . . 8  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )
261260fnmpt 5713 . . . . . . 7  |-  ( A. y  e.  ( ( A (,) B )  \  { Y } ) ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC  ->  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  y ) )  Fn  ( ( A (,) B )  \  { Y } ) )
262259, 261syl 16 . . . . . 6  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  Fn  ( ( A (,) B )  \  { Y } ) )
263 eqidd 2468 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
264 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  y  =  w )  ->  y  =  w )
265264oveq2d 6311 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  y  =  w )  ->  ( ( N  +  ( 1  /  2
) )  x.  y
)  =  ( ( N  +  ( 1  /  2 ) )  x.  w ) )
266 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  w  e.  ( ( A (,) B )  \  { Y } ) )
26743adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  CC )
26844a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
1  e.  CC )
269268halfcld 10795 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 1  /  2
)  e.  CC )
270267, 269addcld 9627 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( N  +  ( 1  /  2 ) )  e.  CC )
2711sseli 3505 . . . . . . . . . . . . . 14  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  ( A (,) B ) )
2722sseli 3505 . . . . . . . . . . . . . 14  |-  ( w  e.  ( A (,) B )  ->  w  e.  RR )
273271, 272syl 16 . . . . . . . . . . . . 13  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  RR )
27441, 273sseldi 3507 . . . . . . . . . . . 12  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  CC )
275274adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  w  e.  CC )
276270, 275mulcld 9628 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  CC )
277263, 265, 266, 276fvmptd 5962 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w )  =  ( ( N  +  ( 1  /  2
) )  x.  w
) )
278 simpll 753 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ph )
279 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ( ( N  +  ( 1  / 
2 ) )  x.  w )  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )
280275adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  w  e.  CC )
28141, 67sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Y  e.  CC )
282278, 281syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  Y  e.  CC )
283 0re 9608 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
284283a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  e.  RR )
2855nnred 10563 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  RR )
2868a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  RR )
287286rehalfcld 10797 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
288285, 287readdcld 9635 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  RR )
2895nngt0d 10591 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  N )
290 2rp 11237 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  RR+
291290a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  e.  RR+ )
292291rpreccld 11278 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  /  2
)  e.  RR+ )
293285, 292ltaddrpd 11297 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  <  ( N  +  ( 1  / 
2 ) ) )
294284, 285, 288, 289, 293lttrd 9754 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  ( N  +  ( 1  / 
2 ) ) )
295284, 294gtned 9731 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  =/=  0 )
29648, 295jca 532 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  +  ( 1  /  2
) )  e.  CC  /\  ( N  +  ( 1  /  2 ) )  =/=  0 ) )
297296ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ( ( N  +  ( 1  / 
2 ) )  e.  CC  /\  ( N  +  ( 1  / 
2 ) )  =/=  0 ) )
298 mulcan 10198 . . . . . . . . . . . . . . 15  |-  ( ( w  e.  CC  /\  Y  e.  CC  /\  (
( N  +  ( 1  /  2 ) )  e.  CC  /\  ( N  +  (
1  /  2 ) )  =/=  0 ) )  ->  ( (
( N  +  ( 1  /  2 ) )  x.  w )  =  ( ( N  +  ( 1  / 
2 ) )  x.  Y )  <->  w  =  Y ) )
299280, 282, 297, 298syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ( ( ( N  +  ( 1  /  2 ) )  x.  w )  =  ( ( N  +  ( 1  /  2
) )  x.  Y
)  <->  w  =  Y
) )
300279, 299mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  w  =  Y )
301 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( w  =  Y  ->  (
w  mod  ( 2  x.  pi ) )  =  ( Y  mod  ( 2  x.  pi ) ) )
302301adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  =  Y )  ->  (
w  mod  ( 2  x.  pi ) )  =  ( Y  mod  ( 2  x.  pi ) ) )
303 dirkercncflem2.ymod . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Y  mod  (
2  x.  pi ) )  =  0 )
304303adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  =  Y )  ->  ( Y  mod  ( 2  x.  pi ) )  =  0 )
305302, 304eqtrd 2508 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  =  Y )  ->  (
w  mod  ( 2  x.  pi ) )  =  0 )
306278, 300, 305syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ( w  mod  ( 2  x.  pi ) )  =  0 )
307 nfv 1683 . . . . . . . . . . . . . . 15  |-  F/ y ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  ( w  mod  ( 2  x.  pi ) )  =/=  0
)
308 eleq1 2539 . . . . . . . . . . . . . . . . 17  |-  ( y  =  w  ->  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  <->  w  e.  (
( A (,) B
)  \  { Y } ) ) )
309308anbi2d 703 . . . . . . . . . . . . . . . 16  |-  ( y  =  w  ->  (
( ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  <->  ( ph  /\  w  e.  ( ( A (,) B ) 
\  { Y }
) ) ) )
310 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( y  =  w  ->  (
y  mod  ( 2  x.  pi ) )  =  ( w  mod  ( 2  x.  pi ) ) )
311310neeq1d 2744 . . . . . . . . . . . . . . . 16  |-  ( y  =  w  ->  (
( y  mod  (
2  x.  pi ) )  =/=  0  <->  (
w  mod  ( 2  x.  pi ) )  =/=  0 ) )
312309, 311imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
( ( ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  ( y  mod  ( 2  x.  pi ) )  =/=  0
)  <->  ( ( ph  /\  w  e.  ( ( A (,) B ) 
\  { Y }
) )  ->  (
w  mod  ( 2  x.  pi ) )  =/=  0 ) ) )
3131sseli 3505 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
y  e.  ( A (,) B ) )
314 elioore 11571 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( A (,) B )  ->  y  e.  RR )
315313, 314, 1673syl 20 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
y  e.  CC )
316146a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
2  e.  CC )
317147a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  ->  pi  e.  CC )
318152a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
2  =/=  0 )
319 pipos 22720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  pi
320283, 319gtneii 9708 . . . . . . . . . . . . . . . . . . . . . 22  |-  pi  =/=  0
321320a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  ->  pi  =/=  0 )
322315, 316, 317, 318, 321divdiv1d 10363 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
( ( y  / 
2 )  /  pi )  =  ( y  /  ( 2  x.  pi ) ) )
323322eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
( y  /  (
2  x.  pi ) )  =  ( ( y  /  2 )  /  pi ) )
324323adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  (
2  x.  pi ) )  =  ( ( y  /  2 )  /  pi ) )
325 dirkercncflem2.yne0 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
y  /  2 ) )  =/=  0 )
326325neneqd 2669 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( sin `  (
y  /  2 ) )  =  0 )
327130, 154syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  2
)  e.  CC )
328 sineq0 22780 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  /  2 )  e.  CC  ->  (
( sin `  (
y  /  2 ) )  =  0  <->  (
( y  /  2
)  /  pi )  e.  ZZ ) )
329327, 328syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( sin `  (
y  /  2 ) )  =  0  <->  (
( y  /  2
)  /  pi )  e.  ZZ ) )
330326, 329mtbid 300 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( y  / 
2 )  /  pi )  e.  ZZ )
331324, 330eqneltrd 2576 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( y  /  (
2  x.  pi ) )  e.  ZZ )
33218, 319pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( pi  e.  RR  /\  0  <  pi )
333 elrp 11234 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( pi  e.  RR+  <->  ( pi  e.  RR  /\  0  <  pi ) )
334332, 333mpbir 209 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  e.  RR+
335290, 334pm3.2i 455 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  e.  RR+  /\  pi  e.  RR+ )
336 rpmulcl 11253 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  e.  RR+  /\  pi  e.  RR+ )  ->  (
2  x.  pi )  e.  RR+ )
337335, 336ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  x.  pi )  e.  RR+
338337a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 2  x.  pi )  e.  RR+ )
339 mod0 11983 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  RR  /\  ( 2  x.  pi )  e.  RR+ )  -> 
( ( y  mod  ( 2  x.  pi ) )  =  0  <-> 
( y  /  (
2  x.  pi ) )  e.  ZZ ) )
34012, 338, 339syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  mod  ( 2  x.  pi ) )  =  0  <-> 
( y  /  (
2  x.  pi ) )  e.  ZZ ) )
341331, 340mtbird 301 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( y  mod  (
2  x.  pi ) )  =  0 )
342341neqned 2670 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  mod  (
2  x.  pi ) )  =/=  0 )
343307, 312, 342chvar 1982 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( w  mod  (
2  x.  pi ) )  =/=  0 )
344343neneqd 2669 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( w  mod  (
2  x.  pi ) )  =  0 )
345344adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  -.  ( w  mod  ( 2  x.  pi ) )  =  0 )
346306, 345pm2.65da 576 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )
34748, 281mulcld 9628 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  +  ( 1  /  2
) )  x.  Y
)  e.  CC )
348347adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  Y
)  e.  CC )
349 elsnc2g 4063 . . . . . . . . . . . 12  |-  ( ( ( N  +  ( 1  /  2 ) )  x.  Y )  e.  CC  ->  (
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) }  <->  ( ( N  +  ( 1  / 
2 ) )  x.  w )  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) ) )
350348, 349syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( ( N  +  ( 1  / 
2 ) )  x.  w )  e.  {
( ( N  +  ( 1  /  2
) )  x.  Y
) }  <->  ( ( N  +  ( 1  /  2 ) )  x.  w )  =  ( ( N  +  ( 1  /  2
) )  x.  Y
) ) )
351346, 350mtbird 301 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( N  +  ( 1  /  2
) )  x.  w
)  e.  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } )
352276, 351eldifd 3492 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  ( CC 
\  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } ) )
353277, 352eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w )  e.  ( CC  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } ) )
354 sinf 13737 . . . . . . . . . . . 12  |-  sin : CC
--> CC
355354fdmi 5742 . . . . . . . . . . 11  |-  dom  sin  =  CC
356355eqcomi 2480 . . . . . . . . . 10  |-  CC  =  dom  sin
357356a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  CC  =  dom  sin )
358357difeq1d 3626 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( CC  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } )  =  ( dom  sin  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } ) )
359353, 358eleqtrd 2557 . . . . . . 7  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w )  e.  ( dom  sin  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } ) )
360359ralrimiva 2881 . . . . . 6  |-  ( ph  ->  A. w  e.  ( ( A (,) B
)  \  { Y } ) ( ( y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) `  w )  e.  ( dom  sin  \  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } ) )
361 fnfvrnss 6060 . . . . . 6  |-  ( ( ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  Fn  ( ( A (,) B )  \  { Y } )  /\  A. w  e.  ( ( A (,) B ) 
\  { Y }
) ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `  w )  e.  ( dom  sin  \  { ( ( N  +  ( 1  / 
2 ) )  x.  Y ) } ) )  ->  ran  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  C_  ( dom  sin  \  { ( ( N  +  ( 1  / 
2 ) )  x.  Y ) } ) )
362262, 360, 361syl2anc 661 . . . . 5  |-  ( ph  ->  ran  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) 
C_  ( dom  sin  \  { ( ( N  +  ( 1  / 
2 ) )  x.  Y ) } ) )
363 id 22 . . . . . . . . 9  |-  ( ph  ->  ph )
364 uncom 3653 . . . . . . . . . . 11  |-  ( ( ( A (,) B
)  \  { Y } )  u.  { Y } )  =  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) )
365364a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } )  =  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) ) )
36632snssd 4178 . . . . . . . . . . 11  |-  ( ph  ->  { Y }  C_  ( A (,) B ) )
367 undif 3913 . . . . . . . . . . 11  |-  ( { Y }  C_  ( A (,) B )  <->  ( { Y }  u.  (
( A (,) B
)  \  { Y } ) )  =  ( A (,) B
) )
368366, 367sylib 196 . . . . . . . . . 10  |-  ( ph  ->  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) )  =  ( A (,) B
) )
369365, 368eqtrd 2508 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } )  =  ( A (,) B ) )
370363, 369syl 16 . . . . . . . 8  |-  ( ph  ->  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } )  =  ( A (,) B ) )
371370mpteq1d 4534 . . . . . . 7  |-  ( ph  ->  ( w  e.  ( ( ( A (,) B )  \  { Y } )  u.  { Y } )  |->  if ( w  =  Y , 
( ( N  +  ( 1  /  2
) )  x.  Y
) ,  ( ( y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) `  w ) ) )  =  ( w  e.  ( A (,) B
)  |->  if ( w  =  Y ,  ( ( N  +  ( 1  /  2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `  w ) ) ) )
372 iftrue 3951 . . . . . . . . . . . . 13  |-  ( w  =  Y  ->  if ( w  =  Y ,  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) )  =  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) )
373 oveq2 6303 . . . . . . . . . . . . . 14  |-  ( w  =  Y  ->  (
( N  +  ( 1  /  2 ) )  x.  w )  =  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) )
374373eqcomd 2475 . . . . . . . . . . . . 13  |-  ( w  =  Y  ->  (
( N  +  ( 1  /  2 ) )  x.  Y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
375372, 374eqtrd 2508 . . . . . . . . . . . 12  |-  ( w  =  Y  ->  if ( w  =  Y ,  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
376375adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  w  =  Y )  ->  if ( w  =  Y ,  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
377 iffalse 3954 . . . . . . . . . . . . 13  |-  ( -.  w  =  Y  ->  if ( w  =  Y ,  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) )  =  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `  w ) )
378377adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  if ( w  =  Y ,  ( ( N  +  ( 1  /  2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) )  =  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `  w ) )
379 eqidd 2468 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
380 oveq2 6303 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
( N  +  ( 1  /  2 ) )  x.  y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
381380adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  w  e.  ( A (,) B ) )  /\  -.  w  =  Y
)  /\  y  =  w )  ->  (
( N  +  ( 1  /  2 ) )  x.  y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
382 simpl 457 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  w  e.  ( A (,) B ) )
383 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( -.  w  =  Y  ->  -.  w  =  Y
)
384 elsn 4047 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  { Y }  <->  w  =  Y )
385383, 384sylnibr 305 . . . . . . . . . . . . . . . . 17  |-  ( -.  w  =  Y  ->  -.  w  e.  { Y } )
386385adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  -.  w  e.  { Y } )
387382, 386jca 532 . . . . . . . . . . . . . . 15  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  ( w  e.  ( A (,) B
)  /\  -.  w  e.  { Y } ) )
388 eldif 3491 . . . . . . . . . . . . . . 15  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  <->  ( w  e.  (