Theorem elfzle1 13700

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  ‘cfv 6566  (class class class)co 7451   ≤ cle 11383  ℤ_≥cuz 13005  ...cfz 13679

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-neg 11583  df-z 12734  df-uz 13006  df-fz 13680

This theorem is used by:  elfz1eq  13708  fzdisj  13725  elfznn  13727  ssfzunsnext  13743  fznatpl1  13752  fznn0sub2  13809  fz0fzdiffz0  13811  difelfznle  13816  seqf1olem1  14224  seqf1olem2  14225  bcval4  14492  seqcoll  14650  seqcoll2  14651  fsum0diaglem  15986  mertenslem1  16097  fprodntriv  16153  fallfacval4  16253  divalglem6  16612  hashdvds  16996  prmdiveq  17007  4sqlem11  17177  4sqlem12  17178  dvfsumlem3  26403  birthdaylem3  27338  ppiltx  27561  ppiub  27588  lgsdilem2  27717  lgsquadlem1  27764  chtppilimlem1  27857  dchrvmasumiflem1  27885  pntrlog2bndlem5  27965  pntpbnd1  27970  pntpbnd2  27971  pntlemh  27983  pntlemj  27987  ostth2lem2  28018  axlowdimlem16  29592  fzto1st1  33762  smattr  34542  smatbl  34543  smatbr  34544  ballotlem2  35232  ballotlemsdom  35255  ballotlemsima  35259  ballotlemfrcn0  35273  ballotlem1ri  35278  breprexplemc  35372  subfacp1lem1  36152  subfacp1lem5  36157  inffz  36710  poimirlem2  38808  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem11  38817  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  poimirlem24  38830  poimirlem29  38835  poimirlem31  38837  poimirlem32  38838  mblfinlem2  38844  fdc  38945  aks6d1c1  43432  aks6d1c5lem1  43452  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  bcled  43494  bcle2d  43495  unitscyglem2  43512  unitscyglem4  43514  irrapxlem3  44097  acongrep  44253  fzmaxdif  44254  acongeq  44256  jm2.23  44269  jm2.26lem3  44274  jm2.27dlem2  44283  monoords  46586  fmul01lt1lem1  46869  fmul01lt1lem2  46870  sumnnodd  46915  limsupubuzlem  46995  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  iblspltprt  47256  itgspltprt  47262  stoweidlem3  47286  stoweidlem11  47294  stoweidlem20  47303  stoweidlem26  47309  stoweidlem34  47317  wallispi2  47356  dirkeritg  47385  fourierdlem11  47401  fourierdlem12  47402  fourierdlem15  47405  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem52  47441  fourierdlem54  47443  fourierdlem79  47468  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  elaa2lem  47516  etransclem3  47520  etransclem4  47521  etransclem7  47524  etransclem10  47527  etransclem23  47540  etransclem24  47541  etransclem31  47548  etransclem32  47549  etransclem35  47552  etransclem41  47558  etransclem46  47563  caratheodorylem1  47809  iccpartgt  48782