Theorem elfzuz3 13475

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	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Proof of Theorem elfzuz3

Step	Hyp	Ref	Expression
1		elfzuzb 13472	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simprbi 497	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  ℤ_≥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-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095

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-ral 3052  df-rex 3062  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-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-id 5526  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-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-neg 11380  df-z 12525  df-uz 12789  df-fz 13462

This theorem is referenced by:  elfzel2  13476  elfzle2  13482  peano2fzr  13491  fzsplit2  13503  fzsplit  13504  fznn0sub  13510  fzopth  13515  fzss1  13517  fzss2  13518  fzp1elp1  13531  predfz  13607  fzosplit  13647  fzoend  13712  fzofzp1b  13720  uzindi  13944  seqcl2  13982  seqfveq2  13986  monoord  13994  sermono  13996  seqsplit  13997  seqf1olem2  14004  seqid2  14010  seqhomo  14011  seqz  14012  bcval5  14280  seqcoll  14426  seqcoll2  14427  swrdval2  14609  pfxres  14642  pfxf  14643  spllen  14716  splfv2a  14718  repswpfx  14747  fsum0diag2  15745  climcndslem2  15815  prodfn0  15859  lcmflefac  16617  pcbc  16871  vdwlem2  16953  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  prmgaplem1  17020  pfxchn  18576  psgnunilem5  19469  efgsres  19713  efgredleme  19718  efgcpbllemb  19730  imasdsf1olem  24338  volsup  25523  dvn2bss  25897  dvtaylp  26335  wilth  27034  ftalem1  27036  ppisval2  27068  dvdsppwf1o  27149  logfaclbnd  27185  bposlem6  27252  wlkres  29737  fzsplit3  32866  wrdres  32995  pfxf1  33002  swrdrn2  33014  swrdrn3  33015  swrdf1  33016  swrdrndisj  33017  splfv3  33018  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem7  33193  ballotlemsima  34660  ballotlemfrc  34671  ballotlemfrceq  34673  fzssfzo  34683  signstres  34719  fsum2dsub  34751  revpfxsfxrev  35298  swrdrevpfx  35299  pfxwlk  35306  erdszelem7  35379  erdszelem8  35380  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem7  37948  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  mettrifi  38078  fzsplitnd  42421  aks6d1c2lem4  42566  bcc0  44767  iunincfi  45524  monoordxrv  45909  fmulcl  46011  fmul01lt1lem2  46015  dvnprodlem2  46375  stoweidlem11  46439  stoweidlem17  46445  fourierdlem15  46550  ssfz12  47762  smonoord  47825