Theorem eluzelz 9427

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzelz	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 9424	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 998	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2125   class class class wbr 3961  ‘cfv 5163   ≤ cle 7892  ℤcz 9146  ℤ_≥cuz 9418

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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-pow 4130  ax-pr 4164  ax-cnex 7802  ax-resscn 7803

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-rex 2438  df-rab 2441  df-v 2711  df-sbc 2934  df-un 3102  df-in 3104  df-ss 3111  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-br 3962  df-opab 4022  df-mpt 4023  df-id 4248  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-fv 5171  df-ov 5817  df-neg 8028  df-z 9147  df-uz 9419

This theorem is referenced by:  eluzelre  9428  uztrn  9434  uzneg  9436  uzssz  9437  uzss  9438  eluzp1l  9442  eluzaddi  9444  eluzsubi  9445  eluzadd  9446  eluzsub  9447  uzm1  9448  uzin  9450  uzind4  9478  uz2mulcl  9497  elfz5  9898  elfzel2  9904  elfzelz  9906  eluzfz2  9912  peano2fzr  9917  fzsplit2  9930  fzopth  9941  fzsuc  9949  elfzp1  9952  fzdifsuc  9961  uzsplit  9972  uzdisj  9973  fzm1  9980  fzneuz  9981  uznfz  9983  nn0disj  10015  elfzo3  10040  fzoss2  10049  fzouzsplit  10056  eluzgtdifelfzo  10074  fzosplitsnm1  10086  fzofzp1b  10105  elfzonelfzo  10107  fzosplitsn  10110  fzisfzounsn  10113  mulp1mod1  10242  m1modge3gt1  10248  frec2uzltd  10280  frecfzen2  10304  uzennn  10313  uzsinds  10319  seq3fveq2  10346  seq3feq2  10347  seq3shft2  10350  monoord  10353  monoord2  10354  ser3mono  10355  seq3split  10356  iseqf1olemjpcl  10372  iseqf1olemqpcl  10373  seq3f1olemqsumk  10376  seq3f1olemp  10379  seq3f1oleml  10380  seq3f1o  10381  seq3id  10385  seq3z  10388  fser0const  10393  leexp2a  10450  expnlbnd2  10521  hashfz  10672  hashfzo  10673  hashfzp1  10675  seq3coll  10690  seq3shft  10715  rexuz3  10867  r19.2uz  10870  cau4  10993  caubnd2  10994  clim  11155  climshft2  11180  climaddc1  11203  climmulc2  11205  climsubc1  11206  climsubc2  11207  clim2ser  11211  clim2ser2  11212  iserex  11213  climlec2  11215  climub  11218  climcau  11221  climcaucn  11225  serf0  11226  sumrbdclem  11251  fsum3cvg  11252  summodclem2a  11255  zsumdc  11258  fsum3  11261  fisumss  11266  fsum3cvg2  11268  fsum3ser  11271  fsumcl2lem  11272  fsumadd  11280  fsumm1  11290  fzosump1  11291  fsum1p  11292  fsump1  11294  fsummulc2  11322  telfsumo  11340  fsumparts  11344  iserabs  11349  binomlem  11357  isumshft  11364  isumsplit  11365  isumrpcl  11368  divcnv  11371  trireciplem  11374  geosergap  11380  geolim2  11386  cvgratnnlemseq  11400  cvgratnnlemabsle  11401  cvgratnnlemsumlt  11402  cvgratnnlemrate  11404  cvgratz  11406  cvgratgt0  11407  mertenslemi1  11409  clim2divap  11414  prodrbdclem  11445  fproddccvg  11446  prodmodclem3  11449  prodmodclem2a  11450  zproddc  11453  fprodntrivap  11458  fprodssdc  11464  fprodm1  11472  fprod1p  11473  fprodp1  11474  fprodabs  11490  fprodeq0  11491  efgt1p2  11569  zsupcllemstep  11805  infssuzex  11809  dvdsbnd  11812  ncoprmgcdne1b  11937  isprm3  11966  prmind2  11968  nprm  11971  dvdsprm  11984  exprmfct  11985  phibndlem  12059  phibnd  12060  dfphi2  12063  hashdvds  12064  relogbval  13207  relogbzcl  13208  nnlogbexp  13215  logblt  13218  logbgcd1irr  13223  supfz  13580