Theorem nngt0d 9062

Description: A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnge1d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nngt0d	⊢ (𝜑 → 0 < 𝐴)

Proof of Theorem nngt0d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nngt0 9043	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2175   class class class wbr 4043  0cc0 7907   < clt 8089  ℕcn 9018

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 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-cnex 7998  ax-resscn 7999  ax-1re 8001  ax-addrcl 8004  ax-0lt1 8013  ax-0id 8015  ax-rnegex 8016  ax-pre-ltirr 8019  ax-pre-ltwlin 8020  ax-pre-lttrn 8021  ax-pre-ltadd 8023

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-xp 4679  df-cnv 4681  df-iota 5229  df-fv 5276  df-ov 5937  df-pnf 8091  df-mnf 8092  df-xr 8093  df-ltxr 8094  df-le 8095  df-inn 9019

This theorem is referenced by:  flqdiv  10447  modqmulnn  10468  modifeq2int  10512  modaddmodup  10513  modaddmodlo  10514  modsumfzodifsn  10522  addmodlteq  10524  facubnd  10871  resqrexlemdecn  11242  modfsummodlemstep  11687  divcnv  11727  cvgratnnlemabsle  11757  fprodmodd  11871  efcllemp  11888  ege2le3  11901  eftlub  11920  eflegeo  11931  eirraplem  12007  dvdslelemd  12073  dvdsmod  12092  mulmoddvds  12093  divalgmod  12157  bitsfzo  12185  bitsmod  12186  bitsinv1lem  12191  bezoutlemnewy  12236  bezoutlemstep  12237  sqgcd  12269  eucalglt  12298  qredeu  12338  prmind2  12361  nprm  12364  sqrt2irraplemnn  12420  divdenle  12438  qnumgt0  12439  hashdvds  12462  crth  12465  phimullem  12466  eulerthlema  12471  fermltl  12475  prmdiv  12476  prmdiveq  12477  odzdvds  12487  powm2modprm  12494  modprm0  12496  nnnn0modprm0  12497  pythagtriplem11  12516  pythagtriplem13  12518  pythagtriplem19  12524  pcadd  12582  pcfaclem  12591  qexpz  12594  pockthlem  12598  pockthg  12599  4sqlem5  12624  4sqlem6  12625  4sqlem10  12629  4sqlem12  12644  4sqlem14  12646  4sqlem16  12648  wilthlem1  15370  perfectlem2  15390  lgsvalmod  15414  lgsmod  15421  lgsdirprm  15429  gausslemma2dlem0i  15452  gausslemma2dlem5a  15460  gausslemma2dlem6  15462  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgseisen  15469  lgsquadlem1  15472  lgsquadlem2  15473  2sqlem8  15518