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

Theorem efcan 9869
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 7518 . . 3
2 efadd 9868 . . 3
31, 2mpdan 644 . 2
4 negid 7530 . . . 4
54fveq2d 4765 . . 3
6 ef0 9865 . . 3
75, 6syl6eq 1966 . 2
83, 7eqtr3d 1952 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1414   wcel 1416  cfv 4046  (class class class)co 5032  cc 7255  cc0 7257  c1 7258   caddc 7260   cmul 7262  cneg 7488  ce 9837
This theorem is referenced by:  efne0 9870  efneg 9871  efsub 9873  tanval3 9904  reeff1o 14282
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 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836  ax-inf2 6289  ax-resscn 7311  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-addrcl 7315  ax-mulcl 7316  ax-mulrcl 7317  ax-mulcom 7318  ax-addass 7319  ax-mulass 7320  ax-distr 7321  ax-i2m1 7322  ax-1ne0 7323  ax-1rid 7324  ax-rnegex 7325  ax-rrecex 7326  ax-cnre 7327  ax-pre-lttri 7328  ax-pre-lttrn 7329  ax-pre-ltadd 7330  ax-pre-mulgt0 7331  ax-pre-sup 7332
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 2329  df-sbc 2496  df-csb 2578  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-int 3281  df-iun 3320  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-lim 3723  df-suc 3724  df-om 4001  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-f1 4059  df-fo 4060  df-f1o 4061  df-fv 4062  df-iso 4063  df-ov 5034  df-oprab 5035  df-mpt 5196  df-mpt2 5197  df-1st 5333  df-2nd 5334  df-iota 5444  df-rdg 5535  df-1o 5572  df-oadd 5576  df-er 5710  df-map 5802  df-pm 5803  df-en 5869  df-dom 5870  df-sdom 5871  df-fin 5872  df-riota 6022  df-sup 6201  df-card 6455  df-pnf 7371  df-mnf 7372  df-xr 7373  df-ltxr 7374  df-le 7375  df-sub 7506  df-neg 7508  df-div 7734  df-n 7974  df-2 8020  df-3 8021  df-n0 8166  df-z 8217  df-uz 8411  df-q 8497  df-rp 8625  df-ico 8662  df-fz 8774  df-fl 8860  df-seq 8959  df-exp 9013  df-fac 9148  df-bc 9173  df-hash 9195  df-shft 9243  df-cj 9265  df-re 9266  df-im 9267  df-sqr 9361  df-abs 9362  df-limsup 9522  df-clim 9538  df-rlim 9539  df-sum 9673  df-ef 9843
Copyright terms: Public domain