Theorem facp1

Description: The factorial of a successor. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	facp1	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		peano2nn	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
3		facnn	⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( ! ‘ ( 𝑁 + 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑁 + 1 ) ) )
4	2 3	syl	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 + 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑁 + 1 ) ) )
5		ovex	⊢ ( 𝑁 + 1 ) ∈ V
6		fvi	⊢ ( ( 𝑁 + 1 ) ∈ V → ( I ‘ ( 𝑁 + 1 ) ) = ( 𝑁 + 1 ) )
7	5 6	ax-mp	⊢ ( I ‘ ( 𝑁 + 1 ) ) = ( 𝑁 + 1 )
8	7	oveq2i	⊢ ( ( seq 1 ( · , I ) ‘ 𝑁 ) · ( I ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 1 ( · , I ) ‘ 𝑁 ) · ( 𝑁 + 1 ) )
9		seqp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , I ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , I ) ‘ 𝑁 ) · ( I ‘ ( 𝑁 + 1 ) ) ) )
10		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
11	9 10	eleq2s	⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( · , I ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , I ) ‘ 𝑁 ) · ( I ‘ ( 𝑁 + 1 ) ) ) )
12		facnn	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
13	12	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , I ) ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
14	8 11 13	3eqtr4a	⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( · , I ) ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
15	4 14	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
16		0p1e1	⊢ ( 0 + 1 ) = 1
17	16	fveq2i	⊢ ( ! ‘ ( 0 + 1 ) ) = ( ! ‘ 1 )
18		fac1	⊢ ( ! ‘ 1 ) = 1
19	17 18	eqtri	⊢ ( ! ‘ ( 0 + 1 ) ) = 1
20		fvoveq1	⊢ ( 𝑁 = 0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ! ‘ ( 0 + 1 ) ) )
21		fveq2	⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = ( ! ‘ 0 ) )
22		oveq1	⊢ ( 𝑁 = 0 → ( 𝑁 + 1 ) = ( 0 + 1 ) )
23	21 22	oveq12d	⊢ ( 𝑁 = 0 → ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) = ( ( ! ‘ 0 ) · ( 0 + 1 ) ) )
24		fac0	⊢ ( ! ‘ 0 ) = 1
25	24 16	oveq12i	⊢ ( ( ! ‘ 0 ) · ( 0 + 1 ) ) = ( 1 · 1 )
26		1t1e1	⊢ ( 1 · 1 ) = 1
27	25 26	eqtri	⊢ ( ( ! ‘ 0 ) · ( 0 + 1 ) ) = 1
28	23 27	eqtrdi	⊢ ( 𝑁 = 0 → ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) = 1 )
29	19 20 28	3eqtr4a	⊢ ( 𝑁 = 0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
30	15 29	jaoi	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
31	1 30	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )