Theorem elfzle2 13502

Description: A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzle2	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁)

Proof of Theorem elfzle2

Step	Hyp	Ref	Expression
1		elfzuz3 13495	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
2		eluzle 12832	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ≤ 𝑁)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5148  ‘cfv 6541  (class class class)co 7406   ≤ cle 11246  ℤ_≥cuz 12819  ...cfz 13481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-neg 11444  df-z 12556  df-uz 12820  df-fz 13482

This theorem is referenced by:  elfz1eq  13509  fzdisj  13525  ssfzunsnext  13543  fznatpl1  13552  fzp1disj  13557  uzdisj  13571  fzneuz  13579  fznuz  13580  elfzmlbm  13608  difelfznle  13612  nn0disj  13614  seqf1olem1  14004  seqf1olem2  14005  bcval4  14264  bcp1nk  14274  hashf1  14415  seqcoll  14422  seqcoll2  14423  isercolllem2  15609  isercoll  15611  summolem2a  15658  fsum0diaglem  15719  mertenslem1  15827  prodmolem2a  15875  binomrisefac  15983  bpoly4  16000  fzm1ndvds  16262  prmind2  16619  prmdvdsfz  16639  isprm7  16642  hashdvds  16705  prmdiveq  16716  prmreclem3  16848  prmreclem5  16850  4sqlem11  16885  4sqlem12  16886  vdwlem1  16911  vdwlem3  16913  vdwlem6  16916  vdwlem9  16919  vdwlem10  16920  mndodconglem  19404  oddvds  19410  gexdvds  19447  coe1tmmul  21791  lebnumii  24474  ovolicc2lem4  25029  voliunlem1  25059  dvfsumle  25530  dvfsumge  25531  dvfsumabs  25532  dvfsumlem3  25537  elply2  25702  coeeq2  25748  aaliou3lem6  25853  birthdaylem2  26447  birthdaylem3  26448  wilthlem1  26562  ftalem5  26571  basellem1  26575  basellem3  26577  ppiprm  26645  chtprm  26647  logfac2  26710  lgsval2lem  26800  lgsqrlem2  26840  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgsquadlem1  26873  lgsquadlem2  26874  2lgslem1a  26884  chebbnd1lem1  26962  dchrvmasumiflem1  26994  mulog2sumlem2  27028  pntrlog2bndlem6  27076  pntpbnd1  27079  pntpbnd2  27080  pntlemh  27092  pntlemj  27096  pntlemf  27098  axlowdimlem16  28205  crctcshwlkn0lem2  29055  crctcshlem4  29064  bcm1n  31994  psgnfzto1stlem  32247  cycpmco2lem6  32278  cycpmco2lem7  32279  smatrcl  32765  submateqlem1  32776  madjusmdetlem2  32797  ballotlemimin  33493  ballotlemsdom  33499  ballotlemsel1i  33500  ballotlemsima  33503  ballotlemfrceq  33516  ballotlemfrcn0  33517  fsum2dsub  33608  reprgt  33622  breprexplemc  33633  erdszelem8  34178  cvmliftlem2  34266  cvmliftlem7  34271  supfz  34687  bcprod  34697  bccolsum  34698  gg-dvfsumle  35171  poimirlem2  36479  poimirlem3  36480  poimirlem4  36481  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem12  36489  poimirlem13  36490  poimirlem14  36491  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem23  36500  poimirlem24  36501  poimirlem26  36503  poimirlem28  36505  poimirlem29  36506  poimirlem31  36508  poimirlem32  36509  mblfinlem2  36515  aks4d1p5  40934  aks4d1p6  40935  aks4d1p8  40941  sticksstones6  40956  sticksstones7  40957  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  metakunt1  40974  metakunt7  40980  metakunt15  40988  metakunt16  40989  metakunt22  40995  metakunt28  41001  metakunt30  41003  irrapxlem3  41548  irrapxlem4  41549  fzmaxdif  41706  jm2.23  41721  jm2.26lem3  41726  jm2.27dlem2  41735  binomcxplemnn0  43094  monoords  43994  elfzolem1  44018  fmul01lt1lem1  44287  fmul01lt1lem2  44288  sumnnodd  44333  dvnmul  44646  dvnprodlem1  44649  dvnprodlem2  44650  iblspltprt  44676  itgspltprt  44682  stoweidlem3  44706  stoweidlem17  44720  stoweidlem20  44723  stoweidlem26  44729  stoweidlem34  44737  fourierdlem11  44821  fourierdlem12  44822  fourierdlem15  44825  fourierdlem25  44835  fourierdlem41  44851  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem52  44861  fourierdlem54  44863  fourierdlem79  44888  fourierdlem102  44911  fourierdlem114  44923  elaa2lem  44936  etransclem23  44960  etransclem28  44965  etransclem35  44972  etransclem38  44975  iundjiun  45163  2elfz2melfz  46013  elfzelfzlble  46016  iccpartgt  46082  fmtno4prm  46230  difmodm1lt  47162