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 0 N + 1 ! = N ! N + 1

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 peano2nn N N + 1
3 facnn N + 1 N + 1 ! = seq 1 × I N + 1
4 2 3 syl N N + 1 ! = seq 1 × I N + 1
5 ovex N + 1 V
6 fvi N + 1 V I N + 1 = N + 1
7 5 6 ax-mp I N + 1 = N + 1
8 7 oveq2i seq 1 × I N I N + 1 = seq 1 × I N N + 1
9 seqp1 N 1 seq 1 × I N + 1 = seq 1 × I N I N + 1
10 nnuz = 1
11 9 10 eleq2s N seq 1 × I N + 1 = seq 1 × I N I N + 1
12 facnn N N ! = seq 1 × I N
13 12 oveq1d N N ! N + 1 = seq 1 × I N N + 1
14 8 11 13 3eqtr4a N seq 1 × I N + 1 = N ! N + 1
15 4 14 eqtrd N N + 1 ! = N ! N + 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 N = 0 N + 1 ! = 0 + 1 !
21 fveq2 N = 0 N ! = 0 !
22 oveq1 N = 0 N + 1 = 0 + 1
23 21 22 oveq12d N = 0 N ! N + 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 N = 0 N ! N + 1 = 1
29 19 20 28 3eqtr4a N = 0 N + 1 ! = N ! N + 1
30 15 29 jaoi N N = 0 N + 1 ! = N ! N + 1
31 1 30 sylbi N 0 N + 1 ! = N ! N + 1