This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem facnn2

Description: Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004)

Ref Expression
Assertion facnn2 ⊢ N ∈ ℕ → N ! = N − 1 ! ⋅ N

Proof

Step Hyp Ref Expression
1 elnnnn0 ⊢ N ∈ ℕ ↔ N ∈ ℂ ∧ N − 1 ∈ ℕ 0
2 facp1 ⊢ N − 1 ∈ ℕ 0 → N - 1 + 1 ! = N − 1 ! ⁢ N - 1 + 1
3 2 adantl ⊢ N ∈ ℂ ∧ N − 1 ∈ ℕ 0 → N - 1 + 1 ! = N − 1 ! ⁢ N - 1 + 1
4 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
5 4 fveq2d ⊢ N ∈ ℂ → N - 1 + 1 ! = N !
6 5 adantr ⊢ N ∈ ℂ ∧ N − 1 ∈ ℕ 0 → N - 1 + 1 ! = N !
7 4 oveq2d ⊢ N ∈ ℂ → N − 1 ! ⁢ N - 1 + 1 = N − 1 ! ⋅ N
8 7 adantr ⊢ N ∈ ℂ ∧ N − 1 ∈ ℕ 0 → N − 1 ! ⁢ N - 1 + 1 = N − 1 ! ⋅ N
9 3 6 8 3eqtr3d ⊢ N ∈ ℂ ∧ N − 1 ∈ ℕ 0 → N ! = N − 1 ! ⋅ N
10 1 9 sylbi ⊢ N ∈ ℕ → N ! = N − 1 ! ⋅ N