Theorem nngt0 12193

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 12169	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 12190	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 11676	. . 3 ⊢ 0 < 1
4		0re 11152	. . . 4 ⊢ 0 ∈ ℝ
5		1re 11150	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 11242	. . . 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 5102  ℝcr 11043  0cc0 11044  1c1 11045   < clt 11184   ≤ cle 11185  ℕcn 12162

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163

This theorem is referenced by:  nnnle0  12195  nngt0i  12201  nnsub  12206  nngt0d  12211  nnrecl  12416  nn0ge0  12443  0mnnnnn0  12450  elnnnn0b  12462  nn0sub  12468  elnnz  12515  nnm1ge0  12578  gtndiv  12587  elpq  12910  elpqb  12911  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  nnrp  12939  nnledivrp  13041  qbtwnre  13135  fzo1fzo0n0  13652  ubmelfzo  13667  elfznelfzo  13709  adddivflid  13756  flltdivnn0lt  13771  quoremz  13793  quoremnn0ALT  13795  intfracq  13797  fldiv  13798  expnnval  14005  nnlesq  14146  expnngt1  14182  faclbnd  14231  bc0k  14252  ccatval21sw  14526  ccats1pfxeqrex  14656  harmonic  15801  nndivdvds  16207  evennn2n  16297  nnoddm1d2  16332  ndvdssub  16355  ndvdsadd  16356  nn0rppwr  16507  sqgcd  16508  nn0expgcd  16510  lcmgcdlem  16552  qredeu  16604  isprm5  16653  divdenle  16695  hashgcdlem  16734  oddprm  16757  pythagtriplem12  16773  pythagtriplem13  16774  pythagtriplem14  16775  pythagtriplem16  16777  pythagtriplem19  16780  pc2dvds  16826  fldivp1  16844  prmreclem3  16865  prmgaplem7  17004  mulgnn  18983  mulgnegnn  18992  odmodnn0  19446  prmirredlem  21358  znidomb  21447  fvmptnn04if  22712  chfacfscmul0  22721  chfacfpmmul0  22725  dyadss  25471  volivth  25484  vitali  25490  mbfi1fseqlem3  25594  itg2gt0  25637  idomrootle  26054  dgrcolem2  26156  logtayllem  26544  leibpi  26828  eldmgm  26908  basellem6  26972  muinv  27079  logfac2  27104  bcmono  27164  bposlem5  27175  bposlem6  27176  lgsval4a  27206  gausslemma2dlem1a  27252  ostth2lem1  27505  ostth2lem3  27522  clwwlkf1  29951  clwwlknonccat  29998  minvecolem3  30778  xnn0gt0  32665  tgoldbachgtda  34625  subfaclim  35148  subfacval3  35149  snmlff  35289  nn0prpwlem  36283  nndivsub  36418  nndivlub  36419  poimirlem32  37619  fzmul  37708  negn0nposznnd  42243  fimgmcyc  42495  irrapxlem1  42783  irrapxlem2  42784  pellexlem1  42790  monotoddzzfi  42904  rmynn  42918  jm2.24nn  42921  jm2.17c  42924  congabseq  42936  jm2.20nn  42959  rmydioph  42976  dgrsub2  43097  rp-isfinite6  43480  rexanuz2nf  45461  stoweidlem17  45988  stoweidlem49  46020  wallispilem4  46039  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  fourierdlem73  46150  fourierdlem111  46188  2ffzoeq  47301  modlt0b  47337  iccpartltu  47399  fmtnosqrt  47513  2pwp1prm  47563  nneven  47672