Theorem expsubd

Description: Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	expcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	sqrecd.1	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	expclzd.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	expsubd.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion	expsubd	⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑀 − 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		expcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		sqrecd.1	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		expclzd.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		expsubd.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		expsub	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 − 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )
6	1 2 4 3 5	syl22anc	⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑀 − 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )