HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem efcan 10529
Description: Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164.
Assertion
Ref Expression
efcan

Proof of Theorem efcan
StepHypRef Expression
1 negcl 8169 . . 3
2 efadd 10528 . . 3
31, 2mpdan 644 . 2
4 negid 8181 . . . 4
54fveq2d 4914 . . 3
6 ef0 10525 . . 3
75, 6syl6eq 2078 . 2
83, 7eqtr3d 2064 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1526   wcel 1528  cfv 4184  (class class class)co 5206  cc 7906  cc0 7908  c1 7909   caddc 7911   cmul 7913  cneg 8139  ce 10497
This theorem is referenced by:  efne0 10530  efneg 10531  efsub 10533  tanval3 10563  reeff1o 15265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-15 1904  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973  ax-inf2 6607  ax-resscn 7962  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-addrcl 7966  ax-mulcl 7967  ax-mulrcl 7968  ax-mulcom 7969  ax-addass 7970  ax-mulass 7971  ax-distr 7972  ax-i2m1 7973  ax-1ne0 7974  ax-1rid 7975  ax-rnegex 7976  ax-rrecex 7977  ax-cnre 7978  ax-pre-lttri 7979  ax-pre-lttrn 7980  ax-pre-ltadd 7981  ax-pre-mulgt0 7982  ax-pre-sup 7983
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1261  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-nel 2150  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-csb 2691  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-int 3409  df-iun 3451  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-f1 4197  df-fo 4198  df-f1o 4199  df-fv 4200  df-iso 4201  df-ov 5208  df-oprab 5209  df-mpt 5371  df-mpt2 5372  df-1st 5521  df-2nd 5522  df-iota 5647  df-recs 5722  df-rdg 5750  df-1o 5798  df-oadd 5802  df-er 5952  df-map 6044  df-pm 6045  df-en 6121  df-dom 6122  df-sdom 6123  df-fin 6124  df-riota 6281  df-sup 6474  df-card 6824  df-pnf 8022  df-mnf 8023  df-xr 8024  df-ltxr 8025  df-le 8026  df-sub 8157  df-neg 8159  df-div 8385  df-n 8625  df-2 8671  df-3 8672  df-n0 8817  df-z 8868  df-uz 9062  df-q 9148  df-rp 9277  df-ico 9314  df-fz 9426  df-fl 9512  df-seq 9612  df-exp 9667  df-fac 9804  df-bc 9830  df-hash 9852  df-shft 9901  df-cj 9923  df-re 9924  df-im 9925  df-sqr 10021  df-abs 10022  df-limsup 10180  df-clim 10196  df-rlim 10197  df-sum 10331  df-ef 10503
Copyright terms: Public domain