Theorem elfzle2 10187

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

Assertion

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

Proof of Theorem elfzle2

Step	Hyp	Ref	Expression
1		elfzuz3 10181	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
2		eluzle 9697	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ≤ 𝑁)
3	1, 2	syl 14	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2178   class class class wbr 4060  ‘cfv 5291  (class class class)co 5969   ≤ cle 8145  ℤ_≥cuz 9685  ...cfz 10167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4179  ax-pow 4235  ax-pr 4270  ax-setind 4604  ax-cnex 8053  ax-resscn 8054

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2779  df-sbc 3007  df-dif 3177  df-un 3179  df-in 3181  df-ss 3188  df-pw 3629  df-sn 3650  df-pr 3651  df-op 3653  df-uni 3866  df-br 4061  df-opab 4123  df-mpt 4124  df-id 4359  df-xp 4700  df-rel 4701  df-cnv 4702  df-co 4703  df-dm 4704  df-rn 4705  df-res 4706  df-ima 4707  df-iota 5252  df-fun 5293  df-fn 5294  df-f 5295  df-fv 5299  df-ov 5972  df-oprab 5973  df-mpo 5974  df-neg 8283  df-z 9410  df-uz 9686  df-fz 10168

This theorem is referenced by:  elfz1eq  10194  fzdisj  10211  fznatpl1  10235  fzp1disj  10239  uzdisj  10252  fzneuz  10260  fznuz  10261  elfzmlbm  10290  difelfznle  10294  nn0disj  10297  iseqf1olemqcl  10683  iseqf1olemnab  10685  iseqf1olemab  10686  iseqf1olemqk  10691  iseqf1olemfvp  10694  seq3f1olemqsumkj  10695  seq3f1olemqsumk  10696  seq3f1olemqsum  10697  seq3f1oleml  10700  seq3f1o  10701  seqf1oglem1  10703  seqf1oglem2  10704  seqfeq4g  10715  bcval4  10936  bcp1nk  10946  zfz1isolemiso  11023  seq3coll  11026  summodclem3  11852  summodclem2a  11853  fsum3  11859  fsumcl2lem  11870  fsum0diaglem  11912  mertenslemi1  12007  prodmodclem3  12047  prodmodclem2a  12048  fprodseq  12055  fzm1ndvds  12328  prmind2  12603  prmdvdsfz  12622  isprm5lem  12624  hashdvds  12704  eulerthlemrprm  12712  eulerthlema  12713  prmdiveq  12719  4sqlem11  12885  4sqlem12  12886  ennnfonelemim  12956  ctinfomlemom  12959  gsumfzfsumlemm  14510  wilthlem1  15613  lgsval2lem  15648  lgseisenlem1  15708  lgseisenlem2  15709  lgseisenlem3  15710  lgsquadlem1  15715  lgsquadlem2  15716  2lgslem1a  15726  supfz  16320