Theorem eluz2 12755

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 12754	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12753	. . . 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 5096  ‘cfv 6490   ≤ cle 11165  ℤcz 12486  ℤ_≥cuz 12749

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-cnex 11080  ax-resscn 11081

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487  df-uz 12750

This theorem is referenced by:  eluzmn  12756  eluzuzle  12758  eluzelz  12759  eluzle  12762  uztrn  12767  eluzp1p1  12777  eluzadd  12778  eluzsub  12779  subeluzsub  12782  uzm1  12783  uznn0sub  12784  1eluzge0  12791  2eluzge1  12793  5eluz3  12794  uz3m2nn  12805  raluz2  12808  rexuz2  12810  peano2uz  12812  nn0pzuz  12816  uzind4  12817  uzinfi  12839  zsupss  12848  nn01to3  12852  nn0ge2m1nnALT  12853  elfzuzb  13432  uzsubsubfz  13460  ssfzunsn  13484  ige2m1fz  13531  fz0to4untppr  13544  fz0to5un2tp  13545  4fvwrd4  13562  elfzo2  13576  elfzouz2  13588  fzossrbm1  13602  fzossfzop1  13657  ssfzo12bi  13675  fzoopth  13676  elfzonelfzo  13683  elfzomelpfzo  13686  fzosplitprm1  13692  fzostep1  13700  fzind2  13702  flword2  13731  fldiv4p1lem1div2  13753  uzsup  13781  modaddmodup  13855  fzsdom2  14349  ccatdmss  14503  swrdsbslen  14586  swrdspsleq  14587  pfxtrcfv0  14615  pfxtrcfvl  14618  pfxccatin12lem2a  14648  cshwidxmod  14724  rexuzre  15274  limsupgre  15402  rlimclim1  15466  rlimclim  15467  climrlim2  15468  isercolllem1  15586  isercoll  15589  climcndslem1  15770  fallfacval4  15964  oddge22np1  16274  nn0o  16308  bitsmod  16361  smueqlem  16415  dvdsnprmd  16615  2mulprm  16618  oddprmgt2  16624  oddprmge3  16625  ge2nprmge4  16626  modprm0  16731  prm23ge5  16741  vdwlem9  16915  prmgaplem3  16979  prmgaplem5  16981  prmgaplem6  16982  prmgaplem7  16983  strleun  17082  setsstruct  17101  chnub  18543  fislw  19552  efgsp1  19664  efgredleme  19670  lt6abl  19822  telgsumfzs  19916  ablfac1eu  20002  znidomb  21514  chfacfscmul0  22800  chfacfscmulfsupp  22801  chfacfpmmul0  22804  chfacfpmmulfsupp  22805  dvfsumlem1  25986  dvfsumlem3  25989  plyaddlem1  26172  coeidlem  26196  2logb9irr  26759  ppisval  27068  chtdif  27122  ppidif  27127  ppiublem1  27167  ppiub  27169  chtub  27177  lgsdilem2  27298  gausslemma2dlem2  27332  gausslemma2dlem4  27334  gausslemma2dlem5  27336  gausslemma2dlem6  27337  lgsquadlem1  27345  lgsquadlem3  27347  2lgslem1  27359  chebbnd1lem1  27434  chebbnd1lem2  27435  chebbnd1lem3  27436  dchrisumlem2  27455  dchrvmasumiflem1  27466  mulog2sumlem2  27500  logdivbnd  27521  pntlemg  27563  pntlemq  27566  pntlemf  27570  axlowdim  28983  pthdlem1  29788  crctcshwlkn0lem3  29834  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  crctcshwlkn0lem6  29837  wwlksm1edg  29903  wwlksnred  29914  clwlkclwwlklem2fv1  30019  clwlkclwwlklem2  30024  clwwisshclwwslem  30038  clwwlkinwwlk  30064  clwwlkf  30071  clwwlkext2edg  30080  wwlksubclwwlk  30082  frgrreggt1  30417  ssnnssfz  32816  cycpmco2lem6  33162  ballotlemsdom  34618  ballotlemsel1i  34619  ballotlemfrceq  34635  signstfvc  34680  signstfveq0  34683  prodfzo03  34709  erdszelem8  35341  climuzcnv  35814  poimirlem6  37766  fdc  37885  sticksstones12  42351  eluzp1  42504  fimgmcyc  42731  eldioph2lem1  42944  hbt  43314  ssinc  45273  ssdec  45274  monoords  45487  fzdifsuc2  45500  eluzd  45595  fmul01lt1lem2  45773  sumnnodd  45818  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  dvnprodlem2  46133  itgspltprt  46165  stoweidlem11  46197  stoweidlem26  46212  wallispilem4  46254  fourierdlem12  46305  fourierdlem20  46313  fourierdlem41  46334  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem54  46346  fourierdlem79  46371  fourierdlem102  46394  fourierdlem111  46403  fourierdlem114  46406  etransclem23  46443  etransclem48  46468  caratheodorylem1  46712  smfmullem4  46980  eluzge0nn0  47500  ssfz12  47502  elfzlble  47508  fzopredsuc  47511  ceilhalfelfzo1  47518  addmodne  47532  m1modnep2mod  47540  m1modmmod  47546  modm2nep1  47554  modp2nep1  47555  modm1nep2  47556  modm1nem2  47557  modm1p1ne  47558  iccpartipre  47609  iccpartiltu  47610  iccpartgt  47615  fmtnoge3  47718  odz2prm2pw  47751  fmtnoprmfac2lem1  47754  fmtno4prmfac  47760  31prm  47785  lighneallem4b  47797  341fppr2  47922  9fppr8  47925  fpprel2  47929  nfermltl8rev  47930  nfermltl2rev  47931  gbegt5  47949  gbowgt5  47950  sbgoldbm  47972  mogoldbb  47973  sbgoldbo  47975  nnsum3primesle9  47982  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  evengpop3  47986  evengpoap3  47987  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  bgoldbtbndlem3  47995  tgblthelfgott  48003  gpgusgralem  48244  gpgedgvtx1  48250  gpg5nbgrvtx13starlem2  48260  gpg3nbgrvtx0  48264  gpg3nbgrvtx0ALT  48265  gpg5nbgr3star  48269  gpg3kgrtriexlem3  48273  gpg3kgrtriexlem6  48276  gpg5edgnedg  48318  cznnring  48450  ssnn0ssfz  48537  elfzolborelfzop1  48707  rege1logbzge0  48747  fllog2  48756  nnolog2flm1  48778  dignn0ldlem  48790