Theorem nngt0 12291

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 12264	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 12288	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 11760	. . 3 ⊢ 0 < 1
4		0re 11234	. . . 4 ⊢ 0 ∈ ℝ
5		1re 11232	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 11326	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1480	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 709	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 66	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11123  0cc0 11124  1c1 11125   < clt 11267   ≤ cle 11268  ℕcn 12257

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 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

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 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258

This theorem is used by:  nnnle0  12293  nngt0i  12299  nnsub  12304  nngt0d  12309  nnrecl  12526  nn0ge0  12553  0mnnnnn0  12560  elnnnn0b  12572  nn0sub  12578  elnnz  12625  nnm1ge0  12689  gtndiv  12698  elpq  13025  elpqb  13026  rpnnen1lem2  13027  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  nnrp  13054  nnledivrp  13156  qbtwnre  13251  fzo1fzo0n0  13771  ubmelfzo  13786  elfznelfzo  13829  adddivflid  13879  flltdivnn0lt  13894  quoremz  13916  quoremnn0ALT  13918  intfracq  13920  fldiv  13921  expnnval  14128  nnlesq  14269  expnngt1  14305  faclbnd  14354  bc0k  14375  ccatval21sw  14651  ccats1pfxeqrex  14784  harmonic  15948  nndivdvds  16351  evennn2n  16441  nnoddm1d2  16476  ndvdssub  16499  ndvdsadd  16500  nn0rppwr  16651  sqgcd  16652  nn0expgcd  16654  lcmgcdlem  16696  qredeu  16748  isprm5  16798  divdenle  16840  hashgcdlem  16879  oddprm  16902  pythagtriplem12  16918  pythagtriplem13  16919  pythagtriplem14  16920  pythagtriplem16  16922  pythagtriplem19  16925  pc2dvds  16971  fldivp1  16989  prmreclem3  17010  prmgaplem7  17149  mulgnn  19198  mulgnegnn  19207  odmodnn0  19667  prmirredlem  21685  znidomb  21774  fvmptnn04if  23074  chfacfscmul0  23083  chfacfpmmul0  23087  dyadss  25822  volivth  25835  vitali  25841  mbfi1fseqlem3  25945  itg2gt0  25988  idomrootle  26398  dgrcolem2  26500  logtayllem  26896  leibpi  27179  eldmgm  27258  basellem6  27322  muinv  27429  logfac2  27453  bcmono  27513  bposlem5  27524  bposlem6  27525  lgsval4a  27555  gausslemma2dlem1a  27601  ostth2lem1  27854  ostth2lem3  27871  clwwlkf1  30519  clwwlknonccat  30566  minvecolem3  31357  xnn0gt0  33240  tgoldbachgtda  35169  subfaclim  35767  subfacval3  35768  snmlff  35908  nn0prpwlem  36941  nndivsub  37076  nndivlub  37077  poimirlem32  38401  fzmul  38491  negn0nposznnd  43157  fimgmcyc  43416  irrapxlem1  43663  irrapxlem2  43664  pellexlem1  43670  monotoddzzfi  43783  rmynn  43797  jm2.24nn  43800  jm2.17c  43803  congabseq  43815  jm2.20nn  43838  rmydioph  43855  dgrsub2  43976  rp-isfinite6  44358  rexanuz2nf  46320  stoweidlem17  46845  stoweidlem49  46877  wallispilem4  46896  stirlinglem6  46907  stirlinglem7  46908  stirlinglem10  46911  fourierdlem73  47007  fourierdlem111  47045  2ffzoeq  48216  modlt0b  48257  iccpartltu  48325  fmtnosqrt  48442  2pwp1prm  48492  nneven  48614