Theorem eluz2 12741

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 12740	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12739	. . . 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 5092  ‘cfv 6482   ≤ cle 11150  ℤcz 12471  ℤ_≥cuz 12735

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 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  eluzmn  12742  eluzuzle  12744  eluzelz  12745  eluzle  12748  uztrn  12753  eluzp1p1  12763  eluzadd  12764  eluzsub  12765  subeluzsub  12772  uzm1  12773  uznn0sub  12774  1eluzge0  12781  2eluzge1  12783  5eluz3  12784  uz3m2nn  12795  raluz2  12798  rexuz2  12800  peano2uz  12802  nn0pzuz  12806  uzind4  12807  uzinfi  12829  zsupss  12838  nn01to3  12842  nn0ge2m1nnALT  12843  elfzuzb  13421  uzsubsubfz  13449  ssfzunsn  13473  ige2m1fz  13520  fz0to4untppr  13533  fz0to5un2tp  13534  4fvwrd4  13551  elfzo2  13565  elfzouz2  13577  fzossrbm1  13591  fzossfzop1  13646  ssfzo12bi  13664  fzoopth  13665  elfzonelfzo  13672  elfzomelpfzo  13674  fzosplitprm1  13680  fzostep1  13686  fzind2  13688  flword2  13717  fldiv4p1lem1div2  13739  uzsup  13767  modaddmodup  13841  fzsdom2  14335  swrdsbslen  14571  swrdspsleq  14572  pfxtrcfv0  14600  pfxtrcfvl  14603  pfxccatin12lem2a  14633  cshwidxmod  14709  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  fislw  19504  efgsp1  19616  efgredleme  19622  lt6abl  19774  telgsumfzs  19868  ablfac1eu  19954  znidomb  21468  chfacfscmul0  22743  chfacfscmulfsupp  22744  chfacfpmmul0  22747  chfacfpmmulfsupp  22748  dvfsumlem1  25930  dvfsumlem3  25933  plyaddlem1  26116  coeidlem  26140  2logb9irr  26703  ppisval  27012  chtdif  27066  ppidif  27071  ppiublem1  27111  ppiub  27113  chtub  27121  lgsdilem2  27242  gausslemma2dlem2  27276  gausslemma2dlem4  27278  gausslemma2dlem5  27280  gausslemma2dlem6  27281  lgsquadlem1  27289  lgsquadlem3  27291  2lgslem1  27303  chebbnd1lem1  27378  chebbnd1lem2  27379  chebbnd1lem3  27380  dchrisumlem2  27399  dchrvmasumiflem1  27410  mulog2sumlem2  27444  logdivbnd  27465  pntlemg  27507  pntlemq  27510  pntlemf  27514  axlowdim  28906  pthdlem1  29711  crctcshwlkn0lem3  29757  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  crctcshwlkn0lem6  29760  wwlksm1edg  29826  wwlksnred  29837  clwlkclwwlklem2fv1  29939  clwlkclwwlklem2  29944  clwwisshclwwslem  29958  clwwlkinwwlk  29984  clwwlkf  29991  clwwlkext2edg  30000  wwlksubclwwlk  30002  frgrreggt1  30337  ssnnssfz  32730  ccatdmss  32891  chnub  32954  cycpmco2lem6  33073  ballotlemsdom  34480  ballotlemsel1i  34481  ballotlemfrceq  34497  signstfvc  34542  signstfveq0  34545  prodfzo03  34571  erdszelem8  35175  climuzcnv  35648  poimirlem6  37610  fdc  37729  sticksstones12  42135  eluzp1  42284  fimgmcyc  42511  eldioph2lem1  42737  hbt  43107  ssinc  45069  ssdec  45070  monoords  45283  fzdifsuc2  45296  eluzd  45392  fmul01lt1lem2  45570  sumnnodd  45615  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnmul  45928  dvnprodlem2  45932  itgspltprt  45964  stoweidlem11  45996  stoweidlem26  46011  wallispilem4  46053  fourierdlem12  46104  fourierdlem20  46112  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem54  46145  fourierdlem79  46170  fourierdlem102  46193  fourierdlem111  46202  fourierdlem114  46205  etransclem23  46242  etransclem48  46267  caratheodorylem1  46511  smfmullem4  46779  eluzge0nn0  47300  ssfz12  47302  elfzlble  47308  fzopredsuc  47311  ceilhalfelfzo1  47318  addmodne  47332  m1modnep2mod  47340  m1modmmod  47346  modm2nep1  47354  modp2nep1  47355  modm1nep2  47356  modm1nem2  47357  modm1p1ne  47358  iccpartipre  47409  iccpartiltu  47410  iccpartgt  47415  fmtnoge3  47518  odz2prm2pw  47551  fmtnoprmfac2lem1  47554  fmtno4prmfac  47560  31prm  47585  lighneallem4b  47597  341fppr2  47722  9fppr8  47725  fpprel2  47729  nfermltl8rev  47730  nfermltl2rev  47731  gbegt5  47749  gbowgt5  47750  sbgoldbm  47772  mogoldbb  47773  sbgoldbo  47775  nnsum3primesle9  47782  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  evengpop3  47786  evengpoap3  47787  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  wtgoldbnnsum4prm  47790  bgoldbnnsum3prm  47792  bgoldbtbndlem3  47795  tgblthelfgott  47803  gpgusgralem  48044  gpgedgvtx1  48050  gpg5nbgrvtx13starlem2  48060  gpg3nbgrvtx0  48064  gpg3nbgrvtx0ALT  48065  gpg5nbgr3star  48069  gpg3kgrtriexlem3  48073  gpg3kgrtriexlem6  48076  gpg5edgnedg  48118  cznnring  48250  ssnn0ssfz  48337  elfzolborelfzop1  48508  rege1logbzge0  48548  fllog2  48557  nnolog2flm1  48579  dignn0ldlem  48591