Theorem nngt0d 9192

Description: A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnge1d.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nngt0d	|- ( ph -> 0 < A )

Proof of Theorem nngt0d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 |- ( ph -> A e. NN )
2		nngt0 9173	. 2 |- ( A e. NN -> 0 < A )
3	1, 2	syl 14	1 |- ( ph -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 2201   class class class wbr 4089   0cc0 8037   < clt 8219   NNcn 9148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-cnex 8128  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134  ax-0lt1 8143  ax-0id 8145  ax-rnegex 8146  ax-pre-ltirr 8149  ax-pre-ltwlin 8150  ax-pre-lttrn 8151  ax-pre-ltadd 8153

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-rab 2518  df-v 2803  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-br 4090  df-opab 4152  df-xp 4733  df-cnv 4735  df-iota 5288  df-fv 5336  df-ov 6026  df-pnf 8221  df-mnf 8222  df-xr 8223  df-ltxr 8224  df-le 8225  df-inn 9149

This theorem is referenced by:  flqdiv  10589  modqmulnn  10610  modifeq2int  10654  modaddmodup  10655  modaddmodlo  10656  modsumfzodifsn  10664  addmodlteq  10666  facubnd  11013  fihashgt0  11075  resqrexlemdecn  11595  modfsummodlemstep  12041  divcnv  12081  cvgratnnlemabsle  12111  fprodmodd  12225  efcllemp  12242  ege2le3  12255  eftlub  12274  eflegeo  12285  eirraplem  12361  dvdslelemd  12427  dvdsmod  12446  mulmoddvds  12447  divalgmod  12511  bitsfzo  12539  bitsmod  12540  bitsinv1lem  12545  bezoutlemnewy  12590  bezoutlemstep  12591  sqgcd  12623  eucalglt  12652  qredeu  12692  prmind2  12715  nprm  12718  sqrt2irraplemnn  12774  divdenle  12792  qnumgt0  12793  hashdvds  12816  crth  12819  phimullem  12820  eulerthlema  12825  fermltl  12829  prmdiv  12830  prmdiveq  12831  odzdvds  12841  powm2modprm  12848  modprm0  12850  nnnn0modprm0  12851  pythagtriplem11  12870  pythagtriplem13  12872  pythagtriplem19  12878  pcadd  12936  pcfaclem  12945  qexpz  12948  pockthlem  12952  pockthg  12953  4sqlem5  12978  4sqlem6  12979  4sqlem10  12983  4sqlem12  12998  4sqlem14  13000  4sqlem16  13002  wilthlem1  15733  perfectlem2  15753  lgsvalmod  15777  lgsmod  15784  lgsdirprm  15792  gausslemma2dlem0i  15815  gausslemma2dlem5a  15823  gausslemma2dlem6  15825  gausslemma2d  15827  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgseisenlem4  15831  lgseisen  15832  lgsquadlem1  15835  lgsquadlem2  15836  2sqlem8  15881  clwwlkgt0  16276  clwwlknonex2  16319