Natural number addition is defined recursively through the Peano axioms using the successor operation. Natural number addition is used to construct integer addition. Integer addition is used to construct rational addition. Real addition is used to construct complex addition. Since there are different versions of addition for each type of number, the properties are proved for each type of number. (The real numbers have not been constructed yet.)

### Properties

• Commutation: (= (+ a b) (+ b a)) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/addcom
• Association: (= (+ (+ a b) c) (+ a (+ b c))) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/addass
• Identity: (= (+ a (0)) a) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/addid
• Distribution: (= (* a (+ b c)) (+ (* a b) (* a c))) /edit/peano_new/arithmetic/common/add_multiply_min.ghi/distr

• (+ (1) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus1, (+ (1) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus2, (+ (1) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus3, (+ (1) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus4, (+ (1) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus5, (+ (1) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus6, (+ (1) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus7, (+ (1) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus8, (+ (1) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/1plus9
• (+ (2) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus1, (+ (2) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus2, (+ (2) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus3, (+ (2) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus4, (+ (2) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus5, (+ (2) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus6, (+ (2) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus7, (+ (2) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus8, (+ (2) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/2plus9
• (+ (3) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus1, (+ (3) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus2, (+ (3) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus3, (+ (3) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus4, (+ (3) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus5, (+ (3) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus6, (+ (3) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus7, (+ (3) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus8, (+ (3) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/3plus9
• (+ (4) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus1, (+ (4) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus2, (+ (4) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus3, (+ (4) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus4, (+ (4) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus5, (+ (4) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus6, (+ (4) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus7, (+ (4) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus8, (+ (4) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/4plus9
• (+ (5) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus1, (+ (5) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus2, (+ (5) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus3, (+ (5) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus4, (+ (5) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus5, (+ (5) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus6, (+ (5) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus7, (+ (5) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus8, (+ (5) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/5plus9
• (+ (6) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus1, (+ (6) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus2, (+ (6) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus3, (+ (6) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus4, (+ (6) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus5, (+ (6) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus6, (+ (6) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus7, (+ (6) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus8, (+ (6) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/6plus9
• (+ (7) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus1, (+ (7) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus2, (+ (7) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus3, (+ (7) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus4, (+ (7) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus5, (+ (7) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus6, (+ (7) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus7, (+ (7) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus8, (+ (7) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/7plus9
• (+ (8) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus1, (+ (8) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus2, (+ (8) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus3, (+ (8) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus4, (+ (8) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus5, (+ (8) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus6, (+ (8) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus7, (+ (8) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus8, (+ (8) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/8plus9
• (+ (9) (1)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus1, (+ (9) (2)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus2, (+ (9) (3)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus3, (+ (9) (4)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus4, (+ (9) (5)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus5, (+ (9) (6)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus6, (+ (9) (7)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus7, (+ (9) (8)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus8, (+ (9) (9)) /edit/peano_new/arithmetic/common/calculations/naturals.gh/9plus9

### Multi-Digit Examples

• (= (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7))) (+ (* (2) (* (10) (10))) (+ (10) (2)))) /edit/peano_new/arithmetic/common/calculations/naturals.gh/additionExample
• (= (+ (+ (* (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))))) /edit/peano_new/arithmetic/common/calculations/naturals.gh/additionExample2