List of theorems referencing the symbol CM
(925) Theorem 804a: ((X in Re) & (Y in Re)) •imp ([X,Y] in Cm)
(926) Theorem 804: (M in Cm) •eq ((M = [car(M),cdr(M)]) & (car(M) in Re) & (cdr(M) in Re))
(927) Theorem 825: (C_0 in Cm) & (C_1 in Cm)
(928) Theorem 805: ((N in Cm) & (M in Cm)) •imp ((N •C_PLUS M in Cm) & (N •C_TIMES M in Cm))
(929) Theorem 806: ((N in Cm) & (M in Cm)) •imp (N •C_PLUS M = M •C_PLUS N)
(930) Theorem 807: (N in Cm) •imp ((N = N •C_PLUS C_0) & (N = C_0 •C_PLUS N))
(931) Theorem 808: (N in Cm) •imp ((C_Rev(N) in Cm) & (C_Rev(C_Rev(N)) = N))
(932) Theorem 809: (N in Cm) •imp (C_Rev(N) •C_PLUS N = C_0)
(933) Theorem 810: ((N in Cm) & (M in Cm)) •imp (N = M •C_PLUS (N •C_MINUS M))
(934) Theorem 811: ((N in Cm) & (M in Cm)) •imp (N •C_TIMES M = M •C_TIMES N)
(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))
(941) Theorem 819: ((K in Cm) & (N in Cm) & (M in Cm)) •imp (N •C_PLUS (M •C_PLUS K) = (N •C_PLUS M) •C_PLUS K)
(942) Theorem 820: ((K in Cm) & (N in Cm) & (M in Cm)) •imp ((N •C_TIMES (M •C_TIMES K)) = ((N •C_TIMES M) •C_TIMES K))
(943) Theorem 821: ((K in Cm) & (N in Cm) & (M in Cm)) •imp ((N •C_TIMES (M •C_PLUS K)) = ((N •C_TIMES M) •C_PLUS (N •C_TIMES K)))
(944) Theorem 822: (M in Cm) •imp ((M = (M •C_TIMES C_1)) & (M = (C_1 •C_TIMES M)))
(945) Theorem 823: ((M in Cm) & (M /= C_0)) •imp ((C_Recip(M) in Cm) & ((M •C_TIMES C_Recip(M)) = C_1))
(946) Theorem 824: ((N in Cm) & (M in Cm) & (M /= C_0)) •imp (N = M •C_TIMES (N •C_OVER M))
(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])) ))