Theorem eluz2 12775

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 12774	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12773	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 528	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 279	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1094	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 289	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 378	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499   ≤ cle 11185  ℤcz 12505  ℤ_≥cuz 12769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506  df-uz 12770

This theorem is referenced by:  eluzmn  12776  eluzuzle  12778  eluzelz  12779  eluzle  12782  uztrn  12787  eluzp1p1  12797  eluzadd  12798  eluzsub  12799  subeluzsub  12806  uzm1  12807  uznn0sub  12808  1eluzge0  12815  2eluzge1  12817  5eluz3  12818  uz3m2nn  12829  raluz2  12832  rexuz2  12834  peano2uz  12836  nn0pzuz  12840  uzind4  12841  uzinfi  12863  zsupss  12872  nn01to3  12876  nn0ge2m1nnALT  12877  elfzuzb  13455  uzsubsubfz  13483  ssfzunsn  13507  ige2m1fz  13554  fz0to4untppr  13567  fz0to5un2tp  13568  4fvwrd4  13585  elfzo2  13599  elfzouz2  13611  fzossrbm1  13625  fzossfzop1  13680  ssfzo12bi  13698  fzoopth  13699  elfzonelfzo  13706  elfzomelpfzo  13708  fzosplitprm1  13714  fzostep1  13720  fzind2  13722  flword2  13751  fldiv4p1lem1div2  13773  uzsup  13801  modaddmodup  13875  fzsdom2  14369  swrdsbslen  14605  swrdspsleq  14606  pfxtrcfv0  14635  pfxtrcfvl  14638  pfxccatin12lem2a  14668  cshwidxmod  14744  rexuzre  15295  limsupgre  15423  rlimclim1  15487  rlimclim  15488  climrlim2  15489  isercolllem1  15607  isercoll  15610  climcndslem1  15791  fallfacval4  15985  oddge22np1  16295  nn0o  16329  bitsmod  16382  smueqlem  16436  dvdsnprmd  16636  2mulprm  16639  oddprmgt2  16645  oddprmge3  16646  ge2nprmge4  16647  modprm0  16752  prm23ge5  16762  vdwlem9  16936  prmgaplem3  17000  prmgaplem5  17002  prmgaplem6  17003  prmgaplem7  17004  strleun  17103  setsstruct  17122  fislw  19539  efgsp1  19651  efgredleme  19657  lt6abl  19809  telgsumfzs  19903  ablfac1eu  19989  znidomb  21503  chfacfscmul0  22778  chfacfscmulfsupp  22779  chfacfpmmul0  22782  chfacfpmmulfsupp  22783  dvfsumlem1  25965  dvfsumlem3  25968  plyaddlem1  26151  coeidlem  26175  2logb9irr  26738  ppisval  27047  chtdif  27101  ppidif  27106  ppiublem1  27146  ppiub  27148  chtub  27156  lgsdilem2  27277  gausslemma2dlem2  27311  gausslemma2dlem4  27313  gausslemma2dlem5  27315  gausslemma2dlem6  27316  lgsquadlem1  27324  lgsquadlem3  27326  2lgslem1  27338  chebbnd1lem1  27413  chebbnd1lem2  27414  chebbnd1lem3  27415  dchrisumlem2  27434  dchrvmasumiflem1  27445  mulog2sumlem2  27479  logdivbnd  27500  pntlemg  27542  pntlemq  27545  pntlemf  27549  axlowdim  28941  pthdlem1  29746  crctcshwlkn0lem3  29792  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0lem6  29795  wwlksm1edg  29861  wwlksnred  29872  clwlkclwwlklem2fv1  29974  clwlkclwwlklem2  29979  clwwisshclwwslem  29993  clwwlkinwwlk  30019  clwwlkf  30026  clwwlkext2edg  30035  wwlksubclwwlk  30037  frgrreggt1  30372  ssnnssfz  32760  ccatdmss  32921  chnub  32984  cycpmco2lem6  33103  ballotlemsdom  34496  ballotlemsel1i  34497  ballotlemfrceq  34513  signstfvc  34558  signstfveq0  34561  prodfzo03  34587  erdszelem8  35178  climuzcnv  35651  poimirlem6  37613  fdc  37732  sticksstones12  42139  eluzp1  42288  fimgmcyc  42515  eldioph2lem1  42741  hbt  43112  ssinc  45074  ssdec  45075  monoords  45288  fzdifsuc2  45301  eluzd  45398  fmul01lt1lem2  45576  sumnnodd  45621  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  dvnprodlem2  45938  itgspltprt  45970  stoweidlem11  46002  stoweidlem26  46017  wallispilem4  46059  fourierdlem12  46110  fourierdlem20  46118  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem54  46151  fourierdlem79  46176  fourierdlem102  46199  fourierdlem111  46208  fourierdlem114  46211  etransclem23  46248  etransclem48  46273  caratheodorylem1  46517  smfmullem4  46785  eluzge0nn0  47306  ssfz12  47308  elfzlble  47314  fzopredsuc  47317  ceilhalfelfzo1  47324  addmodne  47338  m1modnep2mod  47346  m1modmmod  47352  modm2nep1  47360  modp2nep1  47361  modm1nep2  47362  modm1nem2  47363  modm1p1ne  47364  iccpartipre  47415  iccpartiltu  47416  iccpartgt  47421  fmtnoge3  47524  odz2prm2pw  47557  fmtnoprmfac2lem1  47560  fmtno4prmfac  47566  31prm  47591  lighneallem4b  47603  341fppr2  47728  9fppr8  47731  fpprel2  47735  nfermltl8rev  47736  nfermltl2rev  47737  gbegt5  47755  gbowgt5  47756  sbgoldbm  47778  mogoldbb  47779  sbgoldbo  47781  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  evengpop3  47792  evengpoap3  47793  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem3  47801  tgblthelfgott  47809  gpgusgralem  48040  gpgedgvtx1  48046  gpg5nbgrvtx13starlem2  48056  gpg3nbgrvtx0  48060  gpg3nbgrvtx0ALT  48061  gpg5nbgr3star  48065  gpg3kgrtriexlem3  48069  gpg3kgrtriexlem6  48072  cznnring  48243  ssnn0ssfz  48330  elfzolborelfzop1  48501  rege1logbzge0  48541  fllog2  48550  nnolog2flm1  48572  dignn0ldlem  48584