Theorem elfzel2 13467

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 13466	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
2		eluzelz 12789	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  ℤcz 12515  ℤ_≥cuz 12779  ...cfz 13452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-neg 11371  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  elfz1eq  13480  fzdisj  13496  fzssp1  13512  fzp1disj  13528  fzrev2i  13534  fzrev3  13535  elfz1b  13538  fznuz  13554  fznn0sub2  13580  elfzmlbm  13583  difelfznle  13587  nn0disj  13589  fz1fzo0m1  13656  fzofzp1b  13711  bcm1k  14268  bcp1nk  14270  pfxccatin12lem2  14684  spllen  14707  fsum0diag2  15736  fallfacval3  15968  fallfacval4  15999  psgnunilem2  19461  pntpbnd1  27563  crctcshwlkn0  29904  fzm1ne1  32876  swrdrevpfx  35315  swrdwlk  35325  elfzfzo  45728  sumnnodd  46078  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  stoweidlem34  46480  fourierdlem11  46564  fourierdlem12  46565  fourierdlem15  46568  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem54  46606  fourierdlem79  46631  fourierdlem102  46654  fourierdlem114  46666  etransclem23  46703  etransclem35  46715  iundjiun  46906  2elfz2melfz  47778  elfzelfzlble  47781  iccpartiltu  47894  iccpartgt  47899