Theorem eluz2 12250

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 12249	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1132	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12248	. . . 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 5066  ‘cfv 6355   ≤ cle 10676  ℤcz 11982  ℤ_≥cuz 12244

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 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-cnex 10593  ax-resscn 10594

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983  df-uz 12245

This theorem is referenced by:  eluzmn  12251  eluzuzle  12253  eluzelz  12254  eluzle  12257  uztrn  12262  eluzp1p1  12271  subeluzsub  12276  uzm1  12277  uznn0sub  12278  uz3m2nn  12292  1eluzge0  12293  2eluzge1  12295  raluz2  12298  rexuz2  12300  peano2uz  12302  nn0pzuz  12306  uzind4  12307  uzinfi  12329  zsupss  12338  nn01to3  12342  nn0ge2m1nnALT  12343  elfzuzb  12903  uzsubsubfz  12930  ssfzunsnext  12953  ssfzunsn  12954  ige2m1fz  12998  4fvwrd4  13028  elfzo2  13042  elfzouz2  13053  fzossrbm1  13067  fzossfzop1  13116  ssfzo12bi  13133  elfzonelfzo  13140  elfzomelpfzo  13142  fzosplitprm1  13148  fzostep1  13154  fzind2  13156  flword2  13184  fldiv4p1lem1div2  13206  uzsup  13232  modaddmodup  13303  fzsdom2  13790  swrdsbslen  14026  swrdspsleq  14027  pfxtrcfv0  14056  pfxtrcfvl  14059  pfxccatin12lem2a  14089  cshwidxmod  14165  rexuzre  14712  limsupgre  14838  rlimclim1  14902  rlimclim  14903  climrlim2  14904  isercolllem1  15021  isercoll  15024  climcndslem1  15204  fallfacval4  15397  oddge22np1  15698  nn0o  15734  bitsmod  15785  smueqlem  15839  dvdsnprmd  16034  2mulprm  16037  oddprmgt2  16043  oddprmge3  16044  ge2nprmge4  16045  modprm0  16142  prm23ge5  16152  vdwlem9  16325  prmgaplem3  16389  prmgaplem5  16391  prmgaplem6  16392  prmgaplem7  16393  setsstruct  16523  strleun  16591  fislw  18750  efgsp1  18863  efgredleme  18869  lt6abl  19015  telgsumfzs  19109  ablfac1eu  19195  znidomb  20708  chfacfscmul0  21466  chfacfscmulfsupp  21467  chfacfpmmul0  21470  chfacfpmmulfsupp  21471  dvfsumlem1  24623  dvfsumlem3  24625  plyaddlem1  24803  coeidlem  24827  2logb9irr  25373  ppisval  25681  chtdif  25735  ppidif  25740  ppiublem1  25778  ppiub  25780  chtub  25788  lgsdilem2  25909  gausslemma2dlem2  25943  gausslemma2dlem4  25945  gausslemma2dlem5  25947  gausslemma2dlem6  25948  lgsquadlem1  25956  lgsquadlem3  25958  2lgslem1  25970  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  dchrisumlem2  26066  dchrvmasumiflem1  26077  mulog2sumlem2  26111  logdivbnd  26132  pntlemg  26174  pntlemq  26177  pntlemf  26181  axlowdim  26747  pthdlem1  27547  crctcshwlkn0lem3  27590  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  wwlksm1edg  27659  wwlksnred  27670  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2  27778  clwwisshclwwslem  27792  clwwlkinwwlk  27818  clwwlkf  27826  clwwlkext2edg  27835  wwlksubclwwlk  27837  frgrreggt1  28172  ssnnssfz  30510  cycpmco2lem6  30773  ballotlemsdom  31769  ballotlemsel1i  31770  ballotlemfrceq  31786  signstfvc  31844  signstfveq0  31847  prodfzo03  31874  erdszelem8  32445  climuzcnv  32914  poimirlem6  34913  fdc  35035  eldioph2lem1  39406  hbt  39779  ssinc  41402  ssdec  41403  monoords  41613  fzdifsuc2  41626  eluzd  41731  fmul01lt1lem2  41915  sumnnodd  41960  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnmul  42277  dvnprodlem2  42281  itgspltprt  42313  stoweidlem11  42345  stoweidlem26  42360  wallispilem4  42402  fourierdlem12  42453  fourierdlem20  42461  fourierdlem41  42482  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem54  42494  fourierdlem79  42519  fourierdlem102  42542  fourierdlem111  42551  fourierdlem114  42554  etransclem23  42591  etransclem48  42616  caratheodorylem1  42857  smfmullem4  43118  eluzge0nn0  43561  ssfz12  43563  elfzlble  43569  fzopredsuc  43572  fzoopth  43576  iccpartipre  43630  iccpartiltu  43631  iccpartgt  43636  fmtnoge3  43741  odz2prm2pw  43774  fmtnoprmfac2lem1  43777  fmtno4prmfac  43783  31prm  43809  lighneallem4b  43823  341fppr2  43948  9fppr8  43951  fpprel2  43955  nfermltl8rev  43956  nfermltl2rev  43957  gbegt5  43975  gbowgt5  43976  sbgoldbm  43998  mogoldbb  43999  sbgoldbo  44001  nnsum3primesle9  44008  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  evengpop3  44012  evengpoap3  44013  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  bgoldbtbndlem3  44021  tgblthelfgott  44029  cznnring  44276  ssnn0ssfz  44446  elfzolborelfzop1  44623  m1modmmod  44630  rege1logbzge0  44668  fllog2  44677  nnolog2flm1  44699  dignn0ldlem  44711