Theorem eluz2 12867

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 12866	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1152	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12865	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 537	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 282	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1109	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 381	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6537   ≤ cle 11243  ℤcz 12590  ℤ_≥cuz 12861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-neg 11443  df-z 12591  df-uz 12862

This theorem is referenced by:  eluzmn  12868  eluzuzle  12870  eluzelz  12871  eluzle  12874  uztrn  12879  eluzp1p1  12889  eluzadd  12890  eluzsub  12891  subeluzsub  12894  uzm1  12895  uznn0sub  12896  1eluzge0  12903  2eluzge1  12905  5eluz3  12906  uz3m2nn  12917  raluz2  12920  rexuz2  12922  peano2uz  12924  nn0pzuz  12928  uzind4  12929  uzinfi  12951  zsupss  12960  nn01to3  12964  nn0ge2m1nnALT  12965  elfzuzb  13545  uzsubsubfz  13573  ssfzunsn  13597  ige2m1fz  13644  fz0to4untppr  13657  fz0to5un2tp  13658  4fvwrd4  13675  elfzo2  13689  elfzouz2  13702  fzossrbm1  13716  fzossfzop1  13771  ssfzo12bi  13789  fzoopth  13790  elfzonelfzo  13797  elfzomelpfzo  13800  fzosplitprm1  13806  fzostep1  13814  fzind2  13816  flword2  13845  fldiv4p1lem1div2  13867  uzsup  13895  modaddmodup  13969  fzsdom2  14464  ccatdmss  14618  swrdsbslen  14701  swrdspsleq  14702  pfxtrcfv0  14730  pfxtrcfvl  14733  pfxccatin12lem2a  14763  cshwidxmod  14839  rexuzre  15403  limsupgre  15531  rlimclim1  15595  rlimclim  15596  climrlim2  15597  isercolllem1  15715  isercoll  15718  climcndslem1  15902  fallfacval4  16096  oddge22np1  16406  nn0o  16440  bitsmod  16493  smueqlem  16547  dvdsnprmd  16747  2mulprm  16750  oddprmgt2  16757  oddprmge3  16758  ge2nprmge4  16759  modprm0  16864  prm23ge5  16874  vdwlem9  17048  prmgaplem3  17112  prmgaplem5  17114  prmgaplem6  17115  prmgaplem7  17116  strleun  17216  setsstruct  17235  chnub  18677  fislw  19694  efgsp1  19806  efgredleme  19812  lt6abl  19964  telgsumfzs  20058  ablfac1eu  20144  znidomb  21679  chfacfscmul0  22983  chfacfscmulfsupp  22984  chfacfpmmul0  22987  chfacfpmmulfsupp  22988  dvfsumlem1  26153  dvfsumlem3  26155  plyaddlem1  26338  coeidlem  26362  2logb9irr  26925  ppisval  27233  chtdif  27287  ppidif  27292  ppiublem1  27331  ppiub  27333  chtub  27341  lgsdilem2  27462  gausslemma2dlem2  27496  gausslemma2dlem4  27498  gausslemma2dlem5  27500  gausslemma2dlem6  27501  lgsquadlem1  27509  lgsquadlem3  27511  2lgslem1  27523  chebbnd1lem1  27598  chebbnd1lem2  27599  chebbnd1lem3  27600  dchrisumlem2  27619  dchrvmasumiflem1  27630  mulog2sumlem2  27664  logdivbnd  27685  pntlemg  27727  pntlemq  27730  pntlemf  27734  axlowdim  29251  pthdlem1  30055  crctcshwlkn0lem3  30101  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  wwlksm1edg  30170  wwlksnred  30181  clwlkclwwlklem2fv1  30286  clwlkclwwlklem2  30291  clwwisshclwwslem  30305  clwwlkinwwlk  30331  clwwlkf  30338  clwwlkext2edg  30347  wwlksubclwwlk  30349  frgrreggt1  30684  ssnnssfz  33072  cycpmco2lem6  33391  ballotlemsdom  34846  ballotlemsel1i  34847  ballotlemfrceq  34863  signstfvc  34905  signstfveq0  34908  prodfzo03  34934  erdszelem8  35588  climuzcnv  36061  poimirlem6  38164  fdc  38283  sticksstones12  42814  eluzp1  42957  fimgmcyc  43193  eldioph2lem1  43382  hbt  43748  ssinc  45696  ssdec  45697  monoords  45907  fzdifsuc2  45920  eluzd  46014  fmul01lt1lem2  46192  sumnnodd  46237  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnmul  46548  dvnprodlem2  46552  itgspltprt  46584  stoweidlem11  46616  stoweidlem26  46631  wallispilem4  46673  fourierdlem12  46724  fourierdlem20  46732  fourierdlem41  46753  fourierdlem50  46761  fourierdlem54  46765  fourierdlem79  46790  fourierdlem102  46813  fourierdlem111  46822  fourierdlem114  46825  etransclem23  46862  etransclem48  46887  caratheodorylem1  47131  smfmullem4  47399  eluzge0nn0  47937  ssfz12  47939  elfzlble  47945  fzopredsuc  47949  ceilhalfelfzo1  47959  addmodne  47975  m1modnep2mod  47983  m1modmmod  47989  modm2nep1  47997  modp2nep1  47998  modm1nep2  47999  modm1nem2  48000  modm1p1ne  48001  2timesltsqm1  48004  muldvdsfacgt  48011  muldvdsfacm1  48012  iccpartipre  48058  iccpartiltu  48059  iccpartgt  48064  fmtnoge3  48170  odz2prm2pw  48203  fmtnoprmfac2lem1  48206  fmtno4prmfac  48212  31prm  48237  lighneallem4b  48249  nprmdvdsfacm1lem2  48261  nprmdvdsfacm1lem3  48262  nprmdvdsfacm1lem4  48263  nprmdvdsfacm1  48264  ppivalnnnprmge6  48266  341fppr2  48387  9fppr8  48390  fpprel2  48394  nfermltl8rev  48395  nfermltl2rev  48396  gbegt5  48414  gbowgt5  48415  sbgoldbm  48437  mogoldbb  48438  sbgoldbo  48440  nnsum3primesle9  48447  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  evengpop3  48451  evengpoap3  48452  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  bgoldbtbndlem3  48460  tgblthelfgott  48468  gpgusgralem  48709  gpgedgvtx1  48715  gpg5nbgrvtx13starlem2  48725  gpg3nbgrvtx0  48729  gpg3nbgrvtx0ALT  48730  gpg5nbgr3star  48734  gpg3kgrtriexlem3  48738  gpg3kgrtriexlem6  48741  gpg5edgnedg  48783  cznnring  48915  ssnn0ssfz  49013  elfzolborelfzop1  49183  rege1logbzge0  49223  fllog2  49232  nnolog2flm1  49254  dignn0ldlem  49266