# List of theorems

List of theorems in peano_new/arithmetic/complex/negative_min.gh:

df-neg # <context> # This theorem is part of a series of theorems constructing negative 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. A negative sign for complex numbers negates both the real and # imaginary parts. These theorems demonstrate that this complex negative sign has the essential # properties of a negative operation. # </context> # <title> Definition of Negative </title> # <summary> # The complex negative is defined by negating both the real and imaginary parts. # This is the unary negative sign, not to be confused with binary # <a href="df-minus">subtraction</a> which is defined using the negative sign. # </summary>
(= (-n A) (<,> (r.-n (head A)) (r.-n (tail A))))
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))
(-> (= A B) (= (-n A) (-n B)))
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)
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))
negcan # <summary> This is used just for convenience to get an empty theorem. </summary>
(= (+ A (-n A)) (0))