This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A / B ) ^ N ) = ( ( A ^ N ) / ( B ^ N ) ) )

Proof

Step Hyp Ref Expression
1 divrec 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
2 1 3expb 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
3 2 3adant3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
4 3 oveq1d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A / B ) ^ N ) = ( ( A x. ( 1 / B ) ) ^ N ) )
5 reccl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
6 mulexp 
 |-  ( ( A e. CC /\ ( 1 / B ) e. CC /\ N e. NN0 ) -> ( ( A x. ( 1 / B ) ) ^ N ) = ( ( A ^ N ) x. ( ( 1 / B ) ^ N ) ) )
7 5 6 syl3an2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A x. ( 1 / B ) ) ^ N ) = ( ( A ^ N ) x. ( ( 1 / B ) ^ N ) ) )
8 simp2l 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> B e. CC )
9 simp2r 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> B =/= 0 )
10 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
11 10 3ad2ant3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> N e. ZZ )
12 exprec 
 |-  ( ( B e. CC /\ B =/= 0 /\ N e. ZZ ) -> ( ( 1 / B ) ^ N ) = ( 1 / ( B ^ N ) ) )
13 8 9 11 12 syl3anc 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( 1 / B ) ^ N ) = ( 1 / ( B ^ N ) ) )
14 13 oveq2d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A ^ N ) x. ( ( 1 / B ) ^ N ) ) = ( ( A ^ N ) x. ( 1 / ( B ^ N ) ) ) )
15 expcl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A ^ N ) e. CC )
16 15 3adant2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( A ^ N ) e. CC )
17 expcl 
 |-  ( ( B e. CC /\ N e. NN0 ) -> ( B ^ N ) e. CC )
18 17 adantlr 
 |-  ( ( ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( B ^ N ) e. CC )
19 18 3adant1 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( B ^ N ) e. CC )
20 expne0i 
 |-  ( ( B e. CC /\ B =/= 0 /\ N e. ZZ ) -> ( B ^ N ) =/= 0 )
21 8 9 11 20 syl3anc 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( B ^ N ) =/= 0 )
22 16 19 21 divrecd 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A ^ N ) / ( B ^ N ) ) = ( ( A ^ N ) x. ( 1 / ( B ^ N ) ) ) )
23 14 22 eqtr4d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A ^ N ) x. ( ( 1 / B ) ^ N ) ) = ( ( A ^ N ) / ( B ^ N ) ) )
24 4 7 23 3eqtrd 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A / B ) ^ N ) = ( ( A ^ N ) / ( B ^ N ) ) )