Theorem eluz2 12738

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 12737	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12736	. . . 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 2111   class class class wbr 5089  ‘cfv 6481   ≤ cle 11147  ℤcz 12468  ℤ_≥cuz 12732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-cnex 11062  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469  df-uz 12733

This theorem is referenced by:  eluzmn  12739  eluzuzle  12741  eluzelz  12742  eluzle  12745  uztrn  12750  eluzp1p1  12760  eluzadd  12761  eluzsub  12762  subeluzsub  12769  uzm1  12770  uznn0sub  12771  1eluzge0  12778  2eluzge1  12780  5eluz3  12781  uz3m2nn  12792  raluz2  12795  rexuz2  12797  peano2uz  12799  nn0pzuz  12803  uzind4  12804  uzinfi  12826  zsupss  12835  nn01to3  12839  nn0ge2m1nnALT  12840  elfzuzb  13418  uzsubsubfz  13446  ssfzunsn  13470  ige2m1fz  13517  fz0to4untppr  13530  fz0to5un2tp  13531  4fvwrd4  13548  elfzo2  13562  elfzouz2  13574  fzossrbm1  13588  fzossfzop1  13643  ssfzo12bi  13661  fzoopth  13662  elfzonelfzo  13669  elfzomelpfzo  13672  fzosplitprm1  13678  fzostep1  13686  fzind2  13688  flword2  13717  fldiv4p1lem1div2  13739  uzsup  13767  modaddmodup  13841  fzsdom2  14335  ccatdmss  14489  swrdsbslen  14572  swrdspsleq  14573  pfxtrcfv0  14601  pfxtrcfvl  14604  pfxccatin12lem2a  14634  cshwidxmod  14710  rexuzre  15260  limsupgre  15388  rlimclim1  15452  rlimclim  15453  climrlim2  15454  isercolllem1  15572  isercoll  15575  climcndslem1  15756  fallfacval4  15950  oddge22np1  16260  nn0o  16294  bitsmod  16347  smueqlem  16401  dvdsnprmd  16601  2mulprm  16604  oddprmgt2  16610  oddprmge3  16611  ge2nprmge4  16612  modprm0  16717  prm23ge5  16727  vdwlem9  16901  prmgaplem3  16965  prmgaplem5  16967  prmgaplem6  16968  prmgaplem7  16969  strleun  17068  setsstruct  17087  chnub  18528  fislw  19537  efgsp1  19649  efgredleme  19655  lt6abl  19807  telgsumfzs  19901  ablfac1eu  19987  znidomb  21498  chfacfscmul0  22773  chfacfscmulfsupp  22774  chfacfpmmul0  22777  chfacfpmmulfsupp  22778  dvfsumlem1  25959  dvfsumlem3  25962  plyaddlem1  26145  coeidlem  26169  2logb9irr  26732  ppisval  27041  chtdif  27095  ppidif  27100  ppiublem1  27140  ppiub  27142  chtub  27150  lgsdilem2  27271  gausslemma2dlem2  27305  gausslemma2dlem4  27307  gausslemma2dlem5  27309  gausslemma2dlem6  27310  lgsquadlem1  27318  lgsquadlem3  27320  2lgslem1  27332  chebbnd1lem1  27407  chebbnd1lem2  27408  chebbnd1lem3  27409  dchrisumlem2  27428  dchrvmasumiflem1  27439  mulog2sumlem2  27473  logdivbnd  27494  pntlemg  27536  pntlemq  27539  pntlemf  27543  axlowdim  28939  pthdlem1  29744  crctcshwlkn0lem3  29790  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  crctcshwlkn0lem6  29793  wwlksm1edg  29859  wwlksnred  29870  clwlkclwwlklem2fv1  29975  clwlkclwwlklem2  29980  clwwisshclwwslem  29994  clwwlkinwwlk  30020  clwwlkf  30027  clwwlkext2edg  30036  wwlksubclwwlk  30038  frgrreggt1  30373  ssnnssfz  32770  cycpmco2lem6  33100  ballotlemsdom  34525  ballotlemsel1i  34526  ballotlemfrceq  34542  signstfvc  34587  signstfveq0  34590  prodfzo03  34616  erdszelem8  35242  climuzcnv  35715  poimirlem6  37676  fdc  37795  sticksstones12  42261  eluzp1  42410  fimgmcyc  42637  eldioph2lem1  42863  hbt  43233  ssinc  45194  ssdec  45195  monoords  45408  fzdifsuc2  45421  eluzd  45517  fmul01lt1lem2  45695  sumnnodd  45740  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnmul  46051  dvnprodlem2  46055  itgspltprt  46087  stoweidlem11  46119  stoweidlem26  46134  wallispilem4  46176  fourierdlem12  46227  fourierdlem20  46235  fourierdlem41  46256  fourierdlem48  46262  fourierdlem49  46263  fourierdlem50  46264  fourierdlem54  46268  fourierdlem79  46293  fourierdlem102  46316  fourierdlem111  46325  fourierdlem114  46328  etransclem23  46365  etransclem48  46390  caratheodorylem1  46634  smfmullem4  46902  eluzge0nn0  47422  ssfz12  47424  elfzlble  47430  fzopredsuc  47433  ceilhalfelfzo1  47440  addmodne  47454  m1modnep2mod  47462  m1modmmod  47468  modm2nep1  47476  modp2nep1  47477  modm1nep2  47478  modm1nem2  47479  modm1p1ne  47480  iccpartipre  47531  iccpartiltu  47532  iccpartgt  47537  fmtnoge3  47640  odz2prm2pw  47673  fmtnoprmfac2lem1  47676  fmtno4prmfac  47682  31prm  47707  lighneallem4b  47719  341fppr2  47844  9fppr8  47847  fpprel2  47851  nfermltl8rev  47852  nfermltl2rev  47853  gbegt5  47871  gbowgt5  47872  sbgoldbm  47894  mogoldbb  47895  sbgoldbo  47897  nnsum3primesle9  47904  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  evengpop3  47908  evengpoap3  47909  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  bgoldbtbndlem3  47917  tgblthelfgott  47925  gpgusgralem  48166  gpgedgvtx1  48172  gpg5nbgrvtx13starlem2  48182  gpg3nbgrvtx0  48186  gpg3nbgrvtx0ALT  48187  gpg5nbgr3star  48191  gpg3kgrtriexlem3  48195  gpg3kgrtriexlem6  48198  gpg5edgnedg  48240  cznnring  48372  ssnn0ssfz  48459  elfzolborelfzop1  48630  rege1logbzge0  48670  fllog2  48679  nnolog2flm1  48701  dignn0ldlem  48713