List of theorems

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

NeqReplaceImp1Neq1 # <context> # This theorem is part of a series of theorems constructing addition and multiplication # for integers. <a href="/wiki/peano/arithmetic/integers">An integer is constructed</a> # as a pair of natural numbers which represent the positive and the negative part of the # integers. These theorems demonstrate that this newly constructed version of integer # addition and multiplication have all the essential properties including the commutative, # associatative, and distributive properties. # </context> # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (n.= a b)) , (n.= b c)(-> ph (n.= a c))
NeqReplaceImp1Neq0 # <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))
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))
NeqReplaceBi1Neq0Add0 # <title> Substitution </title> # <table> # (<-> ph (n.= (n.+ [ A ] ] ] C) D)) # (n.= [ A ] [ B ] ) # (<-> ph (n.= (n.+ [ [ [ B ] C) D)) # </table>
(<-> ph (n.= (n.+ a c) d)) , (n.= a b)(<-> ph (n.= (n.+ b c) d))
NeqReplaceBi1Neq0Add1 # <title> Substitution </title> # <table> # (<-> ph (n.= (n.+ a [ B ] ] ] ) D)) # (n.= [ B ] [ C ] ) # (<-> ph (n.= (n.+ a [ [ [ C ] ) D)) # </table>
(<-> ph (n.= (n.+ a b) d)) , (n.= b c)(<-> ph (n.= (n.+ a c) d))
NeqReplaceBi1Neq1Add0 # <title> Substitution </title> # <table> # (<-> ph (n.= a (n.+ [ B ] ] ] D))) # (n.= [ B ] [ C ] ) # (<-> ph (n.= a (n.+ [ [ [ C ] D))) # </table>
(<-> ph (n.= a (n.+ b d))) , (n.= b c)(<-> ph (n.= a (n.+ c d)))
NeqReplaceBi1Neq1Add1 # <title> Substitution </title> # <table> # (<-> ph (n.= a (n.+ b [ C ] ] ] ))) # (n.= [ C ] [ D ] ) # (<-> ph (n.= a (n.+ b [ [ [ D ] ))) # </table>
(<-> ph (n.= a (n.+ b c))) , (n.= c d)(<-> ph (n.= a (n.+ b d)))
zequivalence # <title> Integer Equivalence Class </title>
(= (<,> a b) (<,> (n.+ a c) (n.+ b c)))
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))
df-add # <title> Definition of Integer Addition </title> # <suggest> left('Simplify', '+') </suggest> # <summary> # See <a href="addop">addop</a> for a restatement of # integer addition using ordered pairs and integer equality. # </summary>
(= (+ A B) (<,> (n.+ (head A) (head B)) (n.+ (tail A) (tail B))))
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))
addcan1 # <table> # (<-> (= <g> A <b> B) (= (+ <g> A <r> C) (+ <b> B <r> C))) # </table>
(<-> (= A B) (= (+ A C) (+ B C)))
addcan2 # <table> # (<-> (= <g> A <b> B) (= (+ <r> C <g> A) (+ <r> C <b> B))) # </table>
(<-> (= A B) (= (+ C A) (+ C B)))
(<-> (= (+ A C) (+ B C)) (= A B))
(-> (= A B) (= (+ A C) (+ B C)))
(-> (= 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))
addeq12d # <title> Equality over Addition </title>
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (+ A C) (+ B D)))
addop # <title> Addition on Ordered Pairs </title> # <summary> # This restates the <a href="df-add">original definition</a> # of integer addition using ordered pairs and integer equality. # </summary> # <suggest> right('Equivalence', '+') </suggest>
(= (+ (<,> a b) (<,> c d)) (<,> (n.+ a c) (n.+ b d)))
addhomomorph # <title> Integer Addition is a homomorphism </title> # <summary> The <a href="df-int">int embedding</a> is a homomorphism respecting <a href="df-add">addition</a>. </summary>
(= (+ (int a) (int b)) (int (n.+ a b)))
df-0z # <title> Definition of 0 as an Integer </title>
(= (0) (int (n.0)))
df0z # <title> Def. 0 as an ordered pair </title>
(= (0) (<,> (n.0) (n.0)))
zequivalence0 # <title> 0 equivalence class </title> # <summary> 0 is equivalent to any pair of the same number C </summary>
(= (0) (<,> c c))
df-1z # <title> Definition of 1 as an Integer </title>
(= (1) (int (n.1)))
df1z # <title> Def. 1 as an ordered pair </title>
(= (1) (<,> (n.1) (n.0)))
addid # <title> Integer Addition Identity </title> # <summary> 0 is the additive identity for integer addition </summary> # <suggest> right('Simplify','0') </suggest>
(= (+ A (0)) A)
addcom # <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> (n.= (n.+ <r> A <g> B) (n.+ <g> B <r> A)) </table> # <suggest> right('Commute', '+') </suggest>
(= (+ A B) (+ B A))
addass # <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>
(= (+ (+ A B) C) (+ A (+ B C)))
df-mul # <title> Definition of Integer Multiplication </title> # <suggest> left('Simplify', '∙') </suggest> # <summary> # See <a href="mulop">mulop</a> for a restatement of # integer multiplication using ordered pairs and integer equality. # </summary>
(= (* A B) (<,> (n.+ (n.* (head A) (head B)) (n.* (tail A) (tail B))) (n.+ (n.* (head A) (tail B)) (n.* (tail A) (head B)))))
muleq1 # <title> Multiply Both Sides </title>
(-> (= A B) (= (* A C) (* B C)))
muleq2 # <title> Multiply Both Sides </title>
(-> (= A B) (= (* C A) (* C B)))
muleq1i # <title> Multiply Both Sides </title>
(= 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)))
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)
mulop # <title> Multiplication on Ordered Pairs </title> # <summary> # This restates the <a href="df-mul">original definition</a> # of integer multiplication using ordered pairs and integer equality. # </summary> # <suggest> right('Equivalence', '∙') </suggest>
(= (* (<,> a b) (<,> c d)) (<,> (n.+ (n.* a c) (n.* b d)) (n.+ (n.* a d) (n.* b c))))
NeqReplaceNeq1 # <title> Substitution </title> # <table> # (n.= A [ B ] ] ] ) # (n.= [ B ] [ C ] ) # (n.= A [ [ [ C ] ) # </table>
(n.= a b) , (n.= b c)(n.= a c)
mulhomomorph # <title> Integer Multiplication is a homomorphism </title> # <summary> The <a href="df-int">int embedding</a> is a homomorphism respecting <a href="df-mul">multiplication</a>. </summary>
(= (* (int a) (int b)) (<,> (n.* a b) (n.0)))
mulcom # <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> (= (* <r> A <g> B) (* <g> B <r> A)) </table> # <suggest> right('Commute', '∙') </suggest>
(= (* A B) (* B A))
mulid # <title> Integer Multiplication Identity </title> # <summary> 1 is the identity for integer multiplication. </summary> # <suggest> right('Simplify','1') </suggest>
(= (* A (1)) A)
NeqReplaceNeq1Add0 # <title> Substitution </title> # <table> # (n.= a (n.+ [ B ] ] ] D)) # (n.= [ B ] [ C ] ) # (n.= a (n.+ [ [ [ C ] D)) # </table>
(n.= a (n.+ b d)) , (n.= b c)(n.= a (n.+ c d))
NeqReplaceNeq1Add1 # <title> Substitution </title> # <table> # (n.= a (n.+ b [ C ] ] ] )) # (n.= [ C ] [ D ] ) # (n.= a (n.+ b [ [ [ D ] )) # </table>
(n.= a (n.+ b c)) , (n.= c d)(n.= a (n.+ b d))
NeqReplaceNeq1Add0Mul1 # <title> Substitution </title> # <table> # (n.= a (n.+ (n.* b [ c ] ] ] ) a')) # (n.= [ c ] [ d ] ) # (n.= a (n.+ (n.* b [ [ [ d ] ) a')) # </table>
(n.= a (n.+ (n.* b c) a')) , (n.= c d)(n.= a (n.+ (n.* b d) a'))
NeqReplaceNeq1Add1Mul1 # <title> Substitution </title> # <table> # (n.= a (n.+ b (n.* c [ d ] ] ] ))) # (n.= [ d ] [ a' ] ) # (n.= a (n.+ b (n.* c [ [ [ a' ] ))) # </table>
(n.= a (n.+ b (n.* c d))) , (n.= d a')(n.= a (n.+ b (n.* c a')))
mulass # <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>
(= (* (* A B) C) (* A (* B C)))
distr # <title> Distributive Property </title> # <summary> # Distribution of integer addition through multiplication. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. # </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)))
EqReplaceBi0Eq0 # <title> Substitution </title> # <table> # (<-> (= [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (<-> (= [ [ [ B ] C) ph) # </table>
(<-> (= A C) ph) , (= A B)(<-> (= B C) ph)
EqReplaceBi0Eq1 # <title> Substitution </title> # <table> # (<-> (= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (= A [ [ [ C ] ) ph) # </table>
(<-> (= A B) ph) , (= B C)(<-> (= A C) ph)
0ne1 # <title> One-Digit Inequality </title>
(-. (= (0) (1)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)