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