718 ! Thm ("sym_#mult_-1_3","(-3) * x = -1 * (3 * x)"), |
718 ! Thm ("sym_#mult_-1_3","(-3) * x = -1 * (3 * x)"), |
719 OK Thm ("realpow_twoI","?r1 ^^^ 2 = ?r1 * ?r1" [.]), |
719 OK Thm ("realpow_twoI","?r1 ^^^ 2 = ?r1 * ?r1" [.]), |
720 OK Thm ("sym_real_add_assoc", |
720 OK Thm ("sym_real_add_assoc", |
721 "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"), |
721 "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"), |
722 OK Thm |
722 OK Thm |
723 ("sym_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"), |
723 ("sym_mult.assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"), |
724 OK Thm ("sym_real_mult_left_commute", |
724 OK Thm ("sym_real_mult_left_commute", |
725 "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"), |
725 "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"), |
726 OK Thm ("sym_mult_commute","?w * ?z = ?z * ?w"), |
726 OK Thm ("sym_mult_commute","?w * ?z = ?z * ?w"), |
727 ? Thm ("sym_real_add_mult_distrib2", |
727 ? Thm ("sym_real_add_mult_distrib2", |
728 "?w * ?z1.0 + ?w * ?z2.0 = ?w * (?z1.0 + ?z2.0)"), |
728 "?w * ?z1.0 + ?w * ?z2.0 = ?w * (?z1.0 + ?z2.0)"), |