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

Theorem dirkercncflem2 37525
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
StepHypRef Expression
1 difss 3598 . . . . 5  |-  ( ( A (,) B ) 
\  { Y }
)  C_  ( A (,) B )
2 ioossre 11696 . . . . 5  |-  ( A (,) B )  C_  RR
31, 2sstri 3479 . . . 4  |-  ( ( A (,) B ) 
\  { Y }
)  C_  RR
43a1i 11 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  RR )
5 dirkercncflem2.n . . . . . . . . 9  |-  ( ph  ->  N  e.  NN )
65adantr 466 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  NN )
76nnred 10624 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  RR )
8 halfre 10828 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
98a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 1  /  2
)  e.  RR )
107, 9readdcld 9669 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( N  +  ( 1  /  2 ) )  e.  RR )
114sselda 3470 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
y  e.  RR )
1210, 11remulcld 9670 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  y
)  e.  RR )
1312resincld 14175 . . . 4  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) )  e.  RR )
14 dirkercncflem2.f . . . 4  |-  F  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )
1513, 14fmptd 6061 . . 3  |-  ( ph  ->  F : ( ( A (,) B ) 
\  { Y }
) --> RR )
16 2re 10679 . . . . . . 7  |-  2  e.  RR
17 pire 23269 . . . . . . 7  |-  pi  e.  RR
1816, 17remulcli 9656 . . . . . 6  |-  ( 2  x.  pi )  e.  RR
1918a1i 11 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 2  x.  pi )  e.  RR )
2011rehalfcld 10859 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  2
)  e.  RR )
2120resincld 14175 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
y  /  2 ) )  e.  RR )
2219, 21remulcld 9670 . . . 4  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) )  e.  RR )
23 dirkercncflem2.g . . . 4  |-  G  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )
2422, 23fmptd 6061 . . 3  |-  ( ph  ->  G : ( ( A (,) B ) 
\  { Y }
) --> RR )
25 iooretop 21688 . . . 4  |-  ( A (,) B )  e.  ( topGen `  ran  (,) )
2625a1i 11 . . 3  |-  ( ph  ->  ( A (,) B
)  e.  ( topGen ` 
ran  (,) ) )
27 dirkercncflem2.y . . 3  |-  ( ph  ->  Y  e.  ( A (,) B ) )
28 eqid 2429 . . 3  |-  ( ( A (,) B ) 
\  { Y }
)  =  ( ( A (,) B ) 
\  { Y }
)
2914a1i 11 . . . . . . . 8  |-  ( ph  ->  F  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
3029oveq2d 6321 . . . . . . 7  |-  ( ph  ->  ( RR  _D  F
)  =  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
31 resmpt 5174 . . . . . . . . . . . 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
) ) ) )
323, 31ax-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
) ) )
3332eqcomi 2442 . . . . . . . . . 10  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  =  ( ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  ( ( A (,) B )  \  { Y } ) )
3433a1i 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 } ) ) )
3534oveq2d 6321 . . . . . . . 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 } ) ) ) )
36 ax-resscn 9595 . . . . . . . . . 10  |-  RR  C_  CC
3736a1i 11 . . . . . . . . 9  |-  ( ph  ->  RR  C_  CC )
385nncnd 10625 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  CC )
39 halfcn 10829 . . . . . . . . . . . . . . 15  |-  ( 1  /  2 )  e.  CC
4039a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  /  2
)  e.  CC )
4138, 40addcld 9661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  CC )
4241adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
4337sselda 3470 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
4442, 43mulcld 9662 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
4544sincld 14162 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
46 eqid 2429 . . . . . . . . . 10  |-  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
4745, 46fmptd 6061 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : RR --> CC )
48 ssid 3489 . . . . . . . . . . 11  |-  RR  C_  RR
4948, 3pm3.2i 456 . . . . . . . . . 10  |-  ( RR  C_  RR  /\  ( ( A (,) B ) 
\  { Y }
)  C_  RR )
5049a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( RR  C_  RR  /\  ( ( A (,) B )  \  { Y } )  C_  RR ) )
51 eqid 2429 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5251tgioo2 21723 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
5351, 52dvres 22734 . . . . . . . . 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 } ) ) ) )
5437, 47, 50, 53syl21anc 1263 . . . . . . . 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 } ) ) ) )
55 retop 21684 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
56 rehaus 21719 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Haus
572, 27sseldi 3468 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
58 uniretop 21685 . . . . . . . . . . . . . 14  |-  RR  =  U. ( topGen `  ran  (,) )
5958sncld 20309 . . . . . . . . . . . . 13  |-  ( ( ( topGen `  ran  (,) )  e.  Haus  /\  Y  e.  RR )  ->  { Y }  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
6056, 57, 59sylancr 667 . . . . . . . . . . . 12  |-  ( ph  ->  { Y }  e.  ( Clsd `  ( topGen ` 
ran  (,) ) ) )
6158difopn 19971 . . . . . . . . . . . 12  |-  ( ( ( A (,) B
)  e.  ( topGen ` 
ran  (,) )  /\  { Y }  e.  ( Clsd `  ( topGen `  ran  (,) ) ) )  -> 
( ( A (,) B )  \  { Y } )  e.  (
topGen `  ran  (,) )
)
6225, 60, 61sylancr 667 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  e.  (
topGen `  ran  (,) )
)
63 isopn3i 20020 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( A (,) B ) 
\  { Y }
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) )  =  ( ( A (,) B )  \  { Y } ) )
6455, 62, 63sylancr 667 . . . . . . . . . 10  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) )  =  ( ( A (,) B )  \  { Y } ) )
6564reseq2d 5125 . . . . . . . . 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 } ) ) )
66 reelprrecn 9630 . . . . . . . . . . . . 13  |-  RR  e.  { RR ,  CC }
6766a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  { RR ,  CC } )
6841adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  CC )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
69 simpr 462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  CC )  ->  y  e.  CC )
7068, 69mulcld 9662 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
7170sincld 14162 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  CC )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
72 eqid 2429 . . . . . . . . . . . . 13  |-  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
7371, 72fmptd 6061 . . . . . . . . . . . 12  |-  ( ph  ->  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : CC --> CC )
74 ssid 3489 . . . . . . . . . . . . 13  |-  CC  C_  CC
7574a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  C_  CC )
76 dvsinax 37345 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) ) )
7741, 76syl 17 . . . . . . . . . . . . . . 15  |-  ( 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
) ) ) ) )
7877dmeqd 5057 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) )
79 eqid 2429 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
8070coscld 14163 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
8168, 80mulcld 9662 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  e.  CC )
8279, 81dmmptd 5726 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( y  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  CC )
8378, 82eqtrd 2470 . . . . . . . . . . . . 13  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  CC )
8436, 83syl5sseqr 3519 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
85 dvres3 22736 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
8667, 73, 75, 84, 85syl22anc 1265 . . . . . . . . . . 11  |-  ( 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 ) )
87 resmpt 5174 . . . . . . . . . . . . 13  |-  ( RR  C_  CC  ->  ( (
y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
8836, 87mp1i 13 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
8988oveq2d 6321 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )
)  =  ( RR 
_D  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
9077reseq1d 5124 . . . . . . . . . . . 12  |-  ( 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 ) )
91 resmpt 5174 . . . . . . . . . . . . 13  |-  ( 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
) ) ) ) )
9236, 91ax-mp 5 . . . . . . . . . . . 12  |-  ( ( 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
) ) ) )
9390, 92syl6eq 2486 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
9486, 89, 933eqtr3d 2478 . . . . . . . . . 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
) ) ) ) )
9594reseq1d 5124 . . . . . . . . 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 } ) ) )
96 resmpt 5174 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) )
973, 96mp1i 13 . . . . . . . . 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 ) ) ) ) )
9865, 95, 973eqtrd 2474 . . . . . . . 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
) ) ) ) )
9935, 54, 983eqtrd 2474 . . . . . . 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 ) ) ) ) )
100 dirkercncflem2.h . . . . . . . . 9  |-  H  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
101100a1i 11 . . . . . . . 8  |-  ( ph  ->  H  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
102101eqcomd 2437 . . . . . . 7  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  H )
10330, 99, 1023eqtrd 2474 . . . . . 6  |-  ( ph  ->  ( RR  _D  F
)  =  H )
104103dmeqd 5057 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  F )  =  dom  H )
10511recnd 9668 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
y  e.  CC )
106105, 81syldan 472 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) )  e.  CC )
107100, 106dmmptd 5726 . . . . 5  |-  ( ph  ->  dom  H  =  ( ( A (,) B
)  \  { Y } ) )
108104, 107eqtr2d 2471 . . . 4  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  =  dom  ( RR  _D  F
) )
109 eqimss 3522 . . . 4  |-  ( ( ( A (,) B
)  \  { Y } )  =  dom  ( RR  _D  F
)  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  F
) )
110108, 109syl 17 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  F
) )
111 dirkercncflem2.i . . . . . . . 8  |-  I  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )
112111a1i 11 . . . . . . 7  |-  ( ph  ->  I  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) )
113 resmpt 5174 . . . . . . . . . . . . 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 ) ) ) ) )
1143, 113ax-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 ) ) ) )
115114eqcomi 2442 . . . . . . . . . . 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 } ) )
116115oveq2i 6316 . . . . . . . . . 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 } ) ) )
117116a1i 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 } ) ) ) )
118 2cn 10680 . . . . . . . . . . . . . 14  |-  2  e.  CC
119 picn 23270 . . . . . . . . . . . . . 14  |-  pi  e.  CC
120118, 119mulcli 9647 . . . . . . . . . . . . 13  |-  ( 2  x.  pi )  e.  CC
121120a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( 2  x.  pi )  e.  CC )
12243halfcld 10857 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  /  2 )  e.  CC )
123122sincld 14162 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( sin `  ( y  /  2
) )  e.  CC )
124121, 123mulcld 9662 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) )  e.  CC )
125 eqid 2429 . . . . . . . . . . 11  |-  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
126124, 125fmptd 6061 . . . . . . . . . 10  |-  ( ph  ->  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) : RR --> CC )
12751, 52dvres 22734 . . . . . . . . . 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 } ) ) ) )
12837, 126, 50, 127syl21anc 1263 . . . . . . . . 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 } ) ) ) )
12964reseq2d 5125 . . . . . . . . . 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 } ) ) )
13036sseli 3466 . . . . . . . . . . . . . . . 16  |-  ( y  e.  RR  ->  y  e.  CC )
131 1cnd 9658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  1  e.  CC )
132 2cnd 10682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  2  e.  CC )
133 id 23 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  y  e.  CC )
134 2ne0 10702 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  =/=  0
135134a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  2  =/=  0 )
136131, 132, 133, 135div13d 10406 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( 1  /  2
)  x.  y )  =  ( ( y  /  2 )  x.  1 ) )
137 halfcl 10838 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  (
y  /  2 )  e.  CC )
138137mulid1d 9659 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( y  /  2
)  x.  1 )  =  ( y  / 
2 ) )
139136, 138eqtrd 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  CC  ->  (
( 1  /  2
)  x.  y )  =  ( y  / 
2 ) )
140139fveq2d 5885 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  CC  ->  ( sin `  ( ( 1  /  2 )  x.  y ) )  =  ( sin `  (
y  /  2 ) ) )
141140oveq2d 6321 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  ->  (
( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
142141eqcomd 2437 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
143130, 142syl 17 . . . . . . . . . . . . . . 15  |-  ( y  e.  RR  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
144143adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) )
145144mpteq2dva 4512 . . . . . . . . . . . . 13  |-  ( ph  ->  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) )
146145oveq2d 6321 . . . . . . . . . . . 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 ) ) ) ) ) )
147120a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  CC )  ->  ( 2  x.  pi )  e.  CC )
14839a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  CC )  ->  ( 1  /  2 )  e.  CC )
149148, 69mulcld 9662 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 1  /  2 )  x.  y )  e.  CC )
150149sincld 14162 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  CC )  ->  ( sin `  ( ( 1  / 
2 )  x.  y
) )  e.  CC )
151147, 150mulcld 9662 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) )  e.  CC )
152 eqid 2429 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
153151, 152fmptd 6061 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) : CC --> CC )
154 2cnd 10682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  e.  CC )
155119a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  pi  e.  CC )
156154, 155mulcld 9662 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 2  x.  pi )  e.  CC )
157 dvasinbx 37354 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) ) ) )
158156, 39, 157sylancl 666 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) ) )
159 2cnd 10682 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  2  e.  CC )
160119a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  pi  e.  CC )
161159, 160, 148mul32d 9842 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( 1  / 
2 ) )  =  ( ( 2  x.  ( 1  /  2
) )  x.  pi ) )
162134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  CC )  ->  2  =/=  0 )
163159, 162recidd 10377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  ( 2  x.  ( 1  / 
2 ) )  =  1 )
164163oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  ( 1  /  2 ) )  x.  pi )  =  ( 1  x.  pi ) )
165160mulid2d 9660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( 1  x.  pi )  =  pi )
166161, 164, 1653eqtrd 2474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( 1  / 
2 ) )  =  pi )
167139fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  ( cos `  ( ( 1  /  2 )  x.  y ) )  =  ( cos `  (
y  /  2 ) ) )
168167adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( ( 1  / 
2 )  x.  y
) )  =  ( cos `  ( y  /  2 ) ) )
169166, 168oveq12d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( 2  x.  pi )  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  y ) ) )  =  ( pi  x.  ( cos `  ( y  /  2
) ) ) )
170169mpteq2dva 4512 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( y  e.  CC  |->  ( ( ( 2  x.  pi )  x.  ( 1  /  2
) )  x.  ( cos `  ( ( 1  /  2 )  x.  y ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
171158, 170eqtrd 2470 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
172171dmeqd 5057 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) )
173 eqid 2429 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  / 
2 ) ) ) )
17469halfcld 10857 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( y  /  2 )  e.  CC )
175174coscld 14163 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( y  /  2
) )  e.  CC )
176160, 175mulcld 9662 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  ( pi  x.  ( cos `  (
y  /  2 ) ) )  e.  CC )
177173, 176dmmptd 5726 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  =  CC )
178172, 177eqtrd 2470 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) )  =  CC )
17936, 178syl5sseqr 3519 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) ) )
180 dvres3 22736 . . . . . . . . . . . . . . 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 ) )
18167, 153, 75, 179, 180syl22anc 1265 . . . . . . . . . . . . . 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 ) )
182 resmpt 5174 . . . . . . . . . . . . . . . 16  |-  ( 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
) ) ) ) )
18336, 182mp1i 13 . . . . . . . . . . . . . . 15  |-  ( 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
) ) ) ) )
184183oveq2d 6321 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) ) )
185171reseq1d 5124 . . . . . . . . . . . . . 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 ) )
186181, 184, 1853eqtr3d 2478 . . . . . . . . . . . . 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 ) )
187 resmpt 5174 . . . . . . . . . . . . . 14  |-  ( RR  C_  CC  ->  ( (
y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) ) )
18836, 187ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2
) ) ) )
189186, 188syl6eq 2486 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) ) )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
190146, 189eqtrd 2470 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
191190reseq1d 5124 . . . . . . . . . 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 } ) ) )
1924resmptd 5176 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e.  RR  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  |`  (
( A (,) B
)  \  { Y } ) )  =  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
193129, 191, 1923eqtrd 2474 . . . . . . . . 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
) ) ) ) )
194117, 128, 1933eqtrd 2474 . . . . . . . 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 ) ) ) ) )
195194eqcomd 2437 . . . . . . 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 ) ) ) ) ) )
19623a1i 11 . . . . . . . . 9  |-  ( ph  ->  G  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) )
197196oveq2d 6321 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  G
)  =  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
198197eqcomd 2437 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  ( RR  _D  G ) )
199112, 195, 1983eqtrrd 2475 . . . . . 6  |-  ( ph  ->  ( RR  _D  G
)  =  I )
200199dmeqd 5057 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  G )  =  dom  I )
201105, 176syldan 472 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( pi  x.  ( cos `  ( y  / 
2 ) ) )  e.  CC )
202111, 201dmmptd 5726 . . . . 5  |-  ( ph  ->  dom  I  =  ( ( A (,) B
)  \  { Y } ) )
203200, 202eqtr2d 2471 . . . 4  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  =  dom  ( RR  _D  G
) )
204 eqimss 3522 . . . 4  |-  ( ( ( A (,) B
)  \  { Y } )  =  dom  ( RR  _D  G
)  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  G
) )
205203, 204syl 17 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  G
) )
206105, 70syldan 472 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  y
)  e.  CC )
207206ralrimiva 2846 . . . . . . 7  |-  ( ph  ->  A. y  e.  ( ( A (,) B
)  \  { Y } ) ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
208 eqid 2429 . . . . . . . 8  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )
209208fnmpt 5722 . . . . . . 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 } ) )
210207, 209syl 17 . . . . . 6  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  Fn  ( ( A (,) B )  \  { Y } ) )
211 eqidd 2430 . . . . . . . . . 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 ) ) )
212 simpr 462 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  y  =  w )  ->  y  =  w )
213212oveq2d 6321 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  y  =  w )  ->  ( ( N  +  ( 1  /  2
) )  x.  y
)  =  ( ( N  +  ( 1  /  2 ) )  x.  w ) )
214 simpr 462 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  w  e.  ( ( A (,) B )  \  { Y } ) )
21538adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  CC )
216 1cnd 9658 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
1  e.  CC )
217216halfcld 10857 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 1  /  2
)  e.  CC )
218215, 217addcld 9661 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( N  +  ( 1  /  2 ) )  e.  CC )
219 eldifi 3593 . . . . . . . . . . . . . 14  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  ( A (,) B ) )
220 elioore 11666 . . . . . . . . . . . . . 14  |-  ( w  e.  ( A (,) B )  ->  w  e.  RR )
221219, 220syl 17 . . . . . . . . . . . . 13  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  RR )
222221recnd 9668 . . . . . . . . . . . 12  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  CC )
223222adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  w  e.  CC )
224218, 223mulcld 9662 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  CC )
225211, 213, 214, 224fvmptd 5970 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w )  =  ( ( N  +  ( 1  /  2
) )  x.  w
) )
226 eleq1 2501 . . . . . . . . . . . . . . . 16  |-  ( y  =  w  ->  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  <->  w  e.  (
( A (,) B
)  \  { Y } ) ) )
227226anbi2d 708 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
( ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  <->  ( ph  /\  w  e.  ( ( A (,) B ) 
\  { Y }
) ) ) )
228 oveq1 6312 . . . . . . . . . . . . . . . 16  |-  ( y  =  w  ->  (
y  mod  ( 2  x.  pi ) )  =  ( w  mod  ( 2  x.  pi ) ) )
229228neeq1d 2708 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
( y  mod  (
2  x.  pi ) )  =/=  0  <->  (
w  mod  ( 2  x.  pi ) )  =/=  0 ) )
230227, 229imbi12d 321 . . . . . . . . . . . . . 14  |-  ( 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 ) ) )
231 eldifi 3593 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
y  e.  ( A (,) B ) )
232 elioore 11666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( A (,) B )  ->  y  e.  RR )
233231, 232, 1303syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
y  e.  CC )
234 2cnd 10682 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
2  e.  CC )
235119a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  ->  pi  e.  CC )
236134a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
2  =/=  0 )
237 0re 9642 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
238 pipos 23271 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  pi
239237, 238gtneii 9745 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  =/=  0
240239a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  ->  pi  =/=  0 )
241233, 234, 235, 236, 240divdiv1d 10413 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
( ( y  / 
2 )  /  pi )  =  ( y  /  ( 2  x.  pi ) ) )
242241eqcomd 2437 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
( y  /  (
2  x.  pi ) )  =  ( ( y  /  2 )  /  pi ) )
243242adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  (
2  x.  pi ) )  =  ( ( y  /  2 )  /  pi ) )
244 dirkercncflem2.yne0 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
y  /  2 ) )  =/=  0 )
245244neneqd 2632 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( sin `  (
y  /  2 ) )  =  0 )
246105halfcld 10857 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  2
)  e.  CC )
247 sineq0 23332 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  /  2 )  e.  CC  ->  (
( sin `  (
y  /  2 ) )  =  0  <->  (
( y  /  2
)  /  pi )  e.  ZZ ) )
248246, 247syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( sin `  (
y  /  2 ) )  =  0  <->  (
( y  /  2
)  /  pi )  e.  ZZ ) )
249245, 248mtbid 301 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( y  / 
2 )  /  pi )  e.  ZZ )
250243, 249eqneltrd 2538 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( y  /  (
2  x.  pi ) )  e.  ZZ )
251 2rp 11307 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR+
252 pirp 23272 . . . . . . . . . . . . . . . . . 18  |-  pi  e.  RR+
253 rpmulcl 11324 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR+  /\  pi  e.  RR+ )  ->  (
2  x.  pi )  e.  RR+ )
254251, 252, 253mp2an 676 . . . . . . . . . . . . . . . . 17  |-  ( 2  x.  pi )  e.  RR+
255 mod0 12100 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  RR  /\  ( 2  x.  pi )  e.  RR+ )  -> 
( ( y  mod  ( 2  x.  pi ) )  =  0  <-> 
( y  /  (
2  x.  pi ) )  e.  ZZ ) )
25611, 254, 255sylancl 666 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  mod  ( 2  x.  pi ) )  =  0  <-> 
( y  /  (
2  x.  pi ) )  e.  ZZ ) )
257250, 256mtbird 302 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( y  mod  (
2  x.  pi ) )  =  0 )
258257neqned 2634 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  mod  (
2  x.  pi ) )  =/=  0 )
259230, 258chvarv 2070 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( w  mod  (
2  x.  pi ) )  =/=  0 )
260259neneqd 2632 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( w  mod  (
2  x.  pi ) )  =  0 )
261 simpll 758 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ph )
262 simpr 462 . . . . . . . . . . . . . 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 ) )
263222ad2antlr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  w  e.  CC )
26457recnd 9668 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Y  e.  CC )
265264ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  Y  e.  CC )
266 0red 9643 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  e.  RR )
2675nnred 10624 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  RR )
268 1red 9657 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  RR )
269268rehalfcld 10859 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
270267, 269readdcld 9669 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  RR )
2715nngt0d 10653 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  N )
272251a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  e.  RR+ )
273272rpreccld 11351 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  /  2
)  e.  RR+ )
274267, 273ltaddrpd 11371 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  <  ( N  +  ( 1  / 
2 ) ) )
275266, 267, 270, 271, 274lttrd 9795 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  ( N  +  ( 1  / 
2 ) ) )
276275gt0ne0d 10177 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  =/=  0 )
27741, 276jca 534 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  +  ( 1  /  2
) )  e.  CC  /\  ( N  +  ( 1  /  2 ) )  =/=  0 ) )
278277ad2antrr 730 . . . . . . . . . . . . . . 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 ) )
279 mulcan 10248 . . . . . . . . . . . . . . 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 ) )
280263, 265, 278, 279syl3anc 1264 . . . . . . . . . . . . . 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
) )
281262, 280mpbid 213 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  w  =  Y )
282 oveq1 6312 . . . . . . . . . . . . . 14  |-  ( w  =  Y  ->  (
w  mod  ( 2  x.  pi ) )  =  ( Y  mod  ( 2  x.  pi ) ) )
283 dirkercncflem2.ymod . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y  mod  (
2  x.  pi ) )  =  0 )
284282, 283sylan9eqr 2492 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  =  Y )  ->  (
w  mod  ( 2  x.  pi ) )  =  0 )
285261, 281, 284syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ( w  mod  ( 2  x.  pi ) )  =  0 )
286260, 285mtand 663 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )
28741, 264mulcld 9662 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  +  ( 1  /  2
) )  x.  Y
)  e.  CC )
288287adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  Y
)  e.  CC )
289 elsnc2g 4032 . . . . . . . . . . . 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 ) ) )
290288, 289syl 17 . . . . . . . . . . 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
) ) )
291286, 290mtbird 302 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( N  +  ( 1  /  2
) )  x.  w
)  e.  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } )
292224, 291eldifd 3453 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  ( CC 
\  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } ) )
293225, 292eqeltrd 2517 . . . . . . . 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
) } ) )
294 sinf 14156 . . . . . . . . . . . 12  |-  sin : CC
--> CC
295294fdmi 5751 . . . . . . . . . . 11  |-  dom  sin  =  CC
296295eqcomi 2442 . . . . . . . . . 10  |-  CC  =  dom  sin
297296a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  CC  =  dom  sin )
298297difeq1d 3588 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( CC  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } )  =  ( dom  sin  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } ) )
299293, 298eleqtrd 2519 . . . . . . 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
) } ) )
300299ralrimiva 2846 . . . . . 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 ) } ) )
301 fnfvrnss 6066 . . . . . 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 ) } ) )
302210, 300, 301syl2anc 665 . . . . 5  |-  ( ph  ->  ran  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) 
C_  ( dom  sin  \  { ( ( N  +  ( 1  / 
2 ) )  x.  Y ) } ) )
303 uncom 3616 . . . . . . . . . 10  |-  ( ( ( A (,) B
)  \  { Y } )  u.  { Y } )  =  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) )
304303a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } )  =  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) ) )
30527snssd 4148 . . . . . . . . . 10  |-  ( ph  ->  { Y }  C_  ( A (,) B ) )
306 undif 3882 . . . . . . . . . 10  |-  ( { Y }  C_  ( A (,) B )  <->  ( { Y }  u.  (
( A (,) B
)  \  { Y } ) )  =  ( A (,) B
) )
307305, 306sylib 199 . . . . . . . . 9  |-  ( ph  ->  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) )  =  ( A (,) B
) )
308304, 307eqtrd 2470 . . . . . . . 8  |-  ( ph  ->  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } )  =  ( A (,) B ) )
309308mpteq1d 4507 . . . . . . 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 ) ) ) )
310 iftrue 3921 . . . . . . . . . . . . 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 ) )
311 oveq2 6313 . . . . . . . . . . . . 13  |-  ( w  =  Y  ->  (
( N  +  ( 1  /  2 ) )  x.  w )  =  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) )
312310, 311eqtr4d 2473 . . . . . . . . . . . 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 ) )
313312adantl 467 . . . . . . . . . . 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 ) )
314 iffalse 3924 . . . . . . . . . . . . 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 ) )
315314adantl 467 . . . . . . . . . . . 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 ) )
316 eqidd 2430 . . . . . . . . . . . . 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 ) ) )
317 oveq2 6313 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
( N  +  ( 1  /  2 ) )  x.  y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
318317adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  w  e.  ( A (,) B ) )  /\  -.  w  =  Y
)  /\  y  =  w )  ->  (
( N  +  ( 1  /  2 ) )  x.  y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
319 simpl 458 . . . . . . . . . . . . . . 15  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  w  e.  ( A (,) B ) )
320 id 23 . . . . . . . . . . . . . . . . 17  |-  ( -.  w  =  Y  ->  -.  w  =  Y
)
321 elsn 4016 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  { Y }  <->  w  =  Y )
322320, 321sylnibr 306 . . . . . . . . . . . . . . . 16  |-  ( -.  w  =  Y  ->  -.  w  e.  { Y } )
323322adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  -.  w  e.  { Y } )
324319, 323eldifd 3453 . . . . . . . . . . . . . 14  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  w  e.  ( ( A (,) B )  \  { Y } ) )
325324adantll 718 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  w  e.  ( ( A (,) B ) 
\  { Y }
) )
32641adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
327220recnd 9668 . . . . . . . . . . . . . . . 16  |-  ( w  e.  ( A (,) B )  ->  w  e.  CC )
328327adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  w  e.  CC )
329326, 328mulcld 9662 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  ( ( N  +  ( 1  /  2 ) )  x.  w )  e.  CC )
330329adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  ( ( N  +  ( 1  /  2
) )  x.  w
)  e.  CC )
331316, 318, 325, 330fvmptd 5970 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w )  =  ( ( N  +  ( 1  /  2
) )  x.  w
) )
332315, 331eqtrd 2470 . . . . . . . . . . 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 ) )
333313, 332pm2.61dan 798 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  if (
w  =  Y , 
( ( N  +  ( 1  /  2
) )  x.  Y
) ,  ( ( y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) `  w ) )  =  ( ( N  +  ( 1  /  2
) )  x.  w
) )
334333mpteq2dva 4512 . . . . . . . . 9  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  if ( w  =  Y ,  ( ( N  +  ( 1  /  2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) ) )  =  ( w  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) ) )
335 ioosscn 37166 . . . . . . . . . . . . . 14  |-  ( A (,) B )  C_  CC
336 resmpt 5174 . . . . . . . . . . . . . 14  |-  ( ( A (,) B ) 
C_  CC  ->  ( ( w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  |`  ( A (,) B ) )  =  ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) ) )
337335, 336ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  |`  ( A (,) B ) )  =  ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )
338 eqid 2429 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  =  ( w  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
339338mulc1cncf 21824 . . . . . . . . . . . . . . . 16  |-  ( ( N  +  ( 1  /  2 ) )  e.  CC  ->  (
w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  e.  ( CC
-cn-> CC ) )
34041, 339syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( w  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( CC -cn-> CC ) )
34151cnfldtop 21706 . . . . . . . . . . . . . . . . . . 19  |-  ( TopOpen ` fld )  e.  Top
342 unicntop 37001 . . . . . . . . . . . . . . . . . . . 20  |-  CC  =  U. ( TopOpen ` fld )
343342restid 15282 . . . . . . . . . . . . . . . . . . 19  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
344341, 343ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
345344eqcomi 2442 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
34651, 345, 345cncfcn 21828 . . . . . . . . . . . . . . . 16  |-  ( ( CC  C_  CC  /\  CC  C_  CC )  ->  ( CC -cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
34774, 75, 346sylancr 667 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( CC -cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen ` fld ) ) )
348340, 347eleqtrd 2519 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( w  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
3492, 37syl5ss 3481 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A (,) B
)  C_  CC )
350342cnrest 20223 . . . . . . . . . . . . . 14  |-  ( ( ( w  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )  /\  ( A (,) B )  C_  CC )  ->  ( ( w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  |`  ( A (,) B ) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
351348, 349, 350syl2anc 665 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( w  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )  |`  ( A (,) B ) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
352337, 351syl5eqelr 2522 . . . . . . . . . . . 12  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
35351cnfldtopon 21705 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
354 resttopon 20099 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  ( A (,) B )  C_  CC )  ->  ( (
TopOpen ` fld )t  ( A (,) B
) )  e.  (TopOn `  ( A (,) B
) ) )
355353, 349, 354sylancr 667 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( TopOpen ` fld )t  ( A (,) B ) )  e.  (TopOn `  ( A (,) B ) ) )
356 cncnp 20218 . . . . . . . . . . . . 13  |-  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  e.  (TopOn `  ( A (,) B ) )  /\  ( TopOpen ` fld )  e.  (TopOn `  CC ) )  -> 
( ( w  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) )  <->  ( (
w  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) ) : ( A (,) B ) --> CC 
/\  A. y  e.  ( A (,) B ) ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
) ) ) )
357355, 353, 356sylancl 666 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( w  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) )  <->  ( (
w  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) ) : ( A (,) B ) --> CC 
/\  A. y  e.  ( A (,) B ) ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
) ) ) )
358352, 357mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( ( w  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) ) : ( A (,) B
) --> CC  /\  A. y  e.  ( A (,) B ) ( w  e.  ( A (,) B )  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
) ) )
359358simprd 464 . . . . . . . . . 10  |-  ( ph  ->  A. y  e.  ( A (,) B ) ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
) )
360 fveq2 5881 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  (
( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
)  =  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
361360eleq2d 2499 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
)  <->  ( w  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )  e.  ( ( ( (
TopOpen ` fld )t  ( A (,) B
) )  CnP  ( TopOpen
` fld
) ) `  Y
) ) )
362361rspccva 3187 . . . . . . . . . 10  |-  ( ( A. y  e.  ( A (,) B ) ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
)  /\  Y  e.  ( A (,) B ) )  ->  ( w  e.  ( A (,) B
)  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )  e.  ( ( ( (
TopOpen ` fld )t  ( A (,) B
) )  CnP  ( TopOpen
` fld
) ) `  Y
) )
363359, 27, 362syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
364334, 363eqeltrd 2517 . . . . . . . 8  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  if ( w  =  Y ,  ( ( N  +  ( 1  /  2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
365308eqcomd 2437 . . . . . . . . . . 11  |-  ( ph  ->  ( A (,) B
)  =  ( ( ( A (,) B
)  \  { Y } )  u.  { Y } ) )
366365oveq2d 6321 . . . . . . . . . 10  |-  ( ph  ->  ( ( TopOpen ` fld )t  ( A (,) B ) )  =  ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) ) )
367366oveq1d 6320 . . . . . . . . 9  |-  ( ph  ->  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) )  =  ( ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) )  CnP  ( TopOpen ` fld ) ) )
368367fveq1d 5883 . . . . . . . 8  |-  ( ph  ->  ( ( ( (
TopOpen ` fld )t  ( A (,) B
) )  CnP  ( TopOpen
` fld
) ) `  Y
)  =  ( ( ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
369364, 368eleqtrd 2519 . . . . . . 7  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  if ( w  =  Y ,  ( ( N  +  ( 1  /  2 ) )  x.  Y ) ,  ( ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) `
 w ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
370309, 369eqeltrd 2517 . . . . . 6  |-  ( 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 ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
371 eqid 2429 . . . . . . 7  |-  ( (
TopOpen ` fld )t  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } ) )  =  ( (
TopOpen ` fld )t  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } ) )
372 eqid 2429 . . . . . . 7  |-  ( w  e.  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } )  |->  if ( w  =  Y , 
( ( N  +  ( 1  /  2
) )  x.  Y
) ,  ( ( y  e.  ( (