Theorem eluz2 12757

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 12756	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12755	. . . 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 2113   class class class wbr 5098  ‘cfv 6492   ≤ cle 11167  ℤcz 12488  ℤ_≥cuz 12751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489  df-uz 12752

This theorem is referenced by:  eluzmn  12758  eluzuzle  12760  eluzelz  12761  eluzle  12764  uztrn  12769  eluzp1p1  12779  eluzadd  12780  eluzsub  12781  subeluzsub  12784  uzm1  12785  uznn0sub  12786  1eluzge0  12793  2eluzge1  12795  5eluz3  12796  uz3m2nn  12807  raluz2  12810  rexuz2  12812  peano2uz  12814  nn0pzuz  12818  uzind4  12819  uzinfi  12841  zsupss  12850  nn01to3  12854  nn0ge2m1nnALT  12855  elfzuzb  13434  uzsubsubfz  13462  ssfzunsn  13486  ige2m1fz  13533  fz0to4untppr  13546  fz0to5un2tp  13547  4fvwrd4  13564  elfzo2  13578  elfzouz2  13590  fzossrbm1  13604  fzossfzop1  13659  ssfzo12bi  13677  fzoopth  13678  elfzonelfzo  13685  elfzomelpfzo  13688  fzosplitprm1  13694  fzostep1  13702  fzind2  13704  flword2  13733  fldiv4p1lem1div2  13755  uzsup  13783  modaddmodup  13857  fzsdom2  14351  ccatdmss  14505  swrdsbslen  14588  swrdspsleq  14589  pfxtrcfv0  14617  pfxtrcfvl  14620  pfxccatin12lem2a  14650  cshwidxmod  14726  rexuzre  15276  limsupgre  15404  rlimclim1  15468  rlimclim  15469  climrlim2  15470  isercolllem1  15588  isercoll  15591  climcndslem1  15772  fallfacval4  15966  oddge22np1  16276  nn0o  16310  bitsmod  16363  smueqlem  16417  dvdsnprmd  16617  2mulprm  16620  oddprmgt2  16626  oddprmge3  16627  ge2nprmge4  16628  modprm0  16733  prm23ge5  16743  vdwlem9  16917  prmgaplem3  16981  prmgaplem5  16983  prmgaplem6  16984  prmgaplem7  16985  strleun  17084  setsstruct  17103  chnub  18545  fislw  19554  efgsp1  19666  efgredleme  19672  lt6abl  19824  telgsumfzs  19918  ablfac1eu  20004  znidomb  21516  chfacfscmul0  22802  chfacfscmulfsupp  22803  chfacfpmmul0  22806  chfacfpmmulfsupp  22807  dvfsumlem1  25988  dvfsumlem3  25991  plyaddlem1  26174  coeidlem  26198  2logb9irr  26761  ppisval  27070  chtdif  27124  ppidif  27129  ppiublem1  27169  ppiub  27171  chtub  27179  lgsdilem2  27300  gausslemma2dlem2  27334  gausslemma2dlem4  27336  gausslemma2dlem5  27338  gausslemma2dlem6  27339  lgsquadlem1  27347  lgsquadlem3  27349  2lgslem1  27361  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  dchrisumlem2  27457  dchrvmasumiflem1  27468  mulog2sumlem2  27502  logdivbnd  27523  pntlemg  27565  pntlemq  27568  pntlemf  27572  axlowdim  29034  pthdlem1  29839  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  wwlksm1edg  29954  wwlksnred  29965  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2  30075  clwwisshclwwslem  30089  clwwlkinwwlk  30115  clwwlkf  30122  clwwlkext2edg  30131  wwlksubclwwlk  30133  frgrreggt1  30468  ssnnssfz  32867  cycpmco2lem6  33213  ballotlemsdom  34669  ballotlemsel1i  34670  ballotlemfrceq  34686  signstfvc  34731  signstfveq0  34734  prodfzo03  34760  erdszelem8  35392  climuzcnv  35865  poimirlem6  37827  fdc  37946  sticksstones12  42412  eluzp1  42562  fimgmcyc  42789  eldioph2lem1  43002  hbt  43372  ssinc  45331  ssdec  45332  monoords  45545  fzdifsuc2  45558  eluzd  45653  fmul01lt1lem2  45831  sumnnodd  45876  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnmul  46187  dvnprodlem2  46191  itgspltprt  46223  stoweidlem11  46255  stoweidlem26  46270  wallispilem4  46312  fourierdlem12  46363  fourierdlem20  46371  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem54  46404  fourierdlem79  46429  fourierdlem102  46452  fourierdlem111  46461  fourierdlem114  46464  etransclem23  46501  etransclem48  46526  caratheodorylem1  46770  smfmullem4  47038  eluzge0nn0  47558  ssfz12  47560  elfzlble  47566  fzopredsuc  47569  ceilhalfelfzo1  47576  addmodne  47590  m1modnep2mod  47598  m1modmmod  47604  modm2nep1  47612  modp2nep1  47613  modm1nep2  47614  modm1nem2  47615  modm1p1ne  47616  iccpartipre  47667  iccpartiltu  47668  iccpartgt  47673  fmtnoge3  47776  odz2prm2pw  47809  fmtnoprmfac2lem1  47812  fmtno4prmfac  47818  31prm  47843  lighneallem4b  47855  341fppr2  47980  9fppr8  47983  fpprel2  47987  nfermltl8rev  47988  nfermltl2rev  47989  gbegt5  48007  gbowgt5  48008  sbgoldbm  48030  mogoldbb  48031  sbgoldbo  48033  nnsum3primesle9  48040  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  evengpop3  48044  evengpoap3  48045  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem3  48053  tgblthelfgott  48061  gpgusgralem  48302  gpgedgvtx1  48308  gpg5nbgrvtx13starlem2  48318  gpg3nbgrvtx0  48322  gpg3nbgrvtx0ALT  48323  gpg5nbgr3star  48327  gpg3kgrtriexlem3  48331  gpg3kgrtriexlem6  48334  gpg5edgnedg  48376  cznnring  48508  ssnn0ssfz  48595  elfzolborelfzop1  48765  rege1logbzge0  48805  fllog2  48814  nnolog2flm1  48836  dignn0ldlem  48848