Theorem fzfi 14115

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 9070	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2848	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 261	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13671	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9232	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4134	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3954	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2760	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 14114	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 13028	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 13000	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 18	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7293	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 599	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3906	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 14112	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9201	. . . 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 3038	1 ⊢ (𝑀...𝑁) ∈ Fin

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  Vcvv 3450   ∩ cin 4089  ∅c0 4278   class class class wbr 5102   ↦ cmpt 5185  ^◡ccnv 5649   ↾ cres 5652  Oncon0 6362  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7420  ωcom 7877  reccrdg 8417   ≈ cen 8970  Fincfn 8973  0cc0 11200  1c1 11201   + caddc 11203   − cmin 11541  ℕ₀cn0 12606  ℤ_≥cuz 12965  ...cfz 13639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694  df-uz 12966  df-fz 13640

This theorem is used by:  fzfid  14116  fzofi  14117  fsequb  14118  fsequb2  14119  fseqsupcl  14120  ssnn0fi  14128  seqf1o  14186  isfinite4  14506  hashdom  14523  fzsdom2  14573  fnfz0hashnn0  14593  seqcoll2  14610  caubnd  15526  limsupgre  15648  summolem3  15880  summolem2  15882  zsum  15884  prodmolem3  16100  prodmolem2  16102  zprod  16104  risefallfac  16191  bpolylem  16214  phicl2  16945  phibnd  16948  hashdvds  16952  phiprmpw  16953  eulerth  16960  pcfac  17077  prmreclem2  17095  prmreclem3  17096  prmreclem4  17097  prmreclem5  17098  prmrec  17100  1arith  17105  vdwlem6  17164  vdwlem10  17168  vdwlem12  17170  prmdvdsprmo  17220  prmgaplcmlem1  17229  prmgaplcm  17238  isstruct2  17327  gsumval3lem1  20119  gsumval3lem2  20120  gsumval3  20121  coe1mul2  22588  ehleudis  25739  ehleudisval  25740  ovoliunlem2  25824  uniioombllem6  25909  itg0  26100  itgz  26101  coemullem  26569  plyn0mulidp  26602  aannenlem1  26655  aannenlem2  26656  birthdaylem1  27279  birthdaylem2  27280  wilthlem2  27396  wilthlem3  27397  ftalem5  27404  ppifi  27433  prmdvdsfi  27434  chtdif  27485  ppidif  27490  chp1  27494  ppiltx  27504  prmorcht  27505  mumul  27508  sqff1o  27509  ppiub  27531  pclogsum  27542  logexprlim  27552  gausslemma2dlem1  27693  gausslemma2dlem5  27698  gausslemma2dlem6  27699  lgseisenlem2  27703  axlowdimlem16  29535  pthhashvtx  30315  konigsberglem5  30857  pmtrto1cl  33660  psgnfzto1stlem  33661  fzto1st  33664  psgnfzto1st  33666  smatcl  34434  1smat1  34436  esumpcvgval  34710  esumcvg  34718  carsggect  34950  carsgclctunlem2  34951  oddpwdc  34986  eulerpartlemb  35000  ballotlem1  35119  ballotlem2  35121  ballotlemfelz  35123  ballotlemfp1  35124  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemfmpn  35127  ballotlemiex  35134  ballotlemsup  35137  ballotlemfg  35158  ballotlemfrc  35159  ballotlemfrceq  35161  ballotth  35170  fsum2dsub  35236  reprfi2  35252  breprexpnat  35263  hgt750lemb  35285  hgt750leme  35287  subfacf  35940  subfacp1lem1  35944  subfacp1lem3  35947  subfacp1lem5  35949  subfacp1lem6  35950  erdszelem2  35957  erdszelem10  35965  cvmliftlem15  36063  bcprod  36503  ptrecube  38539  poimirlem25  38564  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  poimirlem29  38568  poimirlem30  38569  poimirlem31  38570  poimirlem32  38571  mblfinlem2  38577  volsupnfl  38584  itg2addnclem2  38591  nnubfi  38685  nninfnub  38686  cntotbnd  38731  lcmfunnnd  43063  lcmineqlem4  43083  lcmineqlem6  43085  lcmineqlem15  43094  lcmineqlem16  43095  lcmineqlem19  43098  lcmineqlem20  43099  lcmineqlem21  43100  lcmineqlem22  43101  sticksstones17  43214  fisdomnn  43296  fz1sumconst  43367  frlmnzcoordinf  43655  eldioph2lem1  43771  eldioph2lem2  43772  eldioph2  43773  pellexlem5  43840  pellex  43842  jm2.22  44002  jm2.23  44003  hbt  44132  rp-isfinite6  44519  dmstructfi  45927  fzisoeu  46316  sumnnodd  46642  stoweidlem37  47047  stoweidlem44  47054  stoweidlem59  47069  fourierdlem37  47154  fourierdlem103  47219  fourierdlem104  47220  etransclem16  47260  etransclem24  47268  etransclem25  47269  etransclem33  47277  etransclem35  47279  etransclem44  47288  etransclem45  47289  sge0reuz  47457  hoidmvlelem2  47606  aacllem  50939  veronesematbasd  50980  veroquadmodzerod  50984  veroquadnolindfd  50985  veroquaddetzerod  50986