Metamath Proof Explorer

Theorem expnprm

Description: A second or higher power of a rational number is not a prime number. Or by contraposition, the n-th root of a prime number is irrational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015)

Ref Expression
Assertion expnprm ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝐴 ↑ 𝑁 ) ∈ ℙ )

Proof

Step Hyp Ref Expression
1 eluz2b3 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
2 1 simprbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≠ 1 )
3 2 adantl ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ≠ 1 )
4 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
5 4 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → 𝑁 ∈ ℤ )
6 simpr ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℙ )
7 simpll ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → 𝐴 ∈ ℚ )
8 prmnn ⊢ ( ( 𝐴 ↑ 𝑁 ) ∈ ℙ → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
9 8 adantl ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
10 9 nnne0d ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ≠ 0 )
11 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
12 11 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → 𝑁 ∈ ℕ )
13 12 0expd ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 0 ↑ 𝑁 ) = 0 )
14 10 13 neeqtrrd ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ≠ ( 0 ↑ 𝑁 ) )
15 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
16 15 necon3i ⊢ ( ( 𝐴 ↑ 𝑁 ) ≠ ( 0 ↑ 𝑁 ) → 𝐴 ≠ 0 )
17 14 16 syl ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → 𝐴 ≠ 0 )
18 pcqcl ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ∈ ℤ )
19 6 7 17 18 syl12anc ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ∈ ℤ )
20 dvdsmul1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ∈ ℤ ) → 𝑁 ∥ ( 𝑁 · ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ) )
21 5 19 20 syl2anc ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → 𝑁 ∥ ( 𝑁 · ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ) )
22 9 nncnd ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
23 22 exp1d ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) ↑ 1 ) = ( 𝐴 ↑ 𝑁 ) )
24 23 oveq2d ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) pCnt ( ( 𝐴 ↑ 𝑁 ) ↑ 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) pCnt ( 𝐴 ↑ 𝑁 ) ) )
25 1z ⊢ 1 ∈ ℤ
26 pcid ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℙ ∧ 1 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑁 ) pCnt ( ( 𝐴 ↑ 𝑁 ) ↑ 1 ) ) = 1 )
27 6 25 26 sylancl ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) pCnt ( ( 𝐴 ↑ 𝑁 ) ↑ 1 ) ) = 1 )
28 pcexp ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑁 ) pCnt ( 𝐴 ↑ 𝑁 ) ) = ( 𝑁 · ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ) )
29 6 7 17 5 28 syl121anc ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) pCnt ( 𝐴 ↑ 𝑁 ) ) = ( 𝑁 · ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ) )
30 24 27 29 3eqtr3rd ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → ( 𝑁 · ( ( 𝐴 ↑ 𝑁 ) pCnt 𝐴 ) ) = 1 )
31 21 30 breqtrd ⊢ ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) → 𝑁 ∥ 1 )
32 31 ex ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 ↑ 𝑁 ) ∈ ℙ → 𝑁 ∥ 1 ) )
33 11 adantl ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ∈ ℕ )
34 33 nnnn0d ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ∈ ℕ0 )
35 dvds1 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∥ 1 ↔ 𝑁 = 1 ) )
36 34 35 syl ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 ∥ 1 ↔ 𝑁 = 1 ) )
37 32 36 sylibd ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 ↑ 𝑁 ) ∈ ℙ → 𝑁 = 1 ) )
38 37 necon3ad ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 ≠ 1 → ¬ ( 𝐴 ↑ 𝑁 ) ∈ ℙ ) )
39 3 38 mpd ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝐴 ↑ 𝑁 ) ∈ ℙ )