List of theorems referencing the symbol DOT_C_PLUS

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