# List of theorems

df-add # <context> # This theorem is part of a series of theorems constructing addition and multiplication # for complex numbers. A complex number is constructed as a pair of real numbers which # represents the real and the imaginary part of the complex number. These theorems demonstrate # that this newly constructed version of complex addition and multiplication have all # the essential properties including the commutative, associatative, and distributive # properties. # </context> # <title> Definition of Complex Addition </title> # <suggest> left('Simplify', '+') </suggest> # <summary> # See <a href="addop">addop</a> for a restatement of # complex addition using ordered pairs and complex equality. # </summary>
(= (+ A B) (<,> (r.+ (head A) (head B)) (r.+ (tail A) (tail B))))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
addeq1 # <summary> This is used just for convenience to get an empty theorem. </summary>
(-> (= A B) (= (+ A C) (+ B C)))
addeq2 # <summary> This is used just for convenience to get an empty theorem. </summary>
(-> (= A B) (= (+ C A) (+ C B)))
(= A B)(= (+ A C) (+ B C))
(-> ph (= A B))(-> ph (= (+ A C) (+ B C)))
(= A B)(= (+ C A) (+ C B))
(-> ph (= A B))(-> ph (= (+ C A) (+ C B)))
(-> (/\ (= A B) (= C D)) (= (+ A C) (+ B D)))
addeq12i # <title> Equality over Addition </title> # <table> # (= A ] ] ] [ B ] ] ) # (= [ [ C ] [ [ [ D) # (= (+ A ] [ C ] ) (+ [ B ] [ D)) # </table>
(= A B) , (= C D)(= (+ A C) (+ B D))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (+ A C) (+ B D)))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)
addcom # <title> Commutative Property of Addition </title> # <table> (= (+ <r> A <g> B) (+ <g> B <r> A)) </table> # <suggest> right('Commute', '+') </suggest>
(= (+ A B) (+ B A))
addop # <title> Addition on Ordered Pairs </title> # <summary> # This restates the <a href="df-add">original definition</a> # of complex addition using ordered pairs and complex equality. # </summary> # <suggest> right('Equivalence', '+') </suggest>
(= (+ (<,> a b) (<,> c d)) (<,> (r.+ a c) (r.+ b d)))
addass # <title> Associative Property </title> # <summary> This is identical to the proof for the integers. </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(= (+ (+ A B) C) (+ A (+ B C)))
df-mul # <title> Definition of Complex Multiplication </title> # <suggest> left('Simplify', '+') </suggest> # <summary> # See <a href="addop">addop</a> for a restatement of # complex addition using ordered pairs and complex equality. # </summary>
(= (* A B) (<,> (r.- (r.* (head A) (head B)) (r.* (tail A) (tail B))) (r.+ (r.* (tail A) (head B)) (r.* (head A) (tail B)))))
ReqReplaceEq1Op0 # <title> Substitution </title> # <table> # (= A (<,> [ b ] ] ] d)) # (r.= [ b ] [ c ] ) # (= A (<,> [ [ [ c ] d)) # </table>
(= A (<,> b d)) , (r.= b c)(= A (<,> c d))
ReqReplaceEq1Op1 # <title> Substitution </title> # <table> # (= A (<,> b [ c ] ] ] )) # (r.= [ c ] [ d ] ) # (= A (<,> b [ [ [ d ] )) # </table>
(= A (<,> b c)) , (r.= c d)(= A (<,> b d))
mulop # <title> Multiplication on Ordered Pairs </title> # <suggest> right('Equivalence', '∙') </suggest>
(= (* (<,> a b) (<,> c d)) (<,> (r.- (r.* a c) (r.* b d)) (r.+ (r.* b c) (r.* a d))))
(-> (= A B) (= (* A C) (* B C)))
(-> (= A B) (= (* C A) (* C B)))
(= A B)(= (* A C) (* B C))
muleq1d # <title> Multiply Both Sides </title>
(-> ph (= A B))(-> ph (= (* A C) (* B C)))
muleq2i # <title> Multiply Both Sides </title>
(= A B)(= (* C A) (* C B))
muleq2d # <title> Multiply Both Sides </title>
(-> ph (= A B))(-> ph (= (* C A) (* C B)))
muleq12 # <title> Multiply Equal Numbers </title>
(-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))
muleq12i # <title> Equality over Multiplication </title> # <table> # (= A ] ] ] [ B ] ] ) # (= [ [ C ] [ [ [ D) # (= (* A ] [ C ] ) (* [ B ] [ D)) # </table>
(= A B) , (= C D)(= (* A C) (* B D))
muleq12d # <title> Equality over Multiplication </title>
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (* A C) (* B D)))
ReqReplaceEq1Op0Rsub0 # <title> Substitution </title> # <table> # (= A (<,> (r.- [ b ] ] ] d) a')) # (r.= [ b ] [ c ] ) # (= A (<,> (r.- [ [ [ c ] d) a')) # </table>
(= A (<,> (r.- b d) a')) , (r.= b c)(= A (<,> (r.- c d) a'))
ReqReplaceEq1Op0Rsub1 # <title> Substitution </title> # <table> # (= A (<,> (r.- b [ c ] ] ] ) a')) # (r.= [ c ] [ d ] ) # (= A (<,> (r.- b [ [ [ d ] ) a')) # </table>
(= A (<,> (r.- b c) a')) , (r.= c d)(= A (<,> (r.- b d) a'))
ReqReplaceEq1Op1Radd0 # <title> Substitution </title> # <table> # (= A (<,> b (r.+ [ c ] ] ] a'))) # (r.= [ c ] [ d ] ) # (= A (<,> b (r.+ [ [ [ d ] a'))) # </table>
(= A (<,> b (r.+ c a'))) , (r.= c d)(= A (<,> b (r.+ d a')))
ReqReplaceEq1Op1Radd1 # <title> Substitution </title> # <table> # (= A (<,> b (r.+ c [ d ] ] ] ))) # (r.= [ d ] [ a' ] ) # (= A (<,> b (r.+ c [ [ [ a' ] ))) # </table>
(= A (<,> b (r.+ c d))) , (r.= d a')(= A (<,> b (r.+ c a')))
mulcom # <title> Commutative Property of Multiplication </title> # <table> (= (* <r> A <g> B) (* <g> B <r> A)) </table> # <suggest> right('Commute', '∙') </suggest>
(= (* A B) (* B A))
ReqReplaceReq0 # <title> Substitution </title> # <table> # (r.= [ a ] ] ] c) # (r.= [ a ] [ b ] ) # (r.= [ [ [ b ] c) # </table>
(r.= a c) , (r.= a b)(r.= b c)
ReqReplaceEq1Op0Radd1 # <title> Substitution </title> # <table> # (= A (<,> (r.+ b [ c ] ] ] ) a')) # (r.= [ c ] [ d ] ) # (= A (<,> (r.+ b [ [ [ d ] ) a')) # </table>
(= A (<,> (r.+ b c) a')) , (r.= c d)(= A (<,> (r.+ b d) a'))
ReqReplaceEq1Op0Radd0 # <title> Substitution </title> # <table> # (= A (<,> (r.+ [ b ] ] ] d) a')) # (r.= [ b ] [ c ] ) # (= A (<,> (r.+ [ [ [ c ] d) a')) # </table>
(= A (<,> (r.+ b d) a')) , (r.= b c)(= A (<,> (r.+ c d) a'))
ReqReplaceEq1Op0Radd0Rsub0 # <title> Substitution </title> # <table> # (= A (<,> (r.+ (r.- [ b ] ] ] d) a') b')) # (r.= [ b ] [ c ] ) # (= A (<,> (r.+ (r.- [ [ [ c ] d) a') b')) # </table>
(= A (<,> (r.+ (r.- b d) a') b')) , (r.= b c)(= A (<,> (r.+ (r.- c d) a') b'))
ReqReplaceEq1Op0Radd0Rsub1 # <title> Substitution </title> # <table> # (= A (<,> (r.+ (r.- b [ c ] ] ] ) a') b')) # (r.= [ c ] [ d ] ) # (= A (<,> (r.+ (r.- b [ [ [ d ] ) a') b')) # </table>
(= A (<,> (r.+ (r.- b c) a') b')) , (r.= c d)(= A (<,> (r.+ (r.- b d) a') b'))
ReqReplaceEq1Op1Radd0Rsub0 # <title> Substitution </title> # <table> # (= A (<,> b (r.+ (r.- [ c ] ] ] a') b'))) # (r.= [ c ] [ d ] ) # (= A (<,> b (r.+ (r.- [ [ [ d ] a') b'))) # </table>
(= A (<,> b (r.+ (r.- c a') b'))) , (r.= c d)(= A (<,> b (r.+ (r.- d a') b')))
ReqReplaceEq1Op1Radd0Rsub1 # <title> Substitution </title> # <table> # (= A (<,> b (r.+ (r.- c [ d ] ] ] ) b'))) # (r.= [ d ] [ a' ] ) # (= A (<,> b (r.+ (r.- c [ [ [ a' ] ) b'))) # </table>
(= A (<,> b (r.+ (r.- c d) b'))) , (r.= d a')(= A (<,> b (r.+ (r.- c a') b')))
ReqReplaceEq1Op1Radd1Radd0 # <title> Substitution </title> # <table> # (= A (<,> b (r.+ c (r.+ [ d ] ] ] b')))) # (r.= [ d ] [ a' ] ) # (= A (<,> b (r.+ c (r.+ [ [ [ a' ] b')))) # </table>
(= A (<,> b (r.+ c (r.+ d b')))) , (r.= d a')(= A (<,> b (r.+ c (r.+ a' b'))))
ReqReplaceEq1Op1Radd1Radd1 # <title> Substitution </title> # <table> # (= A (<,> b (r.+ c (r.+ d [ a' ] ] ] )))) # (r.= [ a' ] [ b' ] ) # (= A (<,> b (r.+ c (r.+ d [ [ [ b' ] )))) # </table>
(= A (<,> b (r.+ c (r.+ d a')))) , (r.= a' b')(= A (<,> b (r.+ c (r.+ d b'))))
ReqReplaceReq1 # <title> Substitution </title> # <table> # (r.= a [ b ] ] ] ) # (r.= [ b ] [ c ] ) # (r.= a [ [ [ c ] ) # </table>
(r.= a b) , (r.= b c)(r.= a c)
ReqReplaceEq0Op0 # <title> Substitution </title> # <table> # (= (<,> [ a ] ] ] c) D) # (r.= [ a ] [ b ] ) # (= (<,> [ [ [ b ] c) D) # </table>
(= (<,> a c) D) , (r.= a b)(= (<,> b c) D)
ReqReplaceEq0Op0Rsub1 # <title> Substitution </title> # <table> # (= (<,> (r.- a [ b ] ] ] ) d) A') # (r.= [ b ] [ c ] ) # (= (<,> (r.- a [ [ [ c ] ) d) A') # </table>
(= (<,> (r.- a b) d) A') , (r.= b c)(= (<,> (r.- a c) d) A')
ReqReplaceEq0Op0Rsub1Rmul1 # <title> Substitution </title> # <table> # (= (<,> (r.- a (r.* b [ c ] ] ] )) a') B') # (r.= [ c ] [ d ] ) # (= (<,> (r.- a (r.* b [ [ [ d ] )) a') B') # </table>
(= (<,> (r.- a (r.* b c)) a') B') , (r.= c d)(= (<,> (r.- a (r.* b d)) a') B')
ReqReplaceEq0Op1 # <title> Substitution </title> # <table> # (= (<,> a [ b ] ] ] ) D) # (r.= [ b ] [ c ] ) # (= (<,> a [ [ [ c ] ) D) # </table>
(= (<,> a b) D) , (r.= b c)(= (<,> a c) D)
ReqReplaceEq0Op1Radd1 # <title> Substitution </title> # <table> # (= (<,> a (r.+ b [ c ] ] ] )) A') # (r.= [ c ] [ d ] ) # (= (<,> a (r.+ b [ [ [ d ] )) A') # </table>
(= (<,> a (r.+ b c)) A') , (r.= c d)(= (<,> a (r.+ b d)) A')
ReqReplaceEq0Op1Radd1Rmul1 # <title> Substitution </title> # <table> # (= (<,> a (r.+ b (r.* c [ d ] ] ] ))) B') # (r.= [ d ] [ a' ] ) # (= (<,> a (r.+ b (r.* c [ [ [ a' ] ))) B') # </table>
(= (<,> a (r.+ b (r.* c d))) B') , (r.= d a')(= (<,> a (r.+ b (r.* c a'))) B')
mulass # <title> Associative Property of Complex Multiplication </title> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(= (* (* A B) C) (* A (* B C)))
df-0 # <title> Definition of 0 as a Complex Number </title>
(= (0) (<,> (r.0) (r.0)))
df-1 # <title> Definition of 1 as a Complex Number </title>
(= (1) (<,> (r.1) (r.0)))
EqReplaceEq0Add0 # <title> Substitution </title> # <table> # (= (+ [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (+ [ [ [ B ] C) D) # </table>
(= (+ A C) D) , (= A B)(= (+ B C) D)
EqReplaceEq0Add1 # <title> Substitution </title> # <table> # (= (+ A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (+ A [ [ [ C ] ) D) # </table>
(= (+ A B) D) , (= B C)(= (+ A C) D)
(= (+ A (0)) A)
mulid # <title> Multiplicative Identity </title>
(= (* A (1)) A)
df-i # <title> Definition of i as a Complex Number </title>
(= (i) (<,> (r.0) (r.1)))
iSquared # <title> i squared equals -1 </title>
(= (+ (* (i) (i)) (1)) (0))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
distr # <title> Distributive Property </title> # <summary> # Distribution of complex addition through multiplication. # </summary> # <table> # (= (* <c> A (+ B C)) (+ (* <c> A B) (* <c> A C))) # </table> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(= (* A (+ B C)) (+ (* A B) (* A C)))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
0ne1 # <summary> This is used just for convenience to get an empty theorem. </summary>
(-. (= (0) (1)))
EqReplaceImp1Eq0Add1 # <title> Substitution </title> # <table> # (-> ph (= (+ A [ B ] ] ] ) D)) # (= [ B ] [ C ] ) # (-> ph (= (+ A [ [ [ C ] ) D)) # </table>
(-> ph (= (+ A B) D)) , (= B C)(-> ph (= (+ A C) D))
EqReplaceImp1Eq1Add1 # <title> Substitution </title> # <table> # (-> ph (= A (+ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (-> ph (= A (+ B [ [ [ D ] ))) # </table>
(-> ph (= A (+ B C))) , (= C D)(-> ph (= A (+ B D)))
ReqReplaceImp1Eq0Add1Op0 # <title> Substitution </title> # <table> # (-> ph (= (+ A (<,> [ b ] ] ] d)) A')) # (r.= [ b ] [ c ] ) # (-> ph (= (+ A (<,> [ [ [ c ] d)) A')) # </table>
(-> ph (= (+ A (<,> b d)) A')) , (r.= b c)(-> ph (= (+ A (<,> c d)) A'))
ReqReplaceImp1Eq0Add1Op1 # <title> Substitution </title> # <table> # (-> ph (= (+ A (<,> b [ c ] ] ] )) A')) # (r.= [ c ] [ d ] ) # (-> ph (= (+ A (<,> b [ [ [ d ] )) A')) # </table>
(-> ph (= (+ A (<,> b c)) A')) , (r.= c d)(-> ph (= (+ A (<,> b d)) A'))
ReqReplaceImp1Eq1Add1Op0 # <title> Substitution </title> # <table> # (-> ph (= A (+ B (<,> [ c ] ] ] a')))) # (r.= [ c ] [ d ] ) # (-> ph (= A (+ B (<,> [ [ [ d ] a')))) # </table>
(-> ph (= A (+ B (<,> c a')))) , (r.= c d)(-> ph (= A (+ B (<,> d a'))))
ReqReplaceImp1Eq1Add1Op1 # <title> Substitution </title> # <table> # (-> ph (= A (+ B (<,> c [ d ] ] ] )))) # (r.= [ d ] [ a' ] ) # (-> ph (= A (+ B (<,> c [ [ [ a' ] )))) # </table>
(-> ph (= A (+ B (<,> c d)))) , (r.= d a')(-> ph (= A (+ B (<,> c a'))))
addcan # <title> Additive Cancellation </title> # <summary> # This proof is more complicated than it should be because it comes # before we have defined the complex negative. # </summary>
(<-> (= (+ A B) (+ C B)) (= A C))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)