Theorem nnap0d 8959

Description: A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)

Hypothesis

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

Assertion

Ref	Expression
nnap0d	⊢ (𝜑 → 𝐴 # 0)

Proof of Theorem nnap0d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnap0 8942	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 # 0)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 # 0)

Syntax hints:   → wi 4   ∈ wcel 2148   class class class wbr 4001  0cc0 7806   # cap 8532  ℕcn 8913

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-cnex 7897  ax-resscn 7898  ax-1cn 7899  ax-1re 7900  ax-icn 7901  ax-addcl 7902  ax-addrcl 7903  ax-mulcl 7904  ax-mulrcl 7905  ax-addcom 7906  ax-mulcom 7907  ax-addass 7908  ax-mulass 7909  ax-distr 7910  ax-i2m1 7911  ax-0lt1 7912  ax-1rid 7913  ax-0id 7914  ax-rnegex 7915  ax-precex 7916  ax-cnre 7917  ax-pre-ltirr 7918  ax-pre-ltwlin 7919  ax-pre-lttrn 7920  ax-pre-apti 7921  ax-pre-ltadd 7922  ax-pre-mulgt0 7923

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-br 4002  df-opab 4063  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-iota 5175  df-fun 5215  df-fv 5221  df-riota 5826  df-ov 5873  df-oprab 5874  df-mpo 5875  df-pnf 7988  df-mnf 7989  df-xr 7990  df-ltxr 7991  df-le 7992  df-sub 8124  df-neg 8125  df-reap 8526  df-ap 8533  df-inn 8914

This theorem is referenced by:  qtri3or  10236  qbtwnrelemcalc  10249  intfracq  10313  flqdiv  10314  modqmulnn  10335  facndiv  10710  bcn0  10726  bcn1  10729  bcm1k  10731  bcp1n  10732  bcp1nk  10733  bcval5  10734  bcpasc  10737  permnn  10742  divcnv  11496  trireciplem  11499  trirecip  11500  expcnvap0  11501  geo2sum  11513  geo2lim  11515  cvgratnnlemfm  11528  cvgratnnlemrate  11529  mertenslemi1  11534  eftabs  11655  efcllemp  11657  ege2le3  11670  efcj  11672  efaddlem  11673  eftlub  11689  eirraplem  11775  dvdsflip  11847  dvdsgcdidd  11985  mulgcd  12007  gcddiv  12010  sqgcd  12020  lcmgcdlem  12067  qredeu  12087  prmind2  12110  isprm5lem  12131  divgcdodd  12133  sqrt2irrlem  12151  oddpwdclemxy  12159  oddpwdclemodd  12162  oddpwdclemdc  12163  sqrt2irraplemnn  12169  sqrt2irrap  12170  qmuldeneqnum  12185  divnumden  12186  numdensq  12192  hashdvds  12211  phiprmpw  12212  pythagtriplem19  12272  pcprendvds2  12281  pcpremul  12283  pceulem  12284  pceu  12285  pcdiv  12292  pcqmul  12293  pcid  12313  pc2dvds  12319  dvdsprmpweqle  12326  pcaddlem  12328  pcadd  12329  oddprmdvds  12342  pockthlem  12344  4sqlem5  12370  mul4sqlem  12381  logbgcd1irraplemexp  14168  logbgcd1irraplemap  14169  2sqlem3  14235  2sqlem8  14241  cvgcmp2nlemabs  14551  redcwlpolemeq1  14573