Theorem elfzle1 12344

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

Syntax hints:   → wi 4   ∈ wcel 1990   class class class wbr 4653  ‘cfv 5888  (class class class)co 6650   ≤ cle 10075  ℤ_≥cuz 11687  ...cfz 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-neg 10269  df-z 11378  df-uz 11688  df-fz 12327

This theorem is referenced by:  elfz1eq  12352  fzdisj  12368  elfznn  12370  ssfzunsnext  12386  fznatpl1  12395  fznn0sub2  12446  fz0fzdiffz0  12448  difelfznle  12453  seqf1olem1  12840  seqf1olem2  12841  bcval4  13094  seqcoll  13248  seqcoll2  13249  fsum0diaglem  14508  mertenslem1  14616  fprodntriv  14672  fallfacval4  14774  divalglem6  15121  hashdvds  15480  prmdiveq  15491  4sqlem11  15659  4sqlem12  15660  dvfsumlem3  23791  birthdaylem3  24680  ppiltx  24903  ppiub  24929  lgsdilem2  25058  lgsquadlem1  25105  chtppilimlem1  25162  dchrvmasumiflem1  25190  pntrlog2bndlem5  25270  pntpbnd1  25275  pntpbnd2  25276  pntlemh  25288  pntlemj  25292  ostth2lem2  25323  axlowdimlem16  25837  fzto1st1  29852  smattr  29865  smatbl  29866  smatbr  29867  ballotlem2  30550  ballotlemsdom  30573  ballotlemsima  30577  ballotlemfrcn0  30591  ballotlem1ri  30596  breprexplemc  30710  subfacp1lem1  31161  subfacp1lem5  31166  inffz  31614  inffzOLD  31615  poimirlem2  33411  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem11  33420  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem24  33433  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  fdc  33541  irrapxlem3  37388  acongrep  37547  fzmaxdif  37548  acongeq  37550  jm2.23  37563  jm2.26lem3  37568  jm2.27dlem2  37577  monoords  39511  fmul01lt1lem1  39816  fmul01lt1lem2  39817  sumnnodd  39862  limsupubuzlem  39944  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  stoweidlem3  40220  stoweidlem11  40228  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  wallispi2  40290  dirkeritg  40319  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem52  40375  fourierdlem54  40377  fourierdlem79  40402  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  elaa2lem  40450  etransclem3  40454  etransclem4  40455  etransclem7  40458  etransclem10  40461  etransclem23  40474  etransclem24  40475  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem46  40497  caratheodorylem1  40740  iccpartgt  41363