Theorem elfzle1 13550

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 13543	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzle 12870	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝐾)
3	1, 2	syl 18	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536  (class class class)co 7410   ≤ cle 11239  ℤ_≥cuz 12857  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  elfz1eq  13558  fzdisj  13575  elfznn  13577  ssfzunsnext  13593  fznatpl1  13602  fznn0sub2  13659  fz0fzdiffz0  13661  difelfznle  13666  seqf1olem1  14073  seqf1olem2  14074  bcval4  14339  seqcoll  14497  seqcoll2  14498  fsum0diaglem  15823  mertenslem1  15934  fprodntriv  15992  fallfacval4  16092  divalglem6  16451  hashdvds  16829  prmdiveq  16840  4sqlem11  17010  4sqlem12  17011  dvfsumlem3  26187  birthdaylem3  27118  ppiltx  27341  ppiub  27368  lgsdilem2  27497  lgsquadlem1  27544  chtppilimlem1  27637  dchrvmasumiflem1  27665  pntrlog2bndlem5  27745  pntpbnd1  27750  pntpbnd2  27751  pntlemh  27763  pntlemj  27767  ostth2lem2  27798  axlowdimlem16  29307  fzto1st1  33422  smattr  34189  smatbl  34190  smatbr  34191  ballotlem2  34879  ballotlemsdom  34902  ballotlemsima  34906  ballotlemfrcn0  34920  ballotlem1ri  34925  breprexplemc  35019  subfacp1lem1  35671  subfacp1lem5  35676  inffz  36222  poimirlem2  38293  poimirlem6  38297  poimirlem7  38298  poimirlem8  38299  poimirlem11  38302  poimirlem15  38306  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem22  38313  poimirlem24  38315  poimirlem29  38320  poimirlem31  38322  poimirlem32  38323  mblfinlem2  38329  fdc  38416  aks6d1c1  42903  aks6d1c5lem1  42923  sticksstones6  42938  sticksstones7  42939  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  bcled  42965  bcle2d  42966  unitscyglem2  42983  unitscyglem4  42985  irrapxlem3  43571  acongrep  43727  fzmaxdif  43728  acongeq  43730  jm2.23  43743  jm2.26lem3  43748  jm2.27dlem2  43757  monoords  46036  fmul01lt1lem1  46320  fmul01lt1lem2  46321  sumnnodd  46366  limsupubuzlem  46446  dvnmul  46677  dvnprodlem1  46680  dvnprodlem2  46681  iblspltprt  46707  itgspltprt  46713  stoweidlem3  46737  stoweidlem11  46745  stoweidlem20  46754  stoweidlem26  46760  stoweidlem34  46768  wallispi2  46807  dirkeritg  46836  fourierdlem11  46852  fourierdlem12  46853  fourierdlem15  46856  fourierdlem41  46882  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem52  46892  fourierdlem54  46894  fourierdlem79  46919  fourierdlem102  46942  fourierdlem103  46943  fourierdlem104  46944  fourierdlem114  46954  elaa2lem  46967  etransclem3  46971  etransclem4  46972  etransclem7  46975  etransclem10  46978  etransclem23  46991  etransclem24  46992  etransclem31  46999  etransclem32  47000  etransclem35  47003  etransclem41  47009  etransclem46  47014  caratheodorylem1  47260  iccpartgt  48196