Theorem eluzel2 12784

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 6868	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
2		uzf 12782	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6673	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2847	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4542  dom cdm 5624  ‘cfv 6492  ℤcz 12515  ℤ_≥cuz 12779

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 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-cnex 11085  ax-resscn 11086

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  eluz2  12785  uztrn  12797  uzneg  12799  uzss  12802  uz11  12804  eluzadd  12808  subeluzsub  12812  uzm1  12813  uzin  12815  uzind4  12847  uzsupss  12881  elfz5  13461  elfzel1  13468  eluzfz1  13476  fzsplit2  13494  fzopth  13506  ssfzunsn  13515  fzpred  13517  fzpreddisj  13518  uzsplit  13541  uzdisj  13542  fzdif1  13550  fzm1  13552  uznfz  13555  nn0disj  13589  preduz  13595  fzolb  13611  fzoss2  13633  fzouzdisj  13641  fzoun  13642  ige2m2fzo  13674  fzen2  13922  seqp1  13969  seqcl  13975  seqfeq2  13978  seqfveq  13979  seqshft2  13981  seqsplit  13988  seqcaopr3  13990  seqf1olem2a  13993  seqf1olem1  13994  seqf1olem2  13995  seqid  14000  seqhomo  14002  seqz  14003  leexp2a  14125  hashfz  14380  fzsdom2  14381  hashfzo  14382  hashfzp1  14384  seqcoll  14417  rexanuz2  15303  cau4  15310  clim2ser  15608  clim2ser2  15609  climserle  15616  caurcvg  15630  caucvg  15632  fsumcvg  15665  fsumcvg2  15680  fsumsers  15681  fsumm1  15704  fsum1p  15706  fsumrev2  15735  telfsumo  15756  fsumparts  15760  cvgcmp  15770  cvgcmpub  15771  cvgcmpce  15772  isumsplit  15796  clim2prod  15844  clim2div  15845  prodfrec  15851  ntrivcvgtail  15856  fprodcvg  15886  fprodser  15905  fprodm1  15923  fprodeq0  15931  pcaddlem  16850  vdwnnlem2  16958  prmlem0  17067  gsumval2a  18644  telgsumfzs  19955  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  coeid3  26215  ulmres  26366  ulmss  26375  chtdif  27135  ppidif  27140  bcmono  27254  axlowdimlem6  29030  inffz  35928  mettrifi  38092  jm2.25  43445  jm2.16nn0  43450  dvgrat  44757  ssinc  45535  ssdec  45536  fzdifsuc2  45761  iuneqfzuzlem  45782  ssuzfz  45797  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  carageniuncllem1  46967  caratheodorylem1  46972