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 \in ℕ_{0} \to (N + 1)! = N! (N + 1)$

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
3		facnn	$⊢ N + 1 \in ℕ \to (N + 1)! = seq 1 (\times I) (N + 1)$
4	2 3	syl	$⊢ N \in ℕ \to (N + 1)! = seq 1 (\times I) (N + 1)$
5		ovex	$⊢ N + 1 \in V$
6		fvi	$⊢ N + 1 \in V \to I (N + 1) = N + 1$
7	5 6	ax-mp	$⊢ I (N + 1) = N + 1$
8	7	oveq2i	$⊢ seq 1 (\times I) (N) I (N + 1) = seq 1 (\times I) (N) (N + 1)$
9		seqp1	$⊢ N \in ℤ_{\geq 1} \to seq 1 (\times I) (N + 1) = seq 1 (\times I) (N) I (N + 1)$
10		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
11	9 10	eleq2s	$⊢ N \in ℕ \to seq 1 (\times I) (N + 1) = seq 1 (\times I) (N) I (N + 1)$
12		facnn	$⊢ N \in ℕ \to N! = seq 1 (\times I) (N)$
13	12	oveq1d	$⊢ N \in ℕ \to N! (N + 1) = seq 1 (\times I) (N) (N + 1)$
14	8 11 13	3eqtr4a	$⊢ N \in ℕ \to seq 1 (\times I) (N + 1) = N! (N + 1)$
15	4 14	eqtrd	$⊢ N \in ℕ \to (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 \to (N + 1)! = (0 + 1)!$
21		fveq2	$⊢ N = 0 \to N! = 0!$
22		oveq1	$⊢ N = 0 \to N + 1 = 0 + 1$
23	21 22	oveq12d	$⊢ N = 0 \to N! (N + 1) = 0! (0 + 1)$
24		fac0	$⊢ 0! = 1$
25	24 16	oveq12i	$⊢ 0! (0 + 1) = 1 \cdot 1$
26		1t1e1	$⊢ 1 \cdot 1 = 1$
27	25 26	eqtri	$⊢ 0! (0 + 1) = 1$
28	23 27	eqtrdi	$⊢ N = 0 \to N! (N + 1) = 1$
29	19 20 28	3eqtr4a	$⊢ N = 0 \to (N + 1)! = N! (N + 1)$
30	15 29	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (N + 1)! = N! (N + 1)$
31	1 30	sylbi	$⊢ N \in ℕ_{0} \to (N + 1)! = N! (N + 1)$

Metamath Proof Explorer