Theorem fzfi 13899

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 8983	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2825	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13458	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9145	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4191	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3981	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2737	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13898	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12818	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12790	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7233	. . . . . 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 3932	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13896	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9114	. . . 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 3016	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  Vcvv 3441   ∩ cin 3901  ∅c0 4286   class class class wbr 5099   ↦ cmpt 5180  ^◡ccnv 5624   ↾ cres 5627  Oncon0 6318  –1-1-onto→wf1o 6492  ‘cfv 6493  (class class class)co 7360  ωcom 7810  reccrdg 8342   ≈ cen 8884  Fincfn 8887  0cc0 11030  1c1 11031   + caddc 11033   − cmin 11368  ℕ₀cn0 12405  ℤ_≥cuz 12755  ...cfz 13427

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 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12150  df-n0 12406  df-z 12493  df-uz 12756  df-fz 13428

This theorem is referenced by:  fzfid  13900  fzofi  13901  fsequb  13902  fsequb2  13903  fseqsupcl  13904  ssnn0fi  13912  seqf1o  13970  isfinite4  14289  hashdom  14306  fzsdom2  14355  fnfz0hashnn0  14375  seqcoll2  14392  caubnd  15286  limsupgre  15408  summolem3  15641  summolem2  15643  zsum  15645  prodmolem3  15860  prodmolem2  15862  zprod  15864  risefallfac  15951  bpolylem  15975  phicl2  16699  phibnd  16702  hashdvds  16706  phiprmpw  16707  eulerth  16714  pcfac  16831  prmreclem2  16849  prmreclem3  16850  prmreclem4  16851  prmreclem5  16852  prmrec  16854  1arith  16859  vdwlem6  16918  vdwlem10  16922  vdwlem12  16924  prmdvdsprmo  16974  prmgaplcmlem1  16983  prmgaplcm  16992  isstruct2  17080  gsumval3lem1  19838  gsumval3lem2  19839  gsumval3  19840  coe1mul2  22215  ehleudis  25378  ehleudisval  25379  ovoliunlem2  25464  uniioombllem6  25549  itg0  25741  itgz  25742  coemullem  26215  aannenlem1  26296  aannenlem2  26297  birthdaylem1  26921  birthdaylem2  26922  wilthlem2  27039  wilthlem3  27040  ftalem5  27047  ppifi  27076  prmdvdsfi  27077  chtdif  27128  ppidif  27133  chp1  27137  ppiltx  27147  prmorcht  27148  mumul  27151  sqff1o  27152  ppiub  27175  pclogsum  27186  logexprlim  27196  gausslemma2dlem1  27337  gausslemma2dlem5  27342  gausslemma2dlem6  27343  lgseisenlem2  27347  axlowdimlem16  29034  konigsberglem5  30335  pmtrto1cl  33183  psgnfzto1stlem  33184  fzto1st  33187  psgnfzto1st  33189  smatcl  33961  1smat1  33963  esumpcvgval  34237  esumcvg  34245  carsggect  34477  carsgclctunlem2  34478  oddpwdc  34513  eulerpartlemb  34527  ballotlem1  34646  ballotlem2  34648  ballotlemfelz  34650  ballotlemfp1  34651  ballotlemfc0  34652  ballotlemfcc  34653  ballotlemfmpn  34654  ballotlemiex  34661  ballotlemsup  34664  ballotlemfg  34685  ballotlemfrc  34686  ballotlemfrceq  34688  ballotth  34697  plymulx0  34706  fsum2dsub  34766  reprfi2  34782  breprexpnat  34793  hgt750lemb  34815  hgt750leme  34817  pthhashvtx  35324  subfacf  35371  subfacp1lem1  35375  subfacp1lem3  35378  subfacp1lem5  35380  subfacp1lem6  35381  erdszelem2  35388  erdszelem10  35396  cvmliftlem15  35494  bcprod  35934  ptrecube  37823  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  poimirlem29  37852  poimirlem30  37853  poimirlem31  37854  poimirlem32  37855  mblfinlem2  37861  volsupnfl  37868  itg2addnclem2  37875  nnubfi  37953  nninfnub  37954  cntotbnd  37999  lcmfunnnd  42334  lcmineqlem4  42354  lcmineqlem6  42356  lcmineqlem15  42365  lcmineqlem16  42366  lcmineqlem19  42369  lcmineqlem20  42370  lcmineqlem21  42371  lcmineqlem22  42372  sticksstones17  42485  fisdomnn  42566  fz1sumconst  42631  eldioph2lem1  43069  eldioph2lem2  43070  eldioph2  43071  pellexlem5  43142  pellex  43144  jm2.22  43304  jm2.23  43305  hbt  43439  rp-isfinite6  43826  fzisoeu  45615  sumnnodd  45943  stoweidlem37  46348  stoweidlem44  46355  stoweidlem59  46370  fourierdlem37  46455  fourierdlem103  46520  fourierdlem104  46521  etransclem16  46561  etransclem24  46569  etransclem25  46570  etransclem33  46578  etransclem35  46580  etransclem44  46589  etransclem45  46590  sge0reuz  46758  hoidmvlelem2  46907  aacllem  50113