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

Theorem efcan 9568
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 7361 . . 3
2 efadd 9567 . . 3
31, 2mpdan 643 . 2
4 negid 7373 . . . 4
54fveq2d 4694 . . 3
6 ef0 9564 . . 3
75, 6syl6eq 1965 . 2
83, 7eqtr3d 1951 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1413   wcel 1415  cfv 4007  (class class class)co 4944  cc 7105  cc0 7107  c1 7108   caddc 7110   cmul 7112  cneg 7331  ce 9536
This theorem is referenced by:  efne0 9569  efneg 9570  efsub 9572  reeff1o 13273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-15 1791  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-inf2 6154  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-mulcom 7168  ax-addass 7169  ax-mulass 7170  ax-distr 7171  ax-i2m1 7172  ax-1ne0 7173  ax-1rid 7174  ax-rnegex 7175  ax-rrecex 7176  ax-cnre 7177  ax-pre-lttri 7178  ax-pre-lttrn 7179  ax-pre-ltadd 7180  ax-pre-mulgt0 7181  ax-pre-sup 7182
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-nel 2037  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-iso 4024  df-ov 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-1st 5231  df-2nd 5232  df-iota 5336  df-rdg 5424  df-1o 5461  df-oadd 5465  df-er 5598  df-map 5690  df-pm 5691  df-en 5750  df-dom 5751  df-sdom 5752  df-fin 5753  df-riota 5896  df-sup 6075  df-card 6318  df-pnf 7220  df-mnf 7221  df-xr 7222  df-ltxr 7223  df-le 7224  df-sub 7349  df-neg 7351  df-div 7575  df-n 7814  df-2 7860  df-3 7861  df-n0 7984  df-z 8029  df-uz 8149  df-q 8231  df-rp 8356  df-ico 8393  df-fz 8501  df-fl 8595  df-seq 8688  df-exp 8741  df-fac 8873  df-bc 8898  df-hash 8920  df-shft 8962  df-cj 8984  df-re 8985  df-im 8986  df-sqr 9078  df-abs 9079  df-limsup 9233  df-clim 9249  df-rlim 9250  df-sum 9375  df-ef 9542
Copyright terms: Public domain