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	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to \neg A^{N} \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
2	1	simprbi	$⊢ N \in ℤ_{\geq 2} \to N \neq 1$
3	2	adantl	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to N \neq 1$
4		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
5	4	ad2antlr	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to N \in ℤ$
6		simpr	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} \in ℙ$
7		simpll	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A \in ℚ$
8		prmnn	$⊢ A^{N} \in ℙ \to A^{N} \in ℕ$
9	8	adantl	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} \in ℕ$
10	9	nnne0d	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} \neq 0$
11		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
12	11	ad2antlr	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to N \in ℕ$
13	12	0expd	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to 0^{N} = 0$
14	10 13	neeqtrrd	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} \neq 0^{N}$
15		oveq1	$⊢ A = 0 \to A^{N} = 0^{N}$
16	15	necon3i	$⊢ A^{N} \neq 0^{N} \to A \neq 0$
17	14 16	syl	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A \neq 0$
18		pcqcl	$⊢ (A^{N} \in ℙ \land (A \in ℚ \land A \neq 0)) \to A^{N} pCnt A \in ℤ$
19	6 7 17 18	syl12anc	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} pCnt A \in ℤ$
20		dvdsmul1	$⊢ (N \in ℤ \land A^{N} pCnt A \in ℤ) \to N ∥ N (A^{N} pCnt A)$
21	5 19 20	syl2anc	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to N ∥ N (A^{N} pCnt A)$
22	9	nncnd	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} \in ℂ$
23	22	exp1d	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to {(A^{N})}^{1} = A^{N}$
24	23	oveq2d	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} pCnt {(A^{N})}^{1} = A^{N} pCnt A^{N}$
25		1z	$⊢ 1 \in ℤ$
26		pcid	$⊢ (A^{N} \in ℙ \land 1 \in ℤ) \to A^{N} pCnt {(A^{N})}^{1} = 1$
27	6 25 26	sylancl	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} pCnt {(A^{N})}^{1} = 1$
28		pcexp	$⊢ (A^{N} \in ℙ \land (A \in ℚ \land A \neq 0) \land N \in ℤ) \to A^{N} pCnt A^{N} = N (A^{N} pCnt A)$
29	6 7 17 5 28	syl121anc	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to A^{N} pCnt A^{N} = N (A^{N} pCnt A)$
30	24 27 29	3eqtr3rd	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to N (A^{N} pCnt A) = 1$
31	21 30	breqtrd	$⊢ ((A \in ℚ \land N \in ℤ_{\geq 2}) \land A^{N} \in ℙ) \to N ∥ 1$
32	31	ex	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to (A^{N} \in ℙ \to N ∥ 1)$
33	11	adantl	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to N \in ℕ$
34	33	nnnn0d	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to N \in ℕ_{0}$
35		dvds1	$⊢ N \in ℕ_{0} \to (N ∥ 1 \leftrightarrow N = 1)$
36	34 35	syl	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to (N ∥ 1 \leftrightarrow N = 1)$
37	32 36	sylibd	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to (A^{N} \in ℙ \to N = 1)$
38	37	necon3ad	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to (N \neq 1 \to \neg A^{N} \in ℙ)$
39	3 38	mpd	$⊢ (A \in ℚ \land N \in ℤ_{\geq 2}) \to \neg A^{N} \in ℙ$

Metamath Proof Explorer

Theorem expnprm

Proof