Metamath Proof Explorer

Definition df-cncf

Description: Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007)

Ref Expression
Assertion df-cncf 
|- -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccncf 
 |-  -cn->
1 va 
 |-  a
2 cc 
 |-  CC
3 2 cpw 
 |-  ~P CC
4 vb 
 |-  b
5 vf 
 |-  f
6 4 cv 
 |-  b
7 cmap 
 |-  ^m
8 1 cv 
 |-  a
9 6 8 7 co 
 |-  ( b ^m a )
10 vx 
 |-  x
11 ve 
 |-  e
12 crp 
 |-  RR+
13 vd 
 |-  d
14 vy 
 |-  y
15 cabs 
 |-  abs
16 10 cv 
 |-  x
17 cmin 
 |-  -
18 14 cv 
 |-  y
19 16 18 17 co 
 |-  ( x - y )
20 19 15 cfv 
 |-  ( abs ` ( x - y ) )
21 clt 
 |-  <
22 13 cv 
 |-  d
23 20 22 21 wbr 
 |-  ( abs ` ( x - y ) ) < d
24 5 cv 
 |-  f
25 16 24 cfv 
 |-  ( f ` x )
26 18 24 cfv 
 |-  ( f ` y )
27 25 26 17 co 
 |-  ( ( f ` x ) - ( f ` y ) )
28 27 15 cfv 
 |-  ( abs ` ( ( f ` x ) - ( f ` y ) ) )
29 11 cv 
 |-  e
30 28 29 21 wbr 
 |-  ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e
31 23 30 wi 
 |-  ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
32 31 14 8 wral 
 |-  A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
33 32 13 12 wrex 
 |-  E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
34 33 11 12 wral 
 |-  A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
35 34 10 8 wral 
 |-  A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
36 35 5 9 crab 
 |-  { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) }
37 1 4 3 3 36 cmpo 
 |-  ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )
38 0 37 wceq 
 |-  -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )