Theorem eluz2nn 12938

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 12649	. . 3 ⊢ 1 ∈ ℤ
2		1le2 12477	. . 3 ⊢ 1 ≤ 2
3		eluzuzle 12897	. . 3 ⊢ ((1 ∈ ℤ ∧ 1 ≤ 2) → (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1)))
4	1, 2, 3	mp2an 705	. 2 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1))
5		nnuz 12927	. 2 ⊢ ℕ = (ℤ≥‘1)
6	4, 5	eleqtrrdi 2871	1 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533  1c1 11126   ≤ cle 11269  ℕcn 12258  2c2 12320  ℤcz 12616  ℤ_≥cuz 12888

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-2 12328  df-z 12617  df-uz 12889

This theorem is used by:  eluz3nn  12939  eluz4nn  12940  eluzge2nn0  12942  eluz2n0  12943  zgt1rpn0n1  13086  nnge2recico01  13561  mulp1mod1  13976  expnngt1b  14307  relexpaddg  15127  modm1div  16355  ncoprmgcdne1b  16741  isprm3  16774  prmind2  16776  nprm  16779  exprmfct  16796  prmdvdsfz  16797  isprm5  16799  maxprmfct  16801  isprm6  16806  phibndlem  16862  phibnd  16863  dfphi2  16866  pclem  16931  pcprendvds2  16934  pcpre1  16935  dvdsprmpweqnn  16978  expnprm  16995  prmreclem1  17009  4sqlem15  17052  4sqlem16  17053  vdwlem5  17078  vdwlem6  17079  vdwlem8  17081  vdwlem9  17082  vdwlem11  17084  prmgaplem1  17142  prmgaplem2  17143  prmgaplcmlem2  17145  prmgapprmolem  17154  ovolicc1  25745  rtprmirr  26998  logbgcd1irr  27032  wilth  27308  wilthimp  27309  mersenne  27464  bposlem3  27523  lgsquad2lem2  27622  2sqlem6  27660  rplogsumlem1  27721  rplogsumlem2  27722  dchrisum0flblem2  27746  ostthlem2  27865  ostth2lem2  27871  axlowdimlem5  29404  clwwisshclwwslemlem  30484  dlwwlknondlwlknonf1olem1  30845  dlwwlknondlwlknonf1o  30846  signstfveq0  35086  subfacval3  35769  expeqidd  43201  fltne  43491  rmspecsqrtnq  43748  rmxypos  43789  ltrmynn0  43790  jm2.17a  43802  jm2.17b  43803  jm2.17c  43804  jm2.27c  43849  jm3.1lem1  43859  jm3.1lem2  43860  jm3.1lem3  43861  relexpaddss  44559  wallispilem3  46896  elfzo2nn  48218  zplusmodne  48238  m1modne  48243  fmtnonn  48435  fmtnorec3  48452  fmtnorec4  48453  fmtnoprmfac2lem1  48470  fmtnoprmfac2  48471  prmdvdsfmtnof1lem1  48488  prmdvdsfmtnof  48490  lighneallem4a  48512  lighneallem4b  48513  ppivalnnprm  48529  fpprel2  48658  wtgoldbnnsum4prm  48719  bgoldbnnsum3prm  48721  cznnring  49178  expnegico01  49449  fllogbd  49491  logbge0b  49494  logblt1b  49495  nnolog2flm1  49521  blennngt2o2  49523  blengt1fldiv2p1  49524  dignn0ldlem  49533  dignnld  49534  digexp  49538  dig1  49539