Theorem eluz2 12788

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 12787	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1137	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12786	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 528	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 279	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1095	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 289	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 378	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493   ≤ cle 11174  ℤcz 12518  ℤ_≥cuz 12782

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519  df-uz 12783

This theorem is referenced by:  eluzmn  12789  eluzuzle  12791  eluzelz  12792  eluzle  12795  uztrn  12800  eluzp1p1  12810  eluzadd  12811  eluzsub  12812  subeluzsub  12815  uzm1  12816  uznn0sub  12817  1eluzge0  12824  2eluzge1  12826  5eluz3  12827  uz3m2nn  12838  raluz2  12841  rexuz2  12843  peano2uz  12845  nn0pzuz  12849  uzind4  12850  uzinfi  12872  zsupss  12881  nn01to3  12885  nn0ge2m1nnALT  12886  elfzuzb  13466  uzsubsubfz  13494  ssfzunsn  13518  ige2m1fz  13565  fz0to4untppr  13578  fz0to5un2tp  13579  4fvwrd4  13596  elfzo2  13610  elfzouz2  13623  fzossrbm1  13637  fzossfzop1  13692  ssfzo12bi  13710  fzoopth  13711  elfzonelfzo  13718  elfzomelpfzo  13721  fzosplitprm1  13727  fzostep1  13735  fzind2  13737  flword2  13766  fldiv4p1lem1div2  13788  uzsup  13816  modaddmodup  13890  fzsdom2  14384  ccatdmss  14538  swrdsbslen  14621  swrdspsleq  14622  pfxtrcfv0  14650  pfxtrcfvl  14653  pfxccatin12lem2a  14683  cshwidxmod  14759  rexuzre  15309  limsupgre  15437  rlimclim1  15501  rlimclim  15502  climrlim2  15503  isercolllem1  15621  isercoll  15624  climcndslem1  15808  fallfacval4  16002  oddge22np1  16312  nn0o  16346  bitsmod  16399  smueqlem  16453  dvdsnprmd  16653  2mulprm  16656  oddprmgt2  16663  oddprmge3  16664  ge2nprmge4  16665  modprm0  16770  prm23ge5  16780  vdwlem9  16954  prmgaplem3  17018  prmgaplem5  17020  prmgaplem6  17021  prmgaplem7  17022  strleun  17121  setsstruct  17140  chnub  18582  fislw  19594  efgsp1  19706  efgredleme  19712  lt6abl  19864  telgsumfzs  19958  ablfac1eu  20044  znidomb  21554  chfacfscmul0  22836  chfacfscmulfsupp  22837  chfacfpmmul0  22840  chfacfpmmulfsupp  22841  dvfsumlem1  26006  dvfsumlem3  26008  plyaddlem1  26191  coeidlem  26215  2logb9irr  26775  ppisval  27084  chtdif  27138  ppidif  27143  ppiublem1  27182  ppiub  27184  chtub  27192  lgsdilem2  27313  gausslemma2dlem2  27347  gausslemma2dlem4  27349  gausslemma2dlem5  27351  gausslemma2dlem6  27352  lgsquadlem1  27360  lgsquadlem3  27362  2lgslem1  27374  chebbnd1lem1  27449  chebbnd1lem2  27450  chebbnd1lem3  27451  dchrisumlem2  27470  dchrvmasumiflem1  27481  mulog2sumlem2  27515  logdivbnd  27536  pntlemg  27578  pntlemq  27581  pntlemf  27585  axlowdim  29047  pthdlem1  29852  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  wwlksm1edg  29967  wwlksnred  29978  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2  30088  clwwisshclwwslem  30102  clwwlkinwwlk  30128  clwwlkf  30135  clwwlkext2edg  30144  wwlksubclwwlk  30146  frgrreggt1  30481  ssnnssfz  32878  cycpmco2lem6  33210  ballotlemsdom  34675  ballotlemsel1i  34676  ballotlemfrceq  34692  signstfvc  34737  signstfveq0  34740  prodfzo03  34766  erdszelem8  35399  climuzcnv  35872  poimirlem6  37964  fdc  38083  sticksstones12  42614  eluzp1  42756  fimgmcyc  42996  eldioph2lem1  43209  hbt  43579  ssinc  45538  ssdec  45539  monoords  45751  fzdifsuc2  45764  eluzd  45858  fmul01lt1lem2  46036  sumnnodd  46081  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  dvnprodlem2  46396  itgspltprt  46428  stoweidlem11  46460  stoweidlem26  46475  wallispilem4  46517  fourierdlem12  46568  fourierdlem20  46576  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem54  46609  fourierdlem79  46634  fourierdlem102  46657  fourierdlem111  46666  fourierdlem114  46669  etransclem23  46706  etransclem48  46731  caratheodorylem1  46975  smfmullem4  47243  eluzge0nn0  47775  ssfz12  47777  elfzlble  47783  fzopredsuc  47787  ceilhalfelfzo1  47797  addmodne  47813  m1modnep2mod  47821  m1modmmod  47827  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  2timesltsqm1  47842  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartipre  47896  iccpartiltu  47897  iccpartgt  47902  fmtnoge3  48008  odz2prm2pw  48041  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  31prm  48075  lighneallem4b  48087  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem3  48100  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  341fppr2  48225  9fppr8  48228  fpprel2  48232  nfermltl8rev  48233  nfermltl2rev  48234  gbegt5  48252  gbowgt5  48253  sbgoldbm  48275  mogoldbb  48276  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  evengpop3  48289  evengpoap3  48290  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem3  48298  tgblthelfgott  48306  gpgusgralem  48547  gpgedgvtx1  48553  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  gpg3nbgrvtx0ALT  48568  gpg5nbgr3star  48572  gpg3kgrtriexlem3  48576  gpg3kgrtriexlem6  48579  gpg5edgnedg  48621  cznnring  48753  ssnn0ssfz  48840  elfzolborelfzop1  49010  rege1logbzge0  49050  fllog2  49059  nnolog2flm1  49081  dignn0ldlem  49093