Theorem eluz2 12866

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 12865	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12864	. . . 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 2107   class class class wbr 5123  ‘cfv 6541   ≤ cle 11278  ℤcz 12596  ℤ_≥cuz 12860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-cnex 11193  ax-resscn 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  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 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7416  df-neg 11477  df-z 12597  df-uz 12861

This theorem is referenced by:  eluzmn  12867  eluzuzle  12869  eluzelz  12870  eluzle  12873  uztrn  12878  eluzp1p1  12888  eluzadd  12889  eluzsub  12890  subeluzsub  12897  uzm1  12898  uznn0sub  12899  5eluz3  12909  uz3m2nn  12915  1eluzge0  12916  2eluzge1  12918  raluz2  12921  rexuz2  12923  peano2uz  12925  nn0pzuz  12929  uzind4  12930  uzinfi  12952  zsupss  12961  nn01to3  12965  nn0ge2m1nnALT  12966  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  14450  swrdsbslen  14685  swrdspsleq  14686  pfxtrcfv0  14715  pfxtrcfvl  14718  pfxccatin12lem2a  14748  cshwidxmod  14824  rexuzre  15374  limsupgre  15500  rlimclim1  15564  rlimclim  15565  climrlim2  15566  isercolllem1  15684  isercoll  15687  climcndslem1  15868  fallfacval4  16062  oddge22np1  16369  nn0o  16403  bitsmod  16456  smueqlem  16510  dvdsnprmd  16710  2mulprm  16713  oddprmgt2  16719  oddprmge3  16720  ge2nprmge4  16721  modprm0  16826  prm23ge5  16836  vdwlem9  17010  prmgaplem3  17074  prmgaplem5  17076  prmgaplem6  17077  prmgaplem7  17078  strleun  17177  setsstruct  17196  fislw  19612  efgsp1  19724  efgredleme  19730  lt6abl  19882  telgsumfzs  19976  ablfac1eu  20062  znidomb  21535  chfacfscmul0  22813  chfacfscmulfsupp  22814  chfacfpmmul0  22817  chfacfpmmulfsupp  22818  dvfsumlem1  26003  dvfsumlem3  26006  plyaddlem1  26189  coeidlem  26213  2logb9irr  26775  ppisval  27084  chtdif  27138  ppidif  27143  ppiublem1  27183  ppiub  27185  chtub  27193  lgsdilem2  27314  gausslemma2dlem2  27348  gausslemma2dlem4  27350  gausslemma2dlem5  27352  gausslemma2dlem6  27353  lgsquadlem1  27361  lgsquadlem3  27363  2lgslem1  27375  chebbnd1lem1  27450  chebbnd1lem2  27451  chebbnd1lem3  27452  dchrisumlem2  27471  dchrvmasumiflem1  27482  mulog2sumlem2  27516  logdivbnd  27537  pntlemg  27579  pntlemq  27582  pntlemf  27586  axlowdim  28907  pthdlem1  29715  crctcshwlkn0lem3  29761  crctcshwlkn0lem4  29762  crctcshwlkn0lem5  29763  crctcshwlkn0lem6  29764  wwlksm1edg  29830  wwlksnred  29841  clwlkclwwlklem2fv1  29943  clwlkclwwlklem2  29948  clwwisshclwwslem  29962  clwwlkinwwlk  29988  clwwlkf  29995  clwwlkext2edg  30004  wwlksubclwwlk  30006  frgrreggt1  30341  ssnnssfz  32733  ccatdmss  32879  chnub  32946  cycpmco2lem6  33095  ballotlemsdom  34489  ballotlemsel1i  34490  ballotlemfrceq  34506  signstfvc  34564  signstfveq0  34567  prodfzo03  34593  erdszelem8  35178  climuzcnv  35651  poimirlem6  37608  fdc  37727  sticksstones12  42134  eluzp1  42320  fimgmcyc  42523  eldioph2lem1  42749  hbt  43120  ssinc  45064  ssdec  45065  monoords  45281  fzdifsuc2  45294  eluzd  45392  fmul01lt1lem2  45572  sumnnodd  45617  ioodvbdlimc1lem2  45919  ioodvbdlimc2lem  45921  dvnmul  45930  dvnprodlem2  45934  itgspltprt  45966  stoweidlem11  45998  stoweidlem26  46013  wallispilem4  46055  fourierdlem12  46106  fourierdlem20  46114  fourierdlem41  46135  fourierdlem48  46141  fourierdlem49  46142  fourierdlem50  46143  fourierdlem54  46147  fourierdlem79  46172  fourierdlem102  46195  fourierdlem111  46204  fourierdlem114  46207  etransclem23  46244  etransclem48  46269  caratheodorylem1  46513  smfmullem4  46781  eluzge0nn0  47297  ssfz12  47299  elfzlble  47305  fzopredsuc  47308  addmodne  47319  m1modnep2mod  47327  iccpartipre  47381  iccpartiltu  47382  iccpartgt  47387  fmtnoge3  47490  odz2prm2pw  47523  fmtnoprmfac2lem1  47526  fmtno4prmfac  47532  31prm  47557  lighneallem4b  47569  341fppr2  47694  9fppr8  47697  fpprel2  47701  nfermltl8rev  47702  nfermltl2rev  47703  gbegt5  47721  gbowgt5  47722  sbgoldbm  47744  mogoldbb  47745  sbgoldbo  47747  nnsum3primesle9  47754  nnsum4primesodd  47756  nnsum4primesoddALTV  47757  evengpop3  47758  evengpoap3  47759  nnsum4primeseven  47760  nnsum4primesevenALTV  47761  wtgoldbnnsum4prm  47762  bgoldbnnsum3prm  47764  bgoldbtbndlem3  47767  tgblthelfgott  47775  gpgusgralem  47984  ceilhalfelfzo1  47989  gpgedgvtx1  47993  gpg5nbgrvtx13starlem2  48001  gpg3nbgrvtx0  48005  gpg3nbgrvtx0ALT  48006  gpg5nbgr3star  48010  gpg3kgrtriexlem3  48014  gpg3kgrtriexlem6  48017  cznnring  48151  ssnn0ssfz  48238  elfzolborelfzop1  48409  m1modmmod  48415  rege1logbzge0  48453  fllog2  48462  nnolog2flm1  48484  dignn0ldlem  48496