Theorem eluz2 9937

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 9936	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1028	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 9935	. . . 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 8362  ℤcz 9649  ℤ_≥cuz 9931

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 8271  ax-resscn 8272

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 8502  df-z 9650  df-uz 9932

This theorem is used by:  eluzmn  9938  eluzuzle  9940  eluzelz  9941  eluzle  9944  uztrn  9949  eluzp1p1  9958  uznn0sub  9964  5eluz3  9971  uz3m2nn  9983  1eluzge0  9984  2eluzge1  9986  raluz2  9989  rexuz2  9991  peano2uz  9993  nn0pzuz  9997  uzind4  9998  nn0ge2m1nnALT  10028  elfzuzb  10433  uzsubsubfz  10463  ige2m1fz  10528  4fvwrd4  10558  elfzo2  10568  elfzouz2  10580  fzossrbm1  10593  fzossfzop1  10641  ssfzo12bi  10654  elfzonelfzo  10659  elfzomelpfzo  10660  fzosplitprm1  10664  fzostep1  10667  fzind2  10669  suprzubdc  10682  zsupssdc  10684  flqword2  10739  fldiv4p1lem1div2  10755  uzennn  10888  xnn0nnen  10889  seq3split  10940  iseqf1olemqk  10959  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  bcval5  11217  seq3coll  11310  swrdsbslen  11454  swrdspsleq  11455  pfxtrcfv0  11482  pfxtrcfvl  11485  pfxccatin12lem2a  11515  seq3shft  11619  resqrexlemoverl  11803  resqrexlemga  11805  fsum3cvg3  12182  fisumrev2  12232  isumshft  12276  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratz  12318  oddge22np1  12667  nn0o  12693  bitsmod  12742  uzwodc  12833  dvdsnprmd  12922  prmgt1  12930  oddprmgt2  12932  oddprmge3  12933  prm23ge5  13066  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemfrceq  13324  nninfdclemcl  13391  nninfdclemp1  13393  nninfdclemlt  13394  strleund  13510  strleun  13511  gzsumcl  13857  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  znidomb  15077  plyaddlem1  15939  2logb9irr  16168  2logb9irrap  16174  ppiqsval  16201  chtdif  16225  ppidif  16230  ppiublem1  16252  ppiqub  16254  chtqub  16257  bposlem4  16275  lgsdilem2  16321  gausslemma2dlem2  16347  gausslemma2dlem4  16349  gausslemma2dlem5  16351  gausslemma2dlem6  16352  lgsquadlem1  16362  lgsquadlem3  16364  2lgslem1  16376  clwwlkext2edg  16829  trlsegvdeglem6  16872