Theorem elfzuz3 11694

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 11691	. 2 |- ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) )
2	1	simprbi 464	1 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )

Syntax hints:   -> wi 4   e. wcel 1804   ` cfv 5578  (class class class)co 6281   ZZ>=cuz 11090   ...cfz 11681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-1st 6785  df-2nd 6786  df-neg 9813  df-z 10871  df-uz 11091  df-fz 11682

This theorem is referenced by:  elfzel2  11695  elfzle2  11699  peano2fzr  11708  fzsplit2  11719  fzsplit  11720  fznn0sub  11725  fzopth  11729  fzss1  11731  fzss2  11732  fzp1elp1  11742  fzosplit  11837  fzoend  11882  fzofzp1b  11889  uzindi  12070  seqcl2  12104  seqfveq2  12108  monoord  12116  sermono  12118  seqsplit  12119  seqf1olem2  12126  seqid2  12132  seqhomo  12133  seqz  12134  bcval5  12375  seqcoll  12491  seqcoll2  12492  swrdval2  12626  swrd0val  12627  swrd0len  12628  spllen  12709  splfv2a  12711  fsum0diag2  13577  climcndslem2  13641  pcbc  14296  vdwlem2  14377  vdwlem5  14380  vdwlem6  14381  vdwlem8  14383  psgnunilem5  16393  efgsres  16630  efgredleme  16635  efgcpbllemb  16647  imasdsf1olem  20749  volsup  21839  dvn2bss  22206  dvtaylp  22637  wilth  23217  ftalem1  23218  ppisval2  23250  dvdsppwf1o  23334  logfaclbnd  23369  bposlem6  23436  eupares  24847  fzsplit3  27471  ballotlemsima  28327  ballotlemfrc  28338  ballotlemfrceq  28340  fzssfzo  28363  wrdres  28367  signstres  28405  erdszelem7  28514  erdszelem8  28515  prodfn0  29003  predfz  29258  mettrifi  30225  fmulcl  31503  fmul01lt1lem2  31507  stoweidlem11  31682  stoweidlem17  31688  fourierdlem15  31793  ssfz12  32168