Theorem eluz2 12252

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 12251	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1132	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12250	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 531	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 281	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1091	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	syl6bbr 291	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 382	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   ∈ wcel 2114   class class class wbr 5068  ‘cfv 6357   ≤ cle 10678  ℤcz 11984  ℤ_≥cuz 12246

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-cnex 10595  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-ov 7161  df-neg 10875  df-z 11985  df-uz 12247

This theorem is referenced by:  eluzmn  12253  eluzuzle  12255  eluzelz  12256  eluzle  12259  uztrn  12264  eluzp1p1  12273  subeluzsub  12278  uzm1  12279  uznn0sub  12280  uz3m2nn  12294  1eluzge0  12295  2eluzge1  12297  raluz2  12300  rexuz2  12302  peano2uz  12304  nn0pzuz  12308  uzind4  12309  uzinfi  12331  zsupss  12340  nn01to3  12344  nn0ge2m1nnALT  12345  elfzuzb  12905  uzsubsubfz  12932  ssfzunsnext  12955  ssfzunsn  12956  ige2m1fz  13000  4fvwrd4  13030  elfzo2  13044  elfzouz2  13055  fzossrbm1  13069  fzossfzop1  13118  ssfzo12bi  13135  elfzonelfzo  13142  elfzomelpfzo  13144  fzosplitprm1  13150  fzostep1  13156  fzind2  13158  flword2  13186  fldiv4p1lem1div2  13208  uzsup  13234  modaddmodup  13305  fzsdom2  13792  swrdsbslen  14028  swrdspsleq  14029  pfxtrcfv0  14058  pfxtrcfvl  14061  pfxccatin12lem2a  14091  cshwidxmod  14167  rexuzre  14714  limsupgre  14840  rlimclim1  14904  rlimclim  14905  climrlim2  14906  isercolllem1  15023  isercoll  15026  climcndslem1  15206  fallfacval4  15399  oddge22np1  15700  nn0o  15736  bitsmod  15787  smueqlem  15841  dvdsnprmd  16036  2mulprm  16039  oddprmgt2  16045  oddprmge3  16046  ge2nprmge4  16047  modprm0  16144  prm23ge5  16154  vdwlem9  16327  prmgaplem3  16391  prmgaplem5  16393  prmgaplem6  16394  prmgaplem7  16395  setsstruct  16525  strleun  16593  fislw  18752  efgsp1  18865  efgredleme  18871  lt6abl  19017  telgsumfzs  19111  ablfac1eu  19197  znidomb  20710  chfacfscmul0  21468  chfacfscmulfsupp  21469  chfacfpmmul0  21472  chfacfpmmulfsupp  21473  dvfsumlem1  24625  dvfsumlem3  24627  plyaddlem1  24805  coeidlem  24829  2logb9irr  25375  ppisval  25683  chtdif  25737  ppidif  25742  ppiublem1  25780  ppiub  25782  chtub  25790  lgsdilem2  25911  gausslemma2dlem2  25945  gausslemma2dlem4  25947  gausslemma2dlem5  25949  gausslemma2dlem6  25950  lgsquadlem1  25958  lgsquadlem3  25960  2lgslem1  25972  chebbnd1lem1  26047  chebbnd1lem2  26048  chebbnd1lem3  26049  dchrisumlem2  26068  dchrvmasumiflem1  26079  mulog2sumlem2  26113  logdivbnd  26134  pntlemg  26176  pntlemq  26179  pntlemf  26183  axlowdim  26749  pthdlem1  27549  crctcshwlkn0lem3  27592  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  crctcshwlkn0lem6  27595  wwlksm1edg  27661  wwlksnred  27672  clwlkclwwlklem2fv1  27775  clwlkclwwlklem2  27780  clwwisshclwwslem  27794  clwwlkinwwlk  27820  clwwlkf  27828  clwwlkext2edg  27837  wwlksubclwwlk  27839  frgrreggt1  28174  ssnnssfz  30512  cycpmco2lem6  30775  ballotlemsdom  31771  ballotlemsel1i  31772  ballotlemfrceq  31788  signstfvc  31846  signstfveq0  31849  prodfzo03  31876  erdszelem8  32447  climuzcnv  32916  poimirlem6  34900  fdc  35022  eldioph2lem1  39364  hbt  39737  ssinc  41360  ssdec  41361  monoords  41571  fzdifsuc2  41584  eluzd  41689  fmul01lt1lem2  41873  sumnnodd  41918  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnmul  42235  dvnprodlem2  42239  itgspltprt  42271  stoweidlem11  42303  stoweidlem26  42318  wallispilem4  42360  fourierdlem12  42411  fourierdlem20  42419  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem54  42452  fourierdlem79  42477  fourierdlem102  42500  fourierdlem111  42509  fourierdlem114  42512  etransclem23  42549  etransclem48  42574  caratheodorylem1  42815  smfmullem4  43076  eluzge0nn0  43519  ssfz12  43521  elfzlble  43527  fzopredsuc  43530  fzoopth  43534  iccpartipre  43588  iccpartiltu  43589  iccpartgt  43594  fmtnoge3  43699  odz2prm2pw  43732  fmtnoprmfac2lem1  43735  fmtno4prmfac  43741  31prm  43767  lighneallem4b  43781  341fppr2  43906  9fppr8  43909  fpprel2  43913  nfermltl8rev  43914  nfermltl2rev  43915  gbegt5  43933  gbowgt5  43934  sbgoldbm  43956  mogoldbb  43957  sbgoldbo  43959  nnsum3primesle9  43966  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  evengpop3  43970  evengpoap3  43971  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  wtgoldbnnsum4prm  43974  bgoldbnnsum3prm  43976  bgoldbtbndlem3  43979  tgblthelfgott  43987  cznnring  44234  ssnn0ssfz  44404  elfzolborelfzop1  44581  m1modmmod  44588  rege1logbzge0  44626  fllog2  44635  nnolog2flm1  44657  dignn0ldlem  44669