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 ) โ€˜ ๐‘ ) )