Theorem elfzel2 13254

Description: Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzel2	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)

Proof of Theorem elfzel2

Step	Hyp	Ref	Expression
1		elfzuz3 13253	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
2		eluzelz 12592	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6433  (class class class)co 7275  ℤcz 12319  ℤ_≥cuz 12582  ...cfz 13239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-neg 11208  df-z 12320  df-uz 12583  df-fz 13240

This theorem is referenced by:  elfz1eq  13267  fzdisj  13283  fzssp1  13299  fzp1disj  13315  fzrev2i  13321  fzrev3  13322  elfz1b  13325  fznuz  13338  fznn0sub2  13363  elfzmlbm  13366  difelfznle  13370  nn0disj  13372  fz1fzo0m1  13435  fzofzp1b  13485  bcm1k  14029  bcp1nk  14031  pfxccatin12lem2  14444  spllen  14467  fsum0diag2  15495  fallfacval3  15722  fallfacval4  15753  psgnunilem2  19103  pntpbnd1  26734  crctcshwlkn0  28186  fzm1ne1  31110  swrdrevpfx  33078  swrdwlk  33088  elfzfzo  42815  sumnnodd  43171  dvnmul  43484  dvnprodlem1  43487  dvnprodlem2  43488  stoweidlem34  43575  fourierdlem11  43659  fourierdlem12  43660  fourierdlem15  43663  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem54  43701  fourierdlem79  43726  fourierdlem102  43749  fourierdlem114  43761  etransclem23  43798  etransclem35  43810  iundjiun  43998  2elfz2melfz  44810  elfzelfzlble  44813  iccpartiltu  44874  iccpartgt  44879