## Factorial !

The factorial of x is the product of all numbers from (1) to x. It is initially defined as (= (! A) (product (1) A (lambda x x))) /edit/peano/peano_thms.gh/df-factorial. From this definition the recursive definition is derived:

• (= (! A) (* (! (.- A (1))) A)) /edit/peano/peano_thms.gh/factorialpred

### Examples

• (= (! (0)) (1)) /edit/peano/peano_thms.gh/factorial0
• (= (! (1)) (1)) /edit/peano/peano_thms.gh/factorial1
• (/\ (= (! (2)) (* (1) (2))) (= (* (1) (2)) (2))) /edit/peano/arithmetic.gh/factorial2
• (/\ (= (! (3)) (* (* (1) (2)) (3))) (= (* (* (1) (2)) (3)) (6))) /edit/peano/arithmetic.gh/factorial3
• (/\ (= (! (4)) (* (* (* (1) (2)) (3)) (4))) (= (* (* (* (1) (2)) (3)) (4)) (+ (* (2) (10)) (4)) )) /edit/peano/arithmetic.gh/factorial4
• (/\ (= (! (5)) (* (* (* (* (1) (2)) (3)) (4)) (5))) (= (* (* (* (* (1) (2)) (3)) (4)) (5)) (+ (* (10) (10)) (* (2) (10))) )) /edit/peano/arithmetic.gh/factorial5
• (/\ (= (! (6)) (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6))) (= (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (+ (* (7) (* (10) (10))) (* (2) (10))) )) /edit/peano/arithmetic.gh/factorial6
• (/\ (= (! (7)) (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7))) (= (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7)) (+ (* (5) (* (10) (* (10) (10)))) (* (4) (10))) )) /edit/peano/arithmetic.gh/factorial7
• (/\ (= (! (8)) (* (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7)) (8))) (= (* (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7)) (8)) (+ (* (4) (* (10) (* (10) (* (10) (10))))) (+ (* (3) (* (10) (10))) (* (2) (10)))) )) /edit/peano/arithmetic.gh/factorial8