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 ) ) → ¬ ( 𝐴 ↑ 𝑁 ) ∈ ℙ )