# List of theorems

List of theorems in peano_new/arithmetic/common/exponent.gh:

expeq1i # <context> # This theorem is part of a series of proofs on the properties of # <a href="/wiki/peano/arithmetic/exponent">exponents</a>. These theorems # apply generally to natural numbers, integers, rational, real and # complex numbers. # </context>
(= A B)(= (exp A C) (exp B C))
(-> ph (= A B))(-> ph (= (exp A C) (exp B C)))
(= A B)(= (exp C A) (exp C B))
(-> ph (= A B))(-> ph (= (exp C A) (exp C B)))
expeq12 # <title> Equivalence for exp </title>
(-> (/\ (= A B) (= C D)) (/\ (= (exp A C) (exp B C)) (= (exp B C) (exp B D))))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (/\ (= (exp A C) (exp B C)) (= (exp B C) (exp B D))))
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq0Exp1 # <title> Substitution </title> # <table> # (= (exp A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (exp A [ [ [ C ] ) D) # </table>
(= (exp A B) D) , (= B C)(= (exp A C) D)
exp1 # <title> Raise to the power of 1 </title> # <suggest> right('Simplify', '1') </suggest>
(= (exp A (1)) A)
1plus1 # <title> One-digit Addition </title>
(= (+ (1) (1)) (2))
exp2 # <title> Squared means multiply twice </title>
(= (exp A (2)) (* A A))
2plus1 # <title> One-digit Addition </title>
(= (+ (2) (1)) (3))
exp3 # <title> Cubed means multiply thrice </title>
(= (exp A (3)) (* (* A A) A))
3plus1 # <title> One-digit Addition </title>
(= (+ (3) (1)) (4))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
exp4 # <title> Fourth Power </title>
(= (exp A (4)) (* (* (* A A) A) A))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
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'))
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'))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
sqadd # <title> Square an Addition </title> # <suggest> left('Simplify', '2') right('Equivalence', '+') </suggest>
(= (exp (+ A B) (2)) (+ (+ (exp A (2)) (* (* (2) A) B)) (exp B (2))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)