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

Theorem nngt0 11656
Description: A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
Assertion
Ref Expression
nngt0 (𝐴 ∈ ℕ → 0 < 𝐴)

Proof of Theorem nngt0
StepHypRef Expression
1 nnre 11633 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2 nnge1 11653 . 2 (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3 0lt1 11150 . . 3 0 < 1
4 0re 10631 . . . 4 0 ∈ ℝ
5 1re 10629 . . . 4 1 ∈ ℝ
6 ltletr 10720 . . . 4 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
74, 5, 6mp3an12 1442 . . 3 (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
83, 7mpani 692 . 2 (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
91, 2, 8sylc 65 1 (𝐴 ∈ ℕ → 0 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105   class class class wbr 5057  cr 10524  0cc0 10525  1c1 10526   < clt 10663  cle 10664  cn 11626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627
This theorem is referenced by:  nnnle0  11658  nngt0i  11664  nnsub  11669  nngt0d  11674  nnrecl  11883  nn0ge0  11910  0mnnnnn0  11917  elnnnn0b  11929  nn0sub  11935  elnnz  11979  nnm1ge0  12038  gtndiv  12047  elpq  12362  elpqb  12363  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  nnrp  12388  nnledivrp  12489  qbtwnre  12580  fzo1fzo0n0  13076  ubmelfzo  13090  elfznelfzo  13130  adddivflid  13176  flltdivnn0lt  13191  quoremz  13211  quoremnn0ALT  13213  intfracq  13215  fldiv  13216  expnnval  13420  nnlesq  13556  expnngt1  13590  faclbnd  13638  bc0k  13659  ccatval21sw  13927  ccats1pfxeqrex  14065  harmonic  15202  nndivdvds  15604  evennn2n  15688  nnoddm1d2  15725  ndvdssub  15748  ndvdsadd  15749  sqgcd  15897  lcmgcdlem  15938  qredeu  15990  isprm5  16039  divdenle  16077  hashgcdlem  16113  oddprm  16135  pythagtriplem12  16151  pythagtriplem13  16152  pythagtriplem14  16153  pythagtriplem16  16155  pythagtriplem19  16158  pc2dvds  16203  fldivp1  16221  prmreclem3  16242  prmgaplem7  16381  mulgnn  18170  mulgnegnn  18176  odmodnn0  18597  prmirredlem  20568  znidomb  20636  fvmptnn04if  21385  chfacfscmul0  21394  chfacfpmmul0  21398  dyadss  24122  volivth  24135  vitali  24141  mbfi1fseqlem3  24245  itg2gt0  24288  dgrcolem2  24791  logtayllem  25169  leibpi  25447  eldmgm  25526  basellem6  25590  muinv  25697  logfac2  25720  bcmono  25780  bposlem5  25791  bposlem6  25792  lgsval4a  25822  gausslemma2dlem1a  25868  ostth2lem1  26121  ostth2lem3  26138  clwwlkf1  27755  clwwlknonccat  27802  minvecolem3  28580  xnn0gt0  30420  tgoldbachgtda  31831  subfaclim  32332  subfacval3  32333  snmlff  32473  nn0prpwlem  33567  nndivsub  33702  nndivlub  33703  poimirlem32  34805  fzmul  34897  negn0nposznnd  39046  nn0rppwr  39060  nn0expgcd  39062  irrapxlem1  39297  irrapxlem2  39298  pellexlem1  39304  monotoddzzfi  39417  rmynn  39431  jm2.24nn  39434  jm2.17c  39437  congabseq  39449  jm2.20nn  39472  rmydioph  39489  dgrsub2  39613  idomrootle  39673  rp-isfinite6  39762  stoweidlem17  42179  stoweidlem49  42211  wallispilem4  42230  stirlinglem6  42241  stirlinglem7  42242  stirlinglem10  42245  fourierdlem73  42341  fourierdlem111  42379  2ffzoeq  43405  iccpartltu  43462  fmtnosqrt  43578  2pwp1prm  43628  nneven  43740
  Copyright terms: Public domain W3C validator