Theorem eluz2 12874

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 12873	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1133	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12872	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 527	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 278	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1092	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 288	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 377	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   ∈ wcel 2099   class class class wbr 5145  ‘cfv 6546   ≤ cle 11290  ℤcz 12604  ℤ_≥cuz 12868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425  ax-cnex 11205  ax-resscn 11206

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7419  df-neg 11488  df-z 12605  df-uz 12869

This theorem is referenced by:  eluzmn  12875  eluzuzle  12877  eluzelz  12878  eluzle  12881  uztrn  12886  eluzp1p1  12896  eluzadd  12897  eluzsub  12898  subeluzsub  12905  uzm1  12906  uznn0sub  12907  uz3m2nn  12921  1eluzge0  12922  2eluzge1  12924  raluz2  12927  rexuz2  12929  peano2uz  12931  nn0pzuz  12935  uzind4  12936  uzinfi  12958  zsupss  12967  nn01to3  12971  nn0ge2m1nnALT  12972  elfzuzb  13543  uzsubsubfz  13571  ssfzunsn  13595  ige2m1fz  13639  4fvwrd4  13669  elfzo2  13683  elfzouz2  13695  fzossrbm1  13709  fzossfzop1  13758  ssfzo12bi  13775  fzoopth  13776  elfzonelfzo  13783  elfzomelpfzo  13785  fzosplitprm1  13791  fzostep1  13797  fzind2  13799  flword2  13827  fldiv4p1lem1div2  13849  uzsup  13877  modaddmodup  13948  fzsdom2  14440  swrdsbslen  14667  swrdspsleq  14668  pfxtrcfv0  14697  pfxtrcfvl  14700  pfxccatin12lem2a  14730  cshwidxmod  14806  rexuzre  15352  limsupgre  15478  rlimclim1  15542  rlimclim  15543  climrlim2  15544  isercolllem1  15664  isercoll  15667  climcndslem1  15848  fallfacval4  16040  oddge22np1  16346  nn0o  16380  bitsmod  16431  smueqlem  16485  dvdsnprmd  16686  2mulprm  16689  oddprmgt2  16695  oddprmge3  16696  ge2nprmge4  16697  modprm0  16802  prm23ge5  16812  vdwlem9  16986  prmgaplem3  17050  prmgaplem5  17052  prmgaplem6  17053  prmgaplem7  17054  strleun  17154  setsstruct  17173  fislw  19619  efgsp1  19731  efgredleme  19737  lt6abl  19889  telgsumfzs  19983  ablfac1eu  20069  znidomb  21555  chfacfscmul0  22848  chfacfscmulfsupp  22849  chfacfpmmul0  22852  chfacfpmmulfsupp  22853  dvfsumlem1  26048  dvfsumlem3  26051  plyaddlem1  26237  coeidlem  26261  2logb9irr  26820  ppisval  27129  chtdif  27183  ppidif  27188  ppiublem1  27228  ppiub  27230  chtub  27238  lgsdilem2  27359  gausslemma2dlem2  27393  gausslemma2dlem4  27395  gausslemma2dlem5  27397  gausslemma2dlem6  27398  lgsquadlem1  27406  lgsquadlem3  27408  2lgslem1  27420  chebbnd1lem1  27495  chebbnd1lem2  27496  chebbnd1lem3  27497  dchrisumlem2  27516  dchrvmasumiflem1  27527  mulog2sumlem2  27561  logdivbnd  27582  pntlemg  27624  pntlemq  27627  pntlemf  27631  axlowdim  28892  pthdlem1  29700  crctcshwlkn0lem3  29743  crctcshwlkn0lem4  29744  crctcshwlkn0lem5  29745  crctcshwlkn0lem6  29746  wwlksm1edg  29812  wwlksnred  29823  clwlkclwwlklem2fv1  29925  clwlkclwwlklem2  29930  clwwisshclwwslem  29944  clwwlkinwwlk  29970  clwwlkf  29977  clwwlkext2edg  29986  wwlksubclwwlk  29988  frgrreggt1  30323  ssnnssfz  32692  ccatdmss  32816  chnub  32884  cycpmco2lem6  33013  ballotlemsdom  34358  ballotlemsel1i  34359  ballotlemfrceq  34375  signstfvc  34433  signstfveq0  34436  prodfzo03  34462  erdszelem8  35039  climuzcnv  35512  poimirlem6  37340  fdc  37459  sticksstones12  41870  eluzp1  42034  fimgmcyc  42224  eldioph2lem1  42454  hbt  42828  ssinc  44725  ssdec  44726  monoords  44948  fzdifsuc2  44961  eluzd  45060  fmul01lt1lem2  45242  sumnnodd  45287  ioodvbdlimc1lem2  45589  ioodvbdlimc2lem  45591  dvnmul  45600  dvnprodlem2  45604  itgspltprt  45636  stoweidlem11  45668  stoweidlem26  45683  wallispilem4  45725  fourierdlem12  45776  fourierdlem20  45784  fourierdlem41  45805  fourierdlem48  45811  fourierdlem49  45812  fourierdlem50  45813  fourierdlem54  45817  fourierdlem79  45842  fourierdlem102  45865  fourierdlem111  45874  fourierdlem114  45877  etransclem23  45914  etransclem48  45939  caratheodorylem1  46183  smfmullem4  46451  eluzge0nn0  46961  ssfz12  46963  elfzlble  46969  fzopredsuc  46972  iccpartipre  47029  iccpartiltu  47030  iccpartgt  47035  fmtnoge3  47138  odz2prm2pw  47171  fmtnoprmfac2lem1  47174  fmtno4prmfac  47180  31prm  47205  lighneallem4b  47217  341fppr2  47342  9fppr8  47345  fpprel2  47349  nfermltl8rev  47350  nfermltl2rev  47351  gbegt5  47369  gbowgt5  47370  sbgoldbm  47392  mogoldbb  47393  sbgoldbo  47395  nnsum3primesle9  47402  nnsum4primesodd  47404  nnsum4primesoddALTV  47405  evengpop3  47406  evengpoap3  47407  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  wtgoldbnnsum4prm  47410  bgoldbnnsum3prm  47412  bgoldbtbndlem3  47415  tgblthelfgott  47423  cznnring  47675  ssnn0ssfz  47764  elfzolborelfzop1  47938  m1modmmod  47945  rege1logbzge0  47983  fllog2  47992  nnolog2flm1  48014  dignn0ldlem  48026