Theorem eluz2 12409

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 12408	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1138	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12407	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 532	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 282	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1097	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 383	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   ∈ wcel 2112   class class class wbr 5039  ‘cfv 6358   ≤ cle 10833  ℤcz 12141  ℤ_≥cuz 12403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-cnex 10750  ax-resscn 10751

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-ov 7194  df-neg 11030  df-z 12142  df-uz 12404

This theorem is referenced by:  eluzmn  12410  eluzuzle  12412  eluzelz  12413  eluzle  12416  uztrn  12421  eluzp1p1  12431  subeluzsub  12436  uzm1  12437  uznn0sub  12438  uz3m2nn  12452  1eluzge0  12453  2eluzge1  12455  raluz2  12458  rexuz2  12460  peano2uz  12462  nn0pzuz  12466  uzind4  12467  uzinfi  12489  zsupss  12498  nn01to3  12502  nn0ge2m1nnALT  12503  elfzuzb  13071  uzsubsubfz  13099  ssfzunsn  13123  ige2m1fz  13167  4fvwrd4  13197  elfzo2  13211  elfzouz2  13222  fzossrbm1  13236  fzossfzop1  13285  ssfzo12bi  13302  elfzonelfzo  13309  elfzomelpfzo  13311  fzosplitprm1  13317  fzostep1  13323  fzind2  13325  flword2  13353  fldiv4p1lem1div2  13375  uzsup  13401  modaddmodup  13472  fzsdom2  13960  swrdsbslen  14194  swrdspsleq  14195  pfxtrcfv0  14224  pfxtrcfvl  14227  pfxccatin12lem2a  14257  cshwidxmod  14333  rexuzre  14881  limsupgre  15007  rlimclim1  15071  rlimclim  15072  climrlim2  15073  isercolllem1  15193  isercoll  15196  climcndslem1  15376  fallfacval4  15568  oddge22np1  15873  nn0o  15907  bitsmod  15958  smueqlem  16012  dvdsnprmd  16210  2mulprm  16213  oddprmgt2  16219  oddprmge3  16220  ge2nprmge4  16221  modprm0  16321  prm23ge5  16331  vdwlem9  16505  prmgaplem3  16569  prmgaplem5  16571  prmgaplem6  16572  prmgaplem7  16573  setsstruct  16705  strleun  16775  fislw  18968  efgsp1  19081  efgredleme  19087  lt6abl  19234  telgsumfzs  19328  ablfac1eu  19414  znidomb  20480  chfacfscmul0  21709  chfacfscmulfsupp  21710  chfacfpmmul0  21713  chfacfpmmulfsupp  21714  dvfsumlem1  24877  dvfsumlem3  24879  plyaddlem1  25061  coeidlem  25085  2logb9irr  25632  ppisval  25940  chtdif  25994  ppidif  25999  ppiublem1  26037  ppiub  26039  chtub  26047  lgsdilem2  26168  gausslemma2dlem2  26202  gausslemma2dlem4  26204  gausslemma2dlem5  26206  gausslemma2dlem6  26207  lgsquadlem1  26215  lgsquadlem3  26217  2lgslem1  26229  chebbnd1lem1  26304  chebbnd1lem2  26305  chebbnd1lem3  26306  dchrisumlem2  26325  dchrvmasumiflem1  26336  mulog2sumlem2  26370  logdivbnd  26391  pntlemg  26433  pntlemq  26436  pntlemf  26440  axlowdim  27006  pthdlem1  27807  crctcshwlkn0lem3  27850  crctcshwlkn0lem4  27851  crctcshwlkn0lem5  27852  crctcshwlkn0lem6  27853  wwlksm1edg  27919  wwlksnred  27930  clwlkclwwlklem2fv1  28032  clwlkclwwlklem2  28037  clwwisshclwwslem  28051  clwwlkinwwlk  28077  clwwlkf  28084  clwwlkext2edg  28093  wwlksubclwwlk  28095  frgrreggt1  28430  ssnnssfz  30782  cycpmco2lem6  31071  ballotlemsdom  32144  ballotlemsel1i  32145  ballotlemfrceq  32161  signstfvc  32219  signstfveq0  32222  prodfzo03  32249  erdszelem8  32827  climuzcnv  33296  poimirlem6  35469  fdc  35589  sticksstones12  39783  eldioph2lem1  40226  hbt  40599  ssinc  42251  ssdec  42252  monoords  42450  fzdifsuc2  42463  eluzd  42563  fmul01lt1lem2  42744  sumnnodd  42789  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnmul  43102  dvnprodlem2  43106  itgspltprt  43138  stoweidlem11  43170  stoweidlem26  43185  wallispilem4  43227  fourierdlem12  43278  fourierdlem20  43286  fourierdlem41  43307  fourierdlem48  43313  fourierdlem49  43314  fourierdlem50  43315  fourierdlem54  43319  fourierdlem79  43344  fourierdlem102  43367  fourierdlem111  43376  fourierdlem114  43379  etransclem23  43416  etransclem48  43441  caratheodorylem1  43682  smfmullem4  43943  eluzge0nn0  44420  ssfz12  44422  elfzlble  44428  fzopredsuc  44431  fzoopth  44435  iccpartipre  44489  iccpartiltu  44490  iccpartgt  44495  fmtnoge3  44598  odz2prm2pw  44631  fmtnoprmfac2lem1  44634  fmtno4prmfac  44640  31prm  44665  lighneallem4b  44677  341fppr2  44802  9fppr8  44805  fpprel2  44809  nfermltl8rev  44810  nfermltl2rev  44811  gbegt5  44829  gbowgt5  44830  sbgoldbm  44852  mogoldbb  44853  sbgoldbo  44855  nnsum3primesle9  44862  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  evengpop3  44866  evengpoap3  44867  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  bgoldbtbndlem3  44875  tgblthelfgott  44883  cznnring  45130  ssnn0ssfz  45301  elfzolborelfzop1  45476  m1modmmod  45483  rege1logbzge0  45521  fllog2  45530  nnolog2flm1  45552  dignn0ldlem  45564