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

Theorem efcan 9634
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 7424 . . 3
2 efadd 9633 . . 3
31, 2mpdan 644 . 2
4 negid 7436 . . . 4
54fveq2d 4721 . . 3
6 ef0 9630 . . 3
75, 6syl6eq 1966 . 2
83, 7eqtr3d 1952 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1414   wcel 1416  cfv 4019  (class class class)co 4979  cc 7168  cc0 7170  c1 7171   caddc 7173   cmul 7175  cneg 7394  ce 9602
This theorem is referenced by:  efne0 9635  efneg 9636  efsub 9638  reeff1o 13463
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-15 1792  ax-ext 1900  ax-rep 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809  ax-inf2 6217  ax-resscn 7224  ax-1cn 7225  ax-icn 7226  ax-addcl 7227  ax-addrcl 7228  ax-mulcl 7229  ax-mulrcl 7230  ax-mulcom 7231  ax-addass 7232  ax-mulass 7233  ax-distr 7234  ax-i2m1 7235  ax-1ne0 7236  ax-1rid 7237  ax-rnegex 7238  ax-rrecex 7239  ax-cnre 7240  ax-pre-lttri 7241  ax-pre-lttrn 7242  ax-pre-ltadd 7243  ax-pre-mulgt0 7244  ax-pre-sup 7245
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-nel 2038  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2326  df-sbc 2493  df-csb 2575  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-if 3009  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-int 3258  df-iun 3297  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3974  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-f1 4032  df-fo 4033  df-f1o 4034  df-fv 4035  df-iso 4036  df-ov 4981  df-oprab 4982  df-mpt 5142  df-mpt2 5143  df-1st 5269  df-2nd 5270  df-iota 5377  df-rdg 5468  df-1o 5505  df-oadd 5509  df-er 5643  df-map 5735  df-pm 5736  df-en 5800  df-dom 5801  df-sdom 5802  df-fin 5803  df-riota 5951  df-sup 6131  df-card 6381  df-pnf 7283  df-mnf 7284  df-xr 7285  df-ltxr 7286  df-le 7287  df-sub 7412  df-neg 7414  df-div 7638  df-n 7877  df-2 7923  df-3 7924  df-n0 8049  df-z 8094  df-uz 8214  df-q 8296  df-rp 8421  df-ico 8458  df-fz 8566  df-fl 8660  df-seq 8754  df-exp 8807  df-fac 8939  df-bc 8964  df-hash 8986  df-shft 9028  df-cj 9050  df-re 9051  df-im 9052  df-sqr 9144  df-abs 9145  df-limsup 9299  df-clim 9315  df-rlim 9316  df-sum 9441  df-ef 9608
Copyright terms: Public domain