Theorem eluz2 12824

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 12823	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12822	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 529	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 278	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1095	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 288	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 379	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   ∈ wcel 2106   class class class wbr 5147  ‘cfv 6540   ≤ cle 11245  ℤcz 12554  ℤ_≥cuz 12818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555  df-uz 12819

This theorem is referenced by:  eluzmn  12825  eluzuzle  12827  eluzelz  12828  eluzle  12831  uztrn  12836  eluzp1p1  12846  eluzadd  12847  eluzsub  12848  subeluzsub  12855  uzm1  12856  uznn0sub  12857  uz3m2nn  12871  1eluzge0  12872  2eluzge1  12874  raluz2  12877  rexuz2  12879  peano2uz  12881  nn0pzuz  12885  uzind4  12886  uzinfi  12908  zsupss  12917  nn01to3  12921  nn0ge2m1nnALT  12922  elfzuzb  13491  uzsubsubfz  13519  ssfzunsn  13543  ige2m1fz  13587  4fvwrd4  13617  elfzo2  13631  elfzouz2  13643  fzossrbm1  13657  fzossfzop1  13706  ssfzo12bi  13723  elfzonelfzo  13730  elfzomelpfzo  13732  fzosplitprm1  13738  fzostep1  13744  fzind2  13746  flword2  13774  fldiv4p1lem1div2  13796  uzsup  13824  modaddmodup  13895  fzsdom2  14384  swrdsbslen  14610  swrdspsleq  14611  pfxtrcfv0  14640  pfxtrcfvl  14643  pfxccatin12lem2a  14673  cshwidxmod  14749  rexuzre  15295  limsupgre  15421  rlimclim1  15485  rlimclim  15486  climrlim2  15487  isercolllem1  15607  isercoll  15610  climcndslem1  15791  fallfacval4  15983  oddge22np1  16288  nn0o  16322  bitsmod  16373  smueqlem  16427  dvdsnprmd  16623  2mulprm  16626  oddprmgt2  16632  oddprmge3  16633  ge2nprmge4  16634  modprm0  16734  prm23ge5  16744  vdwlem9  16918  prmgaplem3  16982  prmgaplem5  16984  prmgaplem6  16985  prmgaplem7  16986  strleun  17086  setsstruct  17105  fislw  19487  efgsp1  19599  efgredleme  19605  lt6abl  19757  telgsumfzs  19851  ablfac1eu  19937  znidomb  21108  chfacfscmul0  22351  chfacfscmulfsupp  22352  chfacfpmmul0  22355  chfacfpmmulfsupp  22356  dvfsumlem1  25534  dvfsumlem3  25536  plyaddlem1  25718  coeidlem  25742  2logb9irr  26289  ppisval  26597  chtdif  26651  ppidif  26656  ppiublem1  26694  ppiub  26696  chtub  26704  lgsdilem2  26825  gausslemma2dlem2  26859  gausslemma2dlem4  26861  gausslemma2dlem5  26863  gausslemma2dlem6  26864  lgsquadlem1  26872  lgsquadlem3  26874  2lgslem1  26886  chebbnd1lem1  26961  chebbnd1lem2  26962  chebbnd1lem3  26963  dchrisumlem2  26982  dchrvmasumiflem1  26993  mulog2sumlem2  27027  logdivbnd  27048  pntlemg  27090  pntlemq  27093  pntlemf  27097  axlowdim  28208  pthdlem1  29012  crctcshwlkn0lem3  29055  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  crctcshwlkn0lem6  29058  wwlksm1edg  29124  wwlksnred  29135  clwlkclwwlklem2fv1  29237  clwlkclwwlklem2  29242  clwwisshclwwslem  29256  clwwlkinwwlk  29282  clwwlkf  29289  clwwlkext2edg  29298  wwlksubclwwlk  29300  frgrreggt1  29635  ssnnssfz  31985  cycpmco2lem6  32277  ballotlemsdom  33498  ballotlemsel1i  33499  ballotlemfrceq  33515  signstfvc  33573  signstfveq0  33576  prodfzo03  33603  erdszelem8  34177  climuzcnv  34644  poimirlem6  36482  fdc  36601  sticksstones12  40962  eldioph2lem1  41483  hbt  41857  ssinc  43761  ssdec  43762  monoords  43993  fzdifsuc2  44006  eluzd  44105  fmul01lt1lem2  44287  sumnnodd  44332  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  dvnmul  44645  dvnprodlem2  44649  itgspltprt  44681  stoweidlem11  44713  stoweidlem26  44728  wallispilem4  44770  fourierdlem12  44821  fourierdlem20  44829  fourierdlem41  44850  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem54  44862  fourierdlem79  44887  fourierdlem102  44910  fourierdlem111  44919  fourierdlem114  44922  etransclem23  44959  etransclem48  44984  caratheodorylem1  45228  smfmullem4  45496  eluzge0nn0  46006  ssfz12  46008  elfzlble  46014  fzopredsuc  46017  fzoopth  46021  iccpartipre  46075  iccpartiltu  46076  iccpartgt  46081  fmtnoge3  46184  odz2prm2pw  46217  fmtnoprmfac2lem1  46220  fmtno4prmfac  46226  31prm  46251  lighneallem4b  46263  341fppr2  46388  9fppr8  46391  fpprel2  46395  nfermltl8rev  46396  nfermltl2rev  46397  gbegt5  46415  gbowgt5  46416  sbgoldbm  46438  mogoldbb  46439  sbgoldbo  46441  nnsum3primesle9  46448  nnsum4primesodd  46450  nnsum4primesoddALTV  46451  evengpop3  46452  evengpoap3  46453  nnsum4primeseven  46454  nnsum4primesevenALTV  46455  wtgoldbnnsum4prm  46456  bgoldbnnsum3prm  46458  bgoldbtbndlem3  46461  tgblthelfgott  46469  cznnring  46807  ssnn0ssfz  46978  elfzolborelfzop1  47153  m1modmmod  47160  rege1logbzge0  47198  fllog2  47207  nnolog2flm1  47229  dignn0ldlem  47241