# List of theorems

EqReplaceEq0 # <context> # This theorem is part of a series of proofs on the properties of # <a href="/wiki/peano/arithmetic/add">addition</a> and # <a href="/wiki/peano/arithmetic/multiply">multiplication</a>. These theorems # apply generally to natural numbers, integers, rational numbers, and real # numbers. # </context> # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
addidr # <title> Additive Identity </title> # <table> # (= (+ <r> (0) A) A) # </table> # <suggest> auto-right('Simplify', '0') </suggest>
(= (+ (0) A) A)
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))

## Basic Peano arithmetic

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)))
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))
muleq12d # <title> Equality over Multiplication </title>
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (* 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)))
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))
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))
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A 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))
mulidr # <title> Multiplicative Identity </title> # <suggest> auto-right('Simplify', '1') </suggest>
(= (* (1) A) A)
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
mul0 # <title> Multiply by 0 </title> # <summary> # This rederives one of the Peano axioms from a different set of axioms. But those # axioms are valid for any number, not just natural numbers. # </summary>
(= (* A (0)) (0))
mul0r # <title> Multiply by 0 </title>
(= (* (0) A) (0))
add23 # <title> Rearrange Addition Terms </title> # <table> # (= (+ (+ A <r> B) <g> C) (+ (+ A <g> C) <r> B)) # </table>
(= (+ (+ 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)))
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')))
add24 # <title> Rearrange the second and fourth terms </title>
(= (+ (+ A B) (+ C D)) (+ (+ A D) (+ C B)))
(= (+ (+ A B) (+ C D)) (+ (+ A D) (+ B C)))
mul4 # <title> Rearrange Multiplication Terms </title>
(= (* (* A B) (* C D)) (* (* A C) (* B D)))
mul42 # <title> Rearrange Multiplication Terms </title>
(= (* (* A B) (* C D)) (* (* A D) (* C B)))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
mulcom12 # <title> Commutative Property </title>
(= (* A (* B C)) (* 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)))
distrl # <title> Distributive Property </title> # <table> # (= (* (+ <m> A <b> B) (+ <c> C <g> D)) (+ (+ (* <m> A <c> C) (* <b> B <c> C)) (+ (* <m> A <g> D) (* <b> B <g> D)))) # </table> # <summary> Distribution of addition through multiplication, both arguments </summary> # <suggest> right('Distribute', 'RL') left('Distribute', 'RL') </suggest>
(= (* (+ A B) (+ C D)) (+ (+ (* A C) (* B C)) (+ (* A D) (* B D))))
addcan2 # <title> Cancellation of addition </title> # <suggest> right('Cancel', '+') </suggest>
(<-> (= (+ A B) (+ A C)) (= B C))
addcani # <title> Cancel Addition </title> # <table> # (= (+ A ] <r> C ) ] (+ [ B <r> C)) # (= A ] ] [ B) # </table>
(= (+ A C) (+ B C))(= A B)
addcan2i # <title> Cancel Addition </title> # <table> # (= (+ <r> C [ A ) ] (+ <r> C [ B )) # (= [ A ] [ B) # </table>
(= (+ C A) (+ C B))(= A B)
addneq1i # <title> Inequality over Addition </title> # <table> # (-. (= [ A ] ] [ B ] )) # (-. (= (+ [ A ] C ] ) (+ [ B ] C))) # </table>
(-. (= A B))(-. (= (+ A C) (+ B C)))
addneq2i # <title> Inequality over Addition </title> # <table> # (-. (= [ A ] [ [ B )) # (-. (= (+ C [ A ] ) (+ [ C [ B))) # </table>
(-. (= A B))(-. (= (+ C A) (+ C B)))
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)
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)
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)
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
ImpReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (-> ps ch)(-> ph (A. x ch))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
EqReplaceNot0Eq1 # <title> Substitution </title> # <table> # (-. (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-. (= A [ [ [ C ] )) # </table>
(-. (= A B)) , (= B C)(-. (= A C))
BiReplaceBi1Not0Ex1An1 # <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))))
ImpReplaceEx1An1An0 # <title> Substitution </title> # <table> # (E. x (/\ ph (/\ [ ps ] ] ] th))) # (-> [ ps ] [ ch ] ) # (E. x (/\ ph (/\ [ [ [ ch ] th))) # </table>
(E. x (/\ ph (/\ ps th))) , (-> ps ch)(E. x (/\ ph (/\ ch th)))
ImpReplaceEx1An1An1 # <title> Substitution </title> # <table> # (E. x (/\ ph (/\ ps [ ch ] ] ] ))) # (-> [ ch ] [ th ] ) # (E. x (/\ ph (/\ ps [ [ [ th ] ))) # </table>
(E. x (/\ ph (/\ ps ch))) , (-> ch th)(E. x (/\ ph (/\ ps th)))
BiReplaceEx1An1An0Not0 # <title> Substitution </title> # <table> # (E. x (/\ ph (/\ (-. [ ps ] ] ] ) th))) # (<-> [ ps ] [ ch ] ) # (E. x (/\ ph (/\ (-. [ [ [ ch ] ) th))) # </table>
(E. x (/\ ph (/\ (-. ps) th))) , (<-> ps ch)(E. x (/\ ph (/\ (-. ch) th)))
anReplaceEq # <summary> Replace an equal statement in the second part of an AND statement using the first part of the AND. </summary>
(<-> (/\ (= A B) (= B C)) (/\ (= A B) (= A C)))
(<-> (/\ (= A B) (= A C)) (/\ (= A B) (= B C)))
(-> (/\ (= A B) (-. (= B C))) (/\ (= A B) (-. (= A C))))
(<-> (/\ (= A B) (-. (= B C))) (/\ (= A B) (-. (= A C))))
(= A B) , (-. (= B C))(-. (= A C))
(rwff x (= x A))
(rwff x (= A x))
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
df-2 # <title> Definition of 2 </title>
(= (2) (+ (1) (1)))
df-3 # <title> Definition of 3 </title>
(= (3) (+ (2) (1)))
df-4 # <title> Definition of 4 </title>
(= (4) (+ (3) (1)))
df-5 # <title> Definition of 5 </title>
(= (5) (+ (4) (1)))
df-6 # <title> Definition of 6 </title>
(= (6) (+ (5) (1)))
df-7 # <title> Definition of 7 </title>
(= (7) (+ (6) (1)))
df-8 # <title> Definition of 8 </title>
(= (8) (+ (7) (1)))
df-9 # <title> Definition of 9 </title>
(= (9) (+ (8) (1)))
df-10 # <title> Definition of 10 </title>
(= (10) (+ (9) (1)))