Theorem eluz2nn 12832

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 12551	. . 3 ⊢ 1 ∈ ℤ
2		1le2 12379	. . 3 ⊢ 1 ≤ 2
3		eluzuzle 12791	. . 3 ⊢ ((1 ∈ ℤ ∧ 1 ≤ 2) → (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1)))
4	1, 2, 3	mp2an 693	. 2 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1))
5		nnuz 12821	. 2 ⊢ ℕ = (ℤ≥‘1)
6	4, 5	eleqtrrdi 2848	1 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493  1c1 11033   ≤ cle 11174  ℕcn 12168  2c2 12230  ℤcz 12518  ℤ_≥cuz 12782

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 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

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-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-2 12238  df-z 12519  df-uz 12783

This theorem is referenced by:  eluz3nn  12833  eluz4nn  12834  eluzge2nn0  12836  eluz2n0  12837  zgt1rpn0n1  12979  nnge2recico01  13454  mulp1mod1  13867  expnngt1b  14198  relexpaddg  15009  modm1div  16227  ncoprmgcdne1b  16613  isprm3  16646  prmind2  16648  nprm  16651  exprmfct  16668  prmdvdsfz  16669  isprm5  16671  maxprmfct  16673  isprm6  16678  phibndlem  16734  phibnd  16735  dfphi2  16738  pclem  16803  pcprendvds2  16806  pcpre1  16807  dvdsprmpweqnn  16850  expnprm  16867  prmreclem1  16881  4sqlem15  16924  4sqlem16  16925  vdwlem5  16950  vdwlem6  16951  vdwlem8  16953  vdwlem9  16954  vdwlem11  16956  prmgaplem1  17014  prmgaplem2  17015  prmgaplcmlem2  17017  prmgapprmolem  17026  ovolicc1  25496  rtprmirr  26740  logbgcd1irr  26774  wilth  27051  wilthimp  27052  mersenne  27207  bposlem3  27266  lgsquad2lem2  27365  2sqlem6  27403  rplogsumlem1  27464  rplogsumlem2  27465  dchrisum0flblem2  27489  ostthlem2  27608  ostth2lem2  27614  axlowdimlem5  29032  clwwisshclwwslemlem  30101  dlwwlknondlwlknonf1olem1  30452  dlwwlknondlwlknonf1o  30453  signstfveq0  34740  subfacval3  35390  expeqidd  42774  fltne  43094  rmspecsqrtnq  43355  rmxypos  43396  ltrmynn0  43397  jm2.17a  43409  jm2.17b  43410  jm2.17c  43411  jm2.27c  43456  jm3.1lem1  43466  jm3.1lem2  43467  jm3.1lem3  43468  relexpaddss  44166  wallispilem3  46516  elfzo2nn  47792  zplusmodne  47812  m1modne  47817  fmtnonn  48009  fmtnorec3  48026  fmtnorec4  48027  fmtnoprmfac2lem1  48044  fmtnoprmfac2  48045  prmdvdsfmtnof1lem1  48062  prmdvdsfmtnof  48064  lighneallem4a  48086  lighneallem4b  48087  ppivalnnprm  48103  fpprel2  48232  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  cznnring  48753  expnegico01  49009  fllogbd  49051  logbge0b  49054  logblt1b  49055  nnolog2flm1  49081  blennngt2o2  49083  blengt1fldiv2p1  49084  dignn0ldlem  49093  dignnld  49094  digexp  49098  dig1  49099