# List of theorems

## Basic Peano arithmetic

df-1 # <title> Definition of 1 </title>
(= (1) (S (0)))
addeq1 # <title> Add a number to both sides of an equation </title> # <table> # (-> (= <g> A <b> B) (= (+ <g> A <r> C) (+ <b> B <r> C))) # </table>
(-> (= A B) (= (+ A C) (+ B C)))
addeq2 # <title> Add a number to both sides of an equation </title>
(-> (= A B) (= (+ C A) (+ C B)))
addeq12i # <title> Equality over Addition </title> # <table> # (= A ] ] ] [ B ] ] ) # (= [ [ C ] [ [ [ D) # (= (+ A ] [ C ] ) (+ [ B ] [ D)) # </table>
(= A B) , (= C D)(= (+ A C) (+ B D))
(-> ph (= A B))(-> ph (= (+ A C) (+ B C)))
(-> ph (= A B))(-> ph (= (+ C A) (+ C B)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (+ A C) (+ B D)))
pa_ax2i # <title> Equality over Succession </title> # <table> # (= A ] [ B) # (= (S A) ] [ (S B) # </table>
(= A B)(= (S A) (S B))
addeq1i # <title> Add a number to both sides </title> # <table> # (= A ] ] [ B ] ) # (= (+ A ] <g> C) ] (+ [ B ] <g> C)) # </table>
(= A B)(= (+ A C) (+ B C))
addeq2i # <title> Add a number to both sides </title> # <table> # (= [ A ] [ [ B ) # (= (+ <g> C [ A ] ) [ (+ <g> C [ B)) # </table>
(= A B)(= (+ C A) (+ C B))
muleq1 # <title> Equality over Multiplication </title> # <table> # (-> (= A B) (= (* A <r> C) (* B <r> C))) # </table>
(-> (= A B) (= (* A C) (* B C)))
muleq2 # <title> Equality over Multiplication </title> # <table> # (-> (= A B) (= (* <r> C A) (* <r> C B))) # </table>
(-> (= A B) (= (* C A) (* C B)))
muleq12i # <title> Equality over Multiplication </title>
(= A B) , (= C D)(= (* A C) (* B D))
muleq1d # <title> Equality over Multiplication </title>
(-> ph (= A B))(-> ph (= (* A C) (* B C)))
muleq1i # <title> Multiply both sides by a number </title> # <table> # (= A ] [ B ] ) # (= (* A ] C) (* [ B ] C)) # </table>
(= A B)(= (* A C) (* B C))
muleq2i # <title> Multiply both sides by a number </title> # <table> # (= [ A ] [ B ) # (= (* C [ A ] ) (* C [ B)) # </table>
(= A B)(= (* C A) (* C B))
(-> ph (= A B))(-> ph (= (* C A) (* C B)))
(-> ph (= A B))(-> ph (= (S A) (S B)))
finds # <title> Proof by Induction </title>
(-> (= x (0)) (<-> ph ps)) , (-> (= x y) (<-> ph ch)) , (-> (= x (S y)) (<-> ph th)) , (-> (= x A) (<-> ph ta)) , ps , (-> ch th)ta
inductionsuc # <title> Induction </title> # <table> # ([/] (0) z ph) ] ] ] # (-> ([/] y z ph) ] [ ([/] (S y) z [ ph)) # [ [ ([/] A z [ ph) # </table> # <summary> # Induction using substitution and the successor operation. Using substitution, # we can simplify the 6 hypotheses of <a href="finds">finds</a> into just two # the basis case and the inductive step. For a similar proof, using +1 instead of # the successor see <a href="induction">induction</a>. # </summary>
([/] (0) z ph) , (-> ([/] y z ph) ([/] (S y) z ph))([/] A z ph)
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)
EqReplaceEq1Suc0 # <title> Substitution </title> # <table> # (= A (S [ B ] ] ] )) # (= [ B ] [ C ] ) # (= A (S [ [ [ C ] )) # </table>
(= A (S B)) , (= B C)(= A (S C))
a1suc # <title> Successor Adds One </title> # <summary> Successor is equivalent to adding one </summary> # <suggest> right('Equivalence', '+1') </suggest>
(= (S A) (+ A (1)))
EqReplaceImp0Eq1 # <title> Substitution </title> # <table> # (-> (= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (-> (= A [ [ [ C ] ) ph) # </table>
(-> (= A B) ph) , (= B C)(-> (= A C) ph)
findplus1 # <title> Proof by Induction </title> # <summary> # Same as <a href="finds">finds</a> except uses +1 instead of successor. # </summary>
(-> (= x (0)) (<-> ph ps)) , (-> (= x y) (<-> ph ch)) , (-> (= x (+ y (1))) (<-> ph th)) , (-> (= x A) (<-> ph ta)) , ps , (-> ch th)ta
induction # <title> Proof by Induction </title> # <table> # ([/] (0) z ph) ] ] ] # (-> ([/] y z ph) ] [ ([/] (+ y (1)) z [ ph)) # [ [ ([/] A z [ ph) # </table> # <summary> # Using substitution, we simplify the 6 hypotheses of <a href="findplus1">findplus1</a> # into just two the basis case and the inductive step. For a similar proof, using the successor # instead of +1 see <a href="inductionsuc">inductionsuc</a>. # </summary>
([/] (0) z ph) , (-> ([/] y z ph) ([/] (+ y (1)) z ph))([/] A z ph)
pa_ax3r # <title> Additive Identity </title> # <table> # (= (+ <r> (0) A) A) # </table> # <suggest> auto-right('Simplify', '0') </suggest>
(= (+ (0) A) A)
pa_ax4r # <title> Peano Axiom 4: Addition </title> # <suggest> left('Equivalence', 'L') </suggest>
(= (+ (S A) B) (S (+ A B)))
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))
sbc-addcom # <title> Perform a substitution </title> # <summary> # Substitute A in for y in an expression describing the # <a href="addcom">commutative property of addition</a>. # </summary>
(<-> ([/] A y (= (+ y B) (+ B y))) (= (+ A B) (+ B A)))
addcom # <title> Commutative Property of Addition </title> # <table> (= (+ <r> A <g> B) (+ <g> B <r> A)) </table> # <suggest> right('Commute', '+') </suggest>
(= (+ A B) (+ B A))
EqReplaceImp1Eq1Add1 # <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)))
EqReplaceImp1Eq0Add0 # <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))
sbc-addass # <title> Perform a substitution </title> # <summary> # Substitute A in for y in an expression describing the # <a href="addass">associative property of addition</a>. # </summary>
(<-> ([/] A y (= (+ (+ y B) C) (+ y (+ B C)))) (= (+ (+ A B) C) (+ A (+ B C))))
addid # <title> Additive Identity </title> # <summary> # Identical to the third <a href="/wiki/peano/arithmetic/axioms">Peano axiom</a> # for arithmetic. This theorem simply renames it to addid. # </summary> # <suggest> auto-right('Simplify', '0') </suggest>
(= (+ A (0)) A)
addass # <title> Associative Property </title> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(= (+ (+ A B) C) (+ A (+ B C)))
pa_ax5r # <title> Multiply by 0 </title> # <suggest> auto-right('Simplify','0') </suggest>
(= (* (0) A) (0))
pa_ax6r # <title> Peano Axiom 6 Reversed </title>
(= (* (S A) B) (+ (* A B) B))
sbc-mulcom # <title> Perform a substitution </title> # <summary> # Substitute A in for y in an expression describing the # <a href="mulcom">commutative property of multiplication</a>. # </summary>
(<-> ([/] A y (= (* y B) (* B y))) (= (* A B) (* B A)))
mulcom # <title> Commutative Property </title> # <table> # (= (* <r> A <g> B) (* <g> B <r> A)) # </table> # <suggest> right('Commute', '*') </suggest>
(= (* A B) (* B A))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq0Mul1 # <title> Substitution </title> # <table> # (= (* A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (* A [ [ [ C ] ) D) # </table>
(= (* A B) D) , (= B C)(= (* A C) D)
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
mulid # <title> Multiplicative Identity </title> # <summary> # One is the identity of multiplication. Proved from the # <a href="/peano/peano_min.ghi">peano axioms</a>. </summary> # <suggest> right('Simplify', '1') </suggest> # <table> # (= (* A <r> (1)) A) # </table> # <suggest> auto-right('Simplify') </suggest>
(= (* A (1)) A)
(= (+ (+ A B) C) (+ (+ A C) B))
add4 # <title> Rearrange Addition Terms </title> # <table> # (= (+ (+ A <g> B) (+ <r> C D)) (+ (+ A <r> C) (+ <g> B D))) # </table>
(= (+ (+ A B) (+ C D)) (+ (+ A C) (+ B D)))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
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')))
sbc-distr # <title> Perform a substitution </title> # <summary> # Substitute A in for y in an expression describing the # <a href="distr">distributive property</a>. # </summary>
(<-> ([/] A y (= (* y (+ B C)) (+ (* y B) (* y C)))) (= (* A (+ B C)) (+ (* A B) (* A C))))
distr # <title> Distributive Property </title> # <summary> # Distribution of addition through multiplication. See <a href="distl">distl</a> # for distribution in the opposite direction. # </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)))
distl # <title> Distributive Property </title> # <summary> # Distribution of addition through multiplication. See <a href="distr">distr</a> # for distribution in the opposite direction. # </summary> # <table> # (= (* (+ A B) <c> C) (+ (* A <c> C) (* B <c> C))) # </table> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(= (* (+ A B) C) (+ (* A C) (* B C)))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
sbc-mulass # <title> Perform a substitution </title> # <summary> # Substitute A in for y in an expression describing the # <a href="mulass">associate property of multiplication</a>. # </summary>
(<-> ([/] A y (= (* (* y B) C) (* y (* B C)))) (= (* (* A B) C) (* A (* B C))))
mulass # <title> Associative Property </title> # <summary> Multiplication is associative </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(= (* (* A B) C) (* A (* B C)))
addcan # <title> Cancellation of addition </title> # <suggest> right('Cancel', '+') </suggest>
(<-> (= (+ B A) (+ C A)) (= B C))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
addcan2 # <title> Cancellation of addition </title> # <suggest> right('Cancel', '+') </suggest>
(<-> (= (+ A B) (+ A C)) (= B C))
0ne1 # <title> 0 is not equal to 1 </title>
(-. (= (0) (1)))
EqReplaceNot0Eq1 # <title> Substitution </title> # <table> # (-. (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-. (= A [ [ [ C ] )) # </table>
(-. (= A B)) , (= B C)(-. (= A C))
pa_axplus1 # <title> 0 is the first natural number </title>
(-. (= (0) (+ A (1))))
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
BiReplaceImp0An1Al1 # <title> Substitution </title> # <table> # (-> (/\ ph (A. x [ ps ] ] ] )) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph (A. x [ [ [ ch ] )) th) # </table>
(-> (/\ ph (A. x ps)) th) , (<-> ps ch)(-> (/\ ph (A. x ch)) th)
BiReplaceImp0An1Al1Imp1 # <title> Substitution </title> # <table> # (-> (/\ ph (A. x (-> ps [ ch ] ] ] ))) ta) # (<-> [ ch ] [ th ] ) # (-> (/\ ph (A. x (-> ps [ [ [ th ] ))) ta) # </table>
(-> (/\ ph (A. x (-> ps ch))) ta) , (<-> ch th)(-> (/\ ph (A. x (-> ps th))) ta)
BiReplaceImp0An1Al1Imp1Al1 # <title> Substitution </title> # <table> # (-> (/\ ph (A. x (-> ps (A. y [ ch ] ] ] )))) ta) # (<-> [ ch ] [ th ] ) # (-> (/\ ph (A. x (-> ps (A. y [ [ [ th ] )))) ta) # </table>
(-> (/\ ph (A. x (-> ps (A. y ch)))) ta) , (<-> ch th)(-> (/\ ph (A. x (-> ps (A. y th)))) ta)
BiReplaceImp0An1Al1Imp1Al1Imp0 # <title> Substitution </title> # <table> # (-> (/\ ph (A. x (-> ps (A. y (-> [ ch ] ] ] ta))))) et) # (<-> [ ch ] [ th ] ) # (-> (/\ ph (A. x (-> ps (A. y (-> [ [ [ th ] ta))))) et) # </table>
(-> (/\ ph (A. x (-> ps (A. y (-> ch ta))))) et) , (<-> ch th)(-> (/\ ph (A. x (-> ps (A. y (-> th ta))))) et)
EqReplaceImp0An1Al1Imp1Al1Imp0Eq1 # <title> Substitution </title> # <table> # (-> (/\ ph (A. x (-> ps (A. y (-> (= A [ B ] ] ] ) ch))))) th) # (= [ B ] [ C ] ) # (-> (/\ ph (A. x (-> ps (A. y (-> (= A [ [ [ C ] ) ch))))) th) # </table>
(-> (/\ ph (A. x (-> ps (A. y (-> (= A B) ch))))) th) , (= B C)(-> (/\ ph (A. x (-> ps (A. y (-> (= A C) ch))))) th)
pa_indplus1 # <title> Induction </title> # <summary> Induction axiom rewritten using addition instead of successor </title>
(-> (/\ (A. x (-> (= x (0)) ph)) (A. y (-> (A. x (-> (= x y) ph)) (A. x (-> (= x (+ y (1))) ph))))) (A. x ph))
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An1Al1Imp0 # <title> Substitution </title> # <table> # (-> (/\ ph (A. x (-> [ ps ] ] ] th))) ta) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph (A. x (-> [ [ [ ch ] th))) ta) # </table>
(-> (/\ ph (A. x (-> ps th))) ta) , (<-> ps ch)(-> (/\ ph (A. x (-> ch th))) ta)
(-> (/\ ([/] (0) z ph) (A. y (-> ([/] y z ph) ([/] (+ y (1)) z ph)))) ([/] A z ph))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)