Theorem nngt0 11671

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 11647	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 11668	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 11164	. . 3 ⊢ 0 < 1
4		0re 10645	. . . 4 ⊢ 0 ∈ ℝ
5		1re 10643	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 10734	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1447	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 694	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 65	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538  0cc0 10539  1c1 10540   < clt 10677   ≤ cle 10678  ℕcn 11640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641

This theorem is referenced by:  nnnle0  11673  nngt0i  11679  nnsub  11684  nngt0d  11689  nnrecl  11898  nn0ge0  11925  0mnnnnn0  11932  elnnnn0b  11944  nn0sub  11950  elnnz  11994  nnm1ge0  12053  gtndiv  12062  elpq  12377  elpqb  12378  rpnnen1lem2  12379  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem5  12383  nnrp  12403  nnledivrp  12504  qbtwnre  12595  fzo1fzo0n0  13091  ubmelfzo  13105  elfznelfzo  13145  adddivflid  13191  flltdivnn0lt  13206  quoremz  13226  quoremnn0ALT  13228  intfracq  13230  fldiv  13231  expnnval  13435  nnlesq  13571  expnngt1  13605  faclbnd  13653  bc0k  13674  ccatval21sw  13941  ccats1pfxeqrex  14079  harmonic  15216  nndivdvds  15618  evennn2n  15702  nnoddm1d2  15739  ndvdssub  15762  ndvdsadd  15763  sqgcd  15911  lcmgcdlem  15952  qredeu  16004  isprm5  16053  divdenle  16091  hashgcdlem  16127  oddprm  16149  pythagtriplem12  16165  pythagtriplem13  16166  pythagtriplem14  16167  pythagtriplem16  16169  pythagtriplem19  16172  pc2dvds  16217  fldivp1  16235  prmreclem3  16256  prmgaplem7  16395  mulgnn  18234  mulgnegnn  18240  odmodnn0  18670  prmirredlem  20642  znidomb  20710  fvmptnn04if  21459  chfacfscmul0  21468  chfacfpmmul0  21472  dyadss  24197  volivth  24210  vitali  24216  mbfi1fseqlem3  24320  itg2gt0  24363  dgrcolem2  24866  logtayllem  25244  leibpi  25522  eldmgm  25601  basellem6  25665  muinv  25772  logfac2  25795  bcmono  25855  bposlem5  25866  bposlem6  25867  lgsval4a  25897  gausslemma2dlem1a  25943  ostth2lem1  26196  ostth2lem3  26213  clwwlkf1  27830  clwwlknonccat  27877  minvecolem3  28655  xnn0gt0  30496  tgoldbachgtda  31934  subfaclim  32437  subfacval3  32438  snmlff  32578  nn0prpwlem  33672  nndivsub  33807  nndivlub  33808  poimirlem32  34926  fzmul  35018  factwoffsmonot  39105  negn0nposznnd  39175  nn0rppwr  39189  nn0expgcd  39191  irrapxlem1  39426  irrapxlem2  39427  pellexlem1  39433  monotoddzzfi  39546  rmynn  39560  jm2.24nn  39563  jm2.17c  39566  congabseq  39578  jm2.20nn  39601  rmydioph  39618  dgrsub2  39742  idomrootle  39802  rp-isfinite6  39891  stoweidlem17  42309  stoweidlem49  42341  wallispilem4  42360  stirlinglem6  42371  stirlinglem7  42372  stirlinglem10  42375  fourierdlem73  42471  fourierdlem111  42509  2ffzoeq  43535  iccpartltu  43592  fmtnosqrt  43708  2pwp1prm  43758  nneven  43870