Theorem eluz2nn 12652

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 12378	. . 3 ⊢ 1 ∈ ℤ
2		1le2 12210	. . 3 ⊢ 1 ≤ 2
3		eluzuzle 12619	. . 3 ⊢ ((1 ∈ ℤ ∧ 1 ≤ 2) → (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1)))
4	1, 2, 3	mp2an 688	. 2 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1))
5		nnuz 12649	. 2 ⊢ ℕ = (ℤ≥‘1)
6	4, 5	eleqtrrdi 2845	1 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2101   class class class wbr 5077  ‘cfv 6447  1c1 10900   ≤ cle 11038  ℕcn 12001  2c2 12056  ℤcz 12347  ℤ_≥cuz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7608  ax-cnex 10955  ax-resscn 10956  ax-1cn 10957  ax-icn 10958  ax-addcl 10959  ax-addrcl 10960  ax-mulcl 10961  ax-mulrcl 10962  ax-mulcom 10963  ax-addass 10964  ax-mulass 10965  ax-distr 10966  ax-i2m1 10967  ax-1ne0 10968  ax-1rid 10969  ax-rnegex 10970  ax-rrecex 10971  ax-cnre 10972  ax-pre-lttri 10973  ax-pre-lttrn 10974  ax-pre-ltadd 10975  ax-pre-mulgt0 10976

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3908  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-iun 4929  df-br 5078  df-opab 5140  df-mpt 5161  df-tr 5195  df-id 5491  df-eprel 5497  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-riota 7252  df-ov 7298  df-oprab 7299  df-mpo 7300  df-om 7733  df-2nd 7852  df-frecs 8117  df-wrecs 8148  df-recs 8222  df-rdg 8261  df-er 8518  df-en 8754  df-dom 8755  df-sdom 8756  df-pnf 11039  df-mnf 11040  df-xr 11041  df-ltxr 11042  df-le 11043  df-sub 11235  df-neg 11236  df-nn 12002  df-2 12064  df-z 12348  df-uz 12611

This theorem is referenced by:  eluz4nn  12654  eluzge2nn0  12655  eluz2n0  12656  zgt1rpn0n1  12799  mulp1mod1  13660  expnngt1b  13985  relexpaddg  14792  modm1div  16003  ncoprmgcdne1b  16383  isprm3  16416  prmind2  16418  nprm  16421  exprmfct  16437  prmdvdsfz  16438  isprm5  16440  maxprmfct  16442  isprm6  16447  phibndlem  16499  phibnd  16500  dfphi2  16503  pclem  16567  pcprendvds2  16570  pcpre1  16571  dvdsprmpweqnn  16614  expnprm  16631  prmreclem1  16645  4sqlem15  16688  4sqlem16  16689  vdwlem5  16714  vdwlem6  16715  vdwlem8  16717  vdwlem9  16718  vdwlem11  16720  prmgaplem1  16778  prmgaplem2  16779  prmgaplcmlem2  16781  prmgapprmolem  16790  ovolicc1  24708  logbgcd1irr  25972  wilth  26248  wilthimp  26249  mersenne  26403  bposlem3  26462  lgsquad2lem2  26561  2sqlem6  26599  rplogsumlem1  26660  rplogsumlem2  26661  dchrisum0flblem2  26685  ostthlem2  26804  ostth2lem2  26810  axlowdimlem5  27342  clwwisshclwwslemlem  28405  dlwwlknondlwlknonf1olem1  28756  dlwwlknondlwlknonf1o  28757  signstfveq0  32584  subfacval3  33179  rtprmirr  40370  fltne  40504  rmspecsqrtnq  40751  rmxypos  40793  ltrmynn0  40794  jm2.17a  40806  jm2.17b  40807  jm2.17c  40808  jm2.27c  40853  jm3.1lem1  40863  jm3.1lem2  40864  jm3.1lem3  40865  relexpaddss  41350  wallispilem3  43643  fmtnonn  45023  fmtnorec3  45040  fmtnorec4  45041  fmtnoprmfac2lem1  45058  fmtnoprmfac2  45059  prmdvdsfmtnof1lem1  45076  prmdvdsfmtnof  45078  lighneallem4a  45100  lighneallem4b  45101  fpprel2  45233  wtgoldbnnsum4prm  45294  bgoldbnnsum3prm  45296  cznnring  45554  expnegico01  45899  fllogbd  45946  logbge0b  45949  logblt1b  45950  nnolog2flm1  45976  blennngt2o2  45978  blengt1fldiv2p1  45979  dignn0ldlem  45988  dignnld  45989  digexp  45993  dig1  45994