Theorem nngt0d 9330

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 9311	. 2 |- ( A e. NN -> 0 < A )
3	1, 2	syl 14	1 |- ( ph -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 2209   class class class wbr 4128   0cc0 8172   < clt 8353   NNcn 9286

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8263  ax-resscn 8264  ax-1re 8266  ax-addrcl 8269  ax-0lt1 8278  ax-0id 8280  ax-rnegex 8281  ax-pre-ltirr 8284  ax-pre-ltwlin 8285  ax-pre-lttrn 8286  ax-pre-ltadd 8288

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-br 4129  df-opab 4191  df-xp 4778  df-cnv 4780  df-iota 5335  df-fv 5383  df-ov 6081  df-pnf 8355  df-mnf 8356  df-xr 8357  df-ltxr 8358  df-le 8359  df-inn 9287

This theorem is referenced by:  flqdiv  10739  modqmulnn  10760  modifeq2int  10804  modaddmodup  10805  modaddmodlo  10806  modsumfzodifsn  10814  addmodlteq  10816  facubnd  11164  fihashgt0  11227  resqrexlemdecn  11759  modfsummodlemstep  12205  divcnv  12245  cvgratnnlemabsle  12275  fprodmodd  12389  efcllemp  12406  ege2le3  12419  eftlub  12438  eflegeo  12449  eirraplem  12525  dvdslelemd  12591  dvdsmod  12610  mulmoddvds  12611  divalgmod  12675  bitsfzo  12703  bitsmod  12704  bitsinv1lem  12709  bezoutlemnewy  12754  bezoutlemstep  12755  sqgcd  12787  eucalglt  12816  qredeu  12856  prmind2  12879  nprm  12882  sqrt2irraplemnn  12938  divdenle  12956  qnumgt0  12957  hashdvds  12980  crth  12983  phimullem  12984  eulerthlema  12989  fermltl  12993  prmdiv  12994  prmdiveq  12995  odzdvds  13005  powm2modprm  13012  modprm0  13014  nnnn0modprm0  13015  pythagtriplem11  13034  pythagtriplem13  13036  pythagtriplem19  13042  pcadd  13100  pcfaclem  13109  qexpz  13112  pockthlem  13116  pockthg  13117  4sqlem5  13142  4sqlem6  13143  4sqlem10  13147  4sqlem12  13162  4sqlem14  13164  4sqlem16  13166  pellexlem2  16009  wilthlem1  16011  perfectlem2  16031  lgsvalmod  16055  lgsmod  16062  lgsdirprm  16070  gausslemma2dlem0i  16093  gausslemma2dlem5a  16101  gausslemma2dlem6  16103  gausslemma2d  16105  lgseisenlem1  16106  lgseisenlem2  16107  lgseisenlem3  16108  lgseisenlem4  16109  lgseisen  16110  lgsquadlem1  16113  lgsquadlem2  16114  2sqlem8  16159  clwwlkgt0  16554  clwwlknonex2  16597