Theorem elfzle1 13481

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  ‘cfv 6498  (class class class)co 7367   ≤ cle 11180  ℤ_≥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:  elfz1eq  13489  fzdisj  13505  elfznn  13507  ssfzunsnext  13523  fznatpl1  13532  fznn0sub2  13589  fz0fzdiffz0  13591  difelfznle  13596  seqf1olem1  14003  seqf1olem2  14004  bcval4  14269  seqcoll  14426  seqcoll2  14427  fsum0diaglem  15738  mertenslem1  15849  fprodntriv  15907  fallfacval4  16008  divalglem6  16367  hashdvds  16745  prmdiveq  16756  4sqlem11  16926  4sqlem12  16927  dvfsumlem3  25995  birthdaylem3  26917  ppiltx  27140  ppiub  27167  lgsdilem2  27296  lgsquadlem1  27343  chtppilimlem1  27436  dchrvmasumiflem1  27464  pntrlog2bndlem5  27544  pntpbnd1  27549  pntpbnd2  27550  pntlemh  27562  pntlemj  27566  ostth2lem2  27597  axlowdimlem16  29026  fzto1st1  33163  smattr  33943  smatbl  33944  smatbr  33945  ballotlem2  34633  ballotlemsdom  34656  ballotlemsima  34660  ballotlemfrcn0  34674  ballotlem1ri  34679  breprexplemc  34776  subfacp1lem1  35361  subfacp1lem5  35366  inffz  35912  poimirlem2  37943  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem11  37952  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem24  37965  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  fdc  38066  aks6d1c1  42555  aks6d1c5lem1  42575  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  bcled  42617  bcle2d  42618  unitscyglem2  42635  unitscyglem4  42637  irrapxlem3  43252  acongrep  43408  fzmaxdif  43409  acongeq  43411  jm2.23  43424  jm2.26lem3  43429  jm2.27dlem2  43438  monoords  45730  fmul01lt1lem1  46014  fmul01lt1lem2  46015  sumnnodd  46060  limsupubuzlem  46140  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  iblspltprt  46401  itgspltprt  46407  stoweidlem3  46431  stoweidlem11  46439  stoweidlem20  46448  stoweidlem26  46454  stoweidlem34  46462  wallispi2  46501  dirkeritg  46530  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem52  46586  fourierdlem54  46588  fourierdlem79  46613  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  elaa2lem  46661  etransclem3  46665  etransclem4  46666  etransclem7  46669  etransclem10  46672  etransclem23  46685  etransclem24  46686  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem46  46708  caratheodorylem1  46954  iccpartgt  47887