Theorem eluz2 12894

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 12893	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1154	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12892	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 538	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 282	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1111	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 381	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533   ≤ cle 11269  ℤcz 12616  ℤ_≥cuz 12888

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-neg 11469  df-z 12617  df-uz 12889

This theorem is used by:  eluzmn  12895  eluzuzle  12897  eluzelz  12898  eluzle  12901  uztrn  12906  eluzp1p1  12916  eluzadd  12917  eluzsub  12918  subeluzsub  12921  uzm1  12922  uznn0sub  12923  1eluzge0  12930  2eluzge1  12932  5eluz3  12933  uz3m2nn  12944  raluz2  12947  rexuz2  12949  peano2uz  12951  nn0pzuz  12955  uzind4  12956  uzinfi  12978  zsupss  12987  nn01to3  12991  nn0ge2m1nnALT  12992  elfzuzb  13573  uzsubsubfz  13602  ssfzunsn  13626  ige2m1fz  13673  fz0to4untppr  13686  fz0to5un2tp  13687  4fvwrd4  13704  elfzo2  13718  elfzouz2  13731  fzossrbm1  13745  fzossfzop1  13800  ssfzo12bi  13818  fzoopth  13819  elfzonelfzo  13826  elfzomelpfzo  13829  fzosplitprm1  13835  fzostep1  13843  fzind2  13845  flword2  13875  fldiv4p1lem1div2  13897  uzsup  13925  modaddmodup  13999  fzsdom2  14494  ccatdmss  14648  swrdsbslen  14735  swrdspsleq  14736  pfxtrcfv0  14764  pfxtrcfvl  14767  pfxccatin12lem2a  14797  cshwidxmod  14875  rexuzre  15441  limsupgre  15569  rlimclim1  15633  rlimclim  15634  climrlim2  15635  isercolllem1  15753  isercoll  15756  climcndslem1  15939  fallfacval4  16130  oddge22np1  16440  nn0o  16474  bitsmod  16527  smueqlem  16581  dvdsnprmd  16781  2mulprm  16784  oddprmgt2  16791  oddprmge3  16792  ge2nprmge4  16793  modprm0  16898  prm23ge5  16908  vdwlem9  17082  prmgaplem3  17146  prmgaplem5  17148  prmgaplem6  17149  prmgaplem7  17150  strleun  17250  setsstruct  17269  chnub  18711  fislw  19753  efgsp1  19865  efgredleme  19871  lt6abl  20023  telgsumfzs  20117  ablfac1eu  20203  znidomb  21775  chfacfscmul0  23084  chfacfscmulfsupp  23085  chfacfpmmul0  23088  chfacfpmmulfsupp  23089  dvfsumlem1  26254  dvfsumlem3  26256  plyaddlem1  26440  coeidlem  26464  2logb9irr  27033  ppisval  27341  chtdif  27395  ppidif  27400  ppiublem1  27439  ppiub  27441  chtub  27449  lgsdilem2  27570  gausslemma2dlem2  27604  gausslemma2dlem4  27606  gausslemma2dlem5  27608  gausslemma2dlem6  27609  lgsquadlem1  27617  lgsquadlem3  27619  2lgslem1  27631  chebbnd1lem1  27706  chebbnd1lem2  27707  chebbnd1lem3  27708  dchrisumlem2  27727  dchrvmasumiflem1  27738  mulog2sumlem2  27772  logdivbnd  27793  pntlemg  27835  pntlemq  27838  pntlemf  27842  axlowdim  29419  pthdlem1  30232  crctcshwlkn0lem3  30281  crctcshwlkn0lem4  30282  crctcshwlkn0lem5  30283  crctcshwlkn0lem6  30284  wwlksm1edg  30350  wwlksnred  30361  clwlkclwwlklem2fv1  30466  clwlkclwwlklem2  30471  clwwisshclwwslem  30485  clwwlkinwwlk  30511  clwwlkf  30518  clwwlkext2edg  30527  wwlksubclwwlk  30529  frgrreggt1  30874  ssnnssfz  33259  cycpmco2lem6  33572  ballotlemsdom  35024  ballotlemsel1i  35025  ballotlemfrceq  35041  signstfvc  35083  signstfveq0  35086  prodfzo03  35112  erdszelem8  35778  climuzcnv  36251  poimirlem6  38376  fdc  38496  sticksstones12  43025  eluzp1  43183  fimgmcyc  43417  eldioph2lem1  43606  hbt  43972  ssinc  45920  ssdec  45921  monoords  46131  fzdifsuc2  46144  eluzd  46238  fmul01lt1lem2  46416  sumnnodd  46461  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnmul  46772  dvnprodlem2  46776  itgspltprt  46808  stoweidlem11  46840  stoweidlem26  46855  wallispilem4  46897  fourierdlem12  46948  fourierdlem20  46956  fourierdlem41  46977  fourierdlem50  46985  fourierdlem54  46989  fourierdlem79  47014  fourierdlem102  47037  fourierdlem111  47046  fourierdlem114  47049  etransclem23  47086  etransclem48  47111  caratheodorylem1  47355  smfmullem4  47623  eluzge0nn0  48201  ssfz12  48203  elfzlble  48209  fzopredsuc  48213  ceilhalfelfzo1  48223  addmodne  48239  m1modnep2mod  48247  m1modmmod  48253  modm2nep1  48261  modp2nep1  48262  modm1nep2  48263  modm1nem2  48264  modm1p1ne  48265  2timesltsqm1  48268  muldvdsfacgt  48275  muldvdsfacm1  48276  iccpartipre  48322  iccpartiltu  48323  iccpartgt  48328  fmtnoge3  48434  odz2prm2pw  48467  fmtnoprmfac2lem1  48470  fmtno4prmfac  48476  31prm  48501  lighneallem4b  48513  nprmdvdsfacm1lem2  48525  nprmdvdsfacm1lem3  48526  nprmdvdsfacm1lem4  48527  nprmdvdsfacm1  48528  ppivalnnnprmge6  48530  341fppr2  48651  9fppr8  48654  fpprel2  48658  nfermltl8rev  48659  nfermltl2rev  48660  gbegt5  48678  gbowgt5  48679  sbgoldbm  48701  mogoldbb  48702  sbgoldbo  48704  nnsum3primesle9  48711  nnsum4primesodd  48713  nnsum4primesoddALTV  48714  evengpop3  48715  evengpoap3  48716  nnsum4primeseven  48717  nnsum4primesevenALTV  48718  wtgoldbnnsum4prm  48719  bgoldbnnsum3prm  48721  bgoldbtbndlem3  48724  tgblthelfgott  48732  gpgusgralem  48973  gpgedgvtx1  48979  gpg5nbgrvtx13starlem2  48989  gpg3nbgrvtx0  48993  gpg3nbgrvtx0ALT  48994  gpg5nbgr3star  48998  gpg3kgrtriexlem3  49002  gpg3kgrtriexlem6  49005  gpg5edgnedg  49047  cznnring  49178  ssnn0ssfz  49280  elfzolborelfzop1  49450  rege1logbzge0  49490  fllog2  49499  nnolog2flm1  49521  dignn0ldlem  49533