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 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12861	. . . 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 5124  ‘cfv 6536   ≤ cle 11275  ℤcz 12593  ℤ_≥cuz 12857

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-cnex 11190  ax-resscn 11191

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11474  df-z 12594  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  12894  uzm1  12895  uznn0sub  12896  5eluz3  12906  uz3m2nn  12912  1eluzge0  12913  2eluzge1  12915  raluz2  12918  rexuz2  12920  peano2uz  12922  nn0pzuz  12926  uzind4  12927  uzinfi  12949  zsupss  12958  nn01to3  12962  nn0ge2m1nnALT  12963  elfzuzb  13540  uzsubsubfz  13568  ssfzunsn  13592  ige2m1fz  13639  fz0to4untppr  13652  fz0to5un2tp  13653  4fvwrd4  13670  elfzo2  13684  elfzouz2  13696  fzossrbm1  13710  fzossfzop1  13764  ssfzo12bi  13782  fzoopth  13783  elfzonelfzo  13790  elfzomelpfzo  13792  fzosplitprm1  13798  fzostep1  13804  fzind2  13806  flword2  13835  fldiv4p1lem1div2  13857  uzsup  13885  modaddmodup  13957  fzsdom2  14451  swrdsbslen  14687  swrdspsleq  14688  pfxtrcfv0  14717  pfxtrcfvl  14720  pfxccatin12lem2a  14750  cshwidxmod  14826  rexuzre  15376  limsupgre  15502  rlimclim1  15566  rlimclim  15567  climrlim2  15568  isercolllem1  15686  isercoll  15689  climcndslem1  15870  fallfacval4  16064  oddge22np1  16373  nn0o  16407  bitsmod  16460  smueqlem  16514  dvdsnprmd  16714  2mulprm  16717  oddprmgt2  16723  oddprmge3  16724  ge2nprmge4  16725  modprm0  16830  prm23ge5  16840  vdwlem9  17014  prmgaplem3  17078  prmgaplem5  17080  prmgaplem6  17081  prmgaplem7  17082  strleun  17181  setsstruct  17200  fislw  19611  efgsp1  19723  efgredleme  19729  lt6abl  19881  telgsumfzs  19975  ablfac1eu  20061  znidomb  21527  chfacfscmul0  22801  chfacfscmulfsupp  22802  chfacfpmmul0  22805  chfacfpmmulfsupp  22806  dvfsumlem1  25989  dvfsumlem3  25992  plyaddlem1  26175  coeidlem  26199  2logb9irr  26762  ppisval  27071  chtdif  27125  ppidif  27130  ppiublem1  27170  ppiub  27172  chtub  27180  lgsdilem2  27301  gausslemma2dlem2  27335  gausslemma2dlem4  27337  gausslemma2dlem5  27339  gausslemma2dlem6  27340  lgsquadlem1  27348  lgsquadlem3  27350  2lgslem1  27362  chebbnd1lem1  27437  chebbnd1lem2  27438  chebbnd1lem3  27439  dchrisumlem2  27458  dchrvmasumiflem1  27469  mulog2sumlem2  27503  logdivbnd  27524  pntlemg  27566  pntlemq  27569  pntlemf  27573  axlowdim  28945  pthdlem1  29753  crctcshwlkn0lem3  29799  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  crctcshwlkn0lem6  29802  wwlksm1edg  29868  wwlksnred  29879  clwlkclwwlklem2fv1  29981  clwlkclwwlklem2  29986  clwwisshclwwslem  30000  clwwlkinwwlk  30026  clwwlkf  30033  clwwlkext2edg  30042  wwlksubclwwlk  30044  frgrreggt1  30379  ssnnssfz  32769  ccatdmss  32930  chnub  32997  cycpmco2lem6  33147  ballotlemsdom  34549  ballotlemsel1i  34550  ballotlemfrceq  34566  signstfvc  34611  signstfveq0  34614  prodfzo03  34640  erdszelem8  35225  climuzcnv  35698  poimirlem6  37655  fdc  37774  sticksstones12  42176  eluzp1  42325  fimgmcyc  42532  eldioph2lem1  42758  hbt  43129  ssinc  45091  ssdec  45092  monoords  45306  fzdifsuc2  45319  eluzd  45416  fmul01lt1lem2  45594  sumnnodd  45639  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnmul  45952  dvnprodlem2  45956  itgspltprt  45988  stoweidlem11  46020  stoweidlem26  46035  wallispilem4  46077  fourierdlem12  46128  fourierdlem20  46136  fourierdlem41  46157  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem54  46169  fourierdlem79  46194  fourierdlem102  46217  fourierdlem111  46226  fourierdlem114  46229  etransclem23  46266  etransclem48  46291  caratheodorylem1  46535  smfmullem4  46803  eluzge0nn0  47321  ssfz12  47323  elfzlble  47329  fzopredsuc  47332  ceilhalfelfzo1  47339  addmodne  47353  m1modnep2mod  47361  iccpartipre  47415  iccpartiltu  47416  iccpartgt  47421  fmtnoge3  47524  odz2prm2pw  47557  fmtnoprmfac2lem1  47560  fmtno4prmfac  47566  31prm  47591  lighneallem4b  47603  341fppr2  47728  9fppr8  47731  fpprel2  47735  nfermltl8rev  47736  nfermltl2rev  47737  gbegt5  47755  gbowgt5  47756  sbgoldbm  47778  mogoldbb  47779  sbgoldbo  47781  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  evengpop3  47792  evengpoap3  47793  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem3  47801  tgblthelfgott  47809  gpgusgralem  48040  gpgedgvtx1  48046  gpg5nbgrvtx13starlem2  48054  gpg3nbgrvtx0  48058  gpg3nbgrvtx0ALT  48059  gpg5nbgr3star  48063  gpg3kgrtriexlem3  48067  gpg3kgrtriexlem6  48070  cznnring  48217  ssnn0ssfz  48304  elfzolborelfzop1  48475  m1modmmod  48481  rege1logbzge0  48519  fllog2  48528  nnolog2flm1  48550  dignn0ldlem  48562