Theorem elfzle2 9988

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 3990  ‘cfv 5200  (class class class)co 5857   ≤ cle 7959  ℤ_≥cuz 9491  ...cfz 9969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-setind 4522  ax-cnex 7869  ax-resscn 7870

This theorem depends on definitions:  df-bi 116  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-ral 2454  df-rex 2455  df-rab 2458  df-v 2733  df-sbc 2957  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-fv 5208  df-ov 5860  df-oprab 5861  df-mpo 5862  df-neg 8097  df-z 9217  df-uz 9492  df-fz 9970

This theorem is referenced by:  elfz1eq  9995  fzdisj  10012  fznatpl1  10036  fzp1disj  10040  uzdisj  10053  fzneuz  10061  fznuz  10062  elfzmlbm  10091  difelfznle  10095  nn0disj  10098  iseqf1olemqcl  10446  iseqf1olemnab  10448  iseqf1olemab  10449  iseqf1olemqk  10454  iseqf1olemfvp  10457  seq3f1olemqsumkj  10458  seq3f1olemqsumk  10459  seq3f1olemqsum  10460  seq3f1oleml  10463  seq3f1o  10464  bcval4  10690  bcp1nk  10700  zfz1isolemiso  10778  seq3coll  10781  summodclem3  11347  summodclem2a  11348  fsum3  11354  fsumcl2lem  11365  fsum0diaglem  11407  mertenslemi1  11502  prodmodclem3  11542  prodmodclem2a  11543  fprodseq  11550  fzm1ndvds  11820  prmind2  12078  prmdvdsfz  12097  isprm5lem  12099  hashdvds  12179  eulerthlemrprm  12187  eulerthlema  12188  prmdiveq  12194  ennnfonelemim  12383  ctinfomlemom  12386  lgsval2lem  13790  supfz  14185