Theorem elfzuz3 12339

Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuz3	|- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )

Proof of Theorem elfzuz3

Step	Hyp	Ref	Expression
1		elfzuzb 12336	. 2 |- ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) )
2	1	simprbi 480	1 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )

Syntax hints:   -> wi 4   e. wcel 1990   ` cfv 5888  (class class class)co 6650   ZZ>=cuz 11687   ...cfz 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-neg 10269  df-z 11378  df-uz 11688  df-fz 12327

This theorem is referenced by:  elfzel2  12340  elfzle2  12345  peano2fzr  12354  fzsplit2  12366  fzsplit  12367  fznn0sub  12373  fzopth  12378  fzss1  12380  fzss2  12381  fzp1elp1  12394  predfz  12464  fzosplit  12501  fzoend  12559  fzofzp1b  12566  uzindi  12781  seqcl2  12819  seqfveq2  12823  monoord  12831  sermono  12833  seqsplit  12834  seqf1olem2  12841  seqid2  12847  seqhomo  12848  seqz  12849  bcval5  13105  seqcoll  13248  seqcoll2  13249  swrdval2  13420  swrd0val  13421  swrd0len  13422  spllen  13505  splfv2a  13507  fsum0diag2  14515  climcndslem2  14582  prodfn0  14626  lcmflefac  15361  pcbc  15604  vdwlem2  15686  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  prmgaplem1  15753  psgnunilem5  17914  efgsres  18151  efgredleme  18156  efgcpbllemb  18168  imasdsf1olem  22178  volsup  23324  dvn2bss  23693  dvtaylp  24124  wilth  24797  ftalem1  24799  ppisval2  24831  dvdsppwf1o  24912  logfaclbnd  24947  bposlem6  25014  wlkres  26567  fzsplit3  29553  ballotlemsima  30577  ballotlemfrc  30588  ballotlemfrceq  30590  fzssfzo  30613  wrdres  30617  signstres  30652  fsum2dsub  30685  erdszelem7  31179  erdszelem8  31180  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem7  33416  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  mettrifi  33553  bcc0  38539  iunincfi  39272  fmulcl  39813  fmul01lt1lem2  39817  dvnprodlem2  40162  stoweidlem11  40228  stoweidlem17  40234  fourierdlem15  40339  ssfz12  41324  smonoord  41341  pfxres  41388  pfxf  41389  repswpfx  41436