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

Theorem dirkercncflem2 32052
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 3545 . . . . 5  |-  ( ( A (,) B ) 
\  { Y }
)  C_  ( A (,) B )
2 ioossre 11507 . . . . 5  |-  ( A (,) B )  C_  RR
31, 2sstri 3426 . . . 4  |-  ( ( A (,) B ) 
\  { Y }
)  C_  RR
43a1i 11 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  RR )
5 dirkercncflem2.n . . . . . . . . 9  |-  ( ph  ->  N  e.  NN )
65adantr 463 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  NN )
76nnred 10467 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  RR )
8 halfre 10671 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
98a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 1  /  2
)  e.  RR )
107, 9readdcld 9534 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( N  +  ( 1  /  2 ) )  e.  RR )
114sselda 3417 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
y  e.  RR )
1210, 11remulcld 9535 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  y
)  e.  RR )
1312resincld 13880 . . . 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 5957 . . 3  |-  ( ph  ->  F : ( ( A (,) B ) 
\  { Y }
) --> RR )
16 2re 10522 . . . . . . 7  |-  2  e.  RR
17 pire 22936 . . . . . . 7  |-  pi  e.  RR
1816, 17remulcli 9521 . . . . . 6  |-  ( 2  x.  pi )  e.  RR
1918a1i 11 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 2  x.  pi )  e.  RR )
2011rehalfcld 10702 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  2
)  e.  RR )
2120resincld 13880 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( sin `  (
y  /  2 ) )  e.  RR )
2219, 21remulcld 9535 . . . 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 5957 . . 3  |-  ( ph  ->  G : ( ( A (,) B ) 
\  { Y }
) --> RR )
25 iooretop 21358 . . . 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 2382 . . 3  |-  ( ( A (,) B ) 
\  { Y }
)  =  ( ( A (,) B ) 
\  { Y }
)
2914a1i 11 . . . . . . . 8  |-  ( ph  ->  F  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
3029oveq2d 6212 . . . . . . 7  |-  ( ph  ->  ( RR  _D  F
)  =  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) ) ) )
31 resmpt 5235 . . . . . . . . . . . 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 2395 . . . . . . . . . 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 6212 . . . . . . . 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 9460 . . . . . . . . . 10  |-  RR  C_  CC
3736a1i 11 . . . . . . . . 9  |-  ( ph  ->  RR  C_  CC )
385nncnd 10468 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  CC )
39 halfcn 10672 . . . . . . . . . . . . . . 15  |-  ( 1  /  2 )  e.  CC
4039a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  /  2
)  e.  CC )
4138, 40addcld 9526 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  CC )
4241adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
4337sselda 3417 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
4442, 43mulcld 9527 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
4544sincld 13867 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
46 eqid 2382 . . . . . . . . . 10  |-  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
4745, 46fmptd 5957 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  RR  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : RR --> CC )
48 ssid 3436 . . . . . . . . . . 11  |-  RR  C_  RR
4948, 3pm3.2i 453 . . . . . . . . . 10  |-  ( RR  C_  RR  /\  ( ( A (,) B ) 
\  { Y }
)  C_  RR )
5049a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( RR  C_  RR  /\  ( ( A (,) B )  \  { Y } )  C_  RR ) )
51 eqid 2382 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5251tgioo2 21393 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
5351, 52dvres 22400 . . . . . . . . 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 1225 . . . . . . . 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 21353 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
56 rehaus 21389 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Haus
572, 27sseldi 3415 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
58 uniretop 21354 . . . . . . . . . . . . . 14  |-  RR  =  U. ( topGen `  ran  (,) )
5958sncld 19958 . . . . . . . . . . . . 13  |-  ( ( ( topGen `  ran  (,) )  e.  Haus  /\  Y  e.  RR )  ->  { Y }  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
6056, 57, 59sylancr 661 . . . . . . . . . . . 12  |-  ( ph  ->  { Y }  e.  ( Clsd `  ( topGen ` 
ran  (,) ) ) )
6158difopn 19620 . . . . . . . . . . . 12  |-  ( ( ( A (,) B
)  e.  ( topGen ` 
ran  (,) )  /\  { Y }  e.  ( Clsd `  ( topGen `  ran  (,) ) ) )  -> 
( ( A (,) B )  \  { Y } )  e.  (
topGen `  ran  (,) )
)
6225, 60, 61sylancr 661 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  e.  (
topGen `  ran  (,) )
)
63 isopn3i 19669 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( A (,) B ) 
\  { Y }
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) )  =  ( ( A (,) B )  \  { Y } ) )
6455, 62, 63sylancr 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  \  { Y } ) )  =  ( ( A (,) B )  \  { Y } ) )
6564reseq2d 5186 . . . . . . . . 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 9495 . . . . . . . . . . . . 13  |-  RR  e.  { RR ,  CC }
6766a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  { RR ,  CC } )
6841adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  CC )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
69 simpr 459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  CC )  ->  y  e.  CC )
7068, 69mulcld 9527 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
7170sincld 13867 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  CC )  ->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
72 eqid 2382 . . . . . . . . . . . . 13  |-  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2
) )  x.  y
) ) )  =  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) )
7371, 72fmptd 5957 . . . . . . . . . . . 12  |-  ( ph  ->  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) : CC --> CC )
74 ssid 3436 . . . . . . . . . . . . 13  |-  CC  C_  CC
7574a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  C_  CC )
76 dvsinax 31874 . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . 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 5118 . . . . . . . . . . . . . 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 2382 . . . . . . . . . . . . . . 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 13868 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( ( N  +  ( 1  /  2
) )  x.  y
) )  e.  CC )
8168, 80mulcld 9527 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  e.  CC )
8279, 81dmmptd 5619 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( y  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  CC )
8378, 82eqtrd 2423 . . . . . . . . . . . . 13  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  CC )
8436, 83syl5sseqr 3466 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) ) )
85 dvres3 22402 . . . . . . . . . . . 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 1227 . . . . . . . . . . 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 5235 . . . . . . . . . . . . 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 12 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  CC  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) )  |`  RR )  =  ( y  e.  RR  |->  ( sin `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )
8988oveq2d 6212 . . . . . . . . . . 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 5185 . . . . . . . . . . . 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 5235 . . . . . . . . . . . . 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 2439 . . . . . . . . . . 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 2431 . . . . . . . . . 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 5185 . . . . . . . . 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 5235 . . . . . . . . . 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 12 . . . . . . . . 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 2427 . . . . . . . 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 2427 . . . . . . 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 2390 . . . . . . 7  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  ( cos `  (
( N  +  ( 1  /  2 ) )  x.  y ) ) ) )  =  H )
10330, 99, 1023eqtrd 2427 . . . . . 6  |-  ( ph  ->  ( RR  _D  F
)  =  H )
104103dmeqd 5118 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  F )  =  dom  H )
10511recnd 9533 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
y  e.  CC )
106105, 81syldan 468 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  ( cos `  ( ( N  +  ( 1  / 
2 ) )  x.  y ) ) )  e.  CC )
107100, 106dmmptd 5619 . . . . 5  |-  ( ph  ->  dom  H  =  ( ( A (,) B
)  \  { Y } ) )
108104, 107eqtr2d 2424 . . . 4  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  =  dom  ( RR  _D  F
) )
109 eqimss 3469 . . . 4  |-  ( ( ( A (,) B
)  \  { Y } )  =  dom  ( RR  _D  F
)  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  F
) )
110108, 109syl 16 . . 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 5235 . . . . . . . . . . . . 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 2395 . . . . . . . . . . 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 6207 . . . . . . . . . 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 10523 . . . . . . . . . . . . . 14  |-  2  e.  CC
119 picn 22937 . . . . . . . . . . . . . 14  |-  pi  e.  CC
120118, 119mulcli 9512 . . . . . . . . . . . . 13  |-  ( 2  x.  pi )  e.  CC
121120a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( 2  x.  pi )  e.  CC )
12243halfcld 10700 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  /  2 )  e.  CC )
123122sincld 13867 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( sin `  ( y  /  2
) )  e.  CC )
124121, 123mulcld 9527 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) )  e.  CC )
125 eqid 2382 . . . . . . . . . . 11  |-  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
126124, 125fmptd 5957 . . . . . . . . . 10  |-  ( ph  ->  ( y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) ) : RR --> CC )
12751, 52dvres 22400 . . . . . . . . . 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 1225 . . . . . . . . 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 5186 . . . . . . . . . 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 3413 . . . . . . . . . . . . . . . 16  |-  ( y  e.  RR  ->  y  e.  CC )
131 1cnd 9523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  1  e.  CC )
132 2cnd 10525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  2  e.  CC )
133 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  y  e.  CC )
134 2ne0 10545 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  =/=  0
135134a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  2  =/=  0 )
136131, 132, 133, 135div13d 10261 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( 1  /  2
)  x.  y )  =  ( ( y  /  2 )  x.  1 ) )
137 halfcl 10681 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  (
y  /  2 )  e.  CC )
138137mulid1d 9524 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( y  /  2
)  x.  1 )  =  ( y  / 
2 ) )
139136, 138eqtrd 2423 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  CC  ->  (
( 1  /  2
)  x.  y )  =  ( y  / 
2 ) )
140139fveq2d 5778 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  CC  ->  ( sin `  ( ( 1  /  2 )  x.  y ) )  =  ( sin `  (
y  /  2 ) ) )
141140oveq2d 6212 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  CC  ->  (
( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( y  / 
2 ) ) ) )
142141eqcomd 2390 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
143130, 142syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  RR  ->  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) )
144143adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) )  =  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  / 
2 )  x.  y
) ) ) )
145144mpteq2dva 4453 . . . . . . . . . . . . 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 6212 . . . . . . . . . . . 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 9527 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 1  /  2 )  x.  y )  e.  CC )
150149sincld 13867 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  CC )  ->  ( sin `  ( ( 1  / 
2 )  x.  y
) )  e.  CC )
151147, 150mulcld 9527 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) )  e.  CC )
152 eqid 2382 . . . . . . . . . . . . . . . 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 5957 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) : CC --> CC )
154 2cnd 10525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  e.  CC )
155119a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  pi  e.  CC )
156154, 155mulcld 9527 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 2  x.  pi )  e.  CC )
157 dvasinbx 31883 . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . 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 10525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  2  e.  CC )
160119a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  pi  e.  CC )
161159, 160, 148mul32d 9701 . . . . . . . . . . . . . . . . . . . . . 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 10232 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  CC )  ->  ( 2  x.  ( 1  / 
2 ) )  =  1 )
164163oveq1d 6211 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  ( 1  /  2 ) )  x.  pi )  =  ( 1  x.  pi ) )
165160mulid2d 9525 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  CC )  ->  ( 1  x.  pi )  =  pi )
166161, 164, 1653eqtrd 2427 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( 2  x.  pi )  x.  ( 1  / 
2 ) )  =  pi )
167139fveq2d 5778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  ( cos `  ( ( 1  /  2 )  x.  y ) )  =  ( cos `  (
y  /  2 ) ) )
168167adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( ( 1  / 
2 )  x.  y
) )  =  ( cos `  ( y  /  2 ) ) )
169166, 168oveq12d 6214 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( 2  x.  pi )  x.  ( 1  /  2 ) )  x.  ( cos `  (
( 1  /  2
)  x.  y ) ) )  =  ( pi  x.  ( cos `  ( y  /  2
) ) ) )
170169mpteq2dva 4453 . . . . . . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . 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 5118 . . . . . . . . . . . . . . . . 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 2382 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  CC  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) )  =  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  / 
2 ) ) ) )
17469halfcld 10700 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  CC )  ->  ( y  /  2 )  e.  CC )
175174coscld 13868 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  CC )  ->  ( cos `  ( y  /  2
) )  e.  CC )
176160, 175mulcld 9527 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  CC )  ->  ( pi  x.  ( cos `  (
y  /  2 ) ) )  e.  CC )
177173, 176dmmptd 5619 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( y  e.  CC  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )  =  CC )
178172, 177eqtrd 2423 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( CC  _D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  ( ( 1  /  2 )  x.  y ) ) ) ) )  =  CC )
17936, 178syl5sseqr 3466 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  dom  ( CC 
_D  ( y  e.  CC  |->  ( ( 2  x.  pi )  x.  ( sin `  (
( 1  /  2
)  x.  y ) ) ) ) ) )
180 dvres3 22402 . . . . . . . . . . . . . . 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 1227 . . . . . . . . . . . . . 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 5235 . . . . . . . . . . . . . . . 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 12 . . . . . . . . . . . . . . 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 6212 . . . . . . . . . . . . . 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 5185 . . . . . . . . . . . . . 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 2431 . . . . . . . . . . . . 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 5235 . . . . . . . . . . . . . 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 2439 . . . . . . . . . . . 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 2423 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) )  =  ( y  e.  RR  |->  ( pi  x.  ( cos `  (
y  /  2 ) ) ) ) )
191190reseq1d 5185 . . . . . . . . . 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 5237 . . . . . . . . . 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 2427 . . . . . . . . 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 2427 . . . . . . . 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 2390 . . . . . . 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 6212 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  G
)  =  ( RR 
_D  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
198197eqcomd 2390 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  |->  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  ( RR  _D  G ) )
199112, 195, 1983eqtrrd 2428 . . . . . 6  |-  ( ph  ->  ( RR  _D  G
)  =  I )
200199dmeqd 5118 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  G )  =  dom  I )
201105, 176syldan 468 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( pi  x.  ( cos `  ( y  / 
2 ) ) )  e.  CC )
202111, 201dmmptd 5619 . . . . 5  |-  ( ph  ->  dom  I  =  ( ( A (,) B
)  \  { Y } ) )
203200, 202eqtr2d 2424 . . . 4  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  =  dom  ( RR  _D  G
) )
204 eqimss 3469 . . . 4  |-  ( ( ( A (,) B
)  \  { Y } )  =  dom  ( RR  _D  G
)  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  G
) )
205203, 204syl 16 . . 3  |-  ( ph  ->  ( ( A (,) B )  \  { Y } )  C_  dom  ( RR  _D  G
) )
206105, 70syldan 468 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  y
)  e.  CC )
207206ralrimiva 2796 . . . . . . 7  |-  ( ph  ->  A. y  e.  ( ( A (,) B
)  \  { Y } ) ( ( N  +  ( 1  /  2 ) )  x.  y )  e.  CC )
208 eqid 2382 . . . . . . . 8  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  =  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )
209208fnmpt 5615 . . . . . . 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 16 . . . . . 6  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) )  Fn  ( ( A (,) B )  \  { Y } ) )
211 eqidd 2383 . . . . . . . . . 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 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  y  =  w )  ->  y  =  w )
213212oveq2d 6212 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  y  =  w )  ->  ( ( N  +  ( 1  /  2
) )  x.  y
)  =  ( ( N  +  ( 1  /  2 ) )  x.  w ) )
214 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  w  e.  ( ( A (,) B )  \  { Y } ) )
21538adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  N  e.  CC )
216 1cnd 9523 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
1  e.  CC )
217216halfcld 10700 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( 1  /  2
)  e.  CC )
218215, 217addcld 9526 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( N  +  ( 1  /  2 ) )  e.  CC )
219 eldifi 3540 . . . . . . . . . . . . . 14  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  ( A (,) B ) )
220 elioore 11480 . . . . . . . . . . . . . 14  |-  ( w  e.  ( A (,) B )  ->  w  e.  RR )
221219, 220syl 16 . . . . . . . . . . . . 13  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  RR )
222221recnd 9533 . . . . . . . . . . . 12  |-  ( w  e.  ( ( A (,) B )  \  { Y } )  ->  w  e.  CC )
223222adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  w  e.  CC )
224218, 223mulcld 9527 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  CC )
225211, 213, 214, 224fvmptd 5862 . . . . . . . . 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 2454 . . . . . . . . . . . . . . . 16  |-  ( y  =  w  ->  (
y  e.  ( ( A (,) B ) 
\  { Y }
)  <->  w  e.  (
( A (,) B
)  \  { Y } ) ) )
227226anbi2d 701 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
( ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  <->  ( ph  /\  w  e.  ( ( A (,) B ) 
\  { Y }
) ) ) )
228 oveq1 6203 . . . . . . . . . . . . . . . 16  |-  ( y  =  w  ->  (
y  mod  ( 2  x.  pi ) )  =  ( w  mod  ( 2  x.  pi ) ) )
229228neeq1d 2659 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
( y  mod  (
2  x.  pi ) )  =/=  0  <->  (
w  mod  ( 2  x.  pi ) )  =/=  0 ) )
230227, 229imbi12d 318 . . . . . . . . . . . . . 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 3540 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
y  e.  ( A (,) B ) )
232 elioore 11480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( A (,) B )  ->  y  e.  RR )
233231, 232, 1303syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
y  e.  CC )
234 2cnd 10525 . . . . . . . . . . . . . . . . . . . 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 9507 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
238 pipos 22938 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  pi
239237, 238gtneii 9607 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  =/=  0
240239a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  ->  pi  =/=  0 )
241233, 234, 235, 236, 240divdiv1d 10268 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
( ( y  / 
2 )  /  pi )  =  ( y  /  ( 2  x.  pi ) ) )
242241eqcomd 2390 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( ( A (,) B )  \  { Y } )  -> 
( y  /  (
2  x.  pi ) )  =  ( ( y  /  2 )  /  pi ) )
243242adantl 464 . . . . . . . . . . . . . . . . 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 2584 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( sin `  (
y  /  2 ) )  =  0 )
246105halfcld 10700 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  /  2
)  e.  CC )
247 sineq0 22999 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  /  2 )  e.  CC  ->  (
( sin `  (
y  /  2 ) )  =  0  <->  (
( y  /  2
)  /  pi )  e.  ZZ ) )
248246, 247syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( sin `  (
y  /  2 ) )  =  0  <->  (
( y  /  2
)  /  pi )  e.  ZZ ) )
249245, 248mtbid 298 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( y  / 
2 )  /  pi )  e.  ZZ )
250243, 249eqneltrd 2491 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( y  /  (
2  x.  pi ) )  e.  ZZ )
251 2rp 11144 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR+
252 pirp 22939 . . . . . . . . . . . . . . . . . 18  |-  pi  e.  RR+
253 rpmulcl 11161 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR+  /\  pi  e.  RR+ )  ->  (
2  x.  pi )  e.  RR+ )
254251, 252, 253mp2an 670 . . . . . . . . . . . . . . . . 17  |-  ( 2  x.  pi )  e.  RR+
255 mod0 11903 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  RR  /\  ( 2  x.  pi )  e.  RR+ )  -> 
( ( y  mod  ( 2  x.  pi ) )  =  0  <-> 
( y  /  (
2  x.  pi ) )  e.  ZZ ) )
25611, 254, 255sylancl 660 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( y  mod  ( 2  x.  pi ) )  =  0  <-> 
( y  /  (
2  x.  pi ) )  e.  ZZ ) )
257250, 256mtbird 299 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( y  mod  (
2  x.  pi ) )  =  0 )
258257neqned 2585 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( y  mod  (
2  x.  pi ) )  =/=  0 )
259230, 258chvarv 2021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( w  mod  (
2  x.  pi ) )  =/=  0 )
260259neneqd 2584 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( w  mod  (
2  x.  pi ) )  =  0 )
261 simpll 751 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  ph )
262 simpr 459 . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  w  e.  CC )
26457recnd 9533 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Y  e.  CC )
265264ad2antrr 723 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  Y  e.  CC )
266 0red 9508 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  e.  RR )
2675nnred 10467 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  RR )
268 1red 9522 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  RR )
269268rehalfcld 10702 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
270267, 269readdcld 9534 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  e.  RR )
2715nngt0d 10496 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  N )
272251a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  e.  RR+ )
273272rpreccld 11187 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  /  2
)  e.  RR+ )
274267, 273ltaddrpd 11206 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  <  ( N  +  ( 1  / 
2 ) ) )
275266, 267, 270, 271, 274lttrd 9654 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  ( N  +  ( 1  / 
2 ) ) )
276275gt0ne0d 10034 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  +  ( 1  /  2 ) )  =/=  0 )
27741, 276jca 530 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  +  ( 1  /  2
) )  e.  CC  /\  ( N  +  ( 1  /  2 ) )  =/=  0 ) )
278277ad2antrr 723 . . . . . . . . . . . . . . 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 10103 . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  /\  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )  ->  w  =  Y )
282 oveq1 6203 . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  =  Y )  ->  (
w  mod  ( 2  x.  pi ) )  =  0 )
285261, 281, 284syl2anc 659 . . . . . . . . . . . 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 657 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( N  +  ( 1  /  2
) )  x.  w
)  =  ( ( N  +  ( 1  /  2 ) )  x.  Y ) )
28741, 264mulcld 9527 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  +  ( 1  /  2
) )  x.  Y
)  e.  CC )
288287adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  Y
)  e.  CC )
289 elsnc2g 3974 . . . . . . . . . . . 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 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
) ) )
291286, 290mtbird 299 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  -.  ( ( N  +  ( 1  /  2
) )  x.  w
)  e.  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } )
292224, 291eldifd 3400 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( ( N  +  ( 1  /  2
) )  x.  w
)  e.  ( CC 
\  { ( ( N  +  ( 1  /  2 ) )  x.  Y ) } ) )
293225, 292eqeltrd 2470 . . . . . . . 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 13861 . . . . . . . . . . . 12  |-  sin : CC
--> CC
295294fdmi 5644 . . . . . . . . . . 11  |-  dom  sin  =  CC
296295eqcomi 2395 . . . . . . . . . 10  |-  CC  =  dom  sin
297296a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  ->  CC  =  dom  sin )
298297difeq1d 3535 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( ( A (,) B )  \  { Y } ) )  -> 
( CC  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } )  =  ( dom  sin  \  {
( ( N  +  ( 1  /  2
) )  x.  Y
) } ) )
299293, 298eleqtrd 2472 . . . . . . 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 2796 . . . . . 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 5961 . . . . . 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 659 . . . . 5  |-  ( ph  ->  ran  ( y  e.  ( ( A (,) B )  \  { Y } )  |->  ( ( N  +  ( 1  /  2 ) )  x.  y ) ) 
C_  ( dom  sin  \  { ( ( N  +  ( 1  / 
2 ) )  x.  Y ) } ) )
303 uncom 3562 . . . . . . . . . 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 4089 . . . . . . . . . 10  |-  ( ph  ->  { Y }  C_  ( A (,) B ) )
306 undif 3824 . . . . . . . . . 10  |-  ( { Y }  C_  ( A (,) B )  <->  ( { Y }  u.  (
( A (,) B
)  \  { Y } ) )  =  ( A (,) B
) )
307305, 306sylib 196 . . . . . . . . 9  |-  ( ph  ->  ( { Y }  u.  ( ( A (,) B )  \  { Y } ) )  =  ( A (,) B
) )
308304, 307eqtrd 2423 . . . . . . . 8  |-  ( ph  ->  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } )  =  ( A (,) B ) )
309308mpteq1d 4448 . . . . . . 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 3863 . . . . . . . . . . . . 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 6204 . . . . . . . . . . . . 13  |-  ( w  =  Y  ->  (
( N  +  ( 1  /  2 ) )  x.  w )  =  ( ( N  +  ( 1  / 
2 ) )  x.  Y ) )
312310, 311eqtr4d 2426 . . . . . . . . . . . 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 464 . . . . . . . . . . 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 3866 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 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 2383 . . . . . . . . . . . . 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 6204 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
( N  +  ( 1  /  2 ) )  x.  y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
318317adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  w  e.  ( A (,) B ) )  /\  -.  w  =  Y
)  /\  y  =  w )  ->  (
( N  +  ( 1  /  2 ) )  x.  y )  =  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
319 simpl 455 . . . . . . . . . . . . . . 15  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  w  e.  ( A (,) B ) )
320 id 22 . . . . . . . . . . . . . . . . 17  |-  ( -.  w  =  Y  ->  -.  w  =  Y
)
321 elsn 3958 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  { Y }  <->  w  =  Y )
322320, 321sylnibr 303 . . . . . . . . . . . . . . . 16  |-  ( -.  w  =  Y  ->  -.  w  e.  { Y } )
323322adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  -.  w  e.  { Y } )
324319, 323eldifd 3400 . . . . . . . . . . . . . 14  |-  ( ( w  e.  ( A (,) B )  /\  -.  w  =  Y
)  ->  w  e.  ( ( A (,) B )  \  { Y } ) )
325324adantll 711 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  w  e.  ( ( A (,) B ) 
\  { Y }
) )
32641adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  ( N  +  ( 1  / 
2 ) )  e.  CC )
327220recnd 9533 . . . . . . . . . . . . . . . 16  |-  ( w  e.  ( A (,) B )  ->  w  e.  CC )
328327adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  w  e.  CC )
329326, 328mulcld 9527 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  e.  ( A (,) B ) )  ->  ( ( N  +  ( 1  /  2 ) )  x.  w )  e.  CC )
330329adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( A (,) B
) )  /\  -.  w  =  Y )  ->  ( ( N  +  ( 1  /  2
) )  x.  w
)  e.  CC )
331316, 318, 325, 330fvmptd 5862 . . . . . . . . . . . 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 2423 . . . . . . . . . . 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 789 . . . . . . . . . 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 4453 . . . . . . . . 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 31693 . . . . . . . . . . . . . 14  |-  ( A (,) B )  C_  CC
336 resmpt 5235 . . . . . . . . . . . . . 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 2382 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  =  ( w  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )
339338mulc1cncf 21494 . . . . . . . . . . . . . . . 16  |-  ( ( N  +  ( 1  /  2 ) )  e.  CC  ->  (
w  e.  CC  |->  ( ( N  +  ( 1  /  2 ) )  x.  w ) )  e.  ( CC
-cn-> CC ) )
34041, 339syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( w  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( CC -cn-> CC ) )
34151cnfldtop 21376 . . . . . . . . . . . . . . . . . . 19  |-  ( TopOpen ` fld )  e.  Top
342 unicntop 31598 . . . . . . . . . . . . . . . . . . . 20  |-  CC  =  U. ( TopOpen ` fld )
343342restid 14841 . . . . . . . . . . . . . . . . . . 19  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
344341, 343ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
345344eqcomi 2395 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
34651, 345, 345cncfcn 21498 . . . . . . . . . . . . . . . 16  |-  ( ( CC  C_  CC  /\  CC  C_  CC )  ->  ( CC -cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
34774, 75, 346sylancr 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( CC -cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen ` fld ) ) )
348340, 347eleqtrd 2472 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( w  e.  CC  |->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
3492, 37syl5ss 3428 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A (,) B
)  C_  CC )
350342cnrest 19872 . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( w  e.  CC  |->  ( ( N  +  ( 1  / 
2 ) )  x.  w ) )  |`  ( A (,) B ) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
352337, 351syl5eqelr 2475 . . . . . . . . . . . 12  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
35351cnfldtopon 21375 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
354 resttopon 19748 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  ( A (,) B )  C_  CC )  ->  ( (
TopOpen ` fld )t  ( A (,) B
) )  e.  (TopOn `  ( A (,) B
) ) )
355353, 349, 354sylancr 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( TopOpen ` fld )t  ( A (,) B ) )  e.  (TopOn `  ( A (,) B ) ) )
356 cncnp 19867 . . . . . . . . . . . . 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 660 . . . . . . . . . . . 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 210 . . . . . . . . . . 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 461 . . . . . . . . . 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 5774 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  (
( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
)  =  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
361360eleq2d 2452 . . . . . . . . . . 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 3134 . . . . . . . . . 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 659 . . . . . . . . 9  |-  ( ph  ->  ( w  e.  ( A (,) B ) 
|->  ( ( N  +  ( 1  /  2
) )  x.  w
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  Y
) )
364334, 363eqeltrd 2470 . . . . . . . 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 2390 . . . . . . . . . . 11  |-  ( ph  ->  ( A (,) B
)  =  ( ( ( A (,) B
)  \  { Y } )  u.  { Y } ) )
366365oveq2d 6212 . . . . . . . . . 10  |-  ( ph  ->  ( ( TopOpen ` fld )t  ( A (,) B ) )  =  ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) ) )
367366oveq1d 6211 . . . . . . . . 9  |-  ( ph  ->  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) )  =  ( ( ( TopOpen ` fld )t  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } ) )  CnP  ( TopOpen ` fld ) ) )
368367fveq1d 5776 . . . . . . . 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 2472 . . . . . . 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 2470 . . . . . 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 2382 . . . . . . 7  |-  ( (
TopOpen ` fld )t  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } ) )  =  ( (
TopOpen ` fld )t  ( ( ( A (,) B )  \  { Y } )  u. 
{ Y } ) )
372 eqid 2382 . . . . . . 7  |-  ( w  e.  ( ( ( A (,) B ) 
\  { Y }
)  u.  { Y } )  |->  if ( w  =  Y , 
( ( N  +  ( 1  /  2
) )  x.  Y
) ,  ( ( y