zrtelqelz

Description: If the N -th root of an integer A is rational, that root must be an integer. Generalization of zsqrtelqelz 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		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
9	7 8	syl	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to 1^{N} = 1$
10		zcn	$⊢ A \in ℤ \to A \in ℂ$
11	10	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A \in ℂ$
12		cxproot	$⊢ (A \in ℂ \land N \in ℕ) \to {(A^{\frac{1}{N}})}^{N} = A$
13	11 6 12	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to {(A^{\frac{1}{N}})}^{N} = A$
14	13	fveq2d	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom ({(A^{\frac{1}{N}})}^{N}) = denom (A)$
15		zq	$⊢ A \in ℤ \to A \in ℚ$
16		qden1elz	$⊢ A \in ℚ \to (denom (A) = 1 \leftrightarrow A \in ℤ)$
17	15 16	syl	$⊢ A \in ℤ \to (denom (A) = 1 \leftrightarrow A \in ℤ)$
18	17	ibir	$⊢ A \in ℤ \to denom (A) = 1$
19	18	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom (A) = 1$
20	14 19	eqtrd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom ({(A^{\frac{1}{N}})}^{N}) = 1$
21		simp3	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A^{\frac{1}{N}} \in ℚ$
22	6	nnnn0d	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to N \in ℕ_{0}$
23		denexp	$⊢ (A^{\frac{1}{N}} \in ℚ \land N \in ℕ_{0}) \to denom ({(A^{\frac{1}{N}})}^{N}) = {denom (A^{\frac{1}{N}})}^{N}$
24	21 22 23	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}$
25	9 20 24	3eqtr2rd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to {denom (A^{\frac{1}{N}})}^{N} = 1^{N}$
26	3 5 6 25	exp11nnd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to denom (A^{\frac{1}{N}}) = 1$
27		qden1elz	$⊢ A^{\frac{1}{N}} \in ℚ \to (denom (A^{\frac{1}{N}}) = 1 \leftrightarrow A^{\frac{1}{N}} \in ℤ)$
28	27	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 ℤ)$
29	26 28	mpbid	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℚ) \to A^{\frac{1}{N}} \in ℤ$

Metamath Proof Explorer

Theorem zrtelqelz

Proof