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 ) ) · 𝑁 ) )