Theorem nngt0 12217

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 12193	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 12214	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 11700	. . 3 ⊢ 0 < 1
4		0re 11176	. . . 4 ⊢ 0 ∈ ℝ
5		1re 11174	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 11266	. . . 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 5107  ℝcr 11067  0cc0 11068  1c1 11069   < clt 11208   ≤ cle 11209  ℕcn 12186

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187

This theorem is referenced by:  nnnle0  12219  nngt0i  12225  nnsub  12230  nngt0d  12235  nnrecl  12440  nn0ge0  12467  0mnnnnn0  12474  elnnnn0b  12486  nn0sub  12492  elnnz  12539  nnm1ge0  12602  gtndiv  12611  elpq  12934  elpqb  12935  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  nnrp  12963  nnledivrp  13065  qbtwnre  13159  fzo1fzo0n0  13676  ubmelfzo  13691  elfznelfzo  13733  adddivflid  13780  flltdivnn0lt  13795  quoremz  13817  quoremnn0ALT  13819  intfracq  13821  fldiv  13822  expnnval  14029  nnlesq  14170  expnngt1  14206  faclbnd  14255  bc0k  14276  ccatval21sw  14550  ccats1pfxeqrex  14680  harmonic  15825  nndivdvds  16231  evennn2n  16321  nnoddm1d2  16356  ndvdssub  16379  ndvdsadd  16380  nn0rppwr  16531  sqgcd  16532  nn0expgcd  16534  lcmgcdlem  16576  qredeu  16628  isprm5  16677  divdenle  16719  hashgcdlem  16758  oddprm  16781  pythagtriplem12  16797  pythagtriplem13  16798  pythagtriplem14  16799  pythagtriplem16  16801  pythagtriplem19  16804  pc2dvds  16850  fldivp1  16868  prmreclem3  16889  prmgaplem7  17028  mulgnn  19007  mulgnegnn  19016  odmodnn0  19470  prmirredlem  21382  znidomb  21471  fvmptnn04if  22736  chfacfscmul0  22745  chfacfpmmul0  22749  dyadss  25495  volivth  25508  vitali  25514  mbfi1fseqlem3  25618  itg2gt0  25661  idomrootle  26078  dgrcolem2  26180  logtayllem  26568  leibpi  26852  eldmgm  26932  basellem6  26996  muinv  27103  logfac2  27128  bcmono  27188  bposlem5  27199  bposlem6  27200  lgsval4a  27230  gausslemma2dlem1a  27276  ostth2lem1  27529  ostth2lem3  27546  clwwlkf1  29978  clwwlknonccat  30025  minvecolem3  30805  xnn0gt0  32692  tgoldbachgtda  34652  subfaclim  35175  subfacval3  35176  snmlff  35316  nn0prpwlem  36310  nndivsub  36445  nndivlub  36446  poimirlem32  37646  fzmul  37735  negn0nposznnd  42270  fimgmcyc  42522  irrapxlem1  42810  irrapxlem2  42811  pellexlem1  42817  monotoddzzfi  42931  rmynn  42945  jm2.24nn  42948  jm2.17c  42951  congabseq  42963  jm2.20nn  42986  rmydioph  43003  dgrsub2  43124  rp-isfinite6  43507  rexanuz2nf  45488  stoweidlem17  46015  stoweidlem49  46047  wallispilem4  46066  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  fourierdlem73  46177  fourierdlem111  46215  2ffzoeq  47325  modlt0b  47361  iccpartltu  47423  fmtnosqrt  47537  2pwp1prm  47587  nneven  47696