MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fzfi Structured version   Visualization version   GIF version

Theorem fzfi 12811
Description: A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
Assertion
Ref Expression
fzfi (𝑀...𝑁) ∈ Fin

Proof of Theorem fzfi
StepHypRef Expression
1 0fin 8229 . . 3 ∅ ∈ Fin
2 eleq1 2718 . . 3 ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
31, 2mpbiri 248 . 2 ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4 fzn0 12393 . . 3 ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ𝑀))
5 onfin2 8193 . . . . . 6 ω = (On ∩ Fin)
6 inss2 3867 . . . . . 6 (On ∩ Fin) ⊆ Fin
75, 6eqsstri 3668 . . . . 5 ω ⊆ Fin
8 eqid 2651 . . . . . . 7 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
98hashgf1o 12810 . . . . . 6 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10 peano2uz 11779 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
11 uznn0sub 11757 . . . . . . 7 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
1210, 11syl 17 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13 f1ocnvdm 6580 . . . . . 6 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
149, 12, 13sylancr 696 . . . . 5 (𝑁 ∈ (ℤ𝑀) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
157, 14sseldi 3634 . . . 4 (𝑁 ∈ (ℤ𝑀) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
168fzen2 12808 . . . 4 (𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) ≈ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17 enfii 8218 . . . 4 ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
1815, 16, 17syl2anc 694 . . 3 (𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) ∈ Fin)
194, 18sylbi 207 . 2 ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
203, 19pm2.61ine 2906 1 (𝑀...𝑁) ∈ Fin
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  wne 2823  Vcvv 3231  cin 3606  c0 3948   class class class wbr 4685  cmpt 4762  ccnv 5142  cres 5145  Oncon0 5761  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  ωcom 7107  reccrdg 7550  cen 7994  Fincfn 7997  0cc0 9974  1c1 9975   + caddc 9977  cmin 10304  0cn0 11330  cuz 11725  ...cfz 12364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365
This theorem is referenced by:  fzfid  12812  fzofi  12813  fsequb  12814  fsequb2  12815  fseqsupcl  12816  ssnn0fi  12824  seqf1o  12882  isfinite4  13191  hashdom  13206  fzsdom2  13253  fnfz0hashnn0  13270  seqcoll2  13287  caubnd  14142  limsupgre  14256  summolem3  14489  summolem2  14491  zsum  14493  prodmolem3  14707  prodmolem2  14709  zprod  14711  risefallfac  14799  bpolylem  14823  phicl2  15520  phibnd  15523  hashdvds  15527  phiprmpw  15528  eulerth  15535  phisum  15542  pcfac  15650  prmreclem2  15668  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  prmrec  15673  1arith  15678  vdwlem6  15737  vdwlem10  15741  vdwlem12  15743  prmdvdsprmo  15793  prmgaplcmlem1  15802  prmgaplcm  15811  isstruct2  15914  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  coe1mul2  19687  ovoliunlem2  23317  uniioombllem6  23402  itg0  23591  itgz  23592  coemullem  24051  aannenlem1  24128  aannenlem2  24129  birthdaylem1  24723  birthdaylem2  24724  wilthlem2  24840  wilthlem3  24841  ftalem5  24848  ppifi  24877  prmdvdsfi  24878  chtdif  24929  ppidif  24934  chp1  24938  ppiltx  24948  prmorcht  24949  mumul  24952  sqff1o  24953  ppiub  24974  pclogsum  24985  logexprlim  24995  gausslemma2dlem1  25136  gausslemma2dlem5  25141  gausslemma2dlem6  25142  lgseisenlem2  25146  axlowdimlem16  25882  konigsberglem5  27234  pmtrto1cl  29977  psgnfzto1stlem  29978  fzto1st  29981  psgnfzto1st  29983  smatcl  29996  1smat1  29998  esumpcvgval  30268  esumcvg  30276  carsggect  30508  carsgclctunlem2  30509  oddpwdc  30544  eulerpartlemb  30558  ballotlem1  30676  ballotlem2  30678  ballotlemfelz  30680  ballotlemfp1  30681  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemfmpn  30684  ballotlemiex  30691  ballotlemsup  30694  ballotlemfg  30715  ballotlemfrc  30716  ballotlemfrceq  30718  ballotth  30727  plymulx0  30752  fsum2dsub  30813  reprfi2  30829  breprexpnat  30840  hgt750lemb  30862  hgt750leme  30864  subfacf  31283  subfacp1lem1  31287  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  erdszelem2  31300  erdszelem10  31308  cvmliftlem15  31406  bcprod  31750  ptrecube  33539  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  mblfinlem2  33577  volsupnfl  33584  itg2addnclem2  33592  nnubfi  33676  nninfnub  33677  cntotbnd  33725  eldioph2lem1  37640  eldioph2lem2  37641  eldioph2  37642  pellexlem5  37714  pellex  37716  jm2.22  37879  jm2.23  37880  hbt  38017  rp-isfinite6  38181  fzisoeu  39828  sumnnodd  40180  stoweidlem37  40572  stoweidlem44  40579  stoweidlem59  40594  fourierdlem37  40679  fourierdlem103  40744  fourierdlem104  40745  etransclem16  40785  etransclem24  40793  etransclem25  40794  etransclem33  40802  etransclem35  40804  etransclem44  40813  etransclem45  40814  sge0reuz  40982  hoidmvlelem2  41131  aacllem  42875
  Copyright terms: Public domain W3C validator