fac0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fac0		Structured version Visualization version GIF version

Theorem fac0 14183

Description: The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)

**Assertion**
Ref	Expression
fac0	⊢ (!‘0) = 1

**Proof of Theorem fac0**
Step	Hyp	Ref	Expression
1		c0ex 11106	. . . 4 ⊢ 0 ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → 0 ∈ V)
3		1ex 11108	. . . 4 ⊢ 1 ∈ V
4	3	a1i 11	. . 3 ⊢ (⊤ → 1 ∈ V)
5		df-fac 14181	. . . 4 ⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I ))
6		nnuz 12775	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
7		dfn2 12394	. . . . . . . 8 ⊢ ℕ = (ℕ₀ ∖ {0})
8	6, 7	eqtr3i 2756	. . . . . . 7 ⊢ (ℤ_≥‘1) = (ℕ₀ ∖ {0})
9	8	reseq2i 5925	. . . . . 6 ⊢ (seq1( · , I ) ↾ (ℤ_≥‘1)) = (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))
10		1z 12502	. . . . . . 7 ⊢ 1 ∈ ℤ
11		seqfn 13920	. . . . . . 7 ⊢ (1 ∈ ℤ → seq1( · , I ) Fn (ℤ_≥‘1))
12		fnresdm 6600	. . . . . . 7 ⊢ (seq1( · , I ) Fn (ℤ_≥‘1) → (seq1( · , I ) ↾ (ℤ_≥‘1)) = seq1( · , I ))
13	10, 11, 12	mp2b 10	. . . . . 6 ⊢ (seq1( · , I ) ↾ (ℤ_≥‘1)) = seq1( · , I )
14	9, 13	eqtr3i 2756	. . . . 5 ⊢ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})) = seq1( · , I )
15	14	uneq2i 4115	. . . 4 ⊢ ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))) = ({⟨0, 1⟩} ∪ seq1( · , I ))
16	5, 15	eqtr4i 2757	. . 3 ⊢ ! = ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})))
17	2, 4, 16	fvsnun1 7116	. 2 ⊢ (⊤ → (!‘0) = 1)
18	17	mptru 1548	1 ⊢ (!‘0) = 1

Colors of variables: wff setvar class

Syntax hints: = wceq 1541 ⊤wtru 1542 ∈ wcel 2111 Vcvv 3436 ∖ cdif 3899 ∪ cun 3900 {csn 4576 ⟨cop 4582 I cid 5510 ↾ cres 5618 Fn wfn 6476 ‘cfv 6481 0cc0 11006 1c1 11007 · cmul 11011 ℕcn 12125 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 seqcseq 13908 !cfa 14180

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-n0 12382 df-z 12469 df-uz 12733 df-seq 13909 df-fac 14181

This theorem is referenced by: facp1 14185 faccl 14190 facwordi 14196 faclbnd 14197 faclbnd4lem3 14202 facubnd 14207 bcn0 14217 bcval5 14225 hashf1 14364 fprodfac 15880 fallfacfac 15952 ef0lem 15985 ege2le3 15997 eft0val 16021 prmfac1 16631 pcfac 16811 tayl0 26297 logfac 26538 advlogexp 26592 facgam 27004 logexprlim 27164 subfacval2 35229 faclim 35788 bccn0 44382 mccl 45644 dvnxpaek 45986 dvnprodlem3 45992 etransclem14 46292 etransclem24 46302 etransclem25 46303 etransclem35 46313

W3C validator