Metamath Proof Explorer

Theorem expdiv

Description: Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expdiv ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 divrec ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
2 1 3expb ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
4 3 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑ 𝑁 ) )
5 reccl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ ℂ )
6 mulexp ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 / 𝐵 ) ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐵 ) ↑ 𝑁 ) ) )
7 5 6 syl3an2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐵 ) ↑ 𝑁 ) ) )
8 simp2l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
9 simp2r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ≠ 0 )
10 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
11 10 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
12 exprec ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 1 / 𝐵 ) ↑ 𝑁 ) = ( 1 / ( 𝐵 ↑ 𝑁 ) ) )
13 8 9 11 12 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 / 𝐵 ) ↑ 𝑁 ) = ( 1 / ( 𝐵 ↑ 𝑁 ) ) )
14 13 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐵 ) ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) · ( 1 / ( 𝐵 ↑ 𝑁 ) ) ) )
15 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
16 15 3adant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
17 expcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
18 17 adantlr ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
19 18 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
20 expne0i ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐵 ↑ 𝑁 ) ≠ 0 )
21 8 9 11 20 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ≠ 0 )
22 16 19 21 divrecd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑁 ) / ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) · ( 1 / ( 𝐵 ↑ 𝑁 ) ) ) )
23 14 22 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑁 ) · ( ( 1 / 𝐵 ) ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐵 ↑ 𝑁 ) ) )
24 4 7 23 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐵 ↑ 𝑁 ) ) )