Theorem eluz2 11569

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 11568	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1054	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 11567	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 524	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 267	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1035	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	syl6bbr 277	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 367	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   ∈ wcel 1977   class class class wbr 4583  ‘cfv 5804   ≤ cle 9954  ℤcz 11254  ℤ_≥cuz 11563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255  df-uz 11564

This theorem is referenced by:  eluzmn  11570  eluzuzle  11572  eluzelz  11573  eluzle  11576  uztrn  11580  eluzp1p1  11589  uzm1  11594  uznn0sub  11595  uz3m2nn  11607  1eluzge0  11608  2eluzge1  11610  raluz2  11613  rexuz2  11615  peano2uz  11617  nn0pzuz  11621  uzind4  11622  uzinfi  11644  zsupss  11653  nn01to3  11657  nn0ge2m1nnALT  11658  elfzuzb  12207  uzsubsubfz  12234  ssfzunsn  12257  ige2m1fz  12299  4fvwrd4  12328  elfzo2  12342  elfzouz2  12353  fzossrbm1  12366  fzossfzop1  12412  ssfzo12bi  12429  elfzonelfzo  12436  elfzomelpfzo  12438  fzosplitprm1  12443  fzostep1  12446  fzind2  12448  flword2  12476  fldiv4p1lem1div2  12498  uzsup  12524  modaddmodup  12595  fzsdom2  13075  swrdtrcfv0  13294  swrdsbslen  13300  swrdspsleq  13301  swrdtrcfvl  13302  swrdccatin12lem2a  13336  cshwidxmod  13400  rexuzre  13940  limsupgre  14060  rlimclim1  14124  rlimclim  14125  climrlim2  14126  isercolllem1  14243  isercoll  14246  climcndslem1  14420  fallfacval4  14613  oddge22np1  14911  nn0o  14937  bitsmod  14996  smueqlem  15050  dvdsnprmd  15241  prmgt1  15247  oddprmgt2  15249  oddprmge3  15250  modprm0  15348  prm23ge5  15358  vdwlem9  15531  prmgaplem3  15595  prmgaplem5  15597  prmgaplem6  15598  prmgaplem7  15599  strlemor1  15796  strleun  15799  fislw  17863  efgsp1  17973  efgredleme  17979  lt6abl  18119  telgsumfzs  18209  ablfac1eu  18295  znidomb  19729  chfacfscmul0  20482  chfacfscmulfsupp  20483  chfacfpmmul0  20486  chfacfpmmulfsupp  20487  dvfsumlem1  23593  dvfsumlem3  23595  plyaddlem1  23773  coeidlem  23797  ppisval  24630  chtdif  24684  ppidif  24689  ppiublem1  24727  ppiub  24729  chtub  24737  lgsdilem2  24858  gausslemma2dlem2  24892  gausslemma2dlem4  24894  gausslemma2dlem5  24896  gausslemma2dlem6  24897  lgsquadlem1  24905  lgsquadlem3  24907  2lgslem1  24919  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  dchrisumlem2  24979  dchrvmasumiflem1  24990  mulog2sumlem2  25024  logdivbnd  25045  pntlemg  25087  pntlemq  25090  pntlemf  25094  axlowdim  25641  4cycl4v4e  26194  4cycl4dv4e  26196  wwlknred  26251  wwlkm1edg  26263  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem1  26315  clwwlkf  26322  clwwlkext2edg  26330  wwlksubclwwlk  26332  clwwisshclwwlem  26334  usg2cwwkdifex  26349  clwlkfclwwlk  26371  eupath2lem3  26506  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  ssnnssfz  28937  ballotlemsdom  29900  ballotlemsel1i  29901  ballotlemfrceq  29917  signstfvc  29977  signstfveq0  29980  erdszelem8  30434  climuzcnv  30819  poimirlem6  32585  fdc  32711  eldioph2lem1  36341  hbt  36719  ssinc  38292  ssdec  38293  monoords  38452  fzdifsuc2  38466  fmul01lt1lem2  38652  sumnnodd  38697  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  dvnprodlem2  38837  itgspltprt  38871  stoweidlem11  38904  stoweidlem26  38919  wallispilem4  38961  fourierdlem12  39012  fourierdlem20  39020  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem54  39053  fourierdlem79  39078  fourierdlem102  39101  fourierdlem111  39110  fourierdlem114  39113  etransclem23  39150  etransclem48  39175  caratheodorylem1  39416  smfmullem4  39679  fzopredsuc  39946  iccpartipre  39959  iccpartiltu  39960  iccpartgt  39965  fmtnoge3  39980  odz2prm2pw  40013  fmtnoprmfac2lem1  40016  fmtno4prmfac  40022  31prm  40050  lighneallem4b  40064  gbegt5  40183  gbogt5  40184  nnsum3primesle9  40210  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  evengpop3  40214  evengpoap3  40215  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem3  40223  tgblthelfgott  40229  tgblthelfgottOLD  40236  pfxtrcfv0  40265  pfxtrcfvl  40268  eluzge0nn0  40350  ssfz12  40351  elfzlble  40357  fzoopth  40360  pthdlem1  40972  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  wwlksm1edg  41078  wwlksnred  41098  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2  41209  clwwlksf  41222  clwwlksext2edg  41230  wwlksubclwwlks  41232  clwwisshclwwslem  41234  clwlksfclwwlk  41269  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  av-frgrareggt1  41547  cznnring  41748  ssnn0ssfz  41920  elfzolborelfzop1  42103  m1modmmod  42110  rege1logbzge0  42151  fllog2  42160  nnolog2flm1  42182  dignn0ldlem  42194