List of theorems referencing the symbol C_ABS

(935) Theorem 812: (N in Cm) •imp ((C_abs(N) in Re) & R_is_nonneg(C_abs(N)))
(936) Theorem 813: (N in Cm) •imp (C_abs(N) = C_abs(C_Rev(N)))
(937) Theorem 814: ((N in Cm) & (M in Cm)) •imp (((C_abs(N) •R_PLUS C_abs(M)) •R_GT C_abs(N •C_PLUS M)) or (C_abs(N) •R_PLUS C_abs(M) = C_abs(N •C_PLUS M)))
(938) Theorem 815: ((N in Cm) & (M in Cm)) •imp (((C_abs(N) •R_PLUS C_abs(M)) •R_GT C_abs(N •C_MINUS M)) or (C_abs(N) •R_PLUS C_abs(M) = C_abs(N •C_MINUS M)))
(939) Theorem 816: ((N in Cm) & (M in Cm)) •imp (C_abs(N) •R_TIMES C_abs(M) = C_abs(N •C_TIMES M))
(940) Theorem 817: ((N in Cm) & (M in Cm) & (M /= C_0)) •imp (C_abs(N) •R_OVER C_abs(M) = C_abs(N •C_OVER M))
(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])) ))