List of theorems referencing the symbol IS_ANALYTIC_CF

(956) Theorem 20012: [Cauchy integral theorem] is_analytic_CF(f) •imp (EXISTS eps in Re | (eps •R_GT R_0) & (FORALL crv1, crv2 | (is_CD_curv(crv1,R_0,R_1) & is_CD_curv(crv2,R_0,R_1) & ((crv1~[R_0]) = (crv1~[R_1])) & ((crv2~[R_0]) = (crv2~[R_1])) & (FORALL x in Interval(R_0,R_1) | eps •R_GE C_abs((crv1~[x]) •C_MINUS (crv2~[x])))) •imp (Line_Int(f,crv1,R_0,R_1) = Line_Int(f,crv2,R_0,R_1)) ))
(957) Theorem 20013: [Cauchy integral formula] (is_analytic_CF(f) & (domain(f) incs {w in Cm | C_abs(w) •R_GE R_1})) •imp (FORALL w in Cm | (C_abs(w) •R_GT R_1) •imp ((f~[w]) = (Line_Int({[x,(f~[x]) •C_OVER (x •C_MINUS w)]: x in (Cm -{w})}, {[x,C_exp_fcn([R_0,x])]: x in Re}, R_0, pi •R_PLUS pi) •C_OVER ([R_0,pi •R_PLUS pi])) ))