Theorem eluz2 9943

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 9942	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1028	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 9941	. . . 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 4131  ‘cfv 5380   ≤ cle 8367  ℤcz 9655  ℤ_≥cuz 9937

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 4251  ax-pow 4313  ax-pr 4348  ax-cnex 8276  ax-resscn 8277

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 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9656  df-uz 9938

This theorem is used by:  eluzmn  9944  eluzuzle  9946  eluzelz  9947  eluzle  9950  uztrn  9955  eluzp1p1  9964  uznn0sub  9970  5eluz3  9977  uz3m2nn  9989  1eluzge0  9990  2eluzge1  9992  raluz2  9995  rexuz2  9997  peano2uz  9999  nn0pzuz  10003  uzind4  10004  nn0ge2m1nnALT  10034  elfzuzb  10439  uzsubsubfz  10469  ige2m1fz  10534  4fvwrd4  10564  elfzo2  10574  elfzouz2  10586  fzossrbm1  10599  fzossfzop1  10647  ssfzo12bi  10660  elfzonelfzo  10665  elfzomelpfzo  10666  fzosplitprm1  10670  fzostep1  10673  fzind2  10675  suprzubdc  10688  zsupssdc  10690  flqword2  10745  fldiv4p1lem1div2  10761  uzennn  10894  xnn0nnen  10895  seq3split  10946  iseqf1olemqk  10965  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  bcval5  11223  seq3coll  11316  swrdsbslen  11460  swrdspsleq  11461  pfxtrcfv0  11488  pfxtrcfvl  11491  pfxccatin12lem2a  11521  seq3shft  11625  resqrexlemoverl  11809  resqrexlemga  11811  fsum3cvg3  12188  fisumrev2  12238  isumshft  12282  cvgratnnlemseq  12318  cvgratnnlemabsle  12319  cvgratnnlemsumlt  12320  cvgratz  12324  oddge22np1  12673  nn0o  12699  bitsmod  12748  uzwodc  12839  dvdsnprmd  12928  prmgt1  12936  oddprmgt2  12938  oddprmge3  12939  prm23ge5  13072  ballotfilemsdom  13313  ballotfilemsel1i  13314  ballotfilemfrceq  13330  nninfdclemcl  13397  nninfdclemp1  13399  nninfdclemlt  13400  strleund  13516  strleun  13517  gzsumcl  13863  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gzsumsplit0  14238  gzsumshift  14239  gzsumgsum  14245  znidomb  15102  plyaddlem1  15973  2logb9irr  16207  2logb9irrap  16213  ppiqsval  16240  chtdif  16264  ppidif  16269  ppiublem1  16291  ppiqub  16293  chtqub  16296  bposlem4  16314  lgsdilem2  16360  gausslemma2dlem2  16386  gausslemma2dlem4  16388  gausslemma2dlem5  16390  gausslemma2dlem6  16391  lgsquadlem1  16401  lgsquadlem3  16403  2lgslem1  16415  clwwlkext2edg  16868  trlsegvdeglem6  16911