Theorem elfzle1 13544

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

Assertion

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

Proof of Theorem elfzle1

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

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5152  ‘cfv 6553  (class class class)co 7426   ≤ cle 11287  ℤ_≥cuz 12860  ...cfz 13524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-1st 7999  df-2nd 8000  df-neg 11485  df-z 12597  df-uz 12861  df-fz 13525

This theorem is referenced by:  elfz1eq  13552  fzdisj  13568  elfznn  13570  ssfzunsnext  13586  fznatpl1  13595  fznn0sub2  13648  fz0fzdiffz0  13650  difelfznle  13655  seqf1olem1  14046  seqf1olem2  14047  bcval4  14306  seqcoll  14465  seqcoll2  14466  fsum0diaglem  15762  mertenslem1  15870  fprodntriv  15926  fallfacval4  16027  divalglem6  16382  hashdvds  16751  prmdiveq  16762  4sqlem11  16931  4sqlem12  16932  dvfsumlem3  25983  birthdaylem3  26905  ppiltx  27129  ppiub  27157  lgsdilem2  27286  lgsquadlem1  27333  chtppilimlem1  27426  dchrvmasumiflem1  27454  pntrlog2bndlem5  27534  pntpbnd1  27539  pntpbnd2  27540  pntlemh  27552  pntlemj  27556  ostth2lem2  27587  axlowdimlem16  28788  fzto1st1  32844  smattr  33433  smatbl  33434  smatbr  33435  ballotlem2  34141  ballotlemsdom  34164  ballotlemsima  34168  ballotlemfrcn0  34182  ballotlem1ri  34187  breprexplemc  34297  subfacp1lem1  34822  subfacp1lem5  34827  inffz  35357  poimirlem2  37128  poimirlem6  37132  poimirlem7  37133  poimirlem8  37134  poimirlem11  37137  poimirlem15  37141  poimirlem16  37142  poimirlem17  37143  poimirlem19  37145  poimirlem20  37146  poimirlem22  37148  poimirlem24  37150  poimirlem29  37155  poimirlem31  37157  poimirlem32  37158  mblfinlem2  37164  fdc  37251  aks6d1c1  41619  aks6d1c5lem1  41639  sticksstones6  41655  sticksstones7  41656  sticksstones10  41659  sticksstones12a  41661  sticksstones12  41662  bcled  41682  bcle2d  41683  metakunt15  41703  irrapxlem3  42275  acongrep  42432  fzmaxdif  42433  acongeq  42435  jm2.23  42448  jm2.26lem3  42453  jm2.27dlem2  42462  monoords  44708  fmul01lt1lem1  45001  fmul01lt1lem2  45002  sumnnodd  45047  limsupubuzlem  45129  dvnmul  45360  dvnprodlem1  45363  dvnprodlem2  45364  iblspltprt  45390  itgspltprt  45396  stoweidlem3  45420  stoweidlem11  45428  stoweidlem20  45437  stoweidlem26  45443  stoweidlem34  45451  wallispi2  45490  dirkeritg  45519  fourierdlem11  45535  fourierdlem12  45536  fourierdlem15  45539  fourierdlem41  45565  fourierdlem48  45571  fourierdlem49  45572  fourierdlem50  45573  fourierdlem52  45575  fourierdlem54  45577  fourierdlem79  45602  fourierdlem102  45625  fourierdlem103  45626  fourierdlem104  45627  fourierdlem114  45637  elaa2lem  45650  etransclem3  45654  etransclem4  45655  etransclem7  45658  etransclem10  45661  etransclem23  45674  etransclem24  45675  etransclem31  45682  etransclem32  45683  etransclem35  45686  etransclem41  45692  etransclem46  45697  caratheodorylem1  45943  iccpartgt  46796