Theorem eluz2 9859

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 9858	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1024	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 9857	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 301	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 188	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1009	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 198	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 712	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 1005   ∈ wcel 2203   class class class wbr 4109  ‘cfv 5352   ≤ cle 8309  ℤcz 9577  ℤ_≥cuz 9853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-cnex 8218  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578  df-uz 9854

This theorem is referenced by:  eluzmn  9860  eluzuzle  9862  eluzelz  9863  eluzle  9866  uztrn  9871  eluzp1p1  9880  uznn0sub  9886  5eluz3  9893  uz3m2nn  9905  1eluzge0  9906  2eluzge1  9908  raluz2  9911  rexuz2  9913  peano2uz  9915  nn0pzuz  9919  uzind4  9920  nn0ge2m1nnALT  9950  elfzuzb  10353  uzsubsubfz  10381  ige2m1fz  10444  4fvwrd4  10474  elfzo2  10484  elfzouz2  10496  fzossrbm1  10509  fzossfzop1  10557  ssfzo12bi  10570  elfzonelfzo  10575  elfzomelpfzo  10576  fzosplitprm1  10580  fzostep1  10583  fzind2  10585  suprzubdc  10596  zsupssdc  10598  flqword2  10649  fldiv4p1lem1div2  10665  uzennn  10798  xnn0nnen  10799  seq3split  10850  iseqf1olemqk  10869  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  bcval5  11125  seq3coll  11214  swrdsbslen  11358  swrdspsleq  11359  pfxtrcfv0  11386  pfxtrcfvl  11389  pfxccatin12lem2a  11419  seq3shft  11523  resqrexlemoverl  11706  resqrexlemga  11708  fsum3cvg3  12082  fisumrev2  12132  isumshft  12176  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemsumlt  12214  cvgratz  12218  oddge22np1  12567  nn0o  12593  bitsmod  12642  uzwodc  12733  dvdsnprmd  12822  prmgt1  12829  oddprmgt2  12831  oddprmge3  12832  prm23ge5  12962  nninfdclemcl  13199  nninfdclemp1  13201  nninfdclemlt  13202  strleund  13316  strleun  13317  gsumfzz  13708  gsumfzcl  13712  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  gsumsplit0  14063  gsumfzfsum  14736  znidomb  14806  plyaddlem1  15612  2logb9irr  15836  2logb9irrap  15842  lgsdilem2  15909  gausslemma2dlem2  15935  gausslemma2dlem4  15937  gausslemma2dlem5  15939  gausslemma2dlem6  15940  lgsquadlem1  15950  lgsquadlem3  15952  2lgslem1  15964  clwwlkext2edg  16417  trlsegvdeglem6  16460  gsumgfsumlem  16865  gsumgfsum  16866