List of theorems

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

df-neg # <title> Definition of Negative </title> # <summary> # 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. # Integers are defined using a pair of natural numbers that represent the positive # and negative parts of the number. The negative sign is defined by swapping the pair # of numbers. # </summary>
(= (-n A) (<,> (tail A) (head A)))
negop # <summary> Apply the negative operation to an ordered pair. </summary>
(= (-n (<,> a b)) (<,> b a))
NeqReplaceBi1Neq0 # <title> Substitution </title> # <table> # (<-> ph (n.= [ A ] ] ] C)) # (n.= [ A ] [ B ] ) # (<-> ph (n.= [ [ [ B ] C)) # </table>
(<-> ph (n.= a c)) , (n.= a b)(<-> ph (n.= b c))
NeqReplaceBi1Neq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (n.= a b)) , (n.= b c)(<-> ph (n.= a c))
EqReplaceBi1Eq0 # <title> Substitution </title> # <table> # (<-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (= [ [ [ B ] C)) # </table>
(<-> ph (= A C)) , (= A B)(<-> ph (= B C))
EqReplaceBi1Eq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (= A B)) , (= B C)(<-> ph (= A C))
negeq2 # <title> Negative Signs Cancel </title> # <suggest> left('Simplify','-') </suggest>
(<-> (= A B) (= (-n A) (-n B)))
(-> (= A B) (= (-n A) (-n B)))
(= A B)(= (-n A) (-n B))
negcan # <title> Cancel using subtraction </title> # <suggest> right('Simplify','-') </suggest>
(= (+ A (-n A)) (0))