Theorem expne0d 13722

Description: Nonnegative integer exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
expcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
sqrecd.1	⊢ (𝜑 → 𝐴 ≠ 0)
expclzd.3	⊢ (𝜑 → 𝑁 ∈ ℤ)

Assertion

Ref	Expression
expne0d	⊢ (𝜑 → (𝐴↑𝑁) ≠ 0)

Proof of Theorem expne0d

Step	Hyp	Ref	Expression
1		expcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		sqrecd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
3		expclzd.3	. 2 ⊢ (𝜑 → 𝑁 ∈ ℤ)
4		expne0i 13667	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ≠ 0)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → (𝐴↑𝑁) ≠ 0)

Syntax hints:   → wi 4   ∈ wcel 2110   ≠ wne 2940  (class class class)co 7213  ℂcc 10727  0cc0 10729  ℤcz 12176  ↑cexp 13635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-seq 13575  df-exp 13636

This theorem is referenced by:  znsqcld  13732  absexpz  14869  0.999...  15445  bitsfzo  15994  bitsmod  15995  bitsinv1lem  16000  bitsuz  16033  pcexp  16412  dvdsprmpweqle  16439  pcaddlem  16441  pcadd  16442  qexpz  16454  dvrecg  24870  dvexp3  24875  plyeq0lem  25104  aareccl  25219  taylthlem2  25266  root1cj  25642  cxpeq  25643  dcubic1lem  25726  dcubic2  25727  cubic2  25731  cubic  25732  lgamgulmlem4  25914  basellem4  25966  basellem8  25970  lgseisenlem1  26256  lgseisenlem2  26257  lgsquadlem1  26261  dya2icoseg  31956  dya2iocucvr  31963  omssubadd  31979  oddpwdc  32033  signsplypnf  32241  signsply0  32242  knoppndvlem7  34435  knoppndvlem17  34445  dvrelogpow2b  39809  aks4d1p1p6  39814  aks4d1p1p7  39815  aks4d1p1p5  39816  exp11d  40033  dffltz  40174  fltdiv  40176  fltnlta  40203  3cubeslem4  40214  rmxyneg  40445  radcnvrat  41605  dvdivbd  43139  iblsplit  43182  wallispi2lem1  43287  wallispi2lem2  43288  wallispi2  43289  stirlinglem3  43292  stirlinglem4  43293  stirlinglem7  43296  stirlinglem8  43297  stirlinglem10  43299  stirlinglem13  43302  stirlinglem14  43303  stirlinglem15  43304  fourierdlem56  43378  fourierdlem57  43379  elaa2lem  43449  sge0ad2en  43644  ovnsubaddlem1  43783  fldivexpfllog2  45584  nn0digval  45619  dignnld  45622  dig2nn1st  45624  dig2bits  45633  dignn0flhalflem1  45634  dignn0flhalflem2  45635  dignn0ehalf  45636  itsclc0xyqsolr  45788