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 14018

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 10997	. . . 4 ⊢ 0 ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → 0 ∈ V)
3		1ex 10999	. . . 4 ⊢ 1 ∈ V
4	3	a1i 11	. . 3 ⊢ (⊤ → 1 ∈ V)
5		df-fac 14016	. . . 4 ⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I ))
6		nnuz 12649	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
7		dfn2 12274	. . . . . . . 8 ⊢ ℕ = (ℕ₀ ∖ {0})
8	6, 7	eqtr3i 2763	. . . . . . 7 ⊢ (ℤ_≥‘1) = (ℕ₀ ∖ {0})
9	8	reseq2i 5891	. . . . . 6 ⊢ (seq1( · , I ) ↾ (ℤ_≥‘1)) = (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))
10		1z 12378	. . . . . . 7 ⊢ 1 ∈ ℤ
11		seqfn 13761	. . . . . . 7 ⊢ (1 ∈ ℤ → seq1( · , I ) Fn (ℤ_≥‘1))
12		fnresdm 6570	. . . . . . 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 2763	. . . . 5 ⊢ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})) = seq1( · , I )
15	14	uneq2i 4097	. . . 4 ⊢ ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))) = ({⟨0, 1⟩} ∪ seq1( · , I ))
16	5, 15	eqtr4i 2764	. . 3 ⊢ ! = ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})))
17	2, 4, 16	fvsnun1 7074	. 2 ⊢ (⊤ → (!‘0) = 1)
18	17	mptru 1544	1 ⊢ (!‘0) = 1

Colors of variables: wff setvar class

Syntax hints: = wceq 1537 ⊤wtru 1538 ∈ wcel 2101 Vcvv 3434 ∖ cdif 3886 ∪ cun 3887 {csn 4564 ⟨cop 4570 I cid 5490 ↾ cres 5593 Fn wfn 6442 ‘cfv 6447 0cc0 10899 1c1 10900 · cmul 10904 ℕcn 12001 ℕ₀cn0 12261 ℤcz 12347 ℤ_≥cuz 12610 seqcseq 13749 !cfa 14015

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7608 ax-cnex 10955 ax-resscn 10956 ax-1cn 10957 ax-icn 10958 ax-addcl 10959 ax-addrcl 10960 ax-mulcl 10961 ax-mulrcl 10962 ax-mulcom 10963 ax-addass 10964 ax-mulass 10965 ax-distr 10966 ax-i2m1 10967 ax-1ne0 10968 ax-1rid 10969 ax-rnegex 10970 ax-rrecex 10971 ax-cnre 10972 ax-pre-lttri 10973 ax-pre-lttrn 10974 ax-pre-ltadd 10975 ax-pre-mulgt0 10976

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3908 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-iun 4929 df-br 5078 df-opab 5140 df-mpt 5161 df-tr 5195 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-riota 7252 df-ov 7298 df-oprab 7299 df-mpo 7300 df-om 7733 df-2nd 7852 df-frecs 8117 df-wrecs 8148 df-recs 8222 df-rdg 8261 df-er 8518 df-en 8754 df-dom 8755 df-sdom 8756 df-pnf 11039 df-mnf 11040 df-xr 11041 df-ltxr 11042 df-le 11043 df-sub 11235 df-neg 11236 df-nn 12002 df-n0 12262 df-z 12348 df-uz 12611 df-seq 13750 df-fac 14016

This theorem is referenced by: facp1 14020 faccl 14025 facwordi 14031 faclbnd 14032 faclbnd4lem3 14037 facubnd 14042 bcn0 14052 bcval5 14060 hashf1 14199 fprodfac 15711 fallfacfac 15783 ef0lem 15816 ege2le3 15827 eft0val 15849 prmfac1 16454 pcfac 16628 tayl0 25549 logfac 25784 advlogexp 25838 facgam 26243 logexprlim 26401 subfacval2 33177 faclim 33740 bccn0 41985 mccl 43174 dvnxpaek 43518 dvnprodlem3 43524 etransclem14 43824 etransclem24 43834 etransclem25 43835 etransclem35 43845

W3C validator