Theorem facnn

Description: Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	facnn	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		c0ex	⊢ 0 ∈ V
2	1	a1i	⊢ ( 𝑁 ∈ ( ℕ0 ∖ { 0 } ) → 0 ∈ V )
3		1ex	⊢ 1 ∈ V
4	3	a1i	⊢ ( 𝑁 ∈ ( ℕ0 ∖ { 0 } ) → 1 ∈ V )
5		df-fac	⊢ ! = ( { ⟨ 0 , 1 ⟩ } ∪ seq 1 ( · , I ) )
6		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
7		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
8	6 7	eqtr3i	⊢ ( ℤ≥ ‘ 1 ) = ( ℕ0 ∖ { 0 } )
9	8	reseq2i	⊢ ( seq 1 ( · , I ) ↾ ( ℤ≥ ‘ 1 ) ) = ( seq 1 ( · , I ) ↾ ( ℕ0 ∖ { 0 } ) )
10		1z	⊢ 1 ∈ ℤ
11		seqfn	⊢ ( 1 ∈ ℤ → seq 1 ( · , I ) Fn ( ℤ≥ ‘ 1 ) )
12		fnresdm	⊢ ( seq 1 ( · , I ) Fn ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , I ) ↾ ( ℤ≥ ‘ 1 ) ) = seq 1 ( · , I ) )
13	10 11 12	mp2b	⊢ ( seq 1 ( · , I ) ↾ ( ℤ≥ ‘ 1 ) ) = seq 1 ( · , I )
14	9 13	eqtr3i	⊢ ( seq 1 ( · , I ) ↾ ( ℕ0 ∖ { 0 } ) ) = seq 1 ( · , I )
15	14	uneq2i	⊢ ( { ⟨ 0 , 1 ⟩ } ∪ ( seq 1 ( · , I ) ↾ ( ℕ0 ∖ { 0 } ) ) ) = ( { ⟨ 0 , 1 ⟩ } ∪ seq 1 ( · , I ) )
16	5 15	eqtr4i	⊢ ! = ( { ⟨ 0 , 1 ⟩ } ∪ ( seq 1 ( · , I ) ↾ ( ℕ0 ∖ { 0 } ) ) )
17		id	⊢ ( 𝑁 ∈ ( ℕ0 ∖ { 0 } ) → 𝑁 ∈ ( ℕ0 ∖ { 0 } ) )
18	2 4 16 17	fvsnun2	⊢ ( 𝑁 ∈ ( ℕ0 ∖ { 0 } ) → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
19	18 7	eleq2s	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )