Theorem eluz2 12769

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500   ≤ cle 11179  ℤcz 12500  ℤ_≥cuz 12763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501  df-uz 12764

This theorem is referenced by:  eluzmn  12770  eluzuzle  12772  eluzelz  12773  eluzle  12776  uztrn  12781  eluzp1p1  12791  eluzadd  12792  eluzsub  12793  subeluzsub  12796  uzm1  12797  uznn0sub  12798  1eluzge0  12805  2eluzge1  12807  5eluz3  12808  uz3m2nn  12819  raluz2  12822  rexuz2  12824  peano2uz  12826  nn0pzuz  12830  uzind4  12831  uzinfi  12853  zsupss  12862  nn01to3  12866  nn0ge2m1nnALT  12867  elfzuzb  13446  uzsubsubfz  13474  ssfzunsn  13498  ige2m1fz  13545  fz0to4untppr  13558  fz0to5un2tp  13559  4fvwrd4  13576  elfzo2  13590  elfzouz2  13602  fzossrbm1  13616  fzossfzop1  13671  ssfzo12bi  13689  fzoopth  13690  elfzonelfzo  13697  elfzomelpfzo  13700  fzosplitprm1  13706  fzostep1  13714  fzind2  13716  flword2  13745  fldiv4p1lem1div2  13767  uzsup  13795  modaddmodup  13869  fzsdom2  14363  ccatdmss  14517  swrdsbslen  14600  swrdspsleq  14601  pfxtrcfv0  14629  pfxtrcfvl  14632  pfxccatin12lem2a  14662  cshwidxmod  14738  rexuzre  15288  limsupgre  15416  rlimclim1  15480  rlimclim  15481  climrlim2  15482  isercolllem1  15600  isercoll  15603  climcndslem1  15784  fallfacval4  15978  oddge22np1  16288  nn0o  16322  bitsmod  16375  smueqlem  16429  dvdsnprmd  16629  2mulprm  16632  oddprmgt2  16638  oddprmge3  16639  ge2nprmge4  16640  modprm0  16745  prm23ge5  16755  vdwlem9  16929  prmgaplem3  16993  prmgaplem5  16995  prmgaplem6  16996  prmgaplem7  16997  strleun  17096  setsstruct  17115  chnub  18557  fislw  19566  efgsp1  19678  efgredleme  19684  lt6abl  19836  telgsumfzs  19930  ablfac1eu  20016  znidomb  21528  chfacfscmul0  22814  chfacfscmulfsupp  22815  chfacfpmmul0  22818  chfacfpmmulfsupp  22819  dvfsumlem1  26000  dvfsumlem3  26003  plyaddlem1  26186  coeidlem  26210  2logb9irr  26773  ppisval  27082  chtdif  27136  ppidif  27141  ppiublem1  27181  ppiub  27183  chtub  27191  lgsdilem2  27312  gausslemma2dlem2  27346  gausslemma2dlem4  27348  gausslemma2dlem5  27350  gausslemma2dlem6  27351  lgsquadlem1  27359  lgsquadlem3  27361  2lgslem1  27373  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  dchrisumlem2  27469  dchrvmasumiflem1  27480  mulog2sumlem2  27514  logdivbnd  27535  pntlemg  27577  pntlemq  27580  pntlemf  27584  axlowdim  29046  pthdlem1  29851  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  wwlksm1edg  29966  wwlksnred  29977  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2  30087  clwwisshclwwslem  30101  clwwlkinwwlk  30127  clwwlkf  30134  clwwlkext2edg  30143  wwlksubclwwlk  30145  frgrreggt1  30480  ssnnssfz  32878  cycpmco2lem6  33225  ballotlemsdom  34690  ballotlemsel1i  34691  ballotlemfrceq  34707  signstfvc  34752  signstfveq0  34755  prodfzo03  34781  erdszelem8  35414  climuzcnv  35887  poimirlem6  37877  fdc  37996  sticksstones12  42528  eluzp1  42677  fimgmcyc  42904  eldioph2lem1  43117  hbt  43487  ssinc  45446  ssdec  45447  monoords  45659  fzdifsuc2  45672  eluzd  45767  fmul01lt1lem2  45945  sumnnodd  45990  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnmul  46301  dvnprodlem2  46305  itgspltprt  46337  stoweidlem11  46369  stoweidlem26  46384  wallispilem4  46426  fourierdlem12  46477  fourierdlem20  46485  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem54  46518  fourierdlem79  46543  fourierdlem102  46566  fourierdlem111  46575  fourierdlem114  46578  etransclem23  46615  etransclem48  46640  caratheodorylem1  46884  smfmullem4  47152  eluzge0nn0  47672  ssfz12  47674  elfzlble  47680  fzopredsuc  47683  ceilhalfelfzo1  47690  addmodne  47704  m1modnep2mod  47712  m1modmmod  47718  modm2nep1  47726  modp2nep1  47727  modm1nep2  47728  modm1nem2  47729  modm1p1ne  47730  iccpartipre  47781  iccpartiltu  47782  iccpartgt  47787  fmtnoge3  47890  odz2prm2pw  47923  fmtnoprmfac2lem1  47926  fmtno4prmfac  47932  31prm  47957  lighneallem4b  47969  341fppr2  48094  9fppr8  48097  fpprel2  48101  nfermltl8rev  48102  nfermltl2rev  48103  gbegt5  48121  gbowgt5  48122  sbgoldbm  48144  mogoldbb  48145  sbgoldbo  48147  nnsum3primesle9  48154  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  evengpop3  48158  evengpoap3  48159  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem3  48167  tgblthelfgott  48175  gpgusgralem  48416  gpgedgvtx1  48422  gpg5nbgrvtx13starlem2  48432  gpg3nbgrvtx0  48436  gpg3nbgrvtx0ALT  48437  gpg5nbgr3star  48441  gpg3kgrtriexlem3  48445  gpg3kgrtriexlem6  48448  gpg5edgnedg  48490  cznnring  48622  ssnn0ssfz  48709  elfzolborelfzop1  48879  rege1logbzge0  48919  fllog2  48928  nnolog2flm1  48950  dignn0ldlem  48962