Metamath Proof Explorer

Theorem facp2

Description: The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024)

Ref Expression
Assertion facp2 ⊢N∈ℕ0→N+2!=N!⁢N+1⁢N+2

Proof

Step Hyp Ref Expression
1 nn0cn ⊢N∈ℕ0→N∈ℂ
2 ax-1cn ⊢1∈ℂ
3 addass ⊢N∈ℂ∧1∈ℂ∧1∈ℂ→N+1+1=N+1+1
4 2 2 3 mp3an23 ⊢N∈ℂ→N+1+1=N+1+1
5 1 4 syl ⊢N∈ℕ0→N+1+1=N+1+1
6 df-2 ⊢2=1+1
7 6 oveq2i ⊢N+2=N+1+1
8 7 eqcomi ⊢N+1+1=N+2
9 8 a1i ⊢N∈ℕ0→N+1+1=N+2
10 5 9 eqtrd ⊢N∈ℕ0→N+1+1=N+2
11 10 fveq2d ⊢N∈ℕ0→N+1+1!=N+2!
12 peano2nn0 ⊢N∈ℕ0→N+1∈ℕ0
13 facp1 ⊢N+1∈ℕ0→N+1+1!=N+1!⁢N+1+1
14 12 13 syl ⊢N∈ℕ0→N+1+1!=N+1!⁢N+1+1
15 11 14 eqtr3d ⊢N∈ℕ0→N+2!=N+1!⁢N+1+1
16 10 oveq2d ⊢N∈ℕ0→N+1!⁢N+1+1=N+1!⁢N+2
17 15 16 eqtrd ⊢N∈ℕ0→N+2!=N+1!⁢N+2
18 facp1 ⊢N∈ℕ0→N+1!=N!⁢N+1
19 18 oveq1d ⊢N∈ℕ0→N+1!⁢N+2=N!⁢N+1⁢N+2
20 17 19 eqtrd ⊢N∈ℕ0→N+2!=N!⁢N+1⁢N+2
21 faccl ⊢N∈ℕ0→N!∈ℕ
22 nncn ⊢N!∈ℕ→N!∈ℂ
23 21 22 syl ⊢N∈ℕ0→N!∈ℂ
24 nn0cn ⊢N+1∈ℕ0→N+1∈ℂ
25 12 24 syl ⊢N∈ℕ0→N+1∈ℂ
26 2cn ⊢2∈ℂ
27 addcl ⊢N∈ℂ∧2∈ℂ→N+2∈ℂ
28 26 27 mpan2 ⊢N∈ℂ→N+2∈ℂ
29 1 28 syl ⊢N∈ℕ0→N+2∈ℂ
30 mulass ⊢N!∈ℂ∧N+1∈ℂ∧N+2∈ℂ→N!⁢N+1⁢N+2=N!⁢N+1⁢N+2
31 23 25 29 30 syl3anc ⊢N∈ℕ0→N!⁢N+1⁢N+2=N!⁢N+1⁢N+2
32 20 31 eqtrd ⊢N∈ℕ0→N+2!=N!⁢N+1⁢N+2