This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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