Theorem eluz2 9468

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 9467	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 987	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 9466	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 299	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 187	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 972	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 197	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 694	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ∧ wa 103   ↔ wb 104   ∧ w3a 968   ∈ wcel 2136   class class class wbr 3981  ‘cfv 5187   ≤ cle 7930  ℤcz 9187  ℤ_≥cuz 9462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186  ax-cnex 7840  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-rab 2452  df-v 2727  df-sbc 2951  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-opab 4043  df-mpt 4044  df-id 4270  df-xp 4609  df-rel 4610  df-cnv 4611  df-co 4612  df-dm 4613  df-rn 4614  df-res 4615  df-ima 4616  df-iota 5152  df-fun 5189  df-fn 5190  df-f 5191  df-fv 5195  df-ov 5844  df-neg 8068  df-z 9188  df-uz 9463

This theorem is referenced by:  eluzuzle  9470  eluzelz  9471  eluzle  9474  uztrn  9478  eluzp1p1  9487  uznn0sub  9493  uz3m2nn  9507  1eluzge0  9508  2eluzge1  9510  raluz2  9513  rexuz2  9515  peano2uz  9517  nn0pzuz  9521  uzind4  9522  nn0ge2m1nnALT  9552  elfzuzb  9950  uzsubsubfz  9978  ige2m1fz  10041  4fvwrd4  10071  elfzo2  10081  elfzouz2  10092  fzossrbm1  10104  fzossfzop1  10143  ssfzo12bi  10156  elfzonelfzo  10161  elfzomelpfzo  10162  fzosplitprm1  10165  fzostep1  10168  fzind2  10170  flqword2  10220  fldiv4p1lem1div2  10236  uzennn  10367  seq3split  10410  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  bcval5  10672  seq3coll  10751  seq3shft  10776  resqrexlemoverl  10959  resqrexlemga  10961  fsum3cvg3  11333  fisumrev2  11383  isumshft  11427  cvgratnnlemseq  11463  cvgratnnlemabsle  11464  cvgratnnlemsumlt  11465  cvgratz  11469  oddge22np1  11814  nn0o  11840  suprzubdc  11881  zsupssdc  11883  uzwodc  11966  dvdsnprmd  12053  prmgt1  12060  oddprmgt2  12062  oddprmge3  12063  prm23ge5  12192  nninfdclemcl  12377  nninfdclemp1  12379  nninfdclemlt  12380  strleund  12478  strleun  12479  2logb9irr  13489  2logb9irrap  13495  lgsdilem2  13537