Theorem eluz2 12517

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 12516	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1134	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12515	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 528	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 278	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1093	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 288	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 379	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2108   class class class wbr 5070  ‘cfv 6418   ≤ cle 10941  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  eluzmn  12518  eluzuzle  12520  eluzelz  12521  eluzle  12524  uztrn  12529  eluzp1p1  12539  subeluzsub  12544  uzm1  12545  uznn0sub  12546  uz3m2nn  12560  1eluzge0  12561  2eluzge1  12563  raluz2  12566  rexuz2  12568  peano2uz  12570  nn0pzuz  12574  uzind4  12575  uzinfi  12597  zsupss  12606  nn01to3  12610  nn0ge2m1nnALT  12611  elfzuzb  13179  uzsubsubfz  13207  ssfzunsn  13231  ige2m1fz  13275  4fvwrd4  13305  elfzo2  13319  elfzouz2  13330  fzossrbm1  13344  fzossfzop1  13393  ssfzo12bi  13410  elfzonelfzo  13417  elfzomelpfzo  13419  fzosplitprm1  13425  fzostep1  13431  fzind2  13433  flword2  13461  fldiv4p1lem1div2  13483  uzsup  13511  modaddmodup  13582  fzsdom2  14071  swrdsbslen  14305  swrdspsleq  14306  pfxtrcfv0  14335  pfxtrcfvl  14338  pfxccatin12lem2a  14368  cshwidxmod  14444  rexuzre  14992  limsupgre  15118  rlimclim1  15182  rlimclim  15183  climrlim2  15184  isercolllem1  15304  isercoll  15307  climcndslem1  15489  fallfacval4  15681  oddge22np1  15986  nn0o  16020  bitsmod  16071  smueqlem  16125  dvdsnprmd  16323  2mulprm  16326  oddprmgt2  16332  oddprmge3  16333  ge2nprmge4  16334  modprm0  16434  prm23ge5  16444  vdwlem9  16618  prmgaplem3  16682  prmgaplem5  16684  prmgaplem6  16685  prmgaplem7  16686  strleun  16786  setsstruct  16805  fislw  19145  efgsp1  19258  efgredleme  19264  lt6abl  19411  telgsumfzs  19505  ablfac1eu  19591  znidomb  20681  chfacfscmul0  21915  chfacfscmulfsupp  21916  chfacfpmmul0  21919  chfacfpmmulfsupp  21920  dvfsumlem1  25095  dvfsumlem3  25097  plyaddlem1  25279  coeidlem  25303  2logb9irr  25850  ppisval  26158  chtdif  26212  ppidif  26217  ppiublem1  26255  ppiub  26257  chtub  26265  lgsdilem2  26386  gausslemma2dlem2  26420  gausslemma2dlem4  26422  gausslemma2dlem5  26424  gausslemma2dlem6  26425  lgsquadlem1  26433  lgsquadlem3  26435  2lgslem1  26447  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  dchrisumlem2  26543  dchrvmasumiflem1  26554  mulog2sumlem2  26588  logdivbnd  26609  pntlemg  26651  pntlemq  26654  pntlemf  26658  axlowdim  27232  pthdlem1  28035  crctcshwlkn0lem3  28078  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  wwlksm1edg  28147  wwlksnred  28158  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2  28265  clwwisshclwwslem  28279  clwwlkinwwlk  28305  clwwlkf  28312  clwwlkext2edg  28321  wwlksubclwwlk  28323  frgrreggt1  28658  ssnnssfz  31010  cycpmco2lem6  31300  ballotlemsdom  32378  ballotlemsel1i  32379  ballotlemfrceq  32395  signstfvc  32453  signstfveq0  32456  prodfzo03  32483  erdszelem8  33060  climuzcnv  33529  poimirlem6  35710  fdc  35830  sticksstones12  40042  eldioph2lem1  40498  hbt  40871  ssinc  42526  ssdec  42527  monoords  42726  fzdifsuc2  42739  eluzd  42839  fmul01lt1lem2  43016  sumnnodd  43061  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  dvnprodlem2  43378  itgspltprt  43410  stoweidlem11  43442  stoweidlem26  43457  wallispilem4  43499  fourierdlem12  43550  fourierdlem20  43558  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem54  43591  fourierdlem79  43616  fourierdlem102  43639  fourierdlem111  43648  fourierdlem114  43651  etransclem23  43688  etransclem48  43713  caratheodorylem1  43954  smfmullem4  44215  eluzge0nn0  44692  ssfz12  44694  elfzlble  44700  fzopredsuc  44703  fzoopth  44707  iccpartipre  44761  iccpartiltu  44762  iccpartgt  44767  fmtnoge3  44870  odz2prm2pw  44903  fmtnoprmfac2lem1  44906  fmtno4prmfac  44912  31prm  44937  lighneallem4b  44949  341fppr2  45074  9fppr8  45077  fpprel2  45081  nfermltl8rev  45082  nfermltl2rev  45083  gbegt5  45101  gbowgt5  45102  sbgoldbm  45124  mogoldbb  45125  sbgoldbo  45127  nnsum3primesle9  45134  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem3  45147  tgblthelfgott  45155  cznnring  45402  ssnn0ssfz  45573  elfzolborelfzop1  45748  m1modmmod  45755  rege1logbzge0  45793  fllog2  45802  nnolog2flm1  45824  dignn0ldlem  45836