# List of theorems

EqReplaceEq0 # <context> # This theorem is part of a series of theorems that demonstrate complex addition, # multiplication, and division. # </context> # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq0Add0 # <title> Substitution </title> # <table> # (= (+ [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (+ [ [ [ B ] C) D) # </table>
(= (+ A C) D) , (= A B)(= (+ B C) D)
iSquared2 # <title> i squared is -1 </title> # <suggest> right('Simplify', '-1') </suggest>
(= (exp (i) (2)) (-n (1)))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
EqReplaceEq1Neg0 # <title> Substitution </title> # <table> # (= A (-n [ B ] ] ] )) # (= [ B ] [ C ] ) # (= A (-n [ [ [ C ] )) # </table>
(= A (-n B)) , (= B C)(= A (-n C))
(= (exp (i) (3)) (-n (i)))
3plus1 # <title> One-digit Addition </title>
(= (+ (3) (1)) (4))
EqReplaceEq0Exp1 # <title> Substitution </title> # <table> # (= (exp A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (exp A [ [ [ C ] ) D) # </table>
(= (exp A B) D) , (= B C)(= (exp A C) D)
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
iPower4 # <title> i to the fourth is 1 </title>
(= (exp (i) (4)) (1))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
(= (+ (+ a (* b (i))) (+ c (* d (i)))) (+ (+ a c) (* (+ b d) (i))))
EqReplaceEq1Add1Add0 # <title> Substitution </title> # <table> # (= A (+ B (+ [ C ] ] ] A'))) # (= [ C ] [ D ] ) # (= A (+ B (+ [ [ [ D ] A'))) # </table>
(= A (+ B (+ C A'))) , (= C D)(= A (+ B (+ D A')))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
EqReplaceEq1Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (+ (+ B [ [ [ D ] ) A')) # </table>
(= A (+ (+ B C) A')) , (= C D)(= A (+ (+ B D) A'))
EqReplaceEq1Add1Add1 # <title> Substitution </title> # <table> # (= A (+ B (+ C [ D ] ] ] ))) # (= [ D ] [ A' ] ) # (= A (+ B (+ C [ [ [ A' ] ))) # </table>
(= A (+ B (+ C D))) , (= D A')(= A (+ B (+ C A')))
EqReplaceEq1Add0Add1Mul1 # <title> Substitution </title> # <table> # (= A (+ (+ B (* C [ D ] ] ] )) B')) # (= [ D ] [ A' ] ) # (= A (+ (+ B (* C [ [ [ A' ] )) B')) # </table>
(= A (+ (+ B (* C D)) B')) , (= D A')(= A (+ (+ B (* C A')) B'))
commul # <title> Complex Multiplication Formula </title>
(= (* (+ a (* b (i))) (+ c (* d (i)))) (+ (- (* a c) (* b d)) (* (+ (* a d) (* b c)) (i))))
EqReplaceEq0Mul1 # <title> Substitution </title> # <table> # (= (* A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (* A [ [ [ C ] ) D) # </table>
(= (* A B) D) , (= B C)(= (* A C) D)
EqReplaceEq0Mul1Add1 # <title> Substitution </title> # <table> # (= (* A (+ B [ C ] ] ] )) A') # (= [ C ] [ D ] ) # (= (* A (+ B [ [ [ D ] )) A') # </table>
(= (* A (+ B C)) A') , (= C D)(= (* A (+ B D)) A')
EqReplaceEq1Add0Minus1 # <title> Substitution </title> # <table> # (= A (+ (- B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (+ (- B [ [ [ D ] ) A')) # </table>
(= A (+ (- B C) A')) , (= C D)(= A (+ (- B D) A'))
EqReplaceEq1Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ B (* [ C ] ] ] A'))) # (= [ C ] [ D ] ) # (= A (+ B (* [ [ [ D ] A'))) # </table>
(= A (+ B (* C A'))) , (= C D)(= A (+ B (* D A')))
EqReplaceEq1Add1Mul0Add0 # <title> Substitution </title> # <table> # (= A (+ B (* (+ [ C ] ] ] A') B'))) # (= [ C ] [ D ] ) # (= A (+ B (* (+ [ [ [ D ] A') B'))) # </table>
(= A (+ B (* (+ C A') B'))) , (= C D)(= A (+ B (* (+ D A') B')))
EqReplaceEq1Div0 # <title> Substitution </title> # <table> # (= A (/ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (/ [ [ [ C ] D)) # </table>
(= A (/ B D)) , (= B C)(= A (/ C D))
EqReplaceEq1Add1Mul0Add1 # <title> Substitution </title> # <table> # (= A (+ B (* (+ C [ D ] ] ] ) B'))) # (= [ D ] [ A' ] ) # (= A (+ B (* (+ C [ [ [ A' ] ) B'))) # </table>
(= A (+ B (* (+ C D) B'))) , (= D A')(= A (+ B (* (+ C A') B')))
EqReplaceEq1Minus1 # <title> Substitution </title> # <table> # (= A (- B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (- B [ [ [ D ] )) # </table>
(= A (- B C)) , (= C D)(= A (- B D))
EqReplaceEq1Div1 # <title> Substitution </title> # <table> # (= A (/ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (/ B [ [ [ D ] )) # </table>
(= A (/ B C)) , (= C D)(= A (/ B D))
comdiv # <title> Complex Division Formula </title>
(/\ (-. (= (+ c (* d (i))) (0))) (-. (= (- c (* d (i))) (0))))(= (/ (+ a (* b (i))) (+ c (* d (i)))) (/ (+ (+ (* a c) (* b d)) (* (- (* b c) (* a d)) (i))) (+ (exp c (2)) (exp d (2)))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)