Metamath Proof Explorer


Theorem efsubd

Description: Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses efsubd.a
|- ( ph -> A e. CC )
efsubd.b
|- ( ph -> B e. CC )
Assertion efsubd
|- ( ph -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) )

Proof

Step Hyp Ref Expression
1 efsubd.a
 |-  ( ph -> A e. CC )
2 efsubd.b
 |-  ( ph -> B e. CC )
3 efsub
 |-  ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) )
4 1 2 3 syl2anc
 |-  ( ph -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) )