This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zrtelqelz

Description: If the N -th root of an integer A is rational, that root is must be an integer. Similar to zsqrtelqelz , generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023)

Ref Expression
Assertion zrtelqelz ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 qdencl ⊢ ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ → ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) ∈ ℕ )
2 1 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) ∈ ℕ )
3 2 nnrpd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) ∈ ℝ+ )
4 1rp ⊢ 1 ∈ ℝ+
5 4 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → 1 ∈ ℝ+ )
6 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → 𝑁 ∈ ℕ )
7 6 nnzd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → 𝑁 ∈ ℤ )
8 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
9 7 8 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( 1 ↑ 𝑁 ) = 1 )
10 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
11 10 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → 𝐴 ∈ ℂ )
12 cxproot ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 𝐴 )
13 11 6 12 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 𝐴 )
14 13 fveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) = ( denom ‘ 𝐴 ) )
15 zq ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℚ )
16 qden1elz ⊢ ( 𝐴 ∈ ℚ → ( ( denom ‘ 𝐴 ) = 1 ↔ 𝐴 ∈ ℤ ) )
17 15 16 syl ⊢ ( 𝐴 ∈ ℤ → ( ( denom ‘ 𝐴 ) = 1 ↔ 𝐴 ∈ ℤ ) )
18 17 ibir ⊢ ( 𝐴 ∈ ℤ → ( denom ‘ 𝐴 ) = 1 )
19 18 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ 𝐴 ) = 1 )
20 14 19 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) = 1 )
21 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ )
22 6 nnnn0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → 𝑁 ∈ ℕ0 )
23 denexp ⊢ ( ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( denom ‘ ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) = ( ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) ↑ 𝑁 ) )
24 21 22 23 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) = ( ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) ↑ 𝑁 ) )
25 9 20 24 3eqtr2rd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
26 3 5 6 25 exp11nnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) = 1 )
27 qden1elz ⊢ ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ → ( ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) = 1 ↔ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℤ ) )
28 27 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( ( denom ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ) = 1 ↔ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℤ ) )
29 26 28 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ) → ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℤ )