Theorem nngt0 9063

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 9045	. 2 |- ( A e. NN -> A e. RR )
2		nnge1 9061	. 2 |- ( A e. NN -> 1 <_ A )
3		0lt1 8201	. . 3 |- 0 < 1
4		0re 8074	. . . 4 |- 0 e. RR
5		1re 8073	. . . 4 |- 1 e. RR
6		ltletr 8164	. . . 4 |- ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 <_ A ) -> 0 < A ) )
7	4, 5, 6	mp3an12 1340	. . 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 2176   class class class wbr 4045   RRcr 7926   0cc0 7927   1c1 7928   < clt 8109   <_ cle 8110   NNcn 9038

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 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254  ax-un 4481  ax-setind 4586  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024  ax-0lt1 8033  ax-0id 8035  ax-rnegex 8036  ax-pre-ltirr 8039  ax-pre-ltwlin 8040  ax-pre-lttrn 8041  ax-pre-ltadd 8043

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-nel 2472  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-br 4046  df-opab 4107  df-xp 4682  df-cnv 4684  df-iota 5233  df-fv 5280  df-ov 5949  df-pnf 8111  df-mnf 8112  df-xr 8113  df-ltxr 8114  df-le 8115  df-inn 9039

This theorem is referenced by:  nnap0  9067  nngt0i  9068  nn2ge  9071  nn1gt1  9072  nnsub  9077  nngt0d  9082  nnrecl  9295  nn0ge0  9322  0mnnnnn0  9329  elnnnn0b  9341  elnnz  9384  elnn0z  9387  ztri3or0  9416  nnnle0  9423  nnm1ge0  9461  gtndiv  9470  elpq  9772  elpqb  9773  nnrp  9787  nnledivrp  9890  fzo1fzo0n0  10309  ubmelfzo  10331  adddivflid  10437  flltdivnn0lt  10449  intfracq  10467  zmodcl  10491  zmodfz  10493  zmodid2  10499  m1modnnsub1  10517  expnnval  10689  nnlesq  10790  facdiv  10885  faclbnd  10888  bc0k  10903  ccatval21sw  11064  dvdsval3  12135  nndivdvds  12140  moddvds  12143  evennn2n  12227  nnoddm1d2  12254  divalglemnn  12262  ndvdssub  12274  ndvdsadd  12275  modgcd  12345  sqgcd  12383  lcmgcdlem  12432  qredeu  12452  divdenle  12552  hashgcdlem  12593  oddprm  12615  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem16  12635  pythagtriplem19  12638  pc2dvds  12686  fldivp1  12704  modsubi  12775  znnen  12802  exmidunben  12830  mulgnn  13495  mulgnegnn  13501  mulgmodid  13530  znf1o  14446  znidomb  14453  lgsval4a  15532  lgsne0  15548  gausslemma2dlem1a  15568