zrtdvds

Description: A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023)

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

Step	Hyp	Ref	Expression
1		nnz	$⊢ A^{\frac{1}{N}} \in ℕ \to A^{\frac{1}{N}} \in ℤ$
2	1	3ad2ant3	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℕ) \to A^{\frac{1}{N}} \in ℤ$
3		simp2	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℕ) \to N \in ℕ$
4		iddvdsexp	$⊢ (A^{\frac{1}{N}} \in ℤ \land N \in ℕ) \to A^{\frac{1}{N}} ∥ {(A^{\frac{1}{N}})}^{N}$
5	2 3 4	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℕ) \to A^{\frac{1}{N}} ∥ {(A^{\frac{1}{N}})}^{N}$
6		zcn	$⊢ A \in ℤ \to A \in ℂ$
7	6	3ad2ant1	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℕ) \to A \in ℂ$
8		cxproot	$⊢ (A \in ℂ \land N \in ℕ) \to {(A^{\frac{1}{N}})}^{N} = A$
9	7 3 8	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℕ) \to {(A^{\frac{1}{N}})}^{N} = A$
10	5 9	breqtrd	$⊢ (A \in ℤ \land N \in ℕ \land A^{\frac{1}{N}} \in ℕ) \to A^{\frac{1}{N}} ∥ A$

Metamath Proof Explorer