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 ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elnnnn0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) )
2 facp1 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) )
3 2 adantl ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ! ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) )
4 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
5 4 fveq2d ⊢ ( 𝑁 ∈ ℂ → ( ! ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ! ‘ 𝑁 ) )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ! ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ! ‘ 𝑁 ) )
7 4 oveq2d ⊢ ( 𝑁 ∈ ℂ → ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
8 7 adantr ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
9 3 6 8 3eqtr3d ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
10 1 9 sylbi ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )