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

Theorem fzfi 12192
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  |-  ( M ... N )  e. 
Fin

Proof of Theorem fzfi
StepHypRef Expression
1 0fin 7809 . . 3  |-  (/)  e.  Fin
2 eleq1 2495 . . 3  |-  ( ( M ... N )  =  (/)  ->  ( ( M ... N )  e.  Fin  <->  (/)  e.  Fin ) )
31, 2mpbiri 236 . 2  |-  ( ( M ... N )  =  (/)  ->  ( M ... N )  e. 
Fin )
4 fzn0 11821 . . 3  |-  ( ( M ... N )  =/=  (/)  <->  N  e.  ( ZZ>=
`  M ) )
5 onfin2 7774 . . . . . 6  |-  om  =  ( On  i^i  Fin )
6 inss2 3683 . . . . . 6  |-  ( On 
i^i  Fin )  C_  Fin
75, 6eqsstri 3494 . . . . 5  |-  om  C_  Fin
8 eqid 2422 . . . . . . 7  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om )
98hashgf1o 12191 . . . . . 6  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0
10 peano2uz 11220 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  +  1 )  e.  ( ZZ>= `  M )
)
11 uznn0sub 11198 . . . . . . 7  |-  ( ( N  +  1 )  e.  ( ZZ>= `  M
)  ->  ( ( N  +  1 )  -  M )  e. 
NN0 )
1210, 11syl 17 . . . . . 6  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ( N  +  1 )  -  M )  e. 
NN0 )
13 f1ocnvdm 6199 . . . . . 6  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0  /\  ( ( N  + 
1 )  -  M
)  e.  NN0 )  ->  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( N  + 
1 )  -  M
) )  e.  om )
149, 12, 13sylancr 667 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( `' ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( ( N  +  1 )  -  M ) )  e.  om )
157, 14sseldi 3462 . . . 4  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( `' ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( ( N  +  1 )  -  M ) )  e.  Fin )
168fzen2 12189 . . . 4  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( M ... N )  ~~  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( N  + 
1 )  -  M
) ) )
17 enfii 7799 . . . 4  |-  ( ( ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( N  + 
1 )  -  M
) )  e.  Fin  /\  ( M ... N
)  ~~  ( `' ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( ( N  +  1 )  -  M ) ) )  ->  ( M ... N )  e.  Fin )
1815, 16, 17syl2anc 665 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( M ... N )  e.  Fin )
194, 18sylbi 198 . 2  |-  ( ( M ... N )  =/=  (/)  ->  ( M ... N )  e.  Fin )
203, 19pm2.61ine 2733 1  |-  ( M ... N )  e. 
Fin
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872    =/= wne 2614   _Vcvv 3080    i^i cin 3435   (/)c0 3761   class class class wbr 4423    |-> cmpt 4482   `'ccnv 4852    |` cres 4855   Oncon0 5442   -1-1-onto->wf1o 5600   ` cfv 5601  (class class class)co 6306   omcom 6707   reccrdg 7139    ~~ cen 7578   Fincfn 7581   0cc0 9547   1c1 9548    + caddc 9550    - cmin 9868   NN0cn0 10877   ZZ>=cuz 11167   ...cfz 11792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-n0 10878  df-z 10946  df-uz 11168  df-fz 11793
This theorem is referenced by:  fzfid  12193  fzofi  12194  fsequb  12195  fsequb2  12196  fseqsupcl  12197  ssnn0fi  12204  seqf1o  12261  isfinite4  12550  hashdom  12565  fzsdom2  12605  hashfzdm  12617  seqcoll2  12633  caubnd  13422  limsupgre  13542  limsupgreOLD  13543  fz1f1o  13776  summolem3  13780  summolem2  13782  zsum  13784  prodmolem3  13987  prodmolem2  13989  zprod  13991  risefallfac  14077  bpolylem  14101  phicl2  14716  phibnd  14719  hashdvds  14723  phiprmpw  14724  eulerth  14731  pcfac  14844  prmreclem2  14861  prmreclem3  14862  prmreclem4  14863  prmreclem5  14864  prmrec  14866  1arith  14871  vdwlem6  14936  vdwlem10  14940  vdwlem12  14942  prmdvdsprmo  15000  prmgaplcmlem1  15009  prmgaplcmlem1OLD  15012  prmdvdsprmorOLD  15015  prmorlelcmsOLDOLD  15022  prmgaplcm  15031  isstruct2  15130  gsumval3lem1  17539  gsumval3lem2  17540  gsumval3  17541  coe1mul2  18862  ovoliunlem2  22455  uniioombllem6  22545  itg0  22736  itgz  22737  coemullem  23203  aannenlem1  23283  aannenlem2  23284  birthdaylem1  23876  birthdaylem2  23877  wilthlem2  23993  wilthlem3  23994  ftalem5  24000  ftalem5OLD  24002  ppifi  24031  prmdvdsfi  24033  chtdif  24084  ppidif  24089  chp1  24093  ppiltx  24103  prmorcht  24104  mumul  24107  sqff1o  24108  ppiub  24131  pclogsum  24142  logexprlim  24152  lgseisenlem2  24277  axlowdimlem16  24986  wlks  25246  wlkres  25249  trls  25265  crcts  25349  cycls  25350  konigsberg  25714  pmtrto1cl  28621  psgnfzto1stlem  28622  fzto1st  28625  psgnfzto1st  28627  smatcl  28637  1smat1  28639  esumpcvgval  28908  esumcvg  28916  carsggect  29159  carsgclctunlem2  29160  oddpwdc  29196  eulerpartlemb  29210  ballotlem1  29328  ballotlem2  29330  ballotlemfelz  29332  ballotlemfp1  29333  ballotlemfc0  29334  ballotlemfcc  29335  ballotlemfmpn  29336  ballotlemiex  29343  ballotlemsup  29346  ballotlemfg  29367  ballotlemfrc  29368  ballotlemfrceq  29370  ballotth  29379  ballotlemiexOLD  29381  ballotlemsupOLD  29384  ballotlemfgOLD  29405  ballotlemfrcOLD  29406  ballotlemfrceqOLD  29408  ballotthOLD  29417  plymulx0  29445  subfacf  29907  subfacp1lem1  29911  subfacp1lem3  29914  subfacp1lem5  29916  subfacp1lem6  29917  erdszelem2  29924  erdszelem10  29932  cvmliftlem15  30030  bcprod  30382  ptrecube  31905  poimirlem25  31930  poimirlem26  31931  poimirlem27  31932  poimirlem28  31933  poimirlem29  31934  poimirlem30  31935  poimirlem31  31936  poimirlem32  31937  mblfinlem2  31943  volsupnfl  31950  itg2addnclem2  31959  nnubfi  32044  nninfnub  32045  cntotbnd  32093  eldioph2lem1  35572  eldioph2lem2  35573  eldioph2  35574  pellexlem5  35648  pellex  35650  jm2.22  35821  jm2.23  35822  hbt  35960  phisum  36047  rp-isfinite6  36134  fzisoeu  37473  sumnnodd  37651  stoweidlem37  37839  stoweidlem44  37846  stoweidlem59  37861  fourierdlem37  37948  fourierdlem103  38014  fourierdlem104  38015  etransclem16  38056  etransclem24  38064  etransclem25  38065  etransclem33  38073  etransclem35  38075  etransclem44  38084  etransclem45  38085  hoidmvlelem2  38323  aacllem  40191
  Copyright terms: Public domain W3C validator