## redirect add_multiply_min.gh param (PROP prop.ghi () "") param (PREDICATE ../../predicate/predicate_all.ghi (PROP) "") param (R_PREDICATE ../../predicate/all.ghi (PROP) "r.") param (R_REALS ../common/reals/common.ghi (PROP R_PREDICATE) "r.") param (EQUALITY_COM equality_com.ghi (PROP R_PREDICATE PREDICATE) "") param (ADD_MULTIPLY_MIN ../common/add_multiply_min.ghi (PROP PREDICATE) "") tvar (wff ph ps ch th ta) tvar (nat A B C D) tvar (r.nat a b c d) var (nat x y z) term (nat (i)) ## i squared equals -1 stmt (iSquared () () (= (+ (* (i) (i)) (1)) (0))) ## Addition on Ordered Pairs ## right('Equivalence', '+') stmt (addop () () (= (+ (<,> a b) (<,> c d)) (<,> (r.+ a c) (r.+ b d)))) ## Multiplication on Ordered Pairs ## right('Equivalence', '∙') stmt (mulop () () (= (* (<,> a b) (<,> c d)) (<,> (r.- (r.* a c) (r.* b d)) (r.+ (r.* b c) (r.* a d))))) ## Definition of 0 as a Complex Number stmt (df-0 () () (= (0) (<,> (r.0) (r.0)))) ## Definition of 1 as a Complex Number stmt (df-1 () () (= (1) (<,> (r.1) (r.0)))) ## Definition of i as a Complex Number stmt (df-i () () (= (i) (<,> (r.0) (r.1))))