Theorem efsubd

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

	Ref	Expression
Hypotheses	efsubd.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	efsubd.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	efsubd	⊢ ( 𝜑 → ( exp ‘ ( 𝐴 − 𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		efsubd.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		efsubd.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		efsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 − 𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( exp ‘ ( 𝐴 − 𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) )