Theorem eluzel2 12793

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
eluzel2	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Proof of Theorem eluzel2

Step	Hyp	Ref	Expression
1		elfvdm 6874	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
2		uzf 12791	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6679	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2846	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4541  dom cdm 5631  ‘cfv 6498  ℤcz 12524  ℤ_≥cuz 12788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  eluz2  12794  uztrn  12806  uzneg  12808  uzss  12811  uz11  12813  eluzadd  12817  subeluzsub  12821  uzm1  12822  uzin  12824  uzind4  12856  uzsupss  12890  elfz5  13470  elfzel1  13477  eluzfz1  13485  fzsplit2  13503  fzopth  13515  ssfzunsn  13524  fzpred  13526  fzpreddisj  13527  uzsplit  13550  uzdisj  13551  fzdif1  13559  fzm1  13561  uznfz  13564  nn0disj  13598  preduz  13604  fzolb  13620  fzoss2  13642  fzouzdisj  13650  fzoun  13651  ige2m2fzo  13683  fzen2  13931  seqp1  13978  seqcl  13984  seqfeq2  13987  seqfveq  13988  seqshft2  13990  seqsplit  13997  seqcaopr3  13999  seqf1olem2a  14002  seqf1olem1  14003  seqf1olem2  14004  seqid  14009  seqhomo  14011  seqz  14012  leexp2a  14134  hashfz  14389  fzsdom2  14390  hashfzo  14391  hashfzp1  14393  seqcoll  14426  rexanuz2  15312  cau4  15319  clim2ser  15617  clim2ser2  15618  climserle  15625  caurcvg  15639  caucvg  15641  fsumcvg  15674  fsumcvg2  15689  fsumsers  15690  fsumm1  15713  fsum1p  15715  fsumrev2  15744  telfsumo  15765  fsumparts  15769  cvgcmp  15779  cvgcmpub  15780  cvgcmpce  15781  isumsplit  15805  clim2prod  15853  clim2div  15854  prodfrec  15860  ntrivcvgtail  15865  fprodcvg  15895  fprodser  15914  fprodm1  15932  fprodeq0  15940  pcaddlem  16859  vdwnnlem2  16967  prmlem0  17076  gsumval2a  18653  telgsumfzs  19964  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  coeid3  26205  ulmres  26353  ulmss  26362  chtdif  27121  ppidif  27126  bcmono  27240  axlowdimlem6  29016  inffz  35912  mettrifi  38078  jm2.25  43427  jm2.16nn0  43432  dvgrat  44739  ssinc  45517  ssdec  45518  fzdifsuc2  45743  iuneqfzuzlem  45764  ssuzfz  45779  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  carageniuncllem1  46949  caratheodorylem1  46954