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 14292

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 11227	. . . 4 ⊢ 0 ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → 0 ∈ V)
3		1ex 11229	. . . 4 ⊢ 1 ∈ V
4	3	a1i 11	. . 3 ⊢ (⊤ → 1 ∈ V)
5		df-fac 14290	. . . 4 ⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I ))
6		nnuz 12893	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
7		dfn2 12512	. . . . . . . 8 ⊢ ℕ = (ℕ₀ ∖ {0})
8	6, 7	eqtr3i 2760	. . . . . . 7 ⊢ (ℤ_≥‘1) = (ℕ₀ ∖ {0})
9	8	reseq2i 5963	. . . . . 6 ⊢ (seq1( · , I ) ↾ (ℤ_≥‘1)) = (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))
10		1z 12620	. . . . . . 7 ⊢ 1 ∈ ℤ
11		seqfn 14029	. . . . . . 7 ⊢ (1 ∈ ℤ → seq1( · , I ) Fn (ℤ_≥‘1))
12		fnresdm 6656	. . . . . . 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 2760	. . . . 5 ⊢ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})) = seq1( · , I )
15	14	uneq2i 4140	. . . 4 ⊢ ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))) = ({⟨0, 1⟩} ∪ seq1( · , I ))
16	5, 15	eqtr4i 2761	. . 3 ⊢ ! = ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})))
17	2, 4, 16	fvsnun1 7173	. 2 ⊢ (⊤ → (!‘0) = 1)
18	17	mptru 1547	1 ⊢ (!‘0) = 1

Colors of variables: wff setvar class

Syntax hints: = wceq 1540 ⊤wtru 1541 ∈ wcel 2108 Vcvv 3459 ∖ cdif 3923 ∪ cun 3924 {csn 4601 ⟨cop 4607 I cid 5547 ↾ cres 5656 Fn wfn 6525 ‘cfv 6530 0cc0 11127 1c1 11128 · cmul 11132 ℕcn 12238 ℕ₀cn0 12499 ℤcz 12586 ℤ_≥cuz 12850 seqcseq 14017 !cfa 14289

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-riota 7360 df-ov 7406 df-oprab 7407 df-mpo 7408 df-om 7860 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-er 8717 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11466 df-neg 11467 df-nn 12239 df-n0 12500 df-z 12587 df-uz 12851 df-seq 14018 df-fac 14290

This theorem is referenced by: facp1 14294 faccl 14299 facwordi 14305 faclbnd 14306 faclbnd4lem3 14311 facubnd 14316 bcn0 14326 bcval5 14334 hashf1 14473 fprodfac 15987 fallfacfac 16059 ef0lem 16092 ege2le3 16104 eft0val 16128 prmfac1 16737 pcfac 16917 tayl0 26319 logfac 26560 advlogexp 26614 facgam 27026 logexprlim 27186 subfacval2 35155 faclim 35709 bccn0 44315 mccl 45575 dvnxpaek 45919 dvnprodlem3 45925 etransclem14 46225 etransclem24 46235 etransclem25 46236 etransclem35 46246

W3C validator