ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nngt0 Unicode version

Theorem nngt0 8385
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
StepHypRef Expression
1 nnre 8367 . 2  |-  ( A  e.  NN  ->  A  e.  RR )
2 nnge1 8383 . 2  |-  ( A  e.  NN  ->  1  <_  A )
3 0lt1 7557 . . 3  |-  0  <  1
4 0re 7435 . . . 4  |-  0  e.  RR
5 1re 7434 . . . 4  |-  1  e.  RR
6 ltletr 7521 . . . 4  |-  ( ( 0  e.  RR  /\  1  e.  RR  /\  A  e.  RR )  ->  (
( 0  <  1  /\  1  <_  A )  ->  0  <  A
) )
74, 5, 6mp3an12 1261 . . 3  |-  ( A  e.  RR  ->  (
( 0  <  1  /\  1  <_  A )  ->  0  <  A
) )
83, 7mpani 421 . 2  |-  ( A  e.  RR  ->  (
1  <_  A  ->  0  <  A ) )
91, 2, 8sylc 61 1  |-  ( A  e.  NN  ->  0  <  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1436   class class class wbr 3822   RRcr 7296   0cc0 7297   1c1 7298    < clt 7469    <_ cle 7470   NNcn 8360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-cnex 7383  ax-resscn 7384  ax-1re 7386  ax-addrcl 7389  ax-0lt1 7398  ax-0id 7400  ax-rnegex 7401  ax-pre-ltirr 7404  ax-pre-ltwlin 7405  ax-pre-lttrn 7406  ax-pre-ltadd 7408
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-br 3823  df-opab 3877  df-xp 4419  df-cnv 4421  df-iota 4948  df-fv 4991  df-ov 5618  df-pnf 7471  df-mnf 7472  df-xr 7473  df-ltxr 7474  df-le 7475  df-inn 8361
This theorem is referenced by:  nnap0  8389  nngt0i  8390  nn2ge  8392  nn1gt1  8393  nnsub  8398  nngt0d  8403  nnrecl  8607  nn0ge0  8634  0mnnnnn0  8641  elnnnn0b  8653  elnnz  8696  elnn0z  8699  ztri3or0  8728  nnm1ge0  8768  gtndiv  8777  nnrp  9078  nnledivrp  9172  fzo1fzo0n0  9525  ubmelfzo  9542  adddivflid  9630  flltdivnn0lt  9642  intfracq  9658  zmodcl  9682  zmodfz  9684  zmodid2  9690  m1modnnsub1  9708  expinnval  9860  nnlesq  9959  facdiv  10046  faclbnd  10049  bc0k  10064  dvdsval3  10706  nndivdvds  10708  moddvds  10711  evennn2n  10789  nnoddm1d2  10816  divalglemnn  10824  ndvdssub  10836  ndvdsadd  10837  modgcd  10888  sqgcd  10924  lcmgcdlem  10965  qredeu  10985  divdenle  11081  hashgcdlem  11109  znnen  11117
  Copyright terms: Public domain W3C validator