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 ) } )