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

Metamath Proof Explorer

Theorem qexpz

Description: If a power of a rational number is an integer, then the number is an integer. In other words, all n-th roots are irrational unless they are integers (so that the original number is an n-th power). (Contributed by Mario Carneiro, 10-Aug-2015)

Ref Expression
Assertion qexpz ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → 𝐴 ∈ ℤ )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ∈ ℤ ↔ 0 ∈ ℤ ) )
2 simpll2 ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ )
3 2 nncnd ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℂ )
4 3 mul01d ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑁 · 0 ) = 0 )
5 simpr ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
6 simpll3 ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
7 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℚ )
8 qcn ⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
9 7 8 syl ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℂ )
10 simplr ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ≠ 0 )
11 2 nnzd ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℤ )
12 9 10 11 expne0d ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
13 pczcl ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ( 𝐴 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝐴 ↑ 𝑁 ) ≠ 0 ) ) → ( 𝑝 pCnt ( 𝐴 ↑ 𝑁 ) ) ∈ ℕ0 )
14 5 6 12 13 syl12anc ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝐴 ↑ 𝑁 ) ) ∈ ℕ0 )
15 14 nn0ge0d ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( 𝑝 pCnt ( 𝐴 ↑ 𝑁 ) ) )
16 pcexp ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑝 pCnt ( 𝐴 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝑝 pCnt 𝐴 ) ) )
17 5 7 10 11 16 syl121anc ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝐴 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝑝 pCnt 𝐴 ) ) )
18 15 17 breqtrd ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( 𝑁 · ( 𝑝 pCnt 𝐴 ) ) )
19 4 18 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑁 · 0 ) ≤ ( 𝑁 · ( 𝑝 pCnt 𝐴 ) ) )
20 0red ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 0 ∈ ℝ )
21 pcqcl ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑝 pCnt 𝐴 ) ∈ ℤ )
22 5 7 10 21 syl12anc ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℤ )
23 22 zred ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℝ )
24 2 nnred ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℝ )
25 2 nngt0d ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 0 < 𝑁 )
26 lemul2 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 0 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑁 · 0 ) ≤ ( 𝑁 · ( 𝑝 pCnt 𝐴 ) ) ) )
27 20 23 24 25 26 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( 𝑝 pCnt 𝐴 ) ↔ ( 𝑁 · 0 ) ≤ ( 𝑁 · ( 𝑝 pCnt 𝐴 ) ) ) )
28 19 27 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( 𝑝 pCnt 𝐴 ) )
29 28 ralrimiva ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) → ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) )
30 simpl1 ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℚ )
31 pcz ⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ∈ ℤ ↔ ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) ) )
32 30 31 syl ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) → ( 𝐴 ∈ ℤ ↔ ∀ 𝑝 ∈ ℙ 0 ≤ ( 𝑝 pCnt 𝐴 ) ) )
33 29 32 mpbird ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℤ )
34 0zd ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → 0 ∈ ℤ )
35 1 33 34 pm2.61ne ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → 𝐴 ∈ ℤ )