zrtelqelz

Description: zsqrtelqelz generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023)

		Ref	Expression
	Assertion	zrtelqelz	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A^{\frac{1}{N}} \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		qdencl	$⊢ A^{\frac{1}{N}} \in ℚ \to denom (A^{\frac{1}{N}}) \in ℕ$
2	1	3ad2ant3	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom (A^{\frac{1}{N}}) \in ℕ$
3	2	nnrpd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom (A^{\frac{1}{N}}) \in ℝ^{+}$
4		1rp	$⊢ 1 \in ℝ^{+}$
5	4	a1i	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to 1 \in ℝ^{+}$
6		simp2	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to N \in ℕ$
7	6	nnzd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to N \in ℤ$
8	6	nnne0d	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to N \neq 0$
9		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
10	7 9	syl	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to 1^{N} = 1$
11		zcn	$⊢ A \in ℤ \to A \in ℂ$
12	11	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A \in ℂ$
13		cxproot	$⊢ (A \in ℂ \land N \in ℕ) \to {(A^{\frac{1}{N}})}^{N} = A$
14	12 6 13	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to {(A^{\frac{1}{N}})}^{N} = A$
15	14	fveq2d	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom ({(A^{\frac{1}{N}})}^{N}) = denom (A)$
16		zq	$⊢ A \in ℤ \to A \in ℚ$
17		qden1elz	$⊢ A \in ℚ \to (denom (A) = 1 \leftrightarrow A \in ℤ)$
18	16 17	syl	$⊢ A \in ℤ \to (denom (A) = 1 \leftrightarrow A \in ℤ)$
19	18	ibir	$⊢ A \in ℤ \to denom (A) = 1$
20	19	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom (A) = 1$
21	15 20	eqtrd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom ({(A^{\frac{1}{N}})}^{N}) = 1$
22		simp3	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A^{\frac{1}{N}} \in ℚ$
23	6	nnnn0d	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to N \in ℕ_{0}$
24		denexp	$⊢ (A^{\frac{1}{N}} \in ℚ \land N \in ℕ_{0}) \to denom ({(A^{\frac{1}{N}})}^{N}) = {denom (A^{\frac{1}{N}})}^{N}$
25	22 23 24	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom ({(A^{\frac{1}{N}})}^{N}) = {denom (A^{\frac{1}{N}})}^{N}$
26	10 21 25	3eqtr2rd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to {denom (A^{\frac{1}{N}})}^{N} = 1^{N}$
27	3 5 7 8 26	exp11d	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom (A^{\frac{1}{N}}) = 1$
28		qden1elz	$⊢ A^{\frac{1}{N}} \in ℚ \to (denom (A^{\frac{1}{N}}) = 1 \leftrightarrow A^{\frac{1}{N}} \in ℤ)$
29	28	3ad2ant3	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to (denom (A^{\frac{1}{N}}) = 1 \leftrightarrow A^{\frac{1}{N}} \in ℤ)$
30	27 29	mpbid	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A^{\frac{1}{N}} \in ℤ$

Metamath Proof Explorer

Theorem zrtelqelz

Proof