Theorem eluzelz 9531

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 9528	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1013	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2148   class class class wbr 4001  ‘cfv 5213   ≤ cle 7987  ℤcz 9247  ℤ_≥cuz 9522

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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-cnex 7897  ax-resscn 7898

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-opab 4063  df-mpt 4064  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-iota 5175  df-fun 5215  df-fn 5216  df-f 5217  df-fv 5221  df-ov 5873  df-neg 8125  df-z 9248  df-uz 9523

This theorem is referenced by:  eluzelre  9532  uztrn  9538  uzneg  9540  uzssz  9541  uzss  9542  eluzp1l  9546  eluzaddi  9548  eluzsubi  9549  eluzadd  9550  eluzsub  9551  uzm1  9552  uzin  9554  uzind4  9582  uz2mulcl  9602  elfz5  10010  elfzel2  10016  elfzelz  10018  eluzfz2  10025  peano2fzr  10030  fzsplit2  10043  fzopth  10054  fzsuc  10062  elfzp1  10065  fzdifsuc  10074  uzsplit  10085  uzdisj  10086  fzm1  10093  fzneuz  10094  uznfz  10096  nn0disj  10131  elfzo3  10156  fzoss2  10165  fzouzsplit  10172  eluzgtdifelfzo  10190  fzosplitsnm1  10202  fzofzp1b  10221  elfzonelfzo  10223  fzosplitsn  10226  fzisfzounsn  10229  mulp1mod1  10358  m1modge3gt1  10364  frec2uzltd  10396  frecfzen2  10420  uzennn  10429  uzsinds  10435  seq3fveq2  10462  seq3feq2  10463  seq3shft2  10466  monoord  10469  monoord2  10470  ser3mono  10471  seq3split  10472  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  seq3f1olemqsumk  10492  seq3f1olemp  10495  seq3f1oleml  10496  seq3f1o  10497  seq3id  10501  seq3z  10504  fser0const  10509  leexp2a  10566  expnlbnd2  10638  hashfz  10792  hashfzo  10793  hashfzp1  10795  seq3coll  10813  seq3shft  10838  rexuz3  10990  r19.2uz  10993  cau4  11116  caubnd2  11117  clim  11280  climshft2  11305  climaddc1  11328  climmulc2  11330  climsubc1  11331  climsubc2  11332  clim2ser  11336  clim2ser2  11337  iserex  11338  climlec2  11340  climub  11343  climcau  11346  climcaucn  11350  serf0  11351  sumrbdclem  11376  fsum3cvg  11377  summodclem2a  11380  zsumdc  11383  fsum3  11386  fisumss  11391  fsum3cvg2  11393  fsum3ser  11396  fsumcl2lem  11397  fsumadd  11405  fsumm1  11415  fzosump1  11416  fsum1p  11417  fsump1  11419  fsummulc2  11447  telfsumo  11465  fsumparts  11469  iserabs  11474  binomlem  11482  isumshft  11489  isumsplit  11490  isumrpcl  11493  divcnv  11496  trireciplem  11499  geosergap  11505  geolim2  11511  cvgratnnlemseq  11525  cvgratnnlemabsle  11526  cvgratnnlemsumlt  11527  cvgratnnlemrate  11529  cvgratz  11531  cvgratgt0  11532  mertenslemi1  11534  clim2divap  11539  prodrbdclem  11570  fproddccvg  11571  prodmodclem3  11574  prodmodclem2a  11575  zproddc  11578  fprodntrivap  11583  fprodssdc  11589  fprodm1  11597  fprod1p  11598  fprodp1  11599  fprodabs  11615  fprodeq0  11616  efgt1p2  11694  modm1div  11798  zsupcllemstep  11936  infssuzex  11940  suprzubdc  11943  dvdsbnd  11947  uzwodc  12028  ncoprmgcdne1b  12079  isprm3  12108  prmind2  12110  nprm  12113  dvdsprm  12127  exprmfct  12128  isprm5lem  12131  isprm5  12132  phibndlem  12206  phibnd  12207  dfphi2  12210  hashdvds  12211  pclemdc  12278  pcaddlem  12328  pcmptdvds  12333  pcfac  12338  expnprm  12341  relogbval  14151  relogbzcl  14152  nnlogbexp  14159  logblt  14162  logbgcd1irr  14167  lgsne0  14221  2sqlem6  14238  2sqlem8a  14240  2sqlem8  14241  supfz  14589