Theorem nngt0 12177

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 12153	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 12174	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 11660	. . 3 ⊢ 0 < 1
4		0re 11136	. . . 4 ⊢ 0 ∈ ℝ
5		1re 11134	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 11226	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1453	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 696	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 65	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027  0cc0 11028  1c1 11029   < clt 11168   ≤ cle 11169  ℕcn 12146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-nn 12147

This theorem is referenced by:  nnnle0  12179  nngt0i  12185  nnsub  12190  nngt0d  12195  nnrecl  12400  nn0ge0  12427  0mnnnnn0  12434  elnnnn0b  12446  nn0sub  12452  elnnz  12499  nnm1ge0  12562  gtndiv  12571  elpq  12894  elpqb  12895  rpnnen1lem2  12896  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  nnrp  12923  nnledivrp  13025  qbtwnre  13119  fzo1fzo0n0  13636  ubmelfzo  13651  elfznelfzo  13693  adddivflid  13740  flltdivnn0lt  13755  quoremz  13777  quoremnn0ALT  13779  intfracq  13781  fldiv  13782  expnnval  13989  nnlesq  14130  expnngt1  14166  faclbnd  14215  bc0k  14236  ccatval21sw  14510  ccats1pfxeqrex  14639  harmonic  15784  nndivdvds  16190  evennn2n  16280  nnoddm1d2  16315  ndvdssub  16338  ndvdsadd  16339  nn0rppwr  16490  sqgcd  16491  nn0expgcd  16493  lcmgcdlem  16535  qredeu  16587  isprm5  16636  divdenle  16678  hashgcdlem  16717  oddprm  16740  pythagtriplem12  16756  pythagtriplem13  16757  pythagtriplem14  16758  pythagtriplem16  16760  pythagtriplem19  16763  pc2dvds  16809  fldivp1  16827  prmreclem3  16848  prmgaplem7  16987  mulgnn  18972  mulgnegnn  18981  odmodnn0  19437  prmirredlem  21397  znidomb  21486  fvmptnn04if  22752  chfacfscmul0  22761  chfacfpmmul0  22765  dyadss  25511  volivth  25524  vitali  25530  mbfi1fseqlem3  25634  itg2gt0  25677  idomrootle  26094  dgrcolem2  26196  logtayllem  26584  leibpi  26868  eldmgm  26948  basellem6  27012  muinv  27119  logfac2  27144  bcmono  27204  bposlem5  27215  bposlem6  27216  lgsval4a  27246  gausslemma2dlem1a  27292  ostth2lem1  27545  ostth2lem3  27562  clwwlkf1  30011  clwwlknonccat  30058  minvecolem3  30838  xnn0gt0  32725  tgoldbachgtda  34631  subfaclim  35163  subfacval3  35164  snmlff  35304  nn0prpwlem  36298  nndivsub  36433  nndivlub  36434  poimirlem32  37634  fzmul  37723  negn0nposznnd  42258  fimgmcyc  42510  irrapxlem1  42798  irrapxlem2  42799  pellexlem1  42805  monotoddzzfi  42918  rmynn  42932  jm2.24nn  42935  jm2.17c  42938  congabseq  42950  jm2.20nn  42973  rmydioph  42990  dgrsub2  43111  rp-isfinite6  43494  rexanuz2nf  45475  stoweidlem17  46002  stoweidlem49  46034  wallispilem4  46053  stirlinglem6  46064  stirlinglem7  46065  stirlinglem10  46068  fourierdlem73  46164  fourierdlem111  46202  2ffzoeq  47315  modlt0b  47351  iccpartltu  47413  fmtnosqrt  47527  2pwp1prm  47577  nneven  47686