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 14238

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 11138	. . . 4 ⊢ 0 ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → 0 ∈ V)
3		1ex 11140	. . . 4 ⊢ 1 ∈ V
4	3	a1i 11	. . 3 ⊢ (⊤ → 1 ∈ V)
5		df-fac 14236	. . . 4 ⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I ))
6		nnuz 12827	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
7		dfn2 12450	. . . . . . . 8 ⊢ ℕ = (ℕ₀ ∖ {0})
8	6, 7	eqtr3i 2761	. . . . . . 7 ⊢ (ℤ_≥‘1) = (ℕ₀ ∖ {0})
9	8	reseq2i 5941	. . . . . 6 ⊢ (seq1( · , I ) ↾ (ℤ_≥‘1)) = (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))
10		1z 12557	. . . . . . 7 ⊢ 1 ∈ ℤ
11		seqfn 13975	. . . . . . 7 ⊢ (1 ∈ ℤ → seq1( · , I ) Fn (ℤ_≥‘1))
12		fnresdm 6617	. . . . . . 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 2761	. . . . 5 ⊢ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})) = seq1( · , I )
15	14	uneq2i 4105	. . . 4 ⊢ ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0}))) = ({⟨0, 1⟩} ∪ seq1( · , I ))
16	5, 15	eqtr4i 2762	. . 3 ⊢ ! = ({⟨0, 1⟩} ∪ (seq1( · , I ) ↾ (ℕ₀ ∖ {0})))
17	2, 4, 16	fvsnun1 7137	. 2 ⊢ (⊤ → (!‘0) = 1)
18	17	mptru 1549	1 ⊢ (!‘0) = 1

Colors of variables: wff setvar class

Syntax hints: = wceq 1542 ⊤wtru 1543 ∈ wcel 2114 Vcvv 3429 ∖ cdif 3886 ∪ cun 3887 {csn 4567 ⟨cop 4573 I cid 5525 ↾ cres 5633 Fn wfn 6493 ‘cfv 6498 0cc0 11038 1c1 11039 · cmul 11043 ℕcn 12174 ℕ₀cn0 12437 ℤcz 12524 ℤ_≥cuz 12788 seqcseq 13963 !cfa 14235

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-n0 12438 df-z 12525 df-uz 12789 df-seq 13964 df-fac 14236

This theorem is referenced by: facp1 14240 faccl 14245 facwordi 14251 faclbnd 14252 faclbnd4lem3 14257 facubnd 14262 bcn0 14272 bcval5 14280 hashf1 14419 fprodfac 15938 fallfacfac 16010 ef0lem 16043 ege2le3 16055 eft0val 16079 prmfac1 16690 pcfac 16870 tayl0 26327 logfac 26565 advlogexp 26619 facgam 27029 logexprlim 27188 subfacval2 35369 faclim 35928 bccn0 44770 mccl 46028 dvnxpaek 46370 dvnprodlem3 46376 etransclem14 46676 etransclem24 46686 etransclem25 46687 etransclem35 46697

W3C validator