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 ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ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 ‘ 𝐴 ) ↑ 𝑁 ) ) )