![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > faccl | Structured version Visualization version GIF version |
Description: Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
Ref | Expression |
---|---|
faccl | ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6496 | . . 3 ⊢ (𝑗 = 0 → (!‘𝑗) = (!‘0)) | |
2 | 1 | eleq1d 2843 | . 2 ⊢ (𝑗 = 0 → ((!‘𝑗) ∈ ℕ ↔ (!‘0) ∈ ℕ)) |
3 | fveq2 6496 | . . 3 ⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) | |
4 | 3 | eleq1d 2843 | . 2 ⊢ (𝑗 = 𝑘 → ((!‘𝑗) ∈ ℕ ↔ (!‘𝑘) ∈ ℕ)) |
5 | fveq2 6496 | . . 3 ⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) | |
6 | 5 | eleq1d 2843 | . 2 ⊢ (𝑗 = (𝑘 + 1) → ((!‘𝑗) ∈ ℕ ↔ (!‘(𝑘 + 1)) ∈ ℕ)) |
7 | fveq2 6496 | . . 3 ⊢ (𝑗 = 𝑁 → (!‘𝑗) = (!‘𝑁)) | |
8 | 7 | eleq1d 2843 | . 2 ⊢ (𝑗 = 𝑁 → ((!‘𝑗) ∈ ℕ ↔ (!‘𝑁) ∈ ℕ)) |
9 | fac0 13449 | . . 3 ⊢ (!‘0) = 1 | |
10 | 1nn 11450 | . . 3 ⊢ 1 ∈ ℕ | |
11 | 9, 10 | eqeltri 2855 | . 2 ⊢ (!‘0) ∈ ℕ |
12 | facp1 13451 | . . . . 5 ⊢ (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) | |
13 | 12 | adantl 474 | . . . 4 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
14 | nn0p1nn 11746 | . . . . 5 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ) | |
15 | nnmulcl 11462 | . . . . 5 ⊢ (((!‘𝑘) ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ) → ((!‘𝑘) · (𝑘 + 1)) ∈ ℕ) | |
16 | 14, 15 | sylan2 584 | . . . 4 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → ((!‘𝑘) · (𝑘 + 1)) ∈ ℕ) |
17 | 13, 16 | eqeltrd 2859 | . . 3 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (!‘(𝑘 + 1)) ∈ ℕ) |
18 | 17 | expcom 406 | . 2 ⊢ (𝑘 ∈ ℕ0 → ((!‘𝑘) ∈ ℕ → (!‘(𝑘 + 1)) ∈ ℕ)) |
19 | 2, 4, 6, 8, 11, 18 | nn0ind 11888 | 1 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1508 ∈ wcel 2051 ‘cfv 6185 (class class class)co 6974 0cc0 10333 1c1 10334 + caddc 10336 · cmul 10338 ℕcn 11437 ℕ0cn0 11705 !cfa 13446 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-cnex 10389 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 ax-pre-mulgt0 10410 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-nel 3067 df-ral 3086 df-rex 3087 df-reu 3088 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-2nd 7500 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-pnf 10474 df-mnf 10475 df-xr 10476 df-ltxr 10477 df-le 10478 df-sub 10670 df-neg 10671 df-nn 11438 df-n0 11706 df-z 11792 df-uz 12057 df-seq 13183 df-fac 13447 |
This theorem is referenced by: faccld 13457 facne0 13459 facdiv 13460 facndiv 13461 facwordi 13462 faclbnd 13463 faclbnd2 13464 faclbnd3 13465 faclbnd4lem1 13466 faclbnd5 13471 faclbnd6 13472 facubnd 13473 facavg 13474 bcrpcl 13481 bcn0 13483 bcm1k 13488 bcval5 13491 permnn 13499 4bc2eq6 13502 fallfacfac 15257 eftcl 15285 reeftcl 15286 eftabs 15287 ef0lem 15290 ege2le3 15301 efcj 15303 efaddlem 15304 effsumlt 15322 eflegeo 15332 ef01bndlem 15395 eirrlem 15415 prmfac1 15917 pcfac 16089 prmunb 16104 aaliou3lem7 24656 aaliou3lem9 24657 advlogexp 24954 wilth 25365 logfacrlim 25517 logexprlim 25518 bcmono 25570 vmadivsum 25775 subfacval2 32056 subfaclim 32057 subfacval3 32058 bcprod 32527 faclim2 32537 bcccl 40125 bcc0 40126 bccp1k 40127 binomcxplemwb 40134 dvnxpaek 41691 wallispi2lem2 41822 stirlinglem2 41825 stirlinglem3 41826 stirlinglem4 41827 stirlinglem13 41836 stirlinglem14 41837 stirlinglem15 41838 stirlingr 41840 pgrple2abl 43813 |
Copyright terms: Public domain | W3C validator |