numdenexp

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

		Ref	Expression
	Assertion	numdenexp	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to (numer (A^{N}) = {numer (A)}^{N} \land denom (A^{N}) = {denom (A)}^{N})$

Proof

Step	Hyp	Ref	Expression
1		qnumdencoprm	$⊢ A \in ℚ \to numer (A) \gcd denom (A) = 1$
2	1	adantr	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to numer (A) \gcd denom (A) = 1$
3	2	oveq1d	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to {(numer (A) \gcd denom (A))}^{N} = 1^{N}$
4		qnumcl	$⊢ A \in ℚ \to numer (A) \in ℤ$
5	4	adantr	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to numer (A) \in ℤ$
6		qdencl	$⊢ A \in ℚ \to denom (A) \in ℕ$
7	6	adantr	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to denom (A) \in ℕ$
8	7	nnzd	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to denom (A) \in ℤ$
9		simpr	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
10		zexpgcd	$⊢ (numer (A) \in ℤ \land denom (A) \in ℤ \land N \in ℕ_{0}) \to {(numer (A) \gcd denom (A))}^{N} = {numer (A)}^{N} \gcd {denom (A)}^{N}$
11	5 8 9 10	syl3anc	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to {(numer (A) \gcd denom (A))}^{N} = {numer (A)}^{N} \gcd {denom (A)}^{N}$
12		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
13		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
14	9 12 13	3syl	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to 1^{N} = 1$
15	3 11 14	3eqtr3d	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to {numer (A)}^{N} \gcd {denom (A)}^{N} = 1$
16		qeqnumdivden	$⊢ A \in ℚ \to A = \frac{numer (A)}{denom (A)}$
17	16	adantr	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to A = \frac{numer (A)}{denom (A)}$
18	17	oveq1d	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to A^{N} = {(\frac{numer (A)}{denom (A)})}^{N}$
19	5	zcnd	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to numer (A) \in ℂ$
20	7	nncnd	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to denom (A) \in ℂ$
21	7	nnne0d	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to denom (A) \neq 0$
22	19 20 21 9	expdivd	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to {(\frac{numer (A)}{denom (A)})}^{N} = \frac{{numer (A)}^{N}}{{denom (A)}^{N}}$
23	18 22	eqtrd	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to A^{N} = \frac{{numer (A)}^{N}}{{denom (A)}^{N}}$
24		qexpcl	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to A^{N} \in ℚ$
25		zexpcl	$⊢ (numer (A) \in ℤ \land N \in ℕ_{0}) \to {numer (A)}^{N} \in ℤ$
26	4 25	sylan	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to {numer (A)}^{N} \in ℤ$
27	7 9	nnexpcld	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to {denom (A)}^{N} \in ℕ$
28		qnumdenbi	$⊢ (A^{N} \in ℚ \land {numer (A)}^{N} \in ℤ \land {denom (A)}^{N} \in ℕ) \to (({numer (A)}^{N} \gcd {denom (A)}^{N} = 1 \land A^{N} = \frac{{numer (A)}^{N}}{{denom (A)}^{N}}) \leftrightarrow (numer (A^{N}) = {numer (A)}^{N} \land denom (A^{N}) = {denom (A)}^{N}))$
29	24 26 27 28	syl3anc	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to (({numer (A)}^{N} \gcd {denom (A)}^{N} = 1 \land A^{N} = \frac{{numer (A)}^{N}}{{denom (A)}^{N}}) \leftrightarrow (numer (A^{N}) = {numer (A)}^{N} \land denom (A^{N}) = {denom (A)}^{N}))$
30	15 23 29	mpbi2and	$⊢ (A \in ℚ \land N \in ℕ_{0}) \to (numer (A^{N}) = {numer (A)}^{N} \land denom (A^{N}) = {denom (A)}^{N})$

Metamath Proof Explorer

Theorem numdenexp

Proof