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 ( 𝑁 ∈ ℕ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 ) ) )