Theorem fzfi 14139

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

Step	Hyp	Ref	Expression
1		0fi 9095	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2852	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 261	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13695	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9257	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4137	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3959	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2763	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 14138	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶1-1ontoℕ0
10		peano2uz 13052	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 13024	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 18	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7313	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω⟶1-1ontoℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 599	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3911	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 14136	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9226	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 596	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 220	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3042	1 ⊢ (𝑀...𝑁) ∈ Fin

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  Vcvv 3454   ∩ cin 4092  ∅c0 4281   class class class wbr 5106   ↦ cmpt 5189  ^◡ccnv 5654   ↾ cres 5657  Oncon0 6377  ⟶1-1ontowf1o 6554  ‘cfv 6555  (class class class)co 7440  ωcom 7898  reccrdg 8442   ≈ cen 8995  Fincfn 8998  0cc0 11224  1c1 11225   + caddc 11227   − cmin 11565  ℕ₀cn0 12630  ℤ_≥cuz 12989  ...cfz 13663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-n0 12631  df-z 12718  df-uz 12990  df-fz 13664

This theorem is used by:  fzfid  14140  fzofi  14141  fsequb  14142  fsequb2  14143  fseqsupcl  14144  ssnn0fi  14152  seqf1o  14210  isfinite4  14530  hashdom  14547  fzsdom2  14597  fnfz0hashnn0  14617  seqcoll2  14634  caubnd  15552  limsupgre  15674  summolem3  15906  summolem2  15908  zsum  15910  prodmolem3  16126  prodmolem2  16128  zprod  16130  risefallfac  16217  bpolylem  16240  phicl2  16971  phibnd  16974  hashdvds  16978  phiprmpw  16979  eulerth  16986  pcfac  17103  prmreclem3  17122  prmreclem4  17123  prmreclem5  17124  prmrec  17126  1arith  17131  vdwlem6  17190  vdwlem10  17194  vdwlem12  17196  prmdvdsprmo  17246  prmgaplcmlem1  17255  prmgaplcm  17264  isstruct2  17353  gsumval3lem1  20146  gsumval3lem2  20147  gsumval3  20148  coe1mul2  22615  ovoliunlem2  25851  uniioombllem6  25936  itg0  26127  itgz  26128  coemullem  26596  plyn0mulidp  26629  aannenlem1  26682  aannenlem2  26683  birthdaylem1  27306  birthdaylem2  27307  wilthlem2  27423  wilthlem3  27424  ftalem5  27431  ppifi  27460  prmdvdsfi  27461  chtdif  27512  ppidif  27517  chp1  27521  ppiltx  27531  prmorcht  27532  mumul  27535  sqff1o  27536  ppiub  27558  pclogsum  27569  logexprlim  27579  gausslemma2dlem1  27720  gausslemma2dlem5  27725  gausslemma2dlem6  27726  lgseisenlem2  27730  axlowdimlem16  29562  pthhashvtx  30342  konigsberglem5  30884  pmtrto1cl  33727  psgnfzto1stlem  33728  fzto1st  33731  psgnfzto1st  33733  smatcl  34501  1smat1  34503  esumpcvgval  34777  esumcvg  34785  carsggect  35017  carsgclctunlem2  35018  oddpwdc  35053  eulerpartlemb  35067  ballotlem1  35186  ballotlem2  35188  ballotlemfelz  35190  ballotlemfp1  35191  ballotlemfc0  35192  ballotlemfcc  35193  ballotlemfmpn  35194  ballotlemiex  35201  ballotlemsup  35204  ballotlemfg  35225  ballotlemfrc  35226  ballotlemfrceq  35228  ballotth  35237  fsum2dsub  35303  reprfi2  35319  breprexpnat  35330  hgt750lemb  35352  hgt750leme  35354  subfacf  36106  subfacp1lem1  36110  subfacp1lem3  36113  subfacp1lem5  36115  subfacp1lem6  36116  erdszelem2  36123  erdszelem10  36131  cvmliftlem15  36229  bcprod  36680  ptrecube  38729  poimirlem25  38754  poimirlem26  38755  poimirlem27  38756  poimirlem28  38757  poimirlem29  38758  poimirlem30  38759  poimirlem31  38760  poimirlem32  38761  mblfinlem2  38767  volsupnfl  38774  itg2addnclem2  38781  nnubfi  38875  nninfnub  38876  cntotbnd  38921  lcmfunnnd  43253  lcmineqlem4  43273  lcmineqlem6  43275  lcmineqlem15  43284  lcmineqlem16  43285  lcmineqlem19  43288  lcmineqlem20  43289  lcmineqlem21  43290  lcmineqlem22  43291  sticksstones17  43404  fisdomnn  43486  fz1sumconst  43557  frlmnzcoordinf  43845  eldioph2lem1  43962  eldioph2lem2  43963  eldioph2  43964  pellexlem5  44031  pellex  44033  jm2.22  44193  jm2.23  44194  hbt  44322  rp-isfinite6  44709  dmstructfi  46118  fzisoeu  46519  sumnnodd  46845  stoweidlem37  47250  stoweidlem44  47257  stoweidlem59  47272  fourierdlem37  47357  fourierdlem103  47422  fourierdlem104  47423  etransclem16  47463  etransclem24  47471  etransclem25  47472  etransclem33  47480  etransclem35  47482  etransclem44  47491  etransclem45  47492  sge0reuz  47660  hoidmvlelem2  47809  aacllem  51217  veronesematbasd  51258  veroquadmodzerod  51262  veroquadnolindfd  51263  veroquaddetzerod  51264