Theorem nngt0 9135

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

Assertion

Ref	Expression
nngt0	|- ( A e. NN -> 0 < A )

Proof of Theorem nngt0

Step	Hyp	Ref	Expression
1		nnre 9117	. 2 |- ( A e. NN -> A e. RR )
2		nnge1 9133	. 2 |- ( A e. NN -> 1 <_ A )
3		0lt1 8273	. . 3 |- 0 < 1
4		0re 8146	. . . 4 |- 0 e. RR
5		1re 8145	. . . 4 |- 1 e. RR
6		ltletr 8236	. . . 4 |- ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 <_ A ) -> 0 < A ) )
7	4, 5, 6	mp3an12 1361	. . 3 |- ( A e. RR -> ( ( 0 < 1 /\ 1 <_ A ) -> 0 < A ) )
8	3, 7	mpani 430	. 2 |- ( A e. RR -> ( 1 <_ A -> 0 < A ) )
9	1, 2, 8	sylc 62	1 |- ( A e. NN -> 0 < A )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200   class class class wbr 4083   RRcr 7998   0cc0 7999   1c1 8000   < clt 8181   <_ cle 8182   NNcn 9110

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096  ax-0lt1 8105  ax-0id 8107  ax-rnegex 8108  ax-pre-ltirr 8111  ax-pre-ltwlin 8112  ax-pre-lttrn 8113  ax-pre-ltadd 8115

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-xp 4725  df-cnv 4727  df-iota 5278  df-fv 5326  df-ov 6004  df-pnf 8183  df-mnf 8184  df-xr 8185  df-ltxr 8186  df-le 8187  df-inn 9111

This theorem is referenced by:  nnap0  9139  nngt0i  9140  nn2ge  9143  nn1gt1  9144  nnsub  9149  nngt0d  9154  nnrecl  9367  nn0ge0  9394  0mnnnnn0  9401  elnnnn0b  9413  elnnz  9456  elnn0z  9459  ztri3or0  9488  nnnle0  9495  nnm1ge0  9533  gtndiv  9542  elpq  9844  elpqb  9845  nnrp  9859  nnledivrp  9962  fzo1fzo0n0  10383  ubmelfzo  10406  adddivflid  10512  flltdivnn0lt  10524  intfracq  10542  zmodcl  10566  zmodfz  10568  zmodid2  10574  m1modnnsub1  10592  expnnval  10764  nnlesq  10865  facdiv  10960  faclbnd  10963  bc0k  10978  ccatval21sw  11140  ccats1pfxeqrex  11247  dvdsval3  12302  nndivdvds  12307  moddvds  12310  evennn2n  12394  nnoddm1d2  12421  divalglemnn  12429  ndvdssub  12441  ndvdsadd  12442  modgcd  12512  sqgcd  12550  lcmgcdlem  12599  qredeu  12619  divdenle  12719  hashgcdlem  12760  oddprm  12782  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem16  12802  pythagtriplem19  12805  pc2dvds  12853  fldivp1  12871  modsubi  12942  znnen  12969  exmidunben  12997  mulgnn  13663  mulgnegnn  13669  mulgmodid  13698  znf1o  14615  znidomb  14622  lgsval4a  15701  lgsne0  15717  gausslemma2dlem1a  15737