Theorem eluz2 12863

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 12862	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1154	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12861	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 537	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 282	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1111	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 381	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536   ≤ cle 11239  ℤcz 12586  ℤ_≥cuz 12857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587  df-uz 12858

This theorem is referenced by:  eluzmn  12864  eluzuzle  12866  eluzelz  12867  eluzle  12870  uztrn  12875  eluzp1p1  12885  eluzadd  12886  eluzsub  12887  subeluzsub  12890  uzm1  12891  uznn0sub  12892  1eluzge0  12899  2eluzge1  12901  5eluz3  12902  uz3m2nn  12913  raluz2  12916  rexuz2  12918  peano2uz  12920  nn0pzuz  12924  uzind4  12925  uzinfi  12947  zsupss  12956  nn01to3  12960  nn0ge2m1nnALT  12961  elfzuzb  13541  uzsubsubfz  13570  ssfzunsn  13594  ige2m1fz  13641  fz0to4untppr  13654  fz0to5un2tp  13655  4fvwrd4  13672  elfzo2  13686  elfzouz2  13699  fzossrbm1  13713  fzossfzop1  13768  ssfzo12bi  13786  fzoopth  13787  elfzonelfzo  13794  elfzomelpfzo  13797  fzosplitprm1  13803  fzostep1  13811  fzind2  13813  flword2  13842  fldiv4p1lem1div2  13864  uzsup  13892  modaddmodup  13966  fzsdom2  14461  ccatdmss  14615  swrdsbslen  14698  swrdspsleq  14699  pfxtrcfv0  14727  pfxtrcfvl  14730  pfxccatin12lem2a  14760  cshwidxmod  14836  rexuzre  15400  limsupgre  15528  rlimclim1  15592  rlimclim  15593  climrlim2  15594  isercolllem1  15712  isercoll  15715  climcndslem1  15899  fallfacval4  16092  oddge22np1  16402  nn0o  16436  bitsmod  16489  smueqlem  16543  dvdsnprmd  16743  2mulprm  16746  oddprmgt2  16753  oddprmge3  16754  ge2nprmge4  16755  modprm0  16860  prm23ge5  16870  vdwlem9  17044  prmgaplem3  17108  prmgaplem5  17110  prmgaplem6  17111  prmgaplem7  17112  strleun  17212  setsstruct  17231  chnub  18673  fislw  19690  efgsp1  19802  efgredleme  19808  lt6abl  19960  telgsumfzs  20054  ablfac1eu  20140  znidomb  21711  chfacfscmul0  23015  chfacfscmulfsupp  23016  chfacfpmmul0  23019  chfacfpmmulfsupp  23020  dvfsumlem1  26185  dvfsumlem3  26187  plyaddlem1  26370  coeidlem  26394  2logb9irr  26960  ppisval  27268  chtdif  27322  ppidif  27327  ppiublem1  27366  ppiub  27368  chtub  27376  lgsdilem2  27497  gausslemma2dlem2  27531  gausslemma2dlem4  27533  gausslemma2dlem5  27535  gausslemma2dlem6  27536  lgsquadlem1  27544  lgsquadlem3  27546  2lgslem1  27558  chebbnd1lem1  27633  chebbnd1lem2  27634  chebbnd1lem3  27635  dchrisumlem2  27654  dchrvmasumiflem1  27665  mulog2sumlem2  27699  logdivbnd  27720  pntlemg  27762  pntlemq  27765  pntlemf  27769  axlowdim  29311  pthdlem1  30115  crctcshwlkn0lem3  30161  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  wwlksm1edg  30230  wwlksnred  30241  clwlkclwwlklem2fv1  30346  clwlkclwwlklem2  30351  clwwisshclwwslem  30365  clwwlkinwwlk  30391  clwwlkf  30398  clwwlkext2edg  30407  wwlksubclwwlk  30409  frgrreggt1  30744  ssnnssfz  33132  cycpmco2lem6  33451  ballotlemsdom  34902  ballotlemsel1i  34903  ballotlemfrceq  34919  signstfvc  34961  signstfveq0  34964  prodfzo03  34990  erdszelem8  35690  climuzcnv  36163  poimirlem6  38277  fdc  38396  sticksstones12  42925  eluzp1  43068  fimgmcyc  43302  eldioph2lem1  43491  hbt  43857  ssinc  45805  ssdec  45806  monoords  46016  fzdifsuc2  46029  eluzd  46123  fmul01lt1lem2  46301  sumnnodd  46346  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnmul  46657  dvnprodlem2  46661  itgspltprt  46693  stoweidlem11  46725  stoweidlem26  46740  wallispilem4  46782  fourierdlem12  46833  fourierdlem20  46841  fourierdlem41  46862  fourierdlem50  46870  fourierdlem54  46874  fourierdlem79  46899  fourierdlem102  46922  fourierdlem111  46931  fourierdlem114  46934  etransclem23  46971  etransclem48  46996  caratheodorylem1  47240  smfmullem4  47508  eluzge0nn0  48049  ssfz12  48051  elfzlble  48057  fzopredsuc  48061  ceilhalfelfzo1  48071  addmodne  48087  m1modnep2mod  48095  m1modmmod  48101  modm2nep1  48109  modp2nep1  48110  modm1nep2  48111  modm1nem2  48112  modm1p1ne  48113  2timesltsqm1  48116  muldvdsfacgt  48123  muldvdsfacm1  48124  iccpartipre  48170  iccpartiltu  48171  iccpartgt  48176  fmtnoge3  48282  odz2prm2pw  48315  fmtnoprmfac2lem1  48318  fmtno4prmfac  48324  31prm  48349  lighneallem4b  48361  nprmdvdsfacm1lem2  48373  nprmdvdsfacm1lem3  48374  nprmdvdsfacm1lem4  48375  nprmdvdsfacm1  48376  ppivalnnnprmge6  48378  341fppr2  48499  9fppr8  48502  fpprel2  48506  nfermltl8rev  48507  nfermltl2rev  48508  gbegt5  48526  gbowgt5  48527  sbgoldbm  48549  mogoldbb  48550  sbgoldbo  48552  nnsum3primesle9  48559  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  evengpop3  48563  evengpoap3  48564  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  bgoldbtbndlem3  48572  tgblthelfgott  48580  gpgusgralem  48821  gpgedgvtx1  48827  gpg5nbgrvtx13starlem2  48837  gpg3nbgrvtx0  48841  gpg3nbgrvtx0ALT  48842  gpg5nbgr3star  48846  gpg3kgrtriexlem3  48850  gpg3kgrtriexlem6  48853  gpg5edgnedg  48895  cznnring  49027  ssnn0ssfz  49129  elfzolborelfzop1  49299  rege1logbzge0  49339  fllog2  49348  nnolog2flm1  49370  dignn0ldlem  49382