Metamath Proof Explorer

Theorem expsub

Description: Exponent subtraction law for integer exponentiation. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expsub ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 − 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
2 expaddz ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 + - 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ - 𝑁 ) ) )
3 1 2 sylanr2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 + - 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ - 𝑁 ) ) )
4 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
5 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
6 negsub ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
7 4 5 6 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
8 7 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
9 8 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 + - 𝑁 ) ) = ( 𝐴 ↑ ( 𝑀 − 𝑁 ) ) )
10 expnegz ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
11 10 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
12 11 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
13 12 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ - 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
14 expclz ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
15 14 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
16 15 adantrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
17 expclz ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
18 17 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
19 18 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
20 expne0i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
21 20 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
22 21 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
23 16 19 22 divrecd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
24 13 23 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ - 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )
25 3 9 24 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑀 − 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 𝐴 ↑ 𝑁 ) ) )