Theorem eluz2nn 12903

Description: An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.)

Assertion

Ref	Expression
eluz2nn	⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)

Proof of Theorem eluz2nn

Step	Hyp	Ref	Expression
1		1z 12627	. . 3 ⊢ 1 ∈ ℤ
2		1le2 12454	. . 3 ⊢ 1 ≤ 2
3		eluzuzle 12866	. . 3 ⊢ ((1 ∈ ℤ ∧ 1 ≤ 2) → (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1)))
4	1, 2, 3	mp2an 692	. 2 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1))
5		nnuz 12900	. 2 ⊢ ℕ = (ℤ≥‘1)
6	4, 5	eleqtrrdi 2846	1 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  ‘cfv 6536  1c1 11135   ≤ cle 11275  ℕcn 12245  2c2 12300  ℤcz 12593  ℤ_≥cuz 12857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-2 12308  df-z 12594  df-uz 12858

This theorem is referenced by:  eluz4nn  12907  eluzge2nn0  12908  eluz2n0  12909  zgt1rpn0n1  13055  mulp1mod1  13934  expnngt1b  14265  relexpaddg  15077  modm1div  16289  ncoprmgcdne1b  16674  isprm3  16707  prmind2  16709  nprm  16712  exprmfct  16728  prmdvdsfz  16729  isprm5  16731  maxprmfct  16733  isprm6  16738  phibndlem  16794  phibnd  16795  dfphi2  16798  pclem  16863  pcprendvds2  16866  pcpre1  16867  dvdsprmpweqnn  16910  expnprm  16927  prmreclem1  16941  4sqlem15  16984  4sqlem16  16985  vdwlem5  17010  vdwlem6  17011  vdwlem8  17013  vdwlem9  17014  vdwlem11  17016  prmgaplem1  17074  prmgaplem2  17075  prmgaplcmlem2  17077  prmgapprmolem  17086  ovolicc1  25474  rtprmirr  26727  logbgcd1irr  26761  wilth  27038  wilthimp  27039  mersenne  27195  bposlem3  27254  lgsquad2lem2  27353  2sqlem6  27391  rplogsumlem1  27452  rplogsumlem2  27453  dchrisum0flblem2  27477  ostthlem2  27596  ostth2lem2  27602  axlowdimlem5  28930  clwwisshclwwslemlem  29999  dlwwlknondlwlknonf1olem1  30350  dlwwlknondlwlknonf1o  30351  signstfveq0  34614  subfacval3  35216  expeqidd  42343  fltne  42642  rmspecsqrtnq  42904  rmxypos  42946  ltrmynn0  42947  jm2.17a  42959  jm2.17b  42960  jm2.17c  42961  jm2.27c  43006  jm3.1lem1  43016  jm3.1lem2  43017  jm3.1lem3  43018  relexpaddss  43717  wallispilem3  46076  zplusmodne  47352  m1modne  47357  fmtnonn  47525  fmtnorec3  47542  fmtnorec4  47543  fmtnoprmfac2lem1  47560  fmtnoprmfac2  47561  prmdvdsfmtnof1lem1  47578  prmdvdsfmtnof  47580  lighneallem4a  47602  lighneallem4b  47603  fpprel2  47735  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  cznnring  48217  expnegico01  48474  fllogbd  48520  logbge0b  48523  logblt1b  48524  nnolog2flm1  48550  blennngt2o2  48552  blengt1fldiv2p1  48553  dignn0ldlem  48562  dignnld  48563  digexp  48567  dig1  48568