Theorem eluz2 9751

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

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 1002   ∈ wcel 2200   class class class wbr 4086  ‘cfv 5324   ≤ cle 8205  ℤcz 9469  ℤ_≥cuz 9745

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-cnex 8113  ax-resscn 8114

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470  df-uz 9746

This theorem is referenced by:  eluzmn  9752  eluzuzle  9754  eluzelz  9755  eluzle  9758  uztrn  9763  eluzp1p1  9772  uznn0sub  9778  5eluz3  9785  uz3m2nn  9797  1eluzge0  9798  2eluzge1  9800  raluz2  9803  rexuz2  9805  peano2uz  9807  nn0pzuz  9811  uzind4  9812  nn0ge2m1nnALT  9842  elfzuzb  10244  uzsubsubfz  10272  ige2m1fz  10335  4fvwrd4  10365  elfzo2  10375  elfzouz2  10387  fzossrbm1  10400  fzossfzop1  10447  ssfzo12bi  10460  elfzonelfzo  10465  elfzomelpfzo  10466  fzosplitprm1  10470  fzostep1  10473  fzind2  10475  suprzubdc  10486  zsupssdc  10488  flqword2  10539  fldiv4p1lem1div2  10555  uzennn  10688  xnn0nnen  10689  seq3split  10740  iseqf1olemqk  10759  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  bcval5  11015  seq3coll  11096  swrdsbslen  11237  swrdspsleq  11238  pfxtrcfv0  11265  pfxtrcfvl  11268  pfxccatin12lem2a  11298  seq3shft  11389  resqrexlemoverl  11572  resqrexlemga  11574  fsum3cvg3  11947  fisumrev2  11997  isumshft  12041  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratz  12083  oddge22np1  12432  nn0o  12458  bitsmod  12507  uzwodc  12598  dvdsnprmd  12687  prmgt1  12694  oddprmgt2  12696  oddprmge3  12697  prm23ge5  12827  nninfdclemcl  13059  nninfdclemp1  13061  nninfdclemlt  13062  strleund  13176  strleun  13177  gsumfzz  13568  gsumfzcl  13572  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  gsumfzfsum  14592  znidomb  14662  plyaddlem1  15461  2logb9irr  15685  2logb9irrap  15691  lgsdilem2  15755  gausslemma2dlem2  15781  gausslemma2dlem4  15783  gausslemma2dlem5  15785  gausslemma2dlem6  15786  lgsquadlem1  15796  lgsquadlem3  15798  2lgslem1  15810  clwwlkext2edg  16217