Theorem eluz2 12099

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 12098	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1129	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12097	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 529	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 280	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1088	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	syl6bbr 290	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 380	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   ∈ wcel 2081   class class class wbr 4962  ‘cfv 6225   ≤ cle 10522  ℤcz 11829  ℤ_≥cuz 12093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-cnex 10439  ax-resscn 10440

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-fv 6233  df-ov 7019  df-neg 10720  df-z 11830  df-uz 12094

This theorem is referenced by:  eluzmn  12100  eluzuzle  12102  eluzelz  12103  eluzle  12106  uztrn  12110  eluzp1p1  12119  subeluzsub  12124  uzm1  12125  uznn0sub  12126  uz3m2nn  12140  1eluzge0  12141  2eluzge1  12143  raluz2  12146  rexuz2  12148  peano2uz  12150  nn0pzuz  12154  uzind4  12155  uzinfi  12177  zsupss  12186  nn01to3  12190  nn0ge2m1nnALT  12191  elfzuzb  12752  uzsubsubfz  12779  ssfzunsnext  12802  ssfzunsn  12803  ige2m1fz  12847  4fvwrd4  12877  elfzo2  12891  elfzouz2  12902  fzossrbm1  12916  fzossfzop1  12965  ssfzo12bi  12982  elfzonelfzo  12989  elfzomelpfzo  12991  fzosplitprm1  12997  fzostep1  13003  fzind2  13005  flword2  13033  fldiv4p1lem1div2  13055  uzsup  13081  modaddmodup  13152  fzsdom2  13637  swrdsbslen  13862  swrdspsleq  13863  pfxtrcfv0  13892  pfxtrcfvl  13895  pfxccatin12lem2a  13925  cshwidxmod  14001  rexuzre  14546  limsupgre  14672  rlimclim1  14736  rlimclim  14737  climrlim2  14738  isercolllem1  14855  isercoll  14858  climcndslem1  15037  fallfacval4  15230  oddge22np1  15531  nn0o  15567  bitsmod  15618  smueqlem  15672  dvdsnprmd  15863  2mulprm  15866  oddprmgt2  15872  oddprmge3  15873  ge2nprmge4  15874  modprm0  15971  prm23ge5  15981  vdwlem9  16154  prmgaplem3  16218  prmgaplem5  16220  prmgaplem6  16221  prmgaplem7  16222  setsstruct  16352  strleun  16420  fislw  18480  efgsp1  18590  efgredleme  18596  lt6abl  18736  telgsumfzs  18826  ablfac1eu  18912  znidomb  20390  chfacfscmul0  21150  chfacfscmulfsupp  21151  chfacfpmmul0  21154  chfacfpmmulfsupp  21155  dvfsumlem1  24306  dvfsumlem3  24308  plyaddlem1  24486  coeidlem  24510  2logb9irr  25054  ppisval  25363  chtdif  25417  ppidif  25422  ppiublem1  25460  ppiub  25462  chtub  25470  lgsdilem2  25591  gausslemma2dlem2  25625  gausslemma2dlem4  25627  gausslemma2dlem5  25629  gausslemma2dlem6  25630  lgsquadlem1  25638  lgsquadlem3  25640  2lgslem1  25652  chebbnd1lem1  25727  chebbnd1lem2  25728  chebbnd1lem3  25729  dchrisumlem2  25748  dchrvmasumiflem1  25759  mulog2sumlem2  25793  logdivbnd  25814  pntlemg  25856  pntlemq  25859  pntlemf  25863  axlowdim  26430  pthdlem1  27234  crctcshwlkn0lem3  27277  crctcshwlkn0lem4  27278  crctcshwlkn0lem5  27279  crctcshwlkn0lem6  27280  wwlksm1edg  27346  wwlksnred  27357  clwlkclwwlklem2fv1  27460  clwlkclwwlklem2  27465  clwwisshclwwslem  27479  clwwlkinwwlk  27505  clwwlkf  27513  clwwlkext2edg  27522  wwlksubclwwlk  27524  frgrreggt1  27864  ssnnssfz  30198  ballotlemsdom  31386  ballotlemsel1i  31387  ballotlemfrceq  31403  signstfvc  31461  signstfveq0  31464  prodfzo03  31491  erdszelem8  32053  climuzcnv  32522  poimirlem6  34429  fdc  34552  eldioph2lem1  38842  hbt  39215  ssinc  40892  ssdec  40893  monoords  41105  fzdifsuc2  41118  eluzd  41224  fmul01lt1lem2  41408  sumnnodd  41453  ioodvbdlimc1lem2  41758  ioodvbdlimc2lem  41760  dvnmul  41769  dvnprodlem2  41773  itgspltprt  41805  stoweidlem11  41838  stoweidlem26  41853  wallispilem4  41895  fourierdlem12  41946  fourierdlem20  41954  fourierdlem41  41975  fourierdlem48  41981  fourierdlem49  41982  fourierdlem50  41983  fourierdlem54  41987  fourierdlem79  42012  fourierdlem102  42035  fourierdlem111  42044  fourierdlem114  42047  etransclem23  42084  etransclem48  42109  caratheodorylem1  42350  smfmullem4  42611  eluzge0nn0  43028  ssfz12  43030  elfzlble  43036  fzopredsuc  43039  fzoopth  43043  iccpartipre  43063  iccpartiltu  43064  iccpartgt  43069  fmtnoge3  43174  odz2prm2pw  43207  fmtnoprmfac2lem1  43210  fmtno4prmfac  43216  31prm  43242  lighneallem4b  43256  341fppr2  43381  9fppr8  43384  fpprel2  43388  nfermltl8rev  43389  nfermltl2rev  43390  gbegt5  43408  gbowgt5  43409  sbgoldbm  43431  mogoldbb  43432  sbgoldbo  43434  nnsum3primesle9  43441  nnsum4primesodd  43443  nnsum4primesoddALTV  43444  evengpop3  43445  evengpoap3  43446  nnsum4primeseven  43447  nnsum4primesevenALTV  43448  wtgoldbnnsum4prm  43449  bgoldbnnsum3prm  43451  bgoldbtbndlem3  43454  tgblthelfgott  43462  cznnring  43705  ssnn0ssfz  43875  elfzolborelfzop1  44055  m1modmmod  44062  rege1logbzge0  44100  fllog2  44109  nnolog2flm1  44131  dignn0ldlem  44143