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