Theorem numdenexp

Description: 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 ) ) )