Theorem eluznn 12348

Description: Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.)

Assertion

Ref	Expression
eluznn	⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)

Proof of Theorem eluznn

Step	Hyp	Ref	Expression
1		nnuz 12311	. 2 ⊢ ℕ = (ℤ≥‘1)
2	1	uztrn2 12291	1 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2112  ‘cfv 6333  1c1 10566  ℕcn 11664  ℤ_≥cuz 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-er 8297  df-en 8526  df-dom 8527  df-sdom 8528  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-nn 11665  df-z 12011  df-uz 12273

This theorem is referenced by:  elfzo1  13126  expmulnbnd  13636  bcval5  13718  isercolllem1  15059  isercoll  15062  o1fsum  15206  climcndslem1  15242  climcndslem2  15243  climcnds  15244  mertenslem2  15279  rpnnen2lem6  15610  rpnnen2lem7  15611  rpnnen2lem9  15613  rpnnen2lem11  15615  pcmpt2  16274  pcmptdvds  16275  prmreclem4  16300  prmreclem5  16301  prmreclem6  16302  vdwnnlem2  16377  2expltfac  16474  1stcelcls  22151  lmnn  23953  cmetcaulem  23978  causs  23988  caubl  23998  caublcls  23999  ovolunlem1a  24186  volsuplem  24245  uniioombllem3  24275  mbfi1fseqlem6  24410  aaliou3lem2  25028  birthdaylem2  25627  lgamgulmlem4  25706  lgamcvg2  25729  chtub  25885  bclbnd  25953  bposlem3  25959  bposlem4  25960  bposlem5  25961  bposlem6  25962  lgsdilem2  26006  chebbnd1lem1  26142  chebbnd1lem2  26143  chebbnd1lem3  26144  dchrisumlema  26161  dchrisumlem2  26163  dchrisumlem3  26164  dchrisum0lem1b  26188  dchrisum0lem1  26189  pntrsumbnd2  26240  pntpbnd1  26259  pntpbnd2  26260  pntlemh  26272  pntlemq  26274  pntlemr  26275  pntlemj  26276  pntlemf  26278  minvecolem3  28748  minvecolem4  28752  h2hcau  28851  h2hlm  28852  chscllem2  29510  sinccvglem  33136  lmclim2  35466  geomcau  35467  heibor1lem  35517  rrncmslem  35540  aks4d1p1  39632  divcnvg  42625  stoweidlem7  43005  stirlinglem12  43083  fourierdlem103  43207  fourierdlem104  43208