Theorem eluz2 12971

Description: Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show 𝑀 ∈ ℤ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
eluz2	⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Proof of Theorem eluz2

Step	Hyp	Ref	Expression
1		eluzel2 12970	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1154	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12969	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 538	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 282	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1111	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 381	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6538   ≤ cle 11344  ℤcz 12693  ℤ_≥cuz 12965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  eluzmn  12972  eluzuzle  12974  eluzelz  12975  eluzle  12978  uztrn  12983  eluzp1p1  12993  eluzadd  12994  eluzsub  12995  subeluzsub  12998  uzm1  12999  uznn0sub  13000  1eluzge0  13007  2eluzge1  13009  5eluz3  13010  uz3m2nn  13021  raluz2  13024  rexuz2  13026  peano2uz  13028  nn0pzuz  13032  uzind4  13033  uzinfi  13055  zsupss  13064  nn01to3  13068  nn0ge2m1nnALT  13069  elfzuzb  13650  uzsubsubfz  13680  ssfzunsn  13704  ige2m1fz  13751  fz0to4untppr  13764  fz0to5un2tp  13765  4fvwrd4  13782  elfzo2  13796  elfzouz2  13809  fzossrbm1  13823  fzossfzop1  13878  ssfzo12bi  13896  fzoopth  13897  elfzonelfzo  13904  elfzomelpfzo  13907  fzosplitprm1  13913  fzostep1  13921  fzind2  13923  flword2  13953  fldiv4p1lem1div2  13975  uzsup  14003  modaddmodup  14077  fzsdom2  14573  ccatdmss  14727  swrdsbslen  14814  swrdspsleq  14815  pfxtrcfv0  14843  pfxtrcfvl  14846  pfxccatin12lem2a  14876  cshwidxmod  14954  rexuzre  15520  limsupgre  15648  rlimclim1  15712  rlimclim  15713  climrlim2  15714  isercolllem1  15832  isercoll  15835  climcndslem1  16018  fallfacval4  16209  oddge22np1  16519  nn0o  16553  bitsmod  16606  smueqlem  16660  dvdsnprmd  16865  2mulprm  16868  oddprmgt2  16875  oddprmge3  16876  ge2nprmge4  16877  modprm0  16983  prm23ge5  16993  vdwlem9  17167  prmgaplem3  17231  prmgaplem5  17233  prmgaplem6  17234  prmgaplem7  17235  strleun  17335  setsstruct  17354  chnub  18796  fislw  19839  efgsp1  19951  efgredleme  19957  lt6abl  20109  telgsumfzs  20203  ablfac1eu  20289  znidomb  21867  chfacfscmul0  23176  chfacfscmulfsupp  23177  chfacfpmmul0  23180  chfacfpmmulfsupp  23181  dvfsumlem1  26346  dvfsumlem3  26348  plyaddlem1  26532  coeidlem  26556  2logb9irr  27123  ppisval  27431  chtdif  27485  ppidif  27490  ppiublem1  27529  ppiub  27531  chtub  27539  lgsdilem2  27660  gausslemma2dlem2  27694  gausslemma2dlem4  27696  gausslemma2dlem5  27698  gausslemma2dlem6  27699  lgsquadlem1  27707  lgsquadlem3  27709  2lgslem1  27721  chebbnd1lem1  27796  chebbnd1lem2  27797  chebbnd1lem3  27798  dchrisumlem2  27817  dchrvmasumiflem1  27828  mulog2sumlem2  27862  logdivbnd  27883  pntlemg  27925  pntlemq  27928  pntlemf  27932  fltoprmlem2  27994  axlowdim  29539  pthdlem1  30352  crctcshwlkn0lem3  30401  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshwlkn0lem6  30404  wwlksm1edg  30470  wwlksnred  30481  clwlkclwwlklem2fv1  30586  clwlkclwwlklem2  30591  clwwisshclwwslem  30605  clwwlkinwwlk  30631  clwwlkf  30638  clwwlkext2edg  30647  wwlksubclwwlk  30649  frgrreggt1  30994  ssnnssfz  33379  cycpmco2lem6  33692  ballotlemsdom  35144  ballotlemsel1i  35145  ballotlemfrceq  35161  signstfvc  35203  signstfveq0  35206  prodfzo03  35232  erdszelem8  35963  climuzcnv  36436  poimirlem6  38544  fdc  38679  sticksstones12  43208  eluzp1  43364  fimgmcyc  43598  eldioph2lem1  43770  hbt  44131  ssinc  46101  ssdec  46102  monoords  46312  fzdifsuc2  46325  eluzd  46418  fmul01lt1lem2  46596  sumnnodd  46641  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnmul  46952  dvnprodlem2  46956  itgspltprt  46988  stoweidlem11  47020  stoweidlem26  47035  wallispilem4  47077  fourierdlem12  47128  fourierdlem20  47136  fourierdlem41  47157  fourierdlem50  47165  fourierdlem54  47169  fourierdlem79  47194  fourierdlem102  47217  fourierdlem111  47226  fourierdlem114  47229  etransclem23  47266  etransclem48  47291  caratheodorylem1  47535  smfmullem4  47803  eluzge0nn0  48381  ssfz12  48383  elfzlble  48389  fzopredsuc  48393  ceilhalfelfzo1  48403  addmodne  48419  m1modnep2mod  48427  m1modmmod  48433  modm2nep1  48441  modp2nep1  48442  modm1nep2  48443  modm1nem2  48444  modm1p1ne  48445  2timesltsqm1  48448  muldvdsfacgt  48455  muldvdsfacm1  48456  iccpartipre  48502  iccpartiltu  48503  iccpartgt  48508  fmtnoge3  48614  odz2prm2pw  48647  fmtnoprmfac2lem1  48650  fmtno4prmfac  48656  31prm  48681  lighneallem4b  48693  nprmdvdsfacm1lem2  48705  nprmdvdsfacm1lem3  48706  nprmdvdsfacm1lem4  48707  nprmdvdsfacm1  48708  ppivalnnnprmge6  48710  341fppr2  48831  9fppr8  48834  fpprel2  48838  nfermltl8rev  48839  nfermltl2rev  48840  gbegt5  48858  gbowgt5  48859  sbgoldbm  48881  mogoldbb  48882  sbgoldbo  48884  nnsum3primesle9  48891  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  evengpop3  48895  evengpoap3  48896  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  bgoldbtbndlem3  48904  tgblthelfgott  48912  gpgusgralem  49153  gpgedgvtx1  49159  gpg5nbgrvtx13starlem2  49169  gpg3nbgrvtx0  49173  gpg3nbgrvtx0ALT  49174  gpg5nbgr3star  49178  gpg3kgrtriexlem3  49182  gpg3kgrtriexlem6  49185  gpg5edgnedg  49227  cznnring  49358  ssnn0ssfz  49460  elfzolborelfzop1  49630  rege1logbzge0  49670  fllog2  49679  nnolog2flm1  49701  dignn0ldlem  49713