Theorem eluz2 12909

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 12908	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12907	. . . 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 2108   class class class wbr 5166  ‘cfv 6573   ≤ cle 11325  ℤcz 12639  ℤ_≥cuz 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640  df-uz 12904

This theorem is referenced by:  eluzmn  12910  eluzuzle  12912  eluzelz  12913  eluzle  12916  uztrn  12921  eluzp1p1  12931  eluzadd  12932  eluzsub  12933  subeluzsub  12940  uzm1  12941  uznn0sub  12942  uz3m2nn  12956  1eluzge0  12957  2eluzge1  12959  raluz2  12962  rexuz2  12964  peano2uz  12966  nn0pzuz  12970  uzind4  12971  uzinfi  12993  zsupss  13002  nn01to3  13006  nn0ge2m1nnALT  13007  elfzuzb  13578  uzsubsubfz  13606  ssfzunsn  13630  ige2m1fz  13674  fz0to4untppr  13687  fz0to5un2tp  13688  4fvwrd4  13705  elfzo2  13719  elfzouz2  13731  fzossrbm1  13745  fzossfzop1  13794  ssfzo12bi  13811  fzoopth  13812  elfzonelfzo  13819  elfzomelpfzo  13821  fzosplitprm1  13827  fzostep1  13833  fzind2  13835  flword2  13864  fldiv4p1lem1div2  13886  uzsup  13914  modaddmodup  13985  fzsdom2  14477  swrdsbslen  14712  swrdspsleq  14713  pfxtrcfv0  14742  pfxtrcfvl  14745  pfxccatin12lem2a  14775  cshwidxmod  14851  rexuzre  15401  limsupgre  15527  rlimclim1  15591  rlimclim  15592  climrlim2  15593  isercolllem1  15713  isercoll  15716  climcndslem1  15897  fallfacval4  16091  oddge22np1  16397  nn0o  16431  bitsmod  16482  smueqlem  16536  dvdsnprmd  16737  2mulprm  16740  oddprmgt2  16746  oddprmge3  16747  ge2nprmge4  16748  modprm0  16852  prm23ge5  16862  vdwlem9  17036  prmgaplem3  17100  prmgaplem5  17102  prmgaplem6  17103  prmgaplem7  17104  strleun  17204  setsstruct  17223  fislw  19667  efgsp1  19779  efgredleme  19785  lt6abl  19937  telgsumfzs  20031  ablfac1eu  20117  znidomb  21603  chfacfscmul0  22885  chfacfscmulfsupp  22886  chfacfpmmul0  22889  chfacfpmmulfsupp  22890  dvfsumlem1  26086  dvfsumlem3  26089  plyaddlem1  26272  coeidlem  26296  2logb9irr  26856  ppisval  27165  chtdif  27219  ppidif  27224  ppiublem1  27264  ppiub  27266  chtub  27274  lgsdilem2  27395  gausslemma2dlem2  27429  gausslemma2dlem4  27431  gausslemma2dlem5  27433  gausslemma2dlem6  27434  lgsquadlem1  27442  lgsquadlem3  27444  2lgslem1  27456  chebbnd1lem1  27531  chebbnd1lem2  27532  chebbnd1lem3  27533  dchrisumlem2  27552  dchrvmasumiflem1  27563  mulog2sumlem2  27597  logdivbnd  27618  pntlemg  27660  pntlemq  27663  pntlemf  27667  axlowdim  28994  pthdlem1  29802  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  wwlksm1edg  29914  wwlksnred  29925  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2  30032  clwwisshclwwslem  30046  clwwlkinwwlk  30072  clwwlkf  30079  clwwlkext2edg  30088  wwlksubclwwlk  30090  frgrreggt1  30425  ssnnssfz  32792  ccatdmss  32916  chnub  32984  cycpmco2lem6  33124  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemfrceq  34493  signstfvc  34551  signstfveq0  34554  prodfzo03  34580  erdszelem8  35166  climuzcnv  35639  poimirlem6  37586  fdc  37705  sticksstones12  42115  eluzp1  42295  fimgmcyc  42489  eldioph2lem1  42716  hbt  43087  ssinc  44989  ssdec  44990  monoords  45212  fzdifsuc2  45225  eluzd  45324  fmul01lt1lem2  45506  sumnnodd  45551  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  dvnprodlem2  45868  itgspltprt  45900  stoweidlem11  45932  stoweidlem26  45947  wallispilem4  45989  fourierdlem12  46040  fourierdlem20  46048  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem54  46081  fourierdlem79  46106  fourierdlem102  46129  fourierdlem111  46138  fourierdlem114  46141  etransclem23  46178  etransclem48  46203  caratheodorylem1  46447  smfmullem4  46715  eluzge0nn0  47227  ssfz12  47229  elfzlble  47235  fzopredsuc  47238  iccpartipre  47295  iccpartiltu  47296  iccpartgt  47301  fmtnoge3  47404  odz2prm2pw  47437  fmtnoprmfac2lem1  47440  fmtno4prmfac  47446  31prm  47471  lighneallem4b  47483  341fppr2  47608  9fppr8  47611  fpprel2  47615  nfermltl8rev  47616  nfermltl2rev  47617  gbegt5  47635  gbowgt5  47636  sbgoldbm  47658  mogoldbb  47659  sbgoldbo  47661  nnsum3primesle9  47668  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  evengpop3  47672  evengpoap3  47673  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem3  47681  tgblthelfgott  47689  cznnring  47985  ssnn0ssfz  48074  elfzolborelfzop1  48248  m1modmmod  48255  rege1logbzge0  48293  fllog2  48302  nnolog2flm1  48324  dignn0ldlem  48336