Theorem fzfi 13934

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 8989	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2824	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13492	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9151	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4178	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3968	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2736	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13933	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12851	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12823	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7240	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 588	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3919	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13931	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9120	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 585	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 217	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3015	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  Vcvv 3429   ∩ cin 3888  ∅c0 4273   class class class wbr 5085   ↦ cmpt 5166  ^◡ccnv 5630   ↾ cres 5633  Oncon0 6323  –1-1-onto→wf1o 6497  ‘cfv 6498  (class class class)co 7367  ωcom 7817  reccrdg 8348   ≈ cen 8890  Fincfn 8893  0cc0 11038  1c1 11039   + caddc 11041   − cmin 11377  ℕ₀cn0 12437  ℤ_≥cuz 12788  ...cfz 13461

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-uz 12789  df-fz 13462

This theorem is referenced by:  fzfid  13935  fzofi  13936  fsequb  13937  fsequb2  13938  fseqsupcl  13939  ssnn0fi  13947  seqf1o  14005  isfinite4  14324  hashdom  14341  fzsdom2  14390  fnfz0hashnn0  14410  seqcoll2  14427  caubnd  15321  limsupgre  15443  summolem3  15676  summolem2  15678  zsum  15680  prodmolem3  15898  prodmolem2  15900  zprod  15902  risefallfac  15989  bpolylem  16013  phicl2  16738  phibnd  16741  hashdvds  16745  phiprmpw  16746  eulerth  16753  pcfac  16870  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmrec  16893  1arith  16898  vdwlem6  16957  vdwlem10  16961  vdwlem12  16963  prmdvdsprmo  17013  prmgaplcmlem1  17022  prmgaplcm  17031  isstruct2  17119  gsumval3lem1  19880  gsumval3lem2  19881  gsumval3  19882  coe1mul2  22234  ehleudis  25385  ehleudisval  25386  ovoliunlem2  25470  uniioombllem6  25555  itg0  25747  itgz  25748  coemullem  26215  aannenlem1  26294  aannenlem2  26295  birthdaylem1  26915  birthdaylem2  26916  wilthlem2  27032  wilthlem3  27033  ftalem5  27040  ppifi  27069  prmdvdsfi  27070  chtdif  27121  ppidif  27126  chp1  27130  ppiltx  27140  prmorcht  27141  mumul  27144  sqff1o  27145  ppiub  27167  pclogsum  27178  logexprlim  27188  gausslemma2dlem1  27329  gausslemma2dlem5  27334  gausslemma2dlem6  27335  lgseisenlem2  27339  axlowdimlem16  29026  konigsberglem5  30326  pmtrto1cl  33160  psgnfzto1stlem  33161  fzto1st  33164  psgnfzto1st  33166  smatcl  33946  1smat1  33948  esumpcvgval  34222  esumcvg  34230  carsggect  34462  carsgclctunlem2  34463  oddpwdc  34498  eulerpartlemb  34512  ballotlem1  34631  ballotlem2  34633  ballotlemfelz  34635  ballotlemfp1  34636  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemfmpn  34639  ballotlemiex  34646  ballotlemsup  34649  ballotlemfg  34670  ballotlemfrc  34671  ballotlemfrceq  34673  ballotth  34682  plymulx0  34691  fsum2dsub  34751  reprfi2  34767  breprexpnat  34778  hgt750lemb  34800  hgt750leme  34802  pthhashvtx  35310  subfacf  35357  subfacp1lem1  35361  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  erdszelem2  35374  erdszelem10  35382  cvmliftlem15  35480  bcprod  35920  ptrecube  37941  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  volsupnfl  37986  itg2addnclem2  37993  nnubfi  38071  nninfnub  38072  cntotbnd  38117  lcmfunnnd  42451  lcmineqlem4  42471  lcmineqlem6  42473  lcmineqlem15  42482  lcmineqlem16  42483  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem21  42488  lcmineqlem22  42489  sticksstones17  42602  fisdomnn  42683  fz1sumconst  42741  eldioph2lem1  43192  eldioph2lem2  43193  eldioph2  43194  pellexlem5  43261  pellex  43263  jm2.22  43423  jm2.23  43424  hbt  43558  rp-isfinite6  43945  fzisoeu  45733  sumnnodd  46060  stoweidlem37  46465  stoweidlem44  46472  stoweidlem59  46487  fourierdlem37  46572  fourierdlem103  46637  fourierdlem104  46638  etransclem16  46678  etransclem24  46686  etransclem25  46687  etransclem33  46695  etransclem35  46697  etransclem44  46706  etransclem45  46707  sge0reuz  46875  hoidmvlelem2  47024  aacllem  50276