Theorem nngt0 11934

Description: A positive integer is positive. (Contributed by NM, 26-Sep-1999.)

Assertion

Ref	Expression
nngt0	⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Proof of Theorem nngt0

Step	Hyp	Ref	Expression
1		nnre 11910	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 11931	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 11427	. . 3 ⊢ 0 < 1
4		0re 10908	. . . 4 ⊢ 0 ∈ ℝ
5		1re 10906	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 10997	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1449	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 692	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 65	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801  0cc0 10802  1c1 10803   < clt 10940   ≤ cle 10941  ℕcn 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904

This theorem is referenced by:  nnnle0  11936  nngt0i  11942  nnsub  11947  nngt0d  11952  nnrecl  12161  nn0ge0  12188  0mnnnnn0  12195  elnnnn0b  12207  nn0sub  12213  elnnz  12259  nnm1ge0  12318  gtndiv  12327  elpq  12644  elpqb  12645  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  nnrp  12670  nnledivrp  12771  qbtwnre  12862  fzo1fzo0n0  13366  ubmelfzo  13380  elfznelfzo  13420  adddivflid  13466  flltdivnn0lt  13481  quoremz  13503  quoremnn0ALT  13505  intfracq  13507  fldiv  13508  expnnval  13713  nnlesq  13850  expnngt1  13884  faclbnd  13932  bc0k  13953  ccatval21sw  14218  ccats1pfxeqrex  14356  harmonic  15499  nndivdvds  15900  evennn2n  15988  nnoddm1d2  16023  ndvdssub  16046  ndvdsadd  16047  sqgcd  16198  lcmgcdlem  16239  qredeu  16291  isprm5  16340  divdenle  16381  hashgcdlem  16417  oddprm  16439  pythagtriplem12  16455  pythagtriplem13  16456  pythagtriplem14  16457  pythagtriplem16  16459  pythagtriplem19  16462  pc2dvds  16508  fldivp1  16526  prmreclem3  16547  prmgaplem7  16686  mulgnn  18623  mulgnegnn  18629  odmodnn0  19063  prmirredlem  20606  znidomb  20681  fvmptnn04if  21906  chfacfscmul0  21915  chfacfpmmul0  21919  dyadss  24663  volivth  24676  vitali  24682  mbfi1fseqlem3  24787  itg2gt0  24830  dgrcolem2  25340  logtayllem  25719  leibpi  25997  eldmgm  26076  basellem6  26140  muinv  26247  logfac2  26270  bcmono  26330  bposlem5  26341  bposlem6  26342  lgsval4a  26372  gausslemma2dlem1a  26418  ostth2lem1  26671  ostth2lem3  26688  clwwlkf1  28314  clwwlknonccat  28361  minvecolem3  29139  xnn0gt0  30994  tgoldbachgtda  32541  subfaclim  33050  subfacval3  33051  snmlff  33191  nn0prpwlem  34438  nndivsub  34573  nndivlub  34574  poimirlem32  35736  fzmul  35826  factwoffsmonot  40091  negn0nposznnd  40231  nn0rppwr  40254  nn0expgcd  40256  irrapxlem1  40560  irrapxlem2  40561  pellexlem1  40567  monotoddzzfi  40680  rmynn  40694  jm2.24nn  40697  jm2.17c  40700  congabseq  40712  jm2.20nn  40735  rmydioph  40752  dgrsub2  40876  idomrootle  40936  rp-isfinite6  41023  stoweidlem17  43448  stoweidlem49  43480  wallispilem4  43499  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  fourierdlem73  43610  fourierdlem111  43648  2ffzoeq  44708  iccpartltu  44765  fmtnosqrt  44879  2pwp1prm  44929  nneven  45038