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 6656 | . . 3 ⊢ (𝑗 = 0 → (!‘𝑗) = (!‘0)) | |
2 | 1 | eleq1d 2897 | . 2 ⊢ (𝑗 = 0 → ((!‘𝑗) ∈ ℕ ↔ (!‘0) ∈ ℕ)) |
3 | fveq2 6656 | . . 3 ⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) | |
4 | 3 | eleq1d 2897 | . 2 ⊢ (𝑗 = 𝑘 → ((!‘𝑗) ∈ ℕ ↔ (!‘𝑘) ∈ ℕ)) |
5 | fveq2 6656 | . . 3 ⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) | |
6 | 5 | eleq1d 2897 | . 2 ⊢ (𝑗 = (𝑘 + 1) → ((!‘𝑗) ∈ ℕ ↔ (!‘(𝑘 + 1)) ∈ ℕ)) |
7 | fveq2 6656 | . . 3 ⊢ (𝑗 = 𝑁 → (!‘𝑗) = (!‘𝑁)) | |
8 | 7 | eleq1d 2897 | . 2 ⊢ (𝑗 = 𝑁 → ((!‘𝑗) ∈ ℕ ↔ (!‘𝑁) ∈ ℕ)) |
9 | fac0 13626 | . . 3 ⊢ (!‘0) = 1 | |
10 | 1nn 11635 | . . 3 ⊢ 1 ∈ ℕ | |
11 | 9, 10 | eqeltri 2909 | . 2 ⊢ (!‘0) ∈ ℕ |
12 | facp1 13628 | . . . . 5 ⊢ (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) | |
13 | 12 | adantl 484 | . . . 4 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
14 | nn0p1nn 11923 | . . . . 5 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ) | |
15 | nnmulcl 11648 | . . . . 5 ⊢ (((!‘𝑘) ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ) → ((!‘𝑘) · (𝑘 + 1)) ∈ ℕ) | |
16 | 14, 15 | sylan2 594 | . . . 4 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → ((!‘𝑘) · (𝑘 + 1)) ∈ ℕ) |
17 | 13, 16 | eqeltrd 2913 | . . 3 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (!‘(𝑘 + 1)) ∈ ℕ) |
18 | 17 | expcom 416 | . 2 ⊢ (𝑘 ∈ ℕ0 → ((!‘𝑘) ∈ ℕ → (!‘(𝑘 + 1)) ∈ ℕ)) |
19 | 2, 4, 6, 8, 11, 18 | nn0ind 12064 | 1 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ‘cfv 6341 (class class class)co 7142 0cc0 10523 1c1 10524 + caddc 10526 · cmul 10528 ℕcn 11624 ℕ0cn0 11884 !cfa 13623 |
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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-cnex 10579 ax-resscn 10580 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-mulcom 10587 ax-addass 10588 ax-mulass 10589 ax-distr 10590 ax-i2m1 10591 ax-1ne0 10592 ax-1rid 10593 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 ax-pre-lttri 10597 ax-pre-lttrn 10598 ax-pre-ltadd 10599 ax-pre-mulgt0 10600 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-pss 3942 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-tp 4558 df-op 4560 df-uni 4825 df-iun 4907 df-br 5053 df-opab 5115 df-mpt 5133 df-tr 5159 df-id 5446 df-eprel 5451 df-po 5460 df-so 5461 df-fr 5500 df-we 5502 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-pred 6134 df-ord 6180 df-on 6181 df-lim 6182 df-suc 6183 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7100 df-ov 7145 df-oprab 7146 df-mpo 7147 df-om 7567 df-2nd 7676 df-wrecs 7933 df-recs 7994 df-rdg 8032 df-er 8275 df-en 8496 df-dom 8497 df-sdom 8498 df-pnf 10663 df-mnf 10664 df-xr 10665 df-ltxr 10666 df-le 10667 df-sub 10858 df-neg 10859 df-nn 11625 df-n0 11885 df-z 11969 df-uz 12231 df-seq 13360 df-fac 13624 |
This theorem is referenced by: faccld 13634 facne0 13636 facdiv 13637 facndiv 13638 facwordi 13639 faclbnd 13640 faclbnd2 13641 faclbnd3 13642 faclbnd4lem1 13643 faclbnd5 13648 faclbnd6 13649 facubnd 13650 facavg 13651 bcrpcl 13658 bcn0 13660 bcm1k 13665 bcval5 13668 permnn 13676 4bc2eq6 13679 fallfacfac 15384 eftcl 15412 reeftcl 15413 eftabs 15414 ef0lem 15417 ege2le3 15428 efcj 15430 efaddlem 15431 effsumlt 15449 eflegeo 15459 ef01bndlem 15522 eirrlem 15542 prmfac1 16046 pcfac 16218 prmunb 16233 aaliou3lem7 24924 aaliou3lem9 24925 advlogexp 25224 wilth 25634 logfacrlim 25786 logexprlim 25787 bcmono 25839 vmadivsum 26044 subfacval2 32441 subfaclim 32442 subfacval3 32443 bcprod 32977 faclim2 32987 fac2xp3 39169 facp2 39170 factwoffsmonot 39173 bcccl 40761 bcc0 40762 bccp1k 40763 binomcxplemwb 40770 dvnxpaek 42317 wallispi2lem2 42447 stirlinglem2 42450 stirlinglem3 42451 stirlinglem4 42452 stirlinglem13 42461 stirlinglem14 42462 stirlinglem15 42463 stirlingr 42465 pgrple2abl 44498 |
Copyright terms: Public domain | W3C validator |