Theorem eluz2 9936

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∧ w3a 1009   ∈ wcel 2209   class class class wbr 4130  ‘cfv 5377   ≤ cle 8361  ℤcz 9648  ℤ_≥cuz 9930

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-cnex 8270  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385  df-ov 6088  df-neg 8501  df-z 9649  df-uz 9931

This theorem is used by:  eluzmn  9937  eluzuzle  9939  eluzelz  9940  eluzle  9943  uztrn  9948  eluzp1p1  9957  uznn0sub  9963  5eluz3  9970  uz3m2nn  9982  1eluzge0  9983  2eluzge1  9985  raluz2  9988  rexuz2  9990  peano2uz  9992  nn0pzuz  9996  uzind4  9997  nn0ge2m1nnALT  10027  elfzuzb  10432  uzsubsubfz  10462  ige2m1fz  10527  4fvwrd4  10557  elfzo2  10567  elfzouz2  10579  fzossrbm1  10592  fzossfzop1  10640  ssfzo12bi  10653  elfzonelfzo  10658  elfzomelpfzo  10659  fzosplitprm1  10663  fzostep1  10666  fzind2  10668  suprzubdc  10681  zsupssdc  10683  flqword2  10737  fldiv4p1lem1div2  10753  uzennn  10886  xnn0nnen  10887  seq3split  10938  iseqf1olemqk  10957  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  bcval5  11215  seq3coll  11308  swrdsbslen  11452  swrdspsleq  11453  pfxtrcfv0  11480  pfxtrcfvl  11483  pfxccatin12lem2a  11513  seq3shft  11617  resqrexlemoverl  11801  resqrexlemga  11803  fsum3cvg3  12179  fisumrev2  12229  isumshft  12273  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratz  12315  oddge22np1  12664  nn0o  12690  bitsmod  12739  uzwodc  12830  dvdsnprmd  12919  prmgt1  12927  oddprmgt2  12929  oddprmge3  12930  prm23ge5  13063  ballotfilemsdom  13304  ballotfilemsel1i  13305  ballotfilemfrceq  13321  nninfdclemcl  13388  nninfdclemp1  13390  nninfdclemlt  13391  strleund  13506  strleun  13507  gzsumcl  13853  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gzsumsplit0  14197  gzsumshift  14198  gzsumgsum  14204  znidomb  15042  plyaddlem1  15897  2logb9irr  16126  2logb9irrap  16132  ppiqsval  16156  ppidif  16175  ppiublem1  16192  ppiqub  16194  bposlem4  16212  lgsdilem2  16253  gausslemma2dlem2  16279  gausslemma2dlem4  16281  gausslemma2dlem5  16283  gausslemma2dlem6  16284  lgsquadlem1  16294  lgsquadlem3  16296  2lgslem1  16308  clwwlkext2edg  16761  trlsegvdeglem6  16804