Theorem nngt0 9161

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

Assertion

Ref	Expression
nngt0	⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Proof of Theorem nngt0

Step	Hyp	Ref	Expression
1		nnre 9143	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 9159	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 8299	. . 3 ⊢ 0 < 1
4		0re 8172	. . . 4 ⊢ 0 ∈ ℝ
5		1re 8171	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 8262	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1361	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 430	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 62	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200   class class class wbr 4086  ℝcr 8024  0cc0 8025  1c1 8026   < clt 8207   ≤ cle 8208  ℕcn 9136

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 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8116  ax-resscn 8117  ax-1re 8119  ax-addrcl 8122  ax-0lt1 8131  ax-0id 8133  ax-rnegex 8134  ax-pre-ltirr 8137  ax-pre-ltwlin 8138  ax-pre-lttrn 8139  ax-pre-ltadd 8141

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 2802  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-xp 4729  df-cnv 4731  df-iota 5284  df-fv 5332  df-ov 6016  df-pnf 8209  df-mnf 8210  df-xr 8211  df-ltxr 8212  df-le 8213  df-inn 9137

This theorem is referenced by:  nnap0  9165  nngt0i  9166  nn2ge  9169  nn1gt1  9170  nnsub  9175  nngt0d  9180  nnrecl  9393  nn0ge0  9420  0mnnnnn0  9427  elnnnn0b  9439  elnnz  9482  elnn0z  9485  ztri3or0  9514  nnnle0  9521  nnm1ge0  9559  gtndiv  9568  elpq  9876  elpqb  9877  nnrp  9891  nnledivrp  9994  fzo1fzo0n0  10415  ubmelfzo  10438  adddivflid  10545  flltdivnn0lt  10557  intfracq  10575  zmodcl  10599  zmodfz  10601  zmodid2  10607  m1modnnsub1  10625  expnnval  10797  nnlesq  10898  facdiv  10993  faclbnd  10996  bc0k  11011  ccatval21sw  11175  ccats1pfxeqrex  11289  dvdsval3  12345  nndivdvds  12350  moddvds  12353  evennn2n  12437  nnoddm1d2  12464  divalglemnn  12472  ndvdssub  12484  ndvdsadd  12485  modgcd  12555  sqgcd  12593  lcmgcdlem  12642  qredeu  12662  divdenle  12762  hashgcdlem  12803  oddprm  12825  pythagtriplem12  12841  pythagtriplem13  12842  pythagtriplem14  12843  pythagtriplem16  12845  pythagtriplem19  12848  pc2dvds  12896  fldivp1  12914  modsubi  12985  znnen  13012  exmidunben  13040  mulgnn  13706  mulgnegnn  13712  mulgmodid  13741  znf1o  14658  znidomb  14665  lgsval4a  15744  lgsne0  15760  gausslemma2dlem1a  15780  clwwlknonccat  16242