# List of theorems

List of theorems in peano_new/arithmetic/common/calculations/naturals.gh:

EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
1plus1 # <context> # This theorem is part of a series of theorems that prove basic one-digit addition # formulas. To prove these most basic theorems, we must directly use # the definitions of the numbers. The number 2 is defined as 2 = 1 + 1, 3 = 2 + 1, # 4 = 3 + 1, and so on. This theorem uses these definitions along with the # <a href="/edit/peano/peano_thms.gh/addass">associate property</a>. # </context> ---- Automatically generated with GH.ProofGenerator.evaluator.batchEvaluation('+', [1, 10], [1, 10]); # <title> One-digit Addition </title>
(= (+ (1) (1)) (2))
2plus1 # <title> One-digit Addition </title>
(= (+ (2) (1)) (3))
3plus1 # <title> One-digit Addition </title>
(= (+ (3) (1)) (4))
4plus1 # <title> One-digit Addition </title>
(= (+ (4) (1)) (5))
5plus1 # <title> One-digit Addition </title>
(= (+ (5) (1)) (6))
6plus1 # <title> One-digit Addition </title>
(= (+ (6) (1)) (7))
7plus1 # <title> One-digit Addition </title>
(= (+ (7) (1)) (8))
8plus1 # <title> One-digit Addition </title>
(= (+ (8) (1)) (9))
9plus1 # <title> One-digit Addition </title>
(= (+ (9) (1)) (10))
1plus2 # <title> One-digit Addition </title>
(= (+ (1) (2)) (3))
1plus3 # <title> One-digit Addition </title>
(= (+ (1) (3)) (4))
1plus4 # <title> One-digit Addition </title>
(= (+ (1) (4)) (5))
1plus5 # <title> One-digit Addition </title>
(= (+ (1) (5)) (6))
1plus6 # <title> One-digit Addition </title>
(= (+ (1) (6)) (7))
1plus7 # <title> One-digit Addition </title>
(= (+ (1) (7)) (8))
1plus8 # <title> One-digit Addition </title>
(= (+ (1) (8)) (9))
1plus9 # <title> One-digit Addition </title>
(= (+ (1) (9)) (10))
1plus10 # <title> One-digit Addition </title>
(= (+ (1) (10)) (+ (10) (1)))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
2plus2 # <title> One-digit Addition </title>
(= (+ (2) (2)) (4))
2plus3 # <title> One-digit Addition </title>
(= (+ (2) (3)) (5))
2plus4 # <title> One-digit Addition </title>
(= (+ (2) (4)) (6))
2plus5 # <title> One-digit Addition </title>
(= (+ (2) (5)) (7))
2plus6 # <title> One-digit Addition </title>
(= (+ (2) (6)) (8))
2plus7 # <title> One-digit Addition </title>
(= (+ (2) (7)) (9))
2plus8 # <title> One-digit Addition </title>
(= (+ (2) (8)) (10))
2plus9 # <title> One-digit Addition </title>
(= (+ (2) (9)) (+ (10) (1)))
2plus10 # <title> One-digit Addition </title>
(= (+ (2) (10)) (+ (10) (2)))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
3plus2 # <title> One-digit Addition </title>
(= (+ (3) (2)) (5))
3plus3 # <title> One-digit Addition </title>
(= (+ (3) (3)) (6))
3plus4 # <title> One-digit Addition </title>
(= (+ (3) (4)) (7))
3plus5 # <title> One-digit Addition </title>
(= (+ (3) (5)) (8))
3plus6 # <title> One-digit Addition </title>
(= (+ (3) (6)) (9))
3plus7 # <title> One-digit Addition </title>
(= (+ (3) (7)) (10))
3plus8 # <title> One-digit Addition </title>
(= (+ (3) (8)) (+ (10) (1)))
3plus9 # <title> One-digit Addition </title>
(= (+ (3) (9)) (+ (10) (2)))
3plus10 # <title> One-digit Addition </title>
(= (+ (3) (10)) (+ (10) (3)))
4plus2 # <title> One-digit Addition </title>
(= (+ (4) (2)) (6))
4plus3 # <title> One-digit Addition </title>
(= (+ (4) (3)) (7))
4plus4 # <title> One-digit Addition </title>
(= (+ (4) (4)) (8))
4plus5 # <title> One-digit Addition 4+5=9 </title> # <summary> # This theorem proves that 4 + 5 = 9. To prove such a basic fact, we must directly use # the definitions of the numbers. The number 2 is defined as 2 = 1 + 1, 3 = 2 + 1, # 4 = 3 + 1, and so on. The theorem uses these definitions along with the # <a href="/edit/peano/peano_thms.gh/addass">associate property</a> to prove 4 + 5 = 9. # </summary>
(= (+ (4) (5)) (9))
4plus6 # <title> One-digit Addition </title>
(= (+ (4) (6)) (10))
4plus7 # <title> One-digit Addition </title>
(= (+ (4) (7)) (+ (10) (1)))
4plus8 # <title> One-digit Addition </title>
(= (+ (4) (8)) (+ (10) (2)))
4plus9 # <title> One-digit Addition </title>
(= (+ (4) (9)) (+ (10) (3)))
4plus10 # <title> One-digit Addition </title>
(= (+ (4) (10)) (+ (10) (4)))
5plus2 # <title> One-digit Addition </title>
(= (+ (5) (2)) (7))
5plus3 # <title> One-digit Addition </title>
(= (+ (5) (3)) (8))
5plus4 # <title> One-digit Addition </title>
(= (+ (5) (4)) (9))
5plus5 # <title> One-digit Addition </title>
(= (+ (5) (5)) (10))
5plus6 # <title> One-digit Addition </title>
(= (+ (5) (6)) (+ (10) (1)))
5plus7 # <title> One-digit Addition </title>
(= (+ (5) (7)) (+ (10) (2)))
5plus8 # <title> One-digit Addition </title>
(= (+ (5) (8)) (+ (10) (3)))
5plus9 # <title> One-digit Addition </title>
(= (+ (5) (9)) (+ (10) (4)))
5plus10 # <title> One-digit Addition </title>
(= (+ (5) (10)) (+ (10) (5)))
6plus2 # <title> One-digit Addition </title>
(= (+ (6) (2)) (8))
6plus3 # <title> One-digit Addition </title>
(= (+ (6) (3)) (9))
6plus4 # <title> One-digit Addition </title>
(= (+ (6) (4)) (10))
6plus5 # <title> One-digit Addition </title>
(= (+ (6) (5)) (+ (10) (1)))
6plus6 # <title> One-digit Addition </title>
(= (+ (6) (6)) (+ (10) (2)))
6plus7 # <title> One-digit Addition </title>
(= (+ (6) (7)) (+ (10) (3)))
6plus8 # <title> One-digit Addition </title>
(= (+ (6) (8)) (+ (10) (4)))
6plus9 # <title> One-digit Addition </title>
(= (+ (6) (9)) (+ (10) (5)))
6plus10 # <title> One-digit Addition </title>
(= (+ (6) (10)) (+ (10) (6)))
7plus2 # <title> One-digit Addition </title>
(= (+ (7) (2)) (9))
7plus3 # <title> One-digit Addition </title>
(= (+ (7) (3)) (10))
7plus4 # <title> One-digit Addition </title>
(= (+ (7) (4)) (+ (10) (1)))
7plus5 # <title> One-digit Addition </title>
(= (+ (7) (5)) (+ (10) (2)))
7plus6 # <title> One-digit Addition </title>
(= (+ (7) (6)) (+ (10) (3)))
7plus7 # <title> One-digit Addition </title>
(= (+ (7) (7)) (+ (10) (4)))
7plus8 # <title> One-digit Addition </title>
(= (+ (7) (8)) (+ (10) (5)))
7plus9 # <title> One-digit Addition </title>
(= (+ (7) (9)) (+ (10) (6)))
7plus10 # <title> One-digit Addition </title>
(= (+ (7) (10)) (+ (10) (7)))
8plus2 # <title> One-digit Addition </title>
(= (+ (8) (2)) (10))
8plus3 # <title> One-digit Addition </title>
(= (+ (8) (3)) (+ (10) (1)))
8plus4 # <title> One-digit Addition </title>
(= (+ (8) (4)) (+ (10) (2)))
8plus5 # <title> One-digit Addition </title>
(= (+ (8) (5)) (+ (10) (3)))
8plus6 # <title> One-digit Addition </title>
(= (+ (8) (6)) (+ (10) (4)))
8plus7 # <title> One-digit Addition </title>
(= (+ (8) (7)) (+ (10) (5)))
8plus8 # <title> One-digit Addition </title>
(= (+ (8) (8)) (+ (10) (6)))
8plus9 # <title> One-digit Addition </title>
(= (+ (8) (9)) (+ (10) (7)))
8plus10 # <title> One-digit Addition </title>
(= (+ (8) (10)) (+ (10) (8)))
9plus2 # <title> One-digit Addition </title>
(= (+ (9) (2)) (+ (10) (1)))
9plus3 # <title> One-digit Addition </title>
(= (+ (9) (3)) (+ (10) (2)))
9plus4 # <title> One-digit Addition </title>
(= (+ (9) (4)) (+ (10) (3)))
9plus5 # <title> One-digit Addition </title>
(= (+ (9) (5)) (+ (10) (4)))
9plus6 # <title> One-digit Addition </title>
(= (+ (9) (6)) (+ (10) (5)))
9plus7 # <title> One-digit Addition </title>
(= (+ (9) (7)) (+ (10) (6)))
9plus8 # <title> One-digit Addition </title>
(= (+ (9) (8)) (+ (10) (7)))
9plus9 # <title> One-digit Addition </title>
(= (+ (9) (9)) (+ (10) (8)))
9plus10 # <title> One-digit Addition </title>
(= (+ (9) (10)) (+ (10) (9)))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
10plus10 # <title> One-digit Addition </title>
(= (+ (10) (10)) (* (2) (10)))

## Multiplication Tables

2times2 ---- Automatically generated with GH.ProofGenerator.evaluator.batchEvaluation('*', [2, 9], [2, 9]); # <context> # This theorem is part of a series of theorems that prove basic one-digit multiplication # formulas. These theorems work by splitting a large number into the sum of two smaller numbers # and then applying addition and multiplication formulas for the smaller numbers. # </context> # <title> One-digit Multiplication </title>
(= (* (2) (2)) (4))
2times3 # <title> One-digit Multiplication </title>
(= (* (2) (3)) (6))
2times4 # <title> One-digit Multiplication </title>
(= (* (2) (4)) (8))
2times5 # <title> One-digit Multiplication </title>
(= (* (2) (5)) (10))
2times6 # <title> One-digit Multiplication </title>
(= (* (2) (6)) (+ (10) (2)))
2times7 # <title> One-digit Multiplication </title>
(= (* (2) (7)) (+ (10) (4)))
2times8 # <title> One-digit Multiplication </title>
(= (* (2) (8)) (+ (10) (6)))
2times9 # <title> One-digit Multiplication </title>
(= (* (2) (9)) (+ (10) (8)))
3times2 # <title> One-digit Multiplication </title>
(= (* (3) (2)) (6))
3times3 # <title> One-digit Multiplication </title>
(= (* (3) (3)) (9))
3times4 # <title> One-digit Multiplication </title>
(= (* (3) (4)) (+ (10) (2)))
3times5 # <title> One-digit Multiplication </title>
(= (* (3) (5)) (+ (10) (5)))
3times6 # <title> One-digit Multiplication </title>
(= (* (3) (6)) (+ (10) (8)))
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'))
EqReplaceEq1Add0Mul0 # <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'))
3times7 # <title> One-digit Multiplication </title>
(= (* (3) (7)) (+ (* (2) (10)) (1)))
3times8 # <title> One-digit Multiplication </title>
(= (* (3) (8)) (+ (* (2) (10)) (4)))
3times9 # <title> One-digit Multiplication </title>
(= (* (3) (9)) (+ (* (2) (10)) (7)))
4times2 # <title> One-digit Multiplication </title>
(= (* (4) (2)) (8))
4times3 # <title> One-digit Multiplication </title>
(= (* (4) (3)) (+ (10) (2)))
4times4 # <title> One-digit Multiplication </title>
(= (* (4) (4)) (+ (10) (6)))
4times5 # <title> One-digit Multiplication </title>
(= (* (4) (5)) (* (2) (10)))
4times6 # <title> One-digit Multiplication </title>
(= (* (4) (6)) (+ (* (2) (10)) (4)))
4times7 # <title> One-digit Multiplication </title>
(= (* (4) (7)) (+ (* (2) (10)) (8)))
4times8 # <title> One-digit Multiplication </title>
(= (* (4) (8)) (+ (* (3) (10)) (2)))
4times9 # <title> One-digit Multiplication </title>
(= (* (4) (9)) (+ (* (3) (10)) (6)))
5times2 # <title> One-digit Multiplication </title>
(= (* (5) (2)) (10))
5times3 # <title> One-digit Multiplication </title>
(= (* (5) (3)) (+ (10) (5)))
5times4 # <title> One-digit Multiplication </title>
(= (* (5) (4)) (* (2) (10)))
5times5 # <title> One-digit Multiplication </title>
(= (* (5) (5)) (+ (* (2) (10)) (5)))
5times6 # <title> One-digit Multiplication </title>
(= (* (5) (6)) (* (3) (10)))
5times7 # <title> One-digit Multiplication </title>
(= (* (5) (7)) (+ (* (3) (10)) (5)))
5times8 # <title> One-digit Multiplication </title>
(= (* (5) (8)) (* (4) (10)))
5times9 # <title> One-digit Multiplication </title>
(= (* (5) (9)) (+ (* (4) (10)) (5)))
6times2 # <title> One-digit Multiplication </title>
(= (* (6) (2)) (+ (10) (2)))
6times3 # <title> One-digit Multiplication </title>
(= (* (6) (3)) (+ (10) (8)))
6times4 # <title> One-digit Multiplication </title>
(= (* (6) (4)) (+ (* (2) (10)) (4)))
6times5 # <title> One-digit Multiplication </title>
(= (* (6) (5)) (* (3) (10)))
6times6 # <title> One-digit Multiplication </title>
(= (* (6) (6)) (+ (* (3) (10)) (6)))
6times7 # <title> One-digit Multiplication </title>
(= (* (6) (7)) (+ (* (4) (10)) (2)))
6times8 # <title> One-digit Multiplication </title>
(= (* (6) (8)) (+ (* (4) (10)) (8)))
6times9 # <title> One-digit Multiplication </title>
(= (* (6) (9)) (+ (* (5) (10)) (4)))
7times2 # <title> One-digit Multiplication </title>
(= (* (7) (2)) (+ (10) (4)))
7times3 # <title> One-digit Multiplication </title>
(= (* (7) (3)) (+ (* (2) (10)) (1)))
7times4 # <title> One-digit Multiplication </title>
(= (* (7) (4)) (+ (* (2) (10)) (8)))
7times5 # <title> One-digit Multiplication </title>
(= (* (7) (5)) (+ (* (3) (10)) (5)))
7times6 # <title> One-digit Multiplication </title>
(= (* (7) (6)) (+ (* (4) (10)) (2)))
7times7 # <title> One-digit Multiplication </title>
(= (* (7) (7)) (+ (* (4) (10)) (9)))
7times8 # <title> One-digit Multiplication </title>
(= (* (7) (8)) (+ (* (5) (10)) (6)))
7times9 # <title> One-digit Multiplication </title>
(= (* (7) (9)) (+ (* (6) (10)) (3)))
8times2 # <title> One-digit Multiplication </title>
(= (* (8) (2)) (+ (10) (6)))
8times3 # <title> One-digit Multiplication </title>
(= (* (8) (3)) (+ (* (2) (10)) (4)))
8times4 # <title> One-digit Multiplication </title>
(= (* (8) (4)) (+ (* (3) (10)) (2)))
8times5 # <title> One-digit Multiplication </title>
(= (* (8) (5)) (* (4) (10)))
8times6 # <title> One-digit Multiplication </title>
(= (* (8) (6)) (+ (* (4) (10)) (8)))
8times7 # <title> One-digit Multiplication </title>
(= (* (8) (7)) (+ (* (5) (10)) (6)))
8times8 # <title> One-digit Multiplication </title>
(= (* (8) (8)) (+ (* (6) (10)) (4)))
8times9 # <title> One-digit Multiplication </title>
(= (* (8) (9)) (+ (* (7) (10)) (2)))
9times2 # <title> One-digit Multiplication </title>
(= (* (9) (2)) (+ (10) (8)))
9times3 # <title> One-digit Multiplication </title>
(= (* (9) (3)) (+ (* (2) (10)) (7)))
9times4 # <title> One-digit Multiplication </title>
(= (* (9) (4)) (+ (* (3) (10)) (6)))
9times5 # <title> One-digit Multiplication </title>
(= (* (9) (5)) (+ (* (4) (10)) (5)))
9times6 # <title> One-digit Multiplication </title>
(= (* (9) (6)) (+ (* (5) (10)) (4)))
9times7 # <title> One-digit Multiplication </title>
(= (* (9) (7)) (+ (* (6) (10)) (3)))
9times8 # <title> One-digit Multiplication </title>
(= (* (9) (8)) (+ (* (7) (10)) (2)))
9times9 # <title> One-digit Multiplication </title>
(= (* (9) (9)) (+ (* (8) (10)) (1)))
EqReplaceEq1Add0Add0 # <context> # This theorem is part of a series of theorems demonstrating multi-digit addition and multiplication. # </context> # <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'))
EqReplaceEq1Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ B (* [ C ] ] ] A')) B')) # (= [ C ] [ D ] ) # (= A (+ (+ B (* [ [ [ D ] A')) B')) # </table>
(= A (+ (+ B (* C A')) B')) , (= C D)(= A (+ (+ B (* D A')) B'))
EqReplaceEq1Add0Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (* [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (* [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (* B D) A') B')) , (= B C)(= A (+ (+ (* C D) A') B'))
additionExample # <summary> This is an example of multi-digit addition. There is nothing particularly remarkable about these specific numbers. </summary>
(= (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7))) (+ (* (2) (* (10) (10))) (+ (10) (2))))
EqReplaceEq1Add0Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ [ B ] ] ] D) A') B') C')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ (+ [ [ [ C ] D) A') B') C')) # </table>
(= A (+ (+ (+ (+ B D) A') B') C')) , (= B C)(= A (+ (+ (+ (+ C D) A') B') C'))
EqReplaceEq1Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ B [ C ] ] ] ) A') B') C')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ B [ [ [ D ] ) A') B') C')) # </table>
(= A (+ (+ (+ (+ B C) A') B') C')) , (= C D)(= A (+ (+ (+ (+ B D) A') B') C'))
EqReplaceEq1Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (+ B D) A') B')) , (= B C)(= A (+ (+ (+ C D) A') B'))
EqReplaceEq1Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ B [ C ] ] ] ) A') B')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ B [ [ [ D ] ) A') B')) # </table>
(= A (+ (+ (+ B C) A') B')) , (= C D)(= A (+ (+ (+ B D) A') B'))
EqReplaceEq1Add0Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ (+ B [ C ] ] ] ) A') B') C') D')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ (+ B [ [ [ D ] ) A') B') C') D')) # </table>
(= A (+ (+ (+ (+ (+ B C) A') B') C') D')) , (= C D)(= A (+ (+ (+ (+ (+ B D) A') B') C') D'))
EqReplaceEq1Add0Add0Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ (+ [ B ] ] ] D) A') B') C') D')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ (+ (+ [ [ [ C ] D) A') B') C') D')) # </table>
(= A (+ (+ (+ (+ (+ B D) A') B') C') D')) , (= B C)(= A (+ (+ (+ (+ (+ C D) A') B') C') D'))
EqReplaceEq1Add0Add0Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ (+ (+ B [ C ] ] ] ) A') B') C') D') A0)) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ (+ (+ B [ [ [ D ] ) A') B') C') D') A0)) # </table>
(= A (+ (+ (+ (+ (+ (+ B C) A') B') C') D') A0)) , (= C D)(= A (+ (+ (+ (+ (+ (+ B D) A') B') C') D') A0))
EqReplaceEq1Add0Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ B (* [ C ] ] ] A')) B') C')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ B (* [ [ [ D ] A')) B') C')) # </table>
(= A (+ (+ (+ B (* C A')) B') C')) , (= C D)(= A (+ (+ (+ B (* D A')) B') C'))
EqReplaceEq1Add0Add0Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (* [ B ] ] ] D) A') B') C')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ (* [ [ [ C ] D) A') B') C')) # </table>
(= A (+ (+ (+ (* B D) A') B') C')) , (= B C)(= A (+ (+ (+ (* C D) A') B') C'))
additionExample2 # <summary> This is an example of multi-digit addition. There is nothing particularly remarkable about these specific numbers. </summary>
(= (+ (+ (* (10) (* (10) (10))) (+ (* (4) (* (10) (10))) (+ (* (9) (10)) (2)))) (+ (* (5) (* (10) (* (10) (10)))) (+ (* (4) (* (10) (10))) (+ (* (8) (10)) (3))))) (+ (* (6) (* (10) (* (10) (10)))) (+ (* (9) (* (10) (10))) (+ (* (7) (10)) (5)))))
multiplicationExample # <summary> This is an example of multi-digit multiplication. There is nothing particularly remarkable about these specific numbers. </summary>
(= (* (+ (10) (7)) (+ (10) (3))) (+ (* (2) (* (10) (10))) (+ (* (2) (10)) (1))))
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')))
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
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')))
EqReplaceEq1Add0Add0Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ B (* [ C ] ] ] A')) B') C') D')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ B (* [ [ [ D ] A')) B') C') D')) # </table>
(= A (+ (+ (+ (+ B (* C A')) B') C') D')) , (= C D)(= A (+ (+ (+ (+ B (* D A')) B') C') D'))
multiplicationExample2 # <summary> This is an example of multi-digit multiplication. There is nothing particularly remarkable about these specific numbers. </summary>
(= (* (+ (* (3) (* (10) (10))) (+ (* (8) (10)) (7))) (+ (* (2) (* (10) (10))) (3))) (+ (* (7) (* (10) (* (10) (* (10) (10))))) (+ (* (8) (* (10) (* (10) (10)))) (+ (* (5) (* (10) (10))) (+ (* (6) (10)) (1))))))

## Inequalities

EqReplaceLt0 # <title> Substitution </title> # <table> # (< [ A ] ] ] C) # (= [ A ] [ B ] ) # (< [ [ [ B ] C) # </table>
(< A C) , (= A B)(< B C)
EqReplaceLt1 # <title> Substitution </title> # <table> # (< A [ B ] ] ] ) # (= [ B ] [ C ] ) # (< A [ [ [ C ] ) # </table>
(< A B) , (= B C)(< A C)
1less2 # <title> One-Digit Inequality </title>
(< (1) (2))
LtReplaceLt1 # <title> Substitution </title> # <table> # (< A [ B ] ] ] ) # (< [ B ] [ C ] ) # (< A [ [ [ C ] ) # </table>
(< A B) , (< B C)(< A C)
0less2 # <title> One-Digit Inequality </title>
(< (0) (2))
2less3 # <title> One-Digit Inequality </title>
(< (2) (3))
0less3 # <title> One-Digit Inequality </title>
(< (0) (3))
3less4 # <title> One-Digit Inequality </title>
(< (3) (4))
0less4 # <title> One-Digit Inequality </title>
(< (0) (4))
4less5 # <title> One-Digit Inequality </title>
(< (4) (5))
0less5 # <title> One-Digit Inequality </title>
(< (0) (5))
5less6 # <title> One-Digit Inequality </title>
(< (5) (6))
0less6 # <title> One-Digit Inequality </title>
(< (0) (6))
6less7 # <title> One-Digit Inequality </title>
(< (6) (7))
0less7 # <title> One-Digit Inequality </title>
(< (0) (7))
7less8 # <title> One-Digit Inequality </title>
(< (7) (8))
0less8 # <title> One-Digit Inequality </title>
(< (0) (8))
8less9 # <title> One-Digit Inequality </title>
(< (8) (9))
0less9 # <title> One-Digit Inequality </title>
(< (0) (9))
9less10 # <title> One-Digit Inequality </title>
(< (9) (10))
0less10 # <title> One-Digit Inequality </title>
(< (0) (10))
1less3 # <title> One-Digit Inequality </title>
(< (1) (3))
1less4 # <title> One-Digit Inequality </title>
(< (1) (4))
1less5 # <title> One-Digit Inequality </title>
(< (1) (5))
1less6 # <title> One-Digit Inequality </title>
(< (1) (6))
1less7 # <title> One-Digit Inequality </title>
(< (1) (7))
1less8 # <title> One-Digit Inequality </title>
(< (1) (8))
1less9 # <title> One-Digit Inequality </title>
(< (1) (9))
1less10 # <title> One-Digit Inequality </title>
(< (1) (10))
EqReplaceGt0 # <title> Substitution </title> # <table> # (> [ A ] ] ] C) # (= [ A ] [ B ] ) # (> [ [ [ B ] C) # </table>
(> A C) , (= A B)(> B C)
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
2greater1 # <title> One-Digit Inequality </title>
(> (2) (1))
GtReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (> [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (> B C)(> A C)
2greater0 # <title> One-Digit Inequality </title>
(> (2) (0))
2less4 # <title> One-Digit Inequality </title>
(< (2) (4))
2less5 # <title> One-Digit Inequality </title>
(< (2) (5))
2less6 # <title> One-Digit Inequality </title>
(< (2) (6))
2less7 # <title> One-Digit Inequality </title>
(< (2) (7))
2less8 # <title> One-Digit Inequality </title>
(< (2) (8))
2less9 # <title> One-Digit Inequality </title>
(< (2) (9))
2less10 # <title> One-Digit Inequality </title>
(< (2) (10))
3greater2 # <title> One-Digit Inequality </title>
(> (3) (2))
3greater0 # <title> One-Digit Inequality </title>
(> (3) (0))
3greater1 # <title> One-Digit Inequality </title>
(> (3) (1))
3less5 # <title> One-Digit Inequality </title>
(< (3) (5))
3less6 # <title> One-Digit Inequality </title>
(< (3) (6))
3less7 # <title> One-Digit Inequality </title>
(< (3) (7))
3less8 # <title> One-Digit Inequality </title>
(< (3) (8))
3less9 # <title> One-Digit Inequality </title>
(< (3) (9))
3less10 # <title> One-Digit Inequality </title>
(< (3) (10))
4greater3 # <title> One-Digit Inequality </title>
(> (4) (3))
4greater0 # <title> One-Digit Inequality </title>
(> (4) (0))
4greater1 # <title> One-Digit Inequality </title>
(> (4) (1))
4greater2 # <title> One-Digit Inequality </title>
(> (4) (2))
4less6 # <title> One-Digit Inequality </title>
(< (4) (6))
4less7 # <title> One-Digit Inequality </title>
(< (4) (7))
4less8 # <title> One-Digit Inequality </title>
(< (4) (8))
4less9 # <title> One-Digit Inequality </title>
(< (4) (9))
4less10 # <title> One-Digit Inequality </title>
(< (4) (10))
5greater4 # <title> One-Digit Inequality </title>
(> (5) (4))
5greater0 # <title> One-Digit Inequality </title>
(> (5) (0))
5greater1 # <title> One-Digit Inequality </title>
(> (5) (1))
5greater2 # <title> One-Digit Inequality </title>
(> (5) (2))
5greater3 # <title> One-Digit Inequality </title>
(> (5) (3))
5less7 # <title> One-Digit Inequality </title>
(< (5) (7))
5less8 # <title> One-Digit Inequality </title>
(< (5) (8))
5less9 # <title> One-Digit Inequality </title>
(< (5) (9))
5less10 # <title> One-Digit Inequality </title>
(< (5) (10))
6greater5 # <title> One-Digit Inequality </title>
(> (6) (5))
6greater0 # <title> One-Digit Inequality </title>
(> (6) (0))
6greater1 # <title> One-Digit Inequality </title>
(> (6) (1))
6greater2 # <title> One-Digit Inequality </title>
(> (6) (2))
6greater3 # <title> One-Digit Inequality </title>
(> (6) (3))
6greater4 # <title> One-Digit Inequality </title>
(> (6) (4))
6less8 # <title> One-Digit Inequality </title>
(< (6) (8))
6less9 # <title> One-Digit Inequality </title>
(< (6) (9))
6less10 # <title> One-Digit Inequality </title>
(< (6) (10))
7greater6 # <title> One-Digit Inequality </title>
(> (7) (6))
7greater0 # <title> One-Digit Inequality </title>
(> (7) (0))
7greater1 # <title> One-Digit Inequality </title>
(> (7) (1))
7greater2 # <title> One-Digit Inequality </title>
(> (7) (2))
7greater3 # <title> One-Digit Inequality </title>
(> (7) (3))
7greater4 # <title> One-Digit Inequality </title>
(> (7) (4))
7greater5 # <title> One-Digit Inequality </title>
(> (7) (5))
7less9 # <title> One-Digit Inequality </title>
(< (7) (9))
7less10 # <title> One-Digit Inequality </title>
(< (7) (10))
8greater7 # <title> One-Digit Inequality </title>
(> (8) (7))
8greater0 # <title> One-Digit Inequality </title>
(> (8) (0))
8greater1 # <title> One-Digit Inequality </title>
(> (8) (1))
8greater2 # <title> One-Digit Inequality </title>
(> (8) (2))
8greater3 # <title> One-Digit Inequality </title>
(> (8) (3))
8greater4 # <title> One-Digit Inequality </title>
(> (8) (4))
8greater5 # <title> One-Digit Inequality </title>
(> (8) (5))
8greater6 # <title> One-Digit Inequality </title>
(> (8) (6))
8less10 # <title> One-Digit Inequality </title>
(< (8) (10))
9greater8 # <title> One-Digit Inequality </title>
(> (9) (8))
9greater0 # <title> One-Digit Inequality </title>
(> (9) (0))
9greater1 # <title> One-Digit Inequality </title>
(> (9) (1))
9greater2 # <title> One-Digit Inequality </title>
(> (9) (2))
9greater3 # <title> One-Digit Inequality </title>
(> (9) (3))
9greater4 # <title> One-Digit Inequality </title>
(> (9) (4))
9greater5 # <title> One-Digit Inequality </title>
(> (9) (5))
9greater6 # <title> One-Digit Inequality </title>
(> (9) (6))
9greater7 # <title> One-Digit Inequality </title>
(> (9) (7))
10greater9 # <title> One-Digit Inequality </title>
(> (10) (9))
10greater0 # <title> One-Digit Inequality </title>
(> (10) (0))
10greater1 # <title> One-Digit Inequality </title>
(> (10) (1))
10greater2 # <title> One-Digit Inequality </title>
(> (10) (2))
10greater3 # <title> One-Digit Inequality </title>
(> (10) (3))
10greater4 # <title> One-Digit Inequality </title>
(> (10) (4))
10greater5 # <title> One-Digit Inequality </title>
(> (10) (5))
10greater6 # <title> One-Digit Inequality </title>
(> (10) (6))
10greater7 # <title> One-Digit Inequality </title>
(> (10) (7))
10greater8 # <title> One-Digit Inequality </title>
(> (10) (8))
lessThanExample # <context> # This theorem is part of a series of theorems on multi-digit inequalities. # </context>
(< (+ (* (2) (10)) (6)) (+ (* (7) (* (10) (10))) (+ (* (3) (10)) (9))))
(<= (+ (* (4) (10)) (2)) (+ (* (6) (* (10) (10))) (+ (* (3) (10)) (9))))
(> (+ (* (3) (* (10) (10))) (* (4) (10))) (+ (* (8) (10)) (1)))
(-. (= (+ (10) (8)) (+ (* (6) (10)) (7))))
1notEqual0 # <title> One-Digit Inequality </title>
(-. (= (1) (0)))
2notEqual0 # <title> One-Digit Inequality </title>
(-. (= (2) (0)))
3notEqual0 # <title> One-Digit Inequality </title>
(-. (= (3) (0)))
4notEqual0 # <title> One-Digit Inequality </title>
(-. (= (4) (0)))
5notEqual0 # <title> One-Digit Inequality </title>
(-. (= (5) (0)))
6notEqual0 # <title> One-Digit Inequality </title>
(-. (= (6) (0)))
7notEqual0 # <title> One-Digit Inequality </title>
(-. (= (7) (0)))
8notEqual0 # <title> One-Digit Inequality </title>
(-. (= (8) (0)))
9notEqual0 # <title> One-Digit Inequality </title>
(-. (= (9) (0)))
10notEqual0 # <title> One-Digit Inequality </title>
(-. (= (10) (0)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)