Theorem eluz2 12616

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2101   class class class wbr 5077  ‘cfv 6447   ≤ cle 11038  ℤcz 12347  ℤ_≥cuz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-cnex 10955  ax-resscn 10956

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ral 3060  df-rex 3069  df-rab 3224  df-v 3436  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-br 5078  df-opab 5140  df-mpt 5161  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-fv 6455  df-ov 7298  df-neg 11236  df-z 12348  df-uz 12611

This theorem is referenced by:  eluzmn  12617  eluzuzle  12619  eluzelz  12620  eluzle  12623  uztrn  12628  eluzp1p1  12638  subeluzsub  12643  uzm1  12644  uznn0sub  12645  uz3m2nn  12659  1eluzge0  12660  2eluzge1  12662  raluz2  12665  rexuz2  12667  peano2uz  12669  nn0pzuz  12673  uzind4  12674  uzinfi  12696  zsupss  12705  nn01to3  12709  nn0ge2m1nnALT  12710  elfzuzb  13278  uzsubsubfz  13306  ssfzunsn  13330  ige2m1fz  13374  4fvwrd4  13404  elfzo2  13418  elfzouz2  13430  fzossrbm1  13444  fzossfzop1  13493  ssfzo12bi  13510  elfzonelfzo  13517  elfzomelpfzo  13519  fzosplitprm1  13525  fzostep1  13531  fzind2  13533  flword2  13561  fldiv4p1lem1div2  13583  uzsup  13611  modaddmodup  13682  fzsdom2  14171  swrdsbslen  14405  swrdspsleq  14406  pfxtrcfv0  14435  pfxtrcfvl  14438  pfxccatin12lem2a  14468  cshwidxmod  14544  rexuzre  15092  limsupgre  15218  rlimclim1  15282  rlimclim  15283  climrlim2  15284  isercolllem1  15404  isercoll  15407  climcndslem1  15589  fallfacval4  15781  oddge22np1  16086  nn0o  16120  bitsmod  16171  smueqlem  16225  dvdsnprmd  16423  2mulprm  16426  oddprmgt2  16432  oddprmge3  16433  ge2nprmge4  16434  modprm0  16534  prm23ge5  16544  vdwlem9  16718  prmgaplem3  16782  prmgaplem5  16784  prmgaplem6  16785  prmgaplem7  16786  strleun  16886  setsstruct  16905  fislw  19258  efgsp1  19371  efgredleme  19377  lt6abl  19524  telgsumfzs  19618  ablfac1eu  19704  znidomb  20797  chfacfscmul0  22035  chfacfscmulfsupp  22036  chfacfpmmul0  22039  chfacfpmmulfsupp  22040  dvfsumlem1  25218  dvfsumlem3  25220  plyaddlem1  25402  coeidlem  25426  2logb9irr  25973  ppisval  26281  chtdif  26335  ppidif  26340  ppiublem1  26378  ppiub  26380  chtub  26388  lgsdilem2  26509  gausslemma2dlem2  26543  gausslemma2dlem4  26545  gausslemma2dlem5  26547  gausslemma2dlem6  26548  lgsquadlem1  26556  lgsquadlem3  26558  2lgslem1  26570  chebbnd1lem1  26645  chebbnd1lem2  26646  chebbnd1lem3  26647  dchrisumlem2  26666  dchrvmasumiflem1  26677  mulog2sumlem2  26711  logdivbnd  26732  pntlemg  26774  pntlemq  26777  pntlemf  26781  axlowdim  27357  pthdlem1  28162  crctcshwlkn0lem3  28205  crctcshwlkn0lem4  28206  crctcshwlkn0lem5  28207  crctcshwlkn0lem6  28208  wwlksm1edg  28274  wwlksnred  28285  clwlkclwwlklem2fv1  28387  clwlkclwwlklem2  28392  clwwisshclwwslem  28406  clwwlkinwwlk  28432  clwwlkf  28439  clwwlkext2edg  28448  wwlksubclwwlk  28450  frgrreggt1  28785  ssnnssfz  31136  cycpmco2lem6  31426  ballotlemsdom  32506  ballotlemsel1i  32507  ballotlemfrceq  32523  signstfvc  32581  signstfveq0  32584  prodfzo03  32611  erdszelem8  33188  climuzcnv  33657  poimirlem6  35811  fdc  35931  sticksstones12  40140  eldioph2lem1  40605  hbt  40979  ssinc  42661  ssdec  42662  monoords  42870  fzdifsuc2  42883  eluzd  42983  fmul01lt1lem2  43161  sumnnodd  43206  ioodvbdlimc1lem2  43508  ioodvbdlimc2lem  43510  dvnmul  43519  dvnprodlem2  43523  itgspltprt  43555  stoweidlem11  43587  stoweidlem26  43602  wallispilem4  43644  fourierdlem12  43695  fourierdlem20  43703  fourierdlem41  43724  fourierdlem48  43730  fourierdlem49  43731  fourierdlem50  43732  fourierdlem54  43736  fourierdlem79  43761  fourierdlem102  43784  fourierdlem111  43793  fourierdlem114  43796  etransclem23  43833  etransclem48  43858  caratheodorylem1  44100  smfmullem4  44368  eluzge0nn0  44844  ssfz12  44846  elfzlble  44852  fzopredsuc  44855  fzoopth  44859  iccpartipre  44913  iccpartiltu  44914  iccpartgt  44919  fmtnoge3  45022  odz2prm2pw  45055  fmtnoprmfac2lem1  45058  fmtno4prmfac  45064  31prm  45089  lighneallem4b  45101  341fppr2  45226  9fppr8  45229  fpprel2  45233  nfermltl8rev  45234  nfermltl2rev  45235  gbegt5  45253  gbowgt5  45254  sbgoldbm  45276  mogoldbb  45277  sbgoldbo  45279  nnsum3primesle9  45286  nnsum4primesodd  45288  nnsum4primesoddALTV  45289  evengpop3  45290  evengpoap3  45291  nnsum4primeseven  45292  nnsum4primesevenALTV  45293  wtgoldbnnsum4prm  45294  bgoldbnnsum3prm  45296  bgoldbtbndlem3  45299  tgblthelfgott  45307  cznnring  45554  ssnn0ssfz  45725  elfzolborelfzop1  45900  m1modmmod  45907  rege1logbzge0  45945  fllog2  45954  nnolog2flm1  45976  dignn0ldlem  45988