# Metamath Proof Explorer

## 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 ${⊢}{N}\in {ℕ}_{0}\to \left({N}+1\right)!={N}!\left({N}+1\right)$

### Proof

Step Hyp Ref Expression
1 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
2 peano2nn ${⊢}{N}\in ℕ\to {N}+1\in ℕ$
3 facnn ${⊢}{N}+1\in ℕ\to \left({N}+1\right)!=seq1\left(×,\mathrm{I}\right)\left({N}+1\right)$
4 2 3 syl ${⊢}{N}\in ℕ\to \left({N}+1\right)!=seq1\left(×,\mathrm{I}\right)\left({N}+1\right)$
5 ovex ${⊢}{N}+1\in \mathrm{V}$
6 fvi ${⊢}{N}+1\in \mathrm{V}\to \mathrm{I}\left({N}+1\right)={N}+1$
7 5 6 ax-mp ${⊢}\mathrm{I}\left({N}+1\right)={N}+1$
8 7 oveq2i ${⊢}seq1\left(×,\mathrm{I}\right)\left({N}\right)\mathrm{I}\left({N}+1\right)=seq1\left(×,\mathrm{I}\right)\left({N}\right)\left({N}+1\right)$
9 seqp1 ${⊢}{N}\in {ℤ}_{\ge 1}\to seq1\left(×,\mathrm{I}\right)\left({N}+1\right)=seq1\left(×,\mathrm{I}\right)\left({N}\right)\mathrm{I}\left({N}+1\right)$
10 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
11 9 10 eleq2s ${⊢}{N}\in ℕ\to seq1\left(×,\mathrm{I}\right)\left({N}+1\right)=seq1\left(×,\mathrm{I}\right)\left({N}\right)\mathrm{I}\left({N}+1\right)$
12 facnn ${⊢}{N}\in ℕ\to {N}!=seq1\left(×,\mathrm{I}\right)\left({N}\right)$
13 12 oveq1d ${⊢}{N}\in ℕ\to {N}!\left({N}+1\right)=seq1\left(×,\mathrm{I}\right)\left({N}\right)\left({N}+1\right)$
14 8 11 13 3eqtr4a ${⊢}{N}\in ℕ\to seq1\left(×,\mathrm{I}\right)\left({N}+1\right)={N}!\left({N}+1\right)$
15 4 14 eqtrd ${⊢}{N}\in ℕ\to \left({N}+1\right)!={N}!\left({N}+1\right)$
16 0p1e1 ${⊢}0+1=1$
17 16 fveq2i ${⊢}\left(0+1\right)!=1!$
18 fac1 ${⊢}1!=1$
19 17 18 eqtri ${⊢}\left(0+1\right)!=1$
20 fvoveq1 ${⊢}{N}=0\to \left({N}+1\right)!=\left(0+1\right)!$
21 fveq2 ${⊢}{N}=0\to {N}!=0!$
22 oveq1 ${⊢}{N}=0\to {N}+1=0+1$
23 21 22 oveq12d ${⊢}{N}=0\to {N}!\left({N}+1\right)=0!\left(0+1\right)$
24 fac0 ${⊢}0!=1$
25 24 16 oveq12i ${⊢}0!\left(0+1\right)=1\cdot 1$
26 1t1e1 ${⊢}1\cdot 1=1$
27 25 26 eqtri ${⊢}0!\left(0+1\right)=1$
28 23 27 eqtrdi ${⊢}{N}=0\to {N}!\left({N}+1\right)=1$
29 19 20 28 3eqtr4a ${⊢}{N}=0\to \left({N}+1\right)!={N}!\left({N}+1\right)$
30 15 29 jaoi ${⊢}\left({N}\in ℕ\vee {N}=0\right)\to \left({N}+1\right)!={N}!\left({N}+1\right)$
31 1 30 sylbi ${⊢}{N}\in {ℕ}_{0}\to \left({N}+1\right)!={N}!\left({N}+1\right)$