Theorem nnap0d 9189

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 9172	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 # 0)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 # 0)

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4088  0cc0 8032   # cap 8761  ℕcn 9143

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-mulrcl 8131  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-precex 8142  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-apti 8147  ax-pre-ltadd 8148  ax-pre-mulgt0 8149

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-reap 8755  df-ap 8762  df-inn 9144

This theorem is referenced by:  qtri3or  10501  qbtwnrelemcalc  10516  intfracq  10583  flqdiv  10584  modqmulnn  10605  facndiv  11002  bcn0  11018  bcn1  11021  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcpasc  11029  permnn  11034  divcnv  12063  trireciplem  12066  trirecip  12067  expcnvap0  12068  geo2sum  12080  geo2lim  12082  cvgratnnlemfm  12095  cvgratnnlemrate  12096  mertenslemi1  12101  eftabs  12222  efcllemp  12224  ege2le3  12237  efcj  12239  efaddlem  12240  eftlub  12256  eirraplem  12343  dvdsflip  12417  bitsp1  12517  bitsfzo  12521  bitsmod  12522  bitscmp  12524  bitsinv1lem  12527  dvdsgcdidd  12570  mulgcd  12592  gcddiv  12595  sqgcd  12605  lcmgcdlem  12654  qredeu  12674  prmind2  12697  isprm5lem  12718  divgcdodd  12720  sqrt2irrlem  12738  oddpwdclemxy  12746  oddpwdclemodd  12749  oddpwdclemdc  12750  sqrt2irraplemnn  12756  sqrt2irrap  12757  qmuldeneqnum  12772  divnumden  12773  numdensq  12779  hashdvds  12798  phiprmpw  12799  pythagtriplem19  12860  pcprendvds2  12869  pcpremul  12871  pceulem  12872  pceu  12873  pcdiv  12880  pcqmul  12881  pcid  12902  pc2dvds  12908  dvdsprmpweqle  12915  pcaddlem  12917  pcadd  12918  oddprmdvds  12932  pockthlem  12934  4sqlem5  12960  mul4sqlem  12971  4sqlem12  12980  4sqlem15  12983  4sqlem16  12984  4sqlem17  12985  znrrg  14680  logbgcd1irraplemexp  15698  logbgcd1irraplemap  15699  mpodvdsmulf1o  15720  mersenne  15727  perfect  15731  lgseisenlem2  15806  lgseisenlem4  15808  lgsquadlem1  15812  m1lgs  15820  2sqlem3  15852  2sqlem8  15858  cvgcmp2nlemabs  16662  redcwlpolemeq1  16685