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

Theorem fzfi 13338
 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 8733 . . 3 ∅ ∈ Fin
2 eleq1 2877 . . 3 ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
31, 2mpbiri 261 . 2 ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4 fzn0 12919 . . 3 ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ𝑀))
5 onfin2 8698 . . . . . 6 ω = (On ∩ Fin)
6 inss2 4156 . . . . . 6 (On ∩ Fin) ⊆ Fin
75, 6eqsstri 3949 . . . . 5 ω ⊆ Fin
8 eqid 2798 . . . . . . 7 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
98hashgf1o 13337 . . . . . 6 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10 peano2uz 12292 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
11 uznn0sub 12268 . . . . . . 7 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
1210, 11syl 17 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13 f1ocnvdm 7020 . . . . . 6 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
149, 12, 13sylancr 590 . . . . 5 (𝑁 ∈ (ℤ𝑀) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
157, 14sseldi 3913 . . . 4 (𝑁 ∈ (ℤ𝑀) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
168fzen2 13335 . . . 4 (𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) ≈ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17 enfii 8722 . . . 4 ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
1815, 16, 17syl2anc 587 . . 3 (𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) ∈ Fin)
194, 18sylbi 220 . 2 ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
203, 19pm2.61ine 3070 1 (𝑀...𝑁) ∈ Fin
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441   ∩ cin 3880  ∅c0 4243   class class class wbr 5031   ↦ cmpt 5111  ◡ccnv 5519   ↾ cres 5522  Oncon0 6160  –1-1-onto→wf1o 6324  ‘cfv 6325  (class class class)co 7136  ωcom 7563  reccrdg 8031   ≈ cen 8492  Fincfn 8495  0cc0 10529  1c1 10530   + caddc 10532   − cmin 10862  ℕ0cn0 11888  ℤ≥cuz 12234  ...cfz 12888 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11629  df-n0 11889  df-z 11973  df-uz 12235  df-fz 12889 This theorem is referenced by:  fzfid  13339  fzofi  13340  fsequb  13341  fsequb2  13342  fseqsupcl  13343  ssnn0fi  13351  seqf1o  13410  isfinite4  13722  hashdom  13739  fzsdom2  13788  fnfz0hashnn0  13805  seqcoll2  13822  caubnd  14713  limsupgre  14833  summolem3  15066  summolem2  15068  zsum  15070  prodmolem3  15282  prodmolem2  15284  zprod  15286  risefallfac  15373  bpolylem  15397  phicl2  16098  phibnd  16101  hashdvds  16105  phiprmpw  16106  eulerth  16113  phisum  16120  pcfac  16228  prmreclem2  16246  prmreclem3  16247  prmreclem4  16248  prmreclem5  16249  prmrec  16251  1arith  16256  vdwlem6  16315  vdwlem10  16319  vdwlem12  16321  prmdvdsprmo  16371  prmgaplcmlem1  16380  prmgaplcm  16389  isstruct2  16488  gsumval3lem1  19022  gsumval3lem2  19023  gsumval3  19024  coe1mul2  20908  ehleudis  24032  ehleudisval  24033  ovoliunlem2  24117  uniioombllem6  24202  itg0  24393  itgz  24394  coemullem  24857  aannenlem1  24934  aannenlem2  24935  birthdaylem1  25547  birthdaylem2  25548  wilthlem2  25664  wilthlem3  25665  ftalem5  25672  ppifi  25701  prmdvdsfi  25702  chtdif  25753  ppidif  25758  chp1  25762  ppiltx  25772  prmorcht  25773  mumul  25776  sqff1o  25777  ppiub  25798  pclogsum  25809  logexprlim  25819  gausslemma2dlem1  25960  gausslemma2dlem5  25965  gausslemma2dlem6  25966  lgseisenlem2  25970  axlowdimlem16  26761  konigsberglem5  28051  pmtrto1cl  30801  psgnfzto1stlem  30802  fzto1st  30805  psgnfzto1st  30807  smatcl  31170  1smat1  31172  esumpcvgval  31462  esumcvg  31470  carsggect  31701  carsgclctunlem2  31702  oddpwdc  31737  eulerpartlemb  31751  ballotlem1  31869  ballotlem2  31871  ballotlemfelz  31873  ballotlemfp1  31874  ballotlemfc0  31875  ballotlemfcc  31876  ballotlemfmpn  31877  ballotlemiex  31884  ballotlemsup  31887  ballotlemfg  31908  ballotlemfrc  31909  ballotlemfrceq  31911  ballotth  31920  plymulx0  31942  fsum2dsub  32003  reprfi2  32019  breprexpnat  32030  hgt750lemb  32052  hgt750leme  32054  pthhashvtx  32502  subfacf  32550  subfacp1lem1  32554  subfacp1lem3  32557  subfacp1lem5  32559  subfacp1lem6  32560  erdszelem2  32567  erdszelem10  32575  cvmliftlem15  32673  bcprod  33098  ptrecube  35076  poimirlem25  35101  poimirlem26  35102  poimirlem27  35103  poimirlem28  35104  poimirlem29  35105  poimirlem30  35106  poimirlem31  35107  poimirlem32  35108  mblfinlem2  35114  volsupnfl  35121  itg2addnclem2  35128  nnubfi  35207  nninfnub  35208  cntotbnd  35253  lcmfunnnd  39319  lcmineqlem4  39339  lcmineqlem6  39341  lcmineqlem15  39350  lcmineqlem16  39351  lcmineqlem19  39354  lcmineqlem20  39355  lcmineqlem21  39356  lcmineqlem22  39357  eldioph2lem1  39744  eldioph2lem2  39745  eldioph2  39746  pellexlem5  39817  pellex  39819  jm2.22  39979  jm2.23  39980  hbt  40117  rp-isfinite6  40269  fzisoeu  41975  sumnnodd  42315  stoweidlem37  42722  stoweidlem44  42729  stoweidlem59  42744  fourierdlem37  42829  fourierdlem103  42894  fourierdlem104  42895  etransclem16  42935  etransclem24  42943  etransclem25  42944  etransclem33  42952  etransclem35  42954  etransclem44  42963  etransclem45  42964  sge0reuz  43129  hoidmvlelem2  43278  aacllem  45370
 Copyright terms: Public domain W3C validator