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

Metamath Proof Explorer

Theorem numdenexp

Description: Elevating a rational number to the power N has the same effect on its canonical components. Same as numdensq , extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023)

Ref Expression
Assertion numdenexp 
|- ( ( A e. QQ /\ N e. NN0 ) -> ( ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) /\ ( denom ` ( A ^ N ) ) = ( ( denom ` A ) ^ N ) ) )

Proof

Step Hyp Ref Expression
1 qnumdencoprm 
 |-  ( A e. QQ -> ( ( numer ` A ) gcd ( denom ` A ) ) = 1 )
2 1 adantr 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( numer ` A ) gcd ( denom ` A ) ) = 1 )
3 2 oveq1d 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( ( numer ` A ) gcd ( denom ` A ) ) ^ N ) = ( 1 ^ N ) )
4 qnumcl 
 |-  ( A e. QQ -> ( numer ` A ) e. ZZ )
5 4 adantr 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( numer ` A ) e. ZZ )
6 qdencl 
 |-  ( A e. QQ -> ( denom ` A ) e. NN )
7 6 adantr 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( denom ` A ) e. NN )
8 7 nnzd 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( denom ` A ) e. ZZ )
9 simpr 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> N e. NN0 )
10 zexpgcd 
 |-  ( ( ( numer ` A ) e. ZZ /\ ( denom ` A ) e. ZZ /\ N e. NN0 ) -> ( ( ( numer ` A ) gcd ( denom ` A ) ) ^ N ) = ( ( ( numer ` A ) ^ N ) gcd ( ( denom ` A ) ^ N ) ) )
11 5 8 9 10 syl3anc 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( ( numer ` A ) gcd ( denom ` A ) ) ^ N ) = ( ( ( numer ` A ) ^ N ) gcd ( ( denom ` A ) ^ N ) ) )
12 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
13 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
14 9 12 13 3syl 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( 1 ^ N ) = 1 )
15 3 11 14 3eqtr3d 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( ( numer ` A ) ^ N ) gcd ( ( denom ` A ) ^ N ) ) = 1 )
16 qeqnumdivden 
 |-  ( A e. QQ -> A = ( ( numer ` A ) / ( denom ` A ) ) )
17 16 adantr 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> A = ( ( numer ` A ) / ( denom ` A ) ) )
18 17 oveq1d 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( A ^ N ) = ( ( ( numer ` A ) / ( denom ` A ) ) ^ N ) )
19 5 zcnd 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( numer ` A ) e. CC )
20 7 nncnd 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( denom ` A ) e. CC )
21 7 nnne0d 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( denom ` A ) =/= 0 )
22 19 20 21 9 expdivd 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( ( numer ` A ) / ( denom ` A ) ) ^ N ) = ( ( ( numer ` A ) ^ N ) / ( ( denom ` A ) ^ N ) ) )
23 18 22 eqtrd 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( A ^ N ) = ( ( ( numer ` A ) ^ N ) / ( ( denom ` A ) ^ N ) ) )
24 qexpcl 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( A ^ N ) e. QQ )
25 zexpcl 
 |-  ( ( ( numer ` A ) e. ZZ /\ N e. NN0 ) -> ( ( numer ` A ) ^ N ) e. ZZ )
26 4 25 sylan 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( numer ` A ) ^ N ) e. ZZ )
27 7 9 nnexpcld 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( denom ` A ) ^ N ) e. NN )
28 qnumdenbi 
 |-  ( ( ( A ^ N ) e. QQ /\ ( ( numer ` A ) ^ N ) e. ZZ /\ ( ( denom ` A ) ^ N ) e. NN ) -> ( ( ( ( ( numer ` A ) ^ N ) gcd ( ( denom ` A ) ^ N ) ) = 1 /\ ( A ^ N ) = ( ( ( numer ` A ) ^ N ) / ( ( denom ` A ) ^ N ) ) ) <-> ( ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) /\ ( denom ` ( A ^ N ) ) = ( ( denom ` A ) ^ N ) ) ) )
29 24 26 27 28 syl3anc 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( ( ( ( numer ` A ) ^ N ) gcd ( ( denom ` A ) ^ N ) ) = 1 /\ ( A ^ N ) = ( ( ( numer ` A ) ^ N ) / ( ( denom ` A ) ^ N ) ) ) <-> ( ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) /\ ( denom ` ( A ^ N ) ) = ( ( denom ` A ) ^ N ) ) ) )
30 15 23 29 mpbi2and 
 |-  ( ( A e. QQ /\ N e. NN0 ) -> ( ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) /\ ( denom ` ( A ^ N ) ) = ( ( denom ` A ) ^ N ) ) )