Theorem numdenexp

Description: numdensq extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023)

	Ref	Expression
Assertion	numdenexp	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( numer ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∧ ( denom ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qnumdencoprm	⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) = 1 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) = 1 )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
4		qnumcl	⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℤ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( numer ‘ 𝐴 ) ∈ ℤ )
6		qdencl	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( denom ‘ 𝐴 ) ∈ ℕ )
8	7	nnzd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( denom ‘ 𝐴 ) ∈ ℤ )
9		simpr	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
10		zexpgcd	⊢ ( ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) gcd ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) )
11	5 8 9 10	syl3anc	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) gcd ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) )
12		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
13		1exp	⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
14	9 12 13	3syl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 1 ↑ 𝑁 ) = 1 )
15	3 11 14	3eqtr3d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) gcd ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) = 1 )
16		qeqnumdivden	⊢ ( 𝐴 ∈ ℚ → 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) )
17	16	adantr	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) )
18	17	oveq1d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ↑ 𝑁 ) )
19	5	zcnd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( numer ‘ 𝐴 ) ∈ ℂ )
20	7	nncnd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( denom ‘ 𝐴 ) ∈ ℂ )
21	7	nnne0d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( denom ‘ 𝐴 ) ≠ 0 )
22	19 20 21 9	expdivd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) / ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) )
23	18 22	eqtrd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) / ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) )
24		qexpcl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ )
25		zexpcl	⊢ ( ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∈ ℤ )
26	4 25	sylan	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∈ ℤ )
27	7 9	nnexpcld	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ∈ ℕ )
28		qnumdenbi	⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℚ ∧ ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∈ ℤ ∧ ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ∈ ℕ ) → ( ( ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) gcd ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) = 1 ∧ ( 𝐴 ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) / ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) ) ↔ ( ( numer ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∧ ( denom ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) ) )
29	24 26 27 28	syl3anc	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) gcd ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) = 1 ∧ ( 𝐴 ↑ 𝑁 ) = ( ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) / ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) ) ↔ ( ( numer ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∧ ( denom ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) ) )
30	15 23 29	mpbi2and	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( ( numer ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( numer ‘ 𝐴 ) ↑ 𝑁 ) ∧ ( denom ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( denom ‘ 𝐴 ) ↑ 𝑁 ) ) )