MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluz2nn Structured version   Visualization version   GIF version

Theorem eluz2nn 11554
Description: An integer is 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
StepHypRef Expression
1 1z 11236 . . 3 1 ∈ ℤ
2 1le2 11084 . . 3 1 ≤ 2
3 eluzuzle 11524 . . 3 ((1 ∈ ℤ ∧ 1 ≤ 2) → (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ (ℤ‘1)))
41, 2, 3mp2an 703 . 2 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ (ℤ‘1))
5 nnuz 11551 . 2 ℕ = (ℤ‘1)
64, 5syl6eleqr 2694 1 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975   class class class wbr 4573  cfv 5786  1c1 9789  cle 9927  cn 10863  2c2 10913  cz 11206  cuz 11515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-er 7602  df-en 7815  df-dom 7816  df-sdom 7817  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-nn 10864  df-2 10922  df-z 11207  df-uz 11516
This theorem is referenced by:  eluzge2nn0  11555  eluz2n0  11556  zgt1rpn0n1  11699  mulp1mod1  12524  relexpaddg  13583  ncoprmgcdne1b  15143  isprm3  15176  prmind2  15178  nprm  15181  exprmfct  15196  prmdvdsfz  15197  isprm5  15199  maxprmfct  15201  isprm6  15206  phibndlem  15255  phibnd  15256  dfphi2  15259  pclem  15323  pcprendvds2  15326  pcpre1  15327  dvdsprmpweqnn  15369  expnprm  15386  prmreclem1  15400  4sqlem15  15443  4sqlem16  15444  vdwlem5  15469  vdwlem6  15470  vdwlem8  15472  vdwlem9  15473  vdwlem11  15475  prmgaplem1  15533  prmgaplem2  15534  prmgaplcmlem2  15536  prmgapprmolem  15545  ovolicc1  23004  wilth  24510  wilthimp  24511  mersenne  24665  bposlem3  24724  lgsquad2lem2  24823  2sqlem6  24861  rplogsumlem1  24886  rplogsumlem2  24887  dchrisum0flblem2  24911  ostthlem2  25030  ostth2lem2  25036  axlowdimlem5  25540  clwwisshclwwlem1  26095  usg2cwwkdifex  26111  signstfveq0  29782  subfacval3  30227  rmspecsqrtnq  36287  rmspecsqrtnqOLD  36288  rmxypos  36331  ltrmynn0  36332  jm2.17a  36344  jm2.17b  36345  jm2.17c  36346  jm2.27c  36391  jm3.1lem1  36401  jm3.1lem2  36402  jm3.1lem3  36403  relexpaddss  36828  wallispilem3  38760  fmtnonn  39782  fmtnorec3  39799  fmtnorec4  39800  fmtnoprmfac2lem1  39817  fmtnoprmfac2  39818  prmdvdsfmtnof1lem1  39835  prmdvdsfmtnof  39837  lighneallem4a  39864  lighneallem4b  39865  wtgoldbnnsum4prm  40019  bgoldbnnsum3prm  40021  clwwisshclwwslemlem  41231  av-numclwwlk3lem  41536  cznnring  41746  expnegico01  42100  fllogbd  42150  logbge0b  42153  logblt1b  42154  nnolog2flm1  42180  blennngt2o2  42182  blengt1fldiv2p1  42183  dignn0ldlem  42192  dignnld  42193  digexp  42197  dig1  42198
  Copyright terms: Public domain W3C validator