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 6103 | . . 3 ⊢ (𝑗 = 0 → (!‘𝑗) = (!‘0)) | |
2 | 1 | eleq1d 2672 | . 2 ⊢ (𝑗 = 0 → ((!‘𝑗) ∈ ℕ ↔ (!‘0) ∈ ℕ)) |
3 | fveq2 6103 | . . 3 ⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) | |
4 | 3 | eleq1d 2672 | . 2 ⊢ (𝑗 = 𝑘 → ((!‘𝑗) ∈ ℕ ↔ (!‘𝑘) ∈ ℕ)) |
5 | fveq2 6103 | . . 3 ⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) | |
6 | 5 | eleq1d 2672 | . 2 ⊢ (𝑗 = (𝑘 + 1) → ((!‘𝑗) ∈ ℕ ↔ (!‘(𝑘 + 1)) ∈ ℕ)) |
7 | fveq2 6103 | . . 3 ⊢ (𝑗 = 𝑁 → (!‘𝑗) = (!‘𝑁)) | |
8 | 7 | eleq1d 2672 | . 2 ⊢ (𝑗 = 𝑁 → ((!‘𝑗) ∈ ℕ ↔ (!‘𝑁) ∈ ℕ)) |
9 | fac0 12925 | . . 3 ⊢ (!‘0) = 1 | |
10 | 1nn 10908 | . . 3 ⊢ 1 ∈ ℕ | |
11 | 9, 10 | eqeltri 2684 | . 2 ⊢ (!‘0) ∈ ℕ |
12 | facp1 12927 | . . . . 5 ⊢ (𝑘 ∈ ℕ0 → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) | |
13 | 12 | adantl 481 | . . . 4 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
14 | nn0p1nn 11209 | . . . . 5 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ) | |
15 | nnmulcl 10920 | . . . . 5 ⊢ (((!‘𝑘) ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ) → ((!‘𝑘) · (𝑘 + 1)) ∈ ℕ) | |
16 | 14, 15 | sylan2 490 | . . . 4 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → ((!‘𝑘) · (𝑘 + 1)) ∈ ℕ) |
17 | 13, 16 | eqeltrd 2688 | . . 3 ⊢ (((!‘𝑘) ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (!‘(𝑘 + 1)) ∈ ℕ) |
18 | 17 | expcom 450 | . 2 ⊢ (𝑘 ∈ ℕ0 → ((!‘𝑘) ∈ ℕ → (!‘(𝑘 + 1)) ∈ ℕ)) |
19 | 2, 4, 6, 8, 11, 18 | nn0ind 11348 | 1 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ‘cfv 5804 (class class class)co 6549 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 ℕcn 10897 ℕ0cn0 11169 !cfa 12922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-seq 12664 df-fac 12923 |
This theorem is referenced by: faccld 12933 facmapnn 12934 facne0 12935 facdiv 12936 facndiv 12937 facwordi 12938 faclbnd 12939 faclbnd2 12940 faclbnd3 12941 faclbnd4lem1 12942 faclbnd5 12947 faclbnd6 12948 facubnd 12949 facavg 12950 bcrpcl 12957 bccmpl 12958 bcn0 12959 bcn1 12962 bcm1k 12964 bcp1n 12965 bcval5 12967 permnn 12975 4bc2eq6 12978 hashf1 13098 hashfac 13099 bcfallfac 14614 fallfacfac 14615 eftcl 14643 reeftcl 14644 eftabs 14645 efcllem 14647 ef0lem 14648 ege2le3 14659 efcj 14661 efaddlem 14662 eftlub 14678 effsumlt 14680 eflegeo 14690 ef01bndlem 14753 eirrlem 14771 dvdsfac 14886 lcmflefac 15199 prmfac1 15269 pcfac 15441 pcbc 15442 infpnlem1 15452 infpnlem2 15453 prmunb 15456 prmgaplem1 15591 prmgaplem2 15592 gexcl3 17825 aaliou3lem1 23901 aaliou3lem2 23902 aaliou3lem3 23903 aaliou3lem8 23904 aaliou3lem5 23906 aaliou3lem6 23907 aaliou3lem7 23908 aaliou3lem9 23909 taylfvallem1 23915 taylply2 23926 taylply 23927 dvtaylp 23928 taylthlem2 23932 advlogexp 24201 birthdaylem2 24479 wilthlem3 24596 wilth 24597 chtublem 24736 logfacubnd 24746 logfaclbnd 24747 logfacbnd3 24748 logfacrlim 24749 logexprlim 24750 bcmono 24802 bposlem3 24811 vmadivsum 24971 subfacval2 30423 subfaclim 30424 subfacval3 30425 bcprod 30877 faclim2 30887 bcccl 37560 bcc0 37561 bccp1k 37562 binomcxplemwb 37569 dvnxpaek 38832 wallispi2lem2 38965 stirlinglem2 38968 stirlinglem3 38969 stirlinglem4 38970 stirlinglem13 38979 stirlinglem14 38980 stirlinglem15 38981 stirlingr 38983 pgrple2abl 41940 |
Copyright terms: Public domain | W3C validator |