# List of theorems

List of theorems in peano/integers.gh:

df-zeq # <context> # This theorem is part of a series of theorems that construct the integers using # natural numbers. We are in the process of reorganizing the theorems and grouping them into # smaller files that concern one specific topic. This theorem should have been moved into # the peano_new/arithmetic/integers directory. # </context> # <title> Definition of Integer Equality </title> # <summary> # An integer is defined as an order pair of natural numbers. The first # number in the pair represents the positive part of the number, the # second number represent the negative part of the number. Thus (0,0), # (1,1), (2,2) are all equivalent to the integer 0, since their negative # and positive parts are equal. (A, 0) presents +A. (0, A) represents -A. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. # </summary> # <suggest> left('Simplify', '=') </suggest>
(<-> (=z A B) (= (+ (head A) (tail B)) (+ (head B) (tail A))))
eqzeq # <title> Convert Natural to Integer Equality </title> # <suggest> right('Infer', '=z') </suggest>
(-> (= A B) (=z A B))
eqzeqi # <title> Convert Natural to Integer Equality </title>
(= A B)(=z A B)
eqzeqd # <title> Convert Natural to Integer Equality </title>
(-> ph (= A B))(-> ph (=z A B))
opzexpand # <title> Expand Ordered Pair </title> # <suggest> left('Simplify', '<,>') </suggest>
(=z A (<,> (head A) (tail A)))
EqReplaceBi1Eq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (= A B)) , (= B C)(<-> ph (= A C))
zeqid # <title> Reflexive Property </title> # <summary> Integer equality is reflexive. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. #</summary>
(=z A A)
zeqcom # <title> Symmetric Property </title> # <summary> Integer equality is symmetric. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. # </summary> # <suggest> right('Commute', '=') </suggest>
(<-> (=z A B) (=z B A))
zeqcomi # <title> Symmetric Property </title> # <table> # (=z <r> A <g> B) # (=z <g> B <r> A) # </table>
(=z A B)(=z B A)
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq1Add0 # <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)))
zeqtr # <title> Transitive Property </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. </summary> # <suggest> right('Simplify', '=') </suggest>
(-> (/\ (=z A B) (=z B C)) (=z A C))
(-> (=z A B) (<-> (=z A C) (=z B C)))
zeqzeq2 # <title> Equivalence over Equality </title>
(-> (=z A B) (<-> (=z C A) (=z C B)))
zeqzeq1i # <title> Equivalence over Equality </title> # <table> # (=z A ] ] [ B ] ) # (<-> (=z A ] C) ] [ (=z B ] C)) # </table>
(=z A B)(<-> (=z A C) (=z B C))
zeqzeq1d # <title> Equivalence over Equality </title> # <table> # (-> ph (= A ] ] [ B ] )) # (-> ph (<-> (= A ] C) ] [ (= B ] C))) # </table>
(-> ph (=z A B))(-> ph (<-> (=z A C) (=z B C)))
zeqzeq2i # <title> Equivalence over Equality </title> # <table> # (=z [ A ] [ [ B) # (<-> (=z C [ A) ] [ (=z C [ B)) # </table>
(=z A B)(<-> (=z C A) (=z C B))
zeqzeq2d # <title> Equivalence over Equality </title> # <table> # (-> ph (= [ A ] [ [ B)) # (-> ph (<-> (= C [ A) ] [ (= C [ B))) # </table>
(-> ph (=z A B))(-> ph (<-> (=z C A) (=z C B)))
zeqzeq12i # <title> Equivalence over Equality </title>
(=z A B) , (=z C D)(<-> (=z A C) (=z B D))
zeqzeq12d # <title> Transitive Property </title>
(-> ph (=z A B)) , (-> ph (=z C D))(-> ph (<-> (=z A C) (=z B D)))
zeqtrd # <title> Transitive Property </title>
(-> ph (=z A B)) , (-> ph (=z B C))(-> ph (=z A C))
EqReplaceBi1Eq0 # <title> Substitution </title> # <table> # (<-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (= [ [ [ B ] C)) # </table>
(<-> ph (= A C)) , (= A B)(<-> ph (= B C))
EqReplaceBi1Eq0Add0 # <title> Substitution </title> # <table> # (<-> ph (= (+ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (<-> ph (= (+ [ [ [ B ] C) D)) # </table>
(<-> ph (= (+ A C) D)) , (= A B)(<-> ph (= (+ B C) D))
EqReplaceBi1Eq0Add1 # <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))
EqReplaceBi1Eq1Add0 # <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)))
EqReplaceBi1Eq1Add1 # <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)))
zequivalence # <title> Integer Equivalence Class </title>
(=z (<,> A B) (<,> (+ A C) (+ B C)))
opzeq # <title> Natural-Integer Equality Conversion </title> # <suggest> right('Equivalence', '=N') left('Equivalence', '=z') </suggest>
(<-> (=z (<,> A B) (<,> C D)) (= (+ A D) (+ C B)))
zeqexpand # <title> Expand Integer Equality </title>
(-> (=z A B) (= (+ (head A) (tail B)) (+ (head B) (tail A))))
df-int # <title> Def. Natural to Integer Mapping </title> # <summary> # Defines a mapping between a natural number to an ordered pair # that represents the same number as an integer. Subsequent # theorems show that this mapping is a homomorphism respecting # <a href="zaddhomomorph">addition</a>, <a href="df-zmul">multiplication</a>, # and <a href="zlehomomorph">inequality</a>. # </summary> # <suggest> left('Simplify', 'int') </suggest>
(=z (int A) (<,> A (0)))
ZeqReplaceImp1Zeq1 # <title> Substitution </title> # <table> # (-> ph (=z A [ B ] ] ] )) # (=z [ B ] [ C ] ) # (-> ph (=z A [ [ [ C ] )) # </table>
(-> ph (=z A B)) , (=z B C)(-> ph (=z A C))
(-> (= A B) (=z (int A) (int B)))
(= A B)(=z (int A) (int B))
(-> ph (= A B))(-> ph (=z (int A) (int B)))
df-zn # <title> Def. Integer to Natural Mapping </title> # <summary> # Reverses the <a href="df-int">natural to integer mapping</a>. # Maps negative integers to 0. # </summary>
(= (zn A) (.- (head A) (tail A)))
EqReplaceImp1Eq1HM0 # <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)))
(-> (=z A B) (= (zn A) (zn B)))
(=z A B)(= (zn A) (zn B))
(-> ph (=z A B))(-> ph (= (zn A) (zn B)))
EqReplaceEq1HM0 # <title> Substitution </title> # <table> # (= A (.- [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (.- [ [ [ C ] D)) # </table>
(= A (.- B D)) , (= B C)(= A (.- C D))
EqReplaceEq1HM1 # <title> Substitution </title> # <table> # (= A (.- B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (.- B [ [ [ D ] )) # </table>
(= A (.- B C)) , (= C D)(= A (.- B D))
znint # <title> Natural-Integer Mappings Cancel </title>
(= (zn (int A)) A)
df-zadd # <title> Definition of Integer Addition </title> # <suggest> left('Simplify', '+') </suggest> # <summary> # See <a href="zaddop">zaddop</a> for a restatement of # integer addition using ordered pairs and integer equality. # </summary>
(=z (+z A B) (<,> (+ (head A) (head B)) (+ (tail A) (tail B))))
EqReplaceEq1Op0 # <title> Substitution </title> # <table> # (= A (<,> [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (<,> [ [ [ C ] D)) # </table>
(= A (<,> B D)) , (= B C)(= A (<,> C D))
EqReplaceEq1Op0Add0 # <title> Substitution </title> # <table> # (= A (<,> (+ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (<,> (+ [ [ [ C ] D) A')) # </table>
(= A (<,> (+ B D) A')) , (= B C)(= A (<,> (+ C D) A'))
EqReplaceEq1Op0Add1 # <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'))
EqReplaceEq1Op1 # <title> Substitution </title> # <table> # (= A (<,> B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (<,> B [ [ [ D ] )) # </table>
(= A (<,> B C)) , (= C D)(= A (<,> B D))
EqReplaceEq1Op1Add0 # <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')))
EqReplaceEq1Op1Add1 # <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')))
ZeqReplaceBi1Zeq0 # <title> Substitution </title> # <table> # (<-> ph (=z [ A ] ] ] C)) # (=z [ A ] [ B ] ) # (<-> ph (=z [ [ [ B ] C)) # </table>
(<-> ph (=z A C)) , (=z A B)(<-> ph (=z B C))
ZeqReplaceBi1Zeq1 # <title> Substitution </title> # <table> # (<-> ph (=z A [ B ] ] ] )) # (=z [ B ] [ C ] ) # (<-> ph (=z A [ [ [ C ] )) # </table>
(<-> ph (=z A B)) , (=z B C)(<-> ph (=z A C))
zaddcan1 # <table> # (<-> (=z <g> A <b> B) (=z (+z <g> A <r> C) (+z <b> B <r> C))) # </table>
(<-> (=z A B) (=z (+z A C) (+z B C)))
zaddcan2 # <table> # (<-> (=z <g> A <b> B) (=z (+z <r> C <g> A) (+z <r> C <b> B))) # </table>
(<-> (=z A B) (=z (+z C A) (+z C B)))
(-> (=z A B) (=z (+z A C) (+z B C)))
(-> (=z A B) (=z (+z C A) (+z C B)))
(=z A B)(=z (+z A C) (+z B C))
(-> ph (=z A B))(-> ph (=z (+z A C) (+z B C)))
(=z A B)(=z (+z C A) (+z C B))
(-> ph (=z A B))(-> ph (=z (+z C A) (+z C B)))
(-> (/\ (=z A B) (=z C D)) (=z (+z A C) (+z B D)))
zaddzeq12i # <title> Equality over Addition </title> # <table> # (=z A ] ] ] [ B ] ] ) # (=z [ [ C ] [ [ [ D) # (=z (+z A ] [ C ] ) (+z [ B ] [ D)) # </table>
(=z A B) , (=z C D)(=z (+z A C) (+z B D))
(-> ph (=z A B)) , (-> ph (=z C D))(-> ph (=z (+z A C) (+z B D)))
zaddop # <title> Addition on Ordered Pairs </title> # <summary> # This restates the <a href="df-zadd">original definition</a> # of integer addition using ordered pairs and integer equality. # </summary> # <suggest> right('Equivalence', '+') </suggest>
(=z (+z (<,> A B) (<,> C D)) (<,> (+ A C) (+ B D)))
(=z (+z (int A) (int B)) (int (+ A B)))
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>
(=z (-n A) (<,> (tail A) (head A)))
negop # <summary> Apply the negative operation to an ordered pair. </summary>
(=z (-n (<,> A B)) (<,> B A))
negzeq2 # <title> Negative Signs Cancel </title> # <suggest> left('Simplify','-') </suggest>
(<-> (=z A B) (=z (-n A) (-n B)))
(-> (=z A B) (=z (-n A) (-n B)))
(=z A B)(=z (-n A) (-n B))
doubleneg # <title> Double Negative </title>
(=z (-n (-n A)) A)
df-0z # <title> Definition of 0 as an Integer </title>
(=z (0z) (int (0)))
df0z # <title> Def. 0 as an ordered pair </title>
(=z (0z) (<,> (0) (0)))
zequivalence0 # <title> 0 equivalence class </title> # <summary> 0 is equivalent to any pair of the same number C </summary>
(=z (0z) (<,> C C))
df-1z # <title> Definition of 1 as an Integer </title>
(=z (1z) (int (1)))
df1z # <title> Def. 1 as an ordered pair </title>
(=z (1z) (<,> (1) (0)))
(=z (+z A (0z)) A)
neg0 # <title> Negative of 0 </title>
(=z (-n (0z)) (0z))
zaddcom # <title> Commutative Property of Addition </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. </summary> # <table> (= (+ <r> A <g> B) (+ <g> B <r> A)) </table> # <suggest> right('Commute', '+') </suggest>
(=z (+z A B) (+z B A))
zaddass # <title> Associative Property </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=z (+z (+z A B) C) (+z A (+z B C)))
(=z (+z (0z) A) A)
df-minus # <title> Definition of Subtraction </title> # <summary> # This is the binary subtraction operation, not to be confused with the # unary <a href="df-neg">negative sign</a> which is used in the definition. # </summary>
(=z (- A B) (+z A (-n B)))
ZeqReplaceImp1Zeq0 # <title> Substitution </title> # <table> # (-> ph (=z [ A ] ] ] C)) # (=z [ A ] [ B ] ) # (-> ph (=z [ [ [ B ] C)) # </table>
(-> ph (=z A C)) , (=z A B)(-> ph (=z B C))
minuszeq1 # <title> Equivalence for - </title> ##
(-> (=z A C) (=z (- A B) (- C B)))
(=z A C)(=z (- A B) (- C B))
minuszeq2 # <title> Equivalence for - </title> ##
(-> (=z B C) (=z (- A B) (- A C)))
(-> ph (=z A C))(-> ph (=z (- A B) (- C B)))
(=z B C)(=z (- A B) (- A C))
(-> ph (=z B C))(-> ph (=z (- A B) (- A C)))
negcan # <title> Cancel using subtraction </title> # <suggest> right('Simplify','-') </suggest>
(=z (+z A (-n A)) (0z))
negcan2 # <title> Cancel using subtraction </title> # <suggest> right('Simplify','-') </suggest>
(=z (+z (-n A) A) (0z))
ZeqReplaceZeq0 # <title> Substitution </title> # <table> # (=z [ A ] ] ] C) # (=z [ A ] [ B ] ) # (=z [ [ [ B ] C) # </table>
(=z A C) , (=z A B)(=z B C)
minuscan # <title> Cancel using subtraction </title> # <suggest> right('Simplify','-') </suggest>
(=z (- A A) (0z))
zaddcan # <title> Addition is the inverse of Subtraction </title> # <suggest> right('Simplify','-') </suggest>
(=z (+z (- A B) B) A)
zaddcanr # <title> Addition is the inverse of Subtraction </title> # <suggest> right('Simplify','-') </suggest>
(=z (- (+z A B) B) A)
dfzmul # <title> Definition of Integer Multiplication </title> # <suggest> left('Simplify', '∙') </suggest> # <summary> # See <a href="zmulop">zmulop</a> for a restatement of # integer multiplication using ordered pairs and integer equality. # </summary>
(= (*z A B) (<,> (+ (* (head A) (head B)) (* (tail A) (tail B))) (+ (* (head A) (tail B)) (* (tail A) (head B)))))
(-> (= A B) (= (*z A C) (*z B C)))
(-> (= A B) (= (*z C A) (*z C B)))
zmulopeq # <title> Multiplication on Ordered Pairs </title> # <summary> This uses natural number equality. </suggest> # <suggest> right('Equivalence', '∙') </suggest>
(= (*z (<,> A B) (<,> C D)) (<,> (+ (* A C) (* B D)) (+ (* A D) (* B C))))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq0Head0 # <title> Substitution </title> # <table> # (= (head [ A ] ] ] ) C) # (= [ A ] [ B ] ) # (= (head [ [ [ B ] ) C) # </table>
EqReplaceEq0Tail0 # <title> Substitution </title> # <table> # (= (tail [ A ] ] ] ) C) # (= [ A ] [ B ] ) # (= (tail [ [ [ B ] ) C) # </table>
(= (tail A) C) , (= A B)(= (tail B) C)
(= (tail (*z A B)) (+ (* (head A) (tail B)) (* (tail A) (head B))))
df-zmul # <title> Definition of Integer Multiplication </title> # <suggest> left('Simplify', '∙') </suggest> # <summary> # See <a href="zmulop">zmulop</a> for a restatement of # integer multiplication using ordered pairs and integer equality. # </summary>
(=z (*z A B) (<,> (+ (* (head A) (head B)) (* (tail A) (tail B))) (+ (* (head A) (tail B)) (* (tail A) (head B)))))
zmulzeq1 # <title> Multiply Both Sides </title>
(-> (=z A B) (=z (*z A C) (*z B C)))
zmulzeq2 # <title> Multiply Both Sides </title>
(-> (=z A B) (=z (*z C A) (*z C B)))
zmulzeq1i # <title> Multiply Both Sides </title>
(=z A B)(=z (*z A C) (*z B C))
zmulzeq1d # <title> Multiply Both Sides </title>
(-> ph (=z A B))(-> ph (=z (*z A C) (*z B C)))
zmulzeq2i # <title> Multiply Both Sides </title>
(=z A B)(=z (*z C A) (*z C B))
zmulzeq2d # <title> Multiply Both Sides </title>
(-> ph (=z A B))(-> ph (=z (*z C A) (*z C B)))
zmulzeq12 # <title> Multiply Equal Numbers </title>
(-> (/\ (=z A B) (=z C D)) (=z (*z A C) (*z B D)))
zmulzeq12i # <title> Equality over Multiplication </title> # <table> # (=z A ] ] ] [ B ] ] ) # (=z [ [ C ] [ [ [ D) # (=z (*z A ] [ C ] ) (*z [ B ] [ D)) # </table>
(=z A B) , (=z C D)(=z (*z A C) (*z B D))
zmulzeq12d # <title> Equality over Multiplication </title>
(-> ph (=z A B)) , (-> ph (=z C D))(-> ph (=z (*z A C) (*z B D)))
ZeqReplaceZeq1 # <title> Substitution </title> # <table> # (=z A [ B ] ] ] ) # (=z [ B ] [ C ] ) # (=z A [ [ [ C ] ) # </table>
(=z A B) , (=z B C)(=z A C)
ZeqReplaceZeq1Zadd0 # <title> Substitution </title> # <table> # (=z A (+z [ B ] ] ] D)) # (=z [ B ] [ C ] ) # (=z A (+z [ [ [ C ] D)) # </table>
(=z A (+z B D)) , (=z B C)(=z A (+z C D))
ZeqReplaceZeq1Zadd1 # <title> Substitution </title> # <table> # (=z A (+z B [ C ] ] ] )) # (=z [ C ] [ D ] ) # (=z A (+z B [ [ [ D ] )) # </table>
(=z A (+z B C)) , (=z C D)(=z A (+z B D))
zmulop # <title> Multiplication on Ordered Pairs </title> # <suggest> right('Equivalence', '∙') </suggest>
(=z (*z (<,> A B) (<,> C D)) (<,> (+ (* A C) (* B D)) (+ (* A D) (* B C))))
zmulhomomorph # <title> Integer Multiplication is a homomorphism </title> # <summary> The <a href="df-int">int embedding</a> is a homomorphism respecting <a href="df-zmul">multiplication</a>. </summary>
(=z (*z (int A) (int B)) (<,> (* A B) (0)))
zmulcom # <title> Commutative Property of Multiplication </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. </summary> # <table> (=z (*z <r> A <g> B) (*z <g> B <r> A)) </table> # <suggest> right('Commute', '∙') </suggest>
(=z (*z A B) (*z B A))
zmul0 # <title> Multiply by 0 </title> # <suggest> right('Simplify','0') </suggest>
(=z (*z A (0z)) (0z))
zmul0r # <title> Multiply by 0 </title> # <suggest> right('Simplify','0') </suggest>
(=z (*z (0z) A) (0z))
zmulid # <title> Integer Multiplication Identity </title> # <summary> 1 is the identity for integer multiplication. </summary> # <suggest> right('Simplify','1') </suggest>
(=z (*z A (1z)) A)
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))
EqReplaceEq1Add0Mul1 # <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'))
EqReplaceEq1Add1Mul1 # <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')))
zmulass # <title> Associative Property of Integer Multiplication </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=z (*z (*z A B) C) (*z A (*z B C)))
zdistr # <title> Distributive Property </title> # <summary> # Distribution of integer addition through multiplication. # See <a href="zdistl">zdistl</a> for distribution in the opposite direction. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. # </summary> # <table> # (=z (*z <c> A (+z B C)) (+z (*z <c> A B) (*z <c> A C))) # </table> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(=z (*z A (+z B C)) (+z (*z A B) (*z A C)))
zdistl # <title> Distributive Property </title> # <summary> # Distribution of integer addition through multiplication. # See <a href="zdistr">zdistr</a> for distribution in the opposite direction. # </summary> # <table> # (=z (*z (+z B C) <c> A ) (+z (*z B <c> A) (*z C <c> A))) # </table> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(=z (*z (+z B C) A) (+z (*z B A) (*z C A)))
df-zle # <title> Def. Integer Less Than or Equal To' </title>
(<-> (<=z A B) (<= (+ (head A) (tail B)) (+ (head B) (tail A))))
EqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (<= [ [ [ B ] C)) # </table>
(<-> ph (<= A C)) , (= A B)(<-> ph (<= B C))
EqReplaceBi1Le1 # <title> Substitution </title> # <table> # (<-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (<= A [ [ [ C ] )) # </table>
(<-> ph (<= A B)) , (= B C)(<-> ph (<= A C))
zleop # <title> Apply ≤ to ordered pair </title>
(<-> (<=z (<,> A B) (<,> C D)) (<= (+ A D) (+ C B)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
(-> (=z A B) (<-> (<=z A C) (<=z B C)))
(-> (=z A B) (<-> (<=z C A) (<=z C B)))
(=z A B)(<-> (<=z A C) (<=z B C))
(-> ph (=z A B))(-> ph (<-> (<=z A C) (<=z B C)))
(=z A B)(<-> (<=z C A) (<=z C B))
(-> ph (=z A B))(-> ph (<-> (<=z C A) (<=z C B)))
zlehomomorph # <title> Integer Inequality Homomorphism </title> # <summary> The <a href="df-int">int embedding</a> is a homomorphism respecting <a href="df-zle">less than or equal to</a>. </summary>
(<-> (<=z (int A) (int B)) (<= A B))
df-zlt # <title> Def. Integer Less Than' </title>
(<-> (<z A B) (< (+ (head A) (tail B)) (+ (head B) (tail A))))
EqReplaceBi1Lt0 # <title> Substitution </title> # <table> # (<-> ph (< [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (< [ [ [ B ] C)) # </table>
(<-> ph (< A C)) , (= A B)(<-> ph (< B C))
EqReplaceBi1Lt1 # <title> Substitution </title> # <table> # (<-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (< A [ [ [ C ] )) # </table>
(<-> ph (< A B)) , (= B C)(<-> ph (< A C))
zltop # <title> Apply ≤ to ordered pair </title>
(<-> (<z (<,> A B) (<,> C D)) (< (+ A D) (+ C B)))
(-> (=z A B) (<-> (<z A C) (<z B C)))
(-> (=z A B) (<-> (<z C A) (<z C B)))
(=z A B)(<-> (<z A C) (<z B C))
(-> ph (=z A B))(-> ph (<-> (<z A C) (<z B C)))
(=z A B)(<-> (<z C A) (<z C B))
(-> ph (=z A B))(-> ph (<-> (<z C A) (<z C B)))
ztlhomomorph # <title> Integer Inequality Homomorphism </title> # <summary> The <a href="df-int">int embedding</a> is a homomorphism respecting <a href="df-ztl">less than</a>. </summary>
(<-> (<z (int A) (int B)) (< A B))
(<-> (=z (*z B A) (*z C A)) (= (+ (* (+ (head B) (tail C)) (head A)) (* (+ (head C) (tail B)) (tail A))) (+ (* (+ (head C) (tail B)) (head A)) (* (+ (head B) (tail C)) (tail A)))))
ImpReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
ImpReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ [ ps ] ] ] th))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (E. x (/\ ps th))) , (-> ps ch)(-> ph (E. x (/\ ch th)))
BiReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (<-> ps ch)(<-> ph (E. x ch))
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (<-> ps ch)(-> ph (E. x ch))
BiReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (E. x (/\ ps th))) , (<-> ps ch)(-> ph (E. x (/\ ch th)))
ImpReplaceImp1Ex1An0An0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (/\ [ ps ] ] ] th) ta))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ (/\ [ [ [ ch ] th) ta))) # </table>
(-> ph (E. x (/\ (/\ ps th) ta))) , (-> ps ch)(-> ph (E. x (/\ (/\ ch th) ta)))
ImpReplaceImp1Ex1An0An1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (/\ ps [ ch ] ] ] ) ta))) # (-> [ ch ] [ th ] ) # (-> ph (E. x (/\ (/\ ps [ [ [ th ] ) ta))) # </table>
(-> ph (E. x (/\ (/\ ps ch) ta))) , (-> ch th)(-> ph (E. x (/\ (/\ ps th) ta)))
BiReplaceImp1Ex1An0An1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (/\ ps [ ch ] ] ] ) ta))) # (<-> [ ch ] [ th ] ) # (-> ph (E. x (/\ (/\ ps [ [ [ th ] ) ta))) # </table>
(-> ph (E. x (/\ (/\ ps ch) ta))) , (<-> ch th)(-> ph (E. x (/\ (/\ ps th) ta)))
BiReplaceImp1Ex1An0Bi1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> ps [ ch ] ] ] ) ta))) # (<-> [ ch ] [ th ] ) # (-> ph (E. x (/\ (<-> ps [ [ [ th ] ) ta))) # </table>
(-> ph (E. x (/\ (<-> ps ch) ta))) , (<-> ch th)(-> ph (E. x (/\ (<-> ps th) ta)))
BiReplaceImp1Ex1An0Bi0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> [ ps ] ] ] th) ta))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ (<-> [ [ [ ch ] th) ta))) # </table>
(-> ph (E. x (/\ (<-> ps th) ta))) , (<-> ps ch)(-> ph (E. x (/\ (<-> ch th) ta)))
EqReplaceImp1Ex1An0Bi0Eq0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> (= [ A ] ] ] C) ps) ch))) # (= [ A ] [ B ] ) # (-> ph (E. x (/\ (<-> (= [ [ [ B ] C) ps) ch))) # </table>
(-> ph (E. x (/\ (<-> (= A C) ps) ch))) , (= A B)(-> ph (E. x (/\ (<-> (= B C) ps) ch)))
EqReplaceImp1Ex1An0Bi0Eq0Add1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> (= (+ A [ B ] ] ] ) D) ps) ch))) # (= [ B ] [ C ] ) # (-> ph (E. x (/\ (<-> (= (+ A [ [ [ C ] ) D) ps) ch))) # </table>
(-> ph (E. x (/\ (<-> (= (+ A B) D) ps) ch))) , (= B C)(-> ph (E. x (/\ (<-> (= (+ A C) D) ps) ch)))
EqReplaceImp1Ex1An0Bi0Eq1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> (= A [ B ] ] ] ) ps) ch))) # (= [ B ] [ C ] ) # (-> ph (E. x (/\ (<-> (= A [ [ [ C ] ) ps) ch))) # </table>
(-> ph (E. x (/\ (<-> (= A B) ps) ch))) , (= B C)(-> ph (E. x (/\ (<-> (= A C) ps) ch)))
EqReplaceImp1Ex1An0Bi0Eq1Add1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> (= A (+ B [ C ] ] ] )) ps) ch))) # (= [ C ] [ D ] ) # (-> ph (E. x (/\ (<-> (= A (+ B [ [ [ D ] )) ps) ch))) # </table>
(-> ph (E. x (/\ (<-> (= A (+ B C)) ps) ch))) , (= C D)(-> ph (E. x (/\ (<-> (= A (+ B D)) ps) ch)))
EqReplaceImp1Ex1An0Bi0Eq0Add0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> (= (+ [ A ] ] ] C) D) ps) ch))) # (= [ A ] [ B ] ) # (-> ph (E. x (/\ (<-> (= (+ [ [ [ B ] C) D) ps) ch))) # </table>
(-> ph (E. x (/\ (<-> (= (+ A C) D) ps) ch))) , (= A B)(-> ph (E. x (/\ (<-> (= (+ B C) D) ps) ch)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
ImpReplaceImp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ ps [ ch ] ] ] ))) # (-> [ ch ] [ th ] ) # (-> ph (E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (E. x (/\ ps ch))) , (-> ch th)(-> ph (E. x (/\ ps th)))
BiReplaceImp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (E. x (/\ ps ch))) , (<-> ch th)(-> ph (E. x (/\ ps th)))
(-> (< (head A) (tail A)) (<-> (=z (*z B A) (*z C A)) (=z B C)))
EqReplaceImp1Ex1An0Bi0Eq1Add0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<-> (= A (+ [ B ] ] ] D)) ps) ch))) # (= [ B ] [ C ] ) # (-> ph (E. x (/\ (<-> (= A (+ [ [ [ C ] D)) ps) ch))) # </table>
(-> ph (E. x (/\ (<-> (= A (+ B D)) ps) ch))) , (= B C)(-> ph (E. x (/\ (<-> (= A (+ C D)) ps) ch)))
(-> (< (tail A) (head A)) (<-> (=z (*z B A) (*z C A)) (=z B C)))
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
ZeqReplaceBi0Zeq1 # <title> Substitution </title> # <table> # (<-> (=z A [ B ] ] ] ) ph) # (=z [ B ] [ C ] ) # (<-> (=z A [ [ [ C ] ) ph) # </table>
(<-> (=z A B) ph) , (=z B C)(<-> (=z A C) ph)
BiReplaceImp0Or1 # <title> Substitution </title> # <table> # (-> (\/ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (\/ ph [ [ [ ch ] ) th) # </table>
(-> (\/ ph ps) th) , (<-> ps ch)(-> (\/ ph ch) th)
zmulcan # <title> Multiplication Cancellation </title>
(-> (-. (=z A (0z))) (<-> (=z (*z B A) (*z C A)) (=z B C)))
ZeqReplaceImp1Bi0Zeq1 # <title> Substitution </title> # <table> # (-> ph (<-> (=z A [ B ] ] ] ) ps)) # (=z [ B ] [ C ] ) # (-> ph (<-> (=z A [ [ [ C ] ) ps)) # </table>
(-> ph (<-> (=z A B) ps)) , (=z B C)(-> ph (<-> (=z A C) ps))
zmulcan0 # <title> Multiplication Cancellation </title>
(-> (-. (=z A (0z))) (<-> (=z (*z B A) (0z)) (=z B (0z))))
BiReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
BiReplaceImp1Imp1Not0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (-. [ [ [ th ] ))) # </table>
(-> ph (-> ps (-. ch))) , (<-> ch th)(-> ph (-> ps (-. th)))
ZeqReplaceImp1Imp1Not0Zeq0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. (=z [ A ] ] ] C)))) # (=z [ A ] [ B ] ) # (-> ph (-> ps (-. (=z [ [ [ B ] C)))) # </table>
(-> ph (-> ps (-. (=z A C)))) , (=z A B)(-> ph (-> ps (-. (=z B C))))
zeroProductz # <title> Zero Product Property </title>
(-> (/\ (-. (=z A (0z))) (-. (=z B (0z)))) (-. (=z (*z A B) (0z))))
BiReplaceBi1Not0Or0 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (\/ [ [ [ ch ] th))) # </table>
(<-> ph (-. (\/ ps th))) , (<-> ps ch)(<-> ph (-. (\/ ch th)))
BiReplaceBi1Not0Or1 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (\/ ps [ [ [ th ] ))) # </table>
(<-> ph (-. (\/ ps ch))) , (<-> ch th)(<-> ph (-. (\/ ps th)))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
zeroFactors # <title> Zero Product Property </title>
(<-> (=z (*z A B) (0z)) (\/ (=z A (0z)) (=z B (0z))))
nonzeroProduct2 # <title> Zero Product Property </title>
(<-> (-. (=z (*z A B) (0z))) (/\ (-. (=z A (0z))) (-. (=z B (0z)))))
ZeqReplaceImp1Imp1Zeq1 # <title> Substitution </title> # <table> # (-> ph (-> ps (=z A [ B ] ] ] ))) # (=z [ B ] [ C ] ) # (-> ph (-> ps (=z A [ [ [ C ] ))) # </table>
(-> ph (-> ps (=z A B))) , (=z B C)(-> ph (-> ps (=z A C)))
ZeqReplaceImp1Imp1Zeq0 # <title> Substitution </title> # <table> # (-> ph (-> ps (=z [ A ] ] ] C))) # (=z [ A ] [ B ] ) # (-> ph (-> ps (=z [ [ [ B ] C))) # </table>
(-> ph (-> ps (=z A C))) , (=z A B)(-> ph (-> ps (=z B C)))
(-> (-. (=z A (0z))) (<-> (=z B (0z)) (=z (*z A B) (0z))))
ZeqReplaceBi0Zle0 # <title> Substitution </title> # <table> # (<-> (<=z [ A ] ] ] C) ph) # (=z [ A ] [ B ] ) # (<-> (<=z [ [ [ B ] C) ph) # </table>
(<-> (<=z A C) ph) , (=z A B)(<-> (<=z B C) ph)
ZeqReplaceBi0Zle1 # <title> Substitution </title> # <table> # (<-> (<=z A [ B ] ] ] ) ph) # (=z [ B ] [ C ] ) # (<-> (<=z A [ [ [ C ] ) ph) # </table>
(<-> (<=z A B) ph) , (=z B C)(<-> (<=z A C) ph)
0zle # <title> No Natural Numbers below 0 </title>
(<=z (0z) (int A))
zlezadd # <title> Addition on Both Sides of Inequality </title> # <suggest> left('Cancel', '+') </suggest>
(<-> (<=z (+z A C) (+z B C)) (<=z A B))
(<=z (0z) (1z))
ZeqReplaceBi0Zlt0 # <title> Substitution </title> # <table> # (<-> (<z [ A ] ] ] C) ph) # (=z [ A ] [ B ] ) # (<-> (<z [ [ [ B ] C) ph) # </table>
(<-> (<z A C) ph) , (=z A B)(<-> (<z B C) ph)
ZeqReplaceBi0Zlt1 # <title> Substitution </title> # <table> # (<-> (<z A [ B ] ] ] ) ph) # (=z [ B ] [ C ] ) # (<-> (<z A [ [ [ C ] ) ph) # </table>
(<-> (<z A B) ph) , (=z B C)(<-> (<z A C) ph)
EqReplaceNot0Eq1 # <title> Substitution </title> # <table> # (-. (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-. (= A [ [ [ C ] )) # </table>
(-. (= A B)) , (= B C)(-. (= A C))
0notEqual1 # <title> One-Digit Inequality </title>
(-. (= (0) (1)))
0less1 # <title> One-Digit Inequality </title> # <table> # (< (0) (1)) # </table>
(< (0) (1))
0zless1 # <title> 0 is less than 1 </title>
(<z (0z) (1z))
EqReplaceImp1Lt0 # <title> Substitution </title> # <table> # (-> ph (< [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (< [ [ [ B ] C)) # </table>
(-> ph (< A C)) , (= A B)(-> ph (< B C))
EqReplaceImp1Lt1 # <title> Substitution </title> # <table> # (-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (< A [ [ [ C ] )) # </table>
(-> ph (< A B)) , (= B C)(-> ph (< A C))
zlezlttr # <title> Transitive Property </title>
(-> (/\ (<=z A B) (<z B C)) (<z A C))
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
zltzletr # <title> Transitive Property </title>
(-> (/\ (<z A B) (<=z B C)) (<z A C))
zltneq # <title> Operator Conversion </title> # <suggest> right('Infer', '≠') </suggest>
(-> (<z A B) (-. (=z A B)))
zltle # <title> Operator Conversion </title> # <suggest> right('Infer', '≤ ') </suggest>
(-> (<z A B) (<=z A B))
0znotEqual1 # <title> 0 does not equal 1 </title>
(-. (=z (0z) (1z)))
zmul4 # <title> Rearrange Multiplication Terms </title>
(=z (*z (*z A B) (*z C D)) (*z (*z A C) (*z B D)))
zmul42 # <title> Rearrange Multiplication Terms </title>
(=z (*z (*z A B) (*z C D)) (*z (*z A D) (*z C B)))
EqReplaceBi1Le1Add1 # <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)))
EqReplaceBi1Le0Add0 # <title> Substitution </title> # <table> # (<-> ph (<= (+ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (<-> ph (<= (+ [ [ [ B ] C) D)) # </table>
(<-> ph (<= (+ A C) D)) , (= A B)(<-> ph (<= (+ B C) D))
EqReplaceBi1Le0Add1 # <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))
EqReplaceBi1Le1Add0 # <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)))
(<-> (<=z A (0z)) (<= (head A) (tail A)))
(<-> (<=z (0z) A) (<= (tail A) (head A)))
intzn # <title> Invert Integer Mapping </title> # <summary> The natural to integer mapping can be inverted for nonnegative numbers. </summary>
(-> (<=z (0z) A) (=z (int (zn A)) A))
(<-> (<=z (1z) A) (<= (+ (1) (tail A)) (head A)))
EqReplaceEq1Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (+ [ [ [ C ] D) A')) # </table>
(= A (+ (+ B D) A')) , (= B C)(= A (+ (+ C D) A'))
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'))
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')))
EqReplaceImp1Le0 # <title> Substitution </title> # <table> # (-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (<= [ [ [ B ] C)) # </table>
(-> ph (<= A C)) , (= A B)(-> ph (<= B C))
zltconold # <title> Less Than Converse </title>
(<-> (<z B A) (-. (<=z A B)))
ZeqReplaceImp0Zlt0 # <title> Substitution </title> # <table> # (-> (<z [ A ] ] ] C) ph) # (=z [ A ] [ B ] ) # (-> (<z [ [ [ B ] C) ph) # </table>
(-> (<z A C) ph) , (=z A B)(-> (<z B C) ph)
(-> (<z (0z) (int (zn A))) (=z (int (zn A)) A))
ZeqReplaceZeq0Neg0 # <title> Substitution </title> # <table> # (=z (-n [ A ] ] ] ) C) # (=z [ A ] [ B ] ) # (=z (-n [ [ [ B ] ) C) # </table>
(=z (-n A) C) , (=z A B)(=z (-n B) C)
ZeqReplaceZeq0Neg0Zmul0 # <title> Substitution </title> # <table> # (=z (-n (*z [ A ] ] ] C)) D) # (=z [ A ] [ B ] ) # (=z (-n (*z [ [ [ B ] C)) D) # </table>
(=z (-n (*z A C)) D) , (=z A B)(=z (-n (*z B C)) D)
ZeqReplaceZeq0Neg0Zmul1 # <title> Substitution </title> # <table> # (=z (-n (*z A [ B ] ] ] )) D) # (=z [ B ] [ C ] ) # (=z (-n (*z A [ [ [ C ] )) D) # </table>
(=z (-n (*z A B)) D) , (=z B C)(=z (-n (*z A C)) D)
negzmul # <title> Multiply Negated Number </title> # <suggest> right('Equivalence', '-') left('Equivalence', '-') </suggest>
(=z (-n (*z A B)) (*z (-n A) B))
df-zgt # <title> Definition of Integer Greater than </title>
(<-> (>z A B) (-. (<=z A B)))
zgtzeq1 # <title> Equivalence for >z </title> ##
(-> (=z A C) (<-> (>z A B) (>z C B)))
(=z A C)(<-> (>z A B) (>z C B))
zgtzeq2 # <title> Equivalence for >z </title> ##
(-> (=z B C) (<-> (>z A B) (>z A C)))
(-> ph (=z A C))(-> ph (<-> (>z A B) (>z C B)))
(=z B C)(<-> (>z A B) (>z A C))
zgtzeq12 # <title> Equivalence for >z </title> ##
(-> (/\ (=z A B) (=z C D)) (<-> (>z A C) (>z B D)))
(-> ph (=z B C))(-> ph (<-> (>z A B) (>z A C)))
(-> ph (=z A B)) , (-> ph (=z C D))(-> ph (<-> (>z A C) (>z B D)))
dfzgt # <title> Alternative Def. Integer Greater Than </title>
(<-> (>z A B) (> (+ (head A) (tail B)) (+ (head B) (tail A))))
zltcon # <title> Less Than Converse </title> # <suggest> left('Commute', '>') right('Commute', '<') </suggest>
(<-> (<z A B) (>z B A))
df-zge # <title> Def. of Integer Greater than or Equal </title>
(<-> (>=z A B) (-. (<z A B)))
zgezeq1 # <title> Equivalence for >=z </title> ##
(-> (=z A C) (<-> (>=z A B) (>=z C B)))
(=z A C)(<-> (>=z A B) (>=z C B))
zgezeq2 # <title> Equivalence for >=z </title> ##
(-> (=z B C) (<-> (>=z A B) (>=z A C)))
(-> ph (=z A C))(-> ph (<-> (>=z A B) (>=z C B)))
(=z B C)(<-> (>=z A B) (>=z A C))
zgezeq12 # <title> Equivalence for >=z </title> ##
(-> (/\ (=z A B) (=z C D)) (<-> (>=z A C) (>=z B D)))
(-> ph (=z B C))(-> ph (<-> (>=z A B) (>=z A C)))
(-> ph (=z A B)) , (-> ph (=z C D))(-> ph (<-> (>=z A C) (>=z B D)))
dfzge # <title> Alternative Def. Integer Greater Than Equal </title>
(<-> (>=z A B) (>= (+ (head A) (tail B)) (+ (head B) (tail A))))
zlecon # <title> Converse of ≤ </title> # <suggest> right('Commute', '≤') left('Commute', '≥') </suggest>
(<-> (<=z A B) (>=z B A))
df-zpos # <title> Definition of a Positive Integer </title> # <suggest> left('Simplify', '+') </suggest>
(<-> (zpos A) (>z A (0z)))
(-> (=z A B) (<-> (zpos A) (zpos B)))
(=z A B)(<-> (zpos A) (zpos B))
(-> ph (=z A B))(-> ph (<-> (zpos A) (zpos B)))
df-zneg # <title> Definition of a Negative Integer </title> # <suggest> left('Simplify', '-') </suggest>
(<-> (zneg A) (<z A (0z)))
(-> (=z A B) (<-> (zneg A) (zneg B)))
ZeqReplaceBi0Zgt1 # <title> Substitution </title> # <table> # (<-> (>z A [ B ] ] ] ) ph) # (=z [ B ] [ C ] ) # (<-> (>z A [ [ [ C ] ) ph) # </table>
(<-> (>z A B) ph) , (=z B C)(<-> (>z A C) ph)
EqReplaceBi1Gt0 # <title> Substitution </title> # <table> # (<-> ph (> [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (> [ [ [ B ] C)) # </table>
(<-> ph (> A C)) , (= A B)(<-> ph (> B C))
EqReplaceBi1Gt0Add1 # <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))
EqReplaceBi1Gt1 # <title> Substitution </title> # <table> # (<-> ph (> A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (> A [ [ [ C ] )) # </table>
(<-> ph (> A B)) , (= B C)(<-> ph (> A C))
EqReplaceBi1Gt1Add0 # <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)))
dfpos # <title> Alternative Def. Positive Integer </title>
(<-> (zpos A) (> (head A) (tail A)))
zmulpos # <title> Positive Product Formula </title>
(<-> (zpos (*z A B)) (> (+ (* (head A) (head B)) (* (tail A) (tail B))) (+ (* (head A) (tail B)) (* (tail A) (head B)))))
EqReplaceBi1Lt0Add1 # <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))
EqReplaceBi1Lt1Add0 # <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)))
dfneg # <title> Alternative Def. Negative Integer </title>
(<-> (zneg A) (< (head A) (tail A)))
(<-> (=z A (0z)) (= (head A) (tail A)))
posproduct1 # <title> Multiply Two Positive Numbers </title>
(-> (/\ (zpos A) (zpos B)) (zpos (*z A B)))
negProduct # <title> Multiply Two Negative Numbers </title>
(-> (/\ (zneg A) (zneg B)) (zpos (*z A B)))
(=z A B)(<-> (zneg A) (zneg B))
(-> ph (=z A B))(-> ph (<-> (zneg A) (zneg B)))
zmulneg # <title> Negative Product Formula </title>
(<-> (zneg (*z A B)) (< (+ (* (head A) (head B)) (* (tail A) (tail B))) (+ (* (head A) (tail B)) (* (tail A) (head B)))))
(-> (/\ (zpos A) (zneg B)) (zneg (*z A B)))
ZeqReplaceImp1Zneg0 # <title> Substitution </title> # <table> # (-> ph (zneg [ A ] ] ] )) # (=z [ A ] [ B ] ) # (-> ph (zneg [ [ [ B ] )) # </table>
(-> ph (zneg A)) , (=z A B)(-> ph (zneg B))
(-> (\/ (/\ (zpos A) (zneg B)) (/\ (zneg A) (zpos B))) (zneg (*z A B)))
BiReplaceOr1Or1 # <title> Substitution </title> # <table> # (\/ ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (\/ ph (\/ ps [ [ [ th ] )) # </table>
(\/ ph (\/ ps ch)) , (<-> ch th)(\/ ph (\/ ps th))
BiReplaceOr1Or0 # <title> Substitution </title> # <table> # (\/ ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (\/ ph (\/ [ [ [ ch ] th)) # </table>
(\/ ph (\/ ps th)) , (<-> ps ch)(\/ ph (\/ ch th))
0negpos # <title> A number is negative, positive or 0 </title>
(\/ (zneg A) (\/ (=z A (0z)) (zpos A)))
negpos # <title> Nonzero numbers are negative or positive </title>
(-> (-. (=z A (0z))) (\/ (zneg A) (zpos A)))
posNotNeg # <title> Positive numbers are not negative </title>
(-> (zpos A) (-. (zneg A)))
negNotPos # <title> Negative numbers are not positive </title>
(-> (zneg A) (-. (zpos A)))
0NotNeg # <title> 0 is not negative </title>
(-> (=z A (0z)) (-. (zneg A)))
0NotPos # <title> 0 is not positive </title>
(-> (=z A (0z)) (-. (zpos A)))
posCases # <title> Positive Proof by Cases </title>
(-> (/\ (-. (zneg A)) (-. (=z A (0z)))) (zpos A))
negCases # <title> Negative Proof by Cases </title>
(-> (/\ (-. (zpos A)) (-. (=z A (0z)))) (zneg A))
BiReplaceBi1Imp1 # <title> Substitution </title> # <table> # (<-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (-> ps [ [ [ th ] )) # </table>
(<-> ph (-> ps ch)) , (<-> ch th)(<-> ph (-> ps th))
(-> (zpos (*z A B)) (-. (=z B (0z))))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
ZeqReplaceImp0Not0Zneg0 # <title> Substitution </title> # <table> # (-> (-. (zneg [ A ] ] ] )) ph) # (=z [ A ] [ B ] ) # (-> (-. (zneg [ [ [ B ] )) ph) # </table>
(-> (-. (zneg A)) ph) , (=z A B)(-> (-. (zneg B)) ph)
ImpReplaceOr0 # <title> Substitution </title> # <table> # (\/ [ ph ] ] ] ch) # (-> [ ph ] [ ps ] ) # (\/ [ [ [ ps ] ch) # </table>
(\/ ph ch) , (-> ph ps)(\/ ps ch)
ImpReplaceOr1 # <title> Substitution </title> # <table> # (\/ ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (\/ ph [ [ [ ch ] ) # </table>
(\/ ph ps) , (-> ps ch)(\/ ph ch)
ImpReplaceOr1Or1 # <title> Substitution </title> # <table> # (\/ ph (\/ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (\/ ph (\/ ps [ [ [ th ] )) # </table>
(\/ ph (\/ ps ch)) , (-> ch th)(\/ ph (\/ ps th))
BiReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (<-> ch th)(-> ph (\/ ps th))
ImpReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (-> ps ch)(-> ph (\/ ch th))
ImpReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (-> ch th)(-> ph (\/ ps th))
ImpReplaceImp1Or1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps (\/ ch [ th ] ] ] ))) # (-> [ th ] [ ta ] ) # (-> ph (\/ ps (\/ ch [ [ [ ta ] ))) # </table>
(-> ph (\/ ps (\/ ch th))) , (-> th ta)(-> ph (\/ ps (\/ ch ta)))
BiReplaceNot0An1 # <title> Substitution </title> # <table> # (-. (/\ ph [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-. (/\ ph [ [ [ ch ] )) # </table>
(-. (/\ ph ps)) , (<-> ps ch)(-. (/\ ph ch))
(<-> (zpos (*z A B)) (\/ (/\ (zneg A) (zneg B)) (/\ (zpos A) (zpos B))))
(-> (zpos (*z A B)) (<-> (zpos A) (zpos B)))
BiReplaceBi1Or0 # <title> Substitution </title> # <table> # (<-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (\/ [ [ [ ch ] th)) # </table>
(<-> ph (\/ ps th)) , (<-> ps ch)(<-> ph (\/ ch th))
BiReplaceBi1Or1 # <title> Substitution </title> # <table> # (<-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (\/ ps [ [ [ th ] )) # </table>
(<-> ph (\/ ps ch)) , (<-> ch th)(<-> ph (\/ ps th))
posSquares # <title> Squares are not negative </title>
(-> (-. (=z A (0z))) (zpos (*z A A)))
BiReplaceBi1An0 # <title> Substitution </title> # <table> # (<-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ [ [ [ ch ] th)) # </table>
(<-> ph (/\ ps th)) , (<-> ps ch)(<-> ph (/\ ch th))
(-> (zpos A) (<-> (zpos (*z A B)) (zpos B)))
df-2z # <title> Definition of 2 as an Integer </title>
(=z (2z) (int (2)))
df-3z # <title> Definition of 3 as an Integer </title>
(=z (3z) (int (3)))
df-4z # <title> Definition of 4 as an Integer </title>
(=z (4z) (int (4)))
df-5z # <title> Definition of 5 as an Integer </title>
(=z (5z) (int (5)))
df-6z # <title> Definition of 6 as an Integer </title>
(=z (6z) (int (6)))
df-7z # <title> Definition of 7 as an Integer </title>
(=z (7z) (int (7)))
df-8z # <title> Definition of 8 as an Integer </title>
(=z (8z) (int (8)))
df-9z # <title> Definition of 9 as an Integer </title>
(=z (9z) (int (9)))
df-10z # <title> Definition of 10 as an Integer </title>
(=z (10z) (int (10)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)