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	$⊢ (A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \to A \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ A = 0 \to (A \in ℤ \leftrightarrow 0 \in ℤ)$
2		simpll2	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to N \in ℕ$
3	2	nncnd	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to N \in ℂ$
4	3	mul01d	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to N \cdot 0 = 0$
5		simpr	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to p \in ℙ$
6		simpll3	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to A^{N} \in ℤ$
7		simpll1	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to A \in ℚ$
8		qcn	$⊢ A \in ℚ \to A \in ℂ$
9	7 8	syl	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to A \in ℂ$
10		simplr	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to A \neq 0$
11	2	nnzd	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to N \in ℤ$
12	9 10 11	expne0d	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to A^{N} \neq 0$
13		pczcl	$⊢ (p \in ℙ \land (A^{N} \in ℤ \land A^{N} \neq 0)) \to p pCnt A^{N} \in ℕ_{0}$
14	5 6 12 13	syl12anc	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to p pCnt A^{N} \in ℕ_{0}$
15	14	nn0ge0d	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to 0 \leq p pCnt A^{N}$
16		pcexp	$⊢ (p \in ℙ \land (A \in ℚ \land A \neq 0) \land N \in ℤ) \to p pCnt A^{N} = N (p pCnt A)$
17	5 7 10 11 16	syl121anc	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to p pCnt A^{N} = N (p pCnt A)$
18	15 17	breqtrd	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to 0 \leq N (p pCnt A)$
19	4 18	eqbrtrd	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to N \cdot 0 \leq N (p pCnt A)$
20		0red	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to 0 \in ℝ$
21		pcqcl	$⊢ (p \in ℙ \land (A \in ℚ \land A \neq 0)) \to p pCnt A \in ℤ$
22	5 7 10 21	syl12anc	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to p pCnt A \in ℤ$
23	22	zred	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to p pCnt A \in ℝ$
24	2	nnred	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to N \in ℝ$
25	2	nngt0d	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to 0 < N$
26		lemul2	$⊢ (0 \in ℝ \land p pCnt A \in ℝ \land (N \in ℝ \land 0 < N)) \to (0 \leq p pCnt A \leftrightarrow N \cdot 0 \leq N (p pCnt A))$
27	20 23 24 25 26	syl112anc	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to (0 \leq p pCnt A \leftrightarrow N \cdot 0 \leq N (p pCnt A))$
28	19 27	mpbird	$⊢ (((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \land p \in ℙ) \to 0 \leq p pCnt A$
29	28	ralrimiva	$⊢ ((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \to \forall p \in ℙ 0 \leq p pCnt A$
30		simpl1	$⊢ ((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \to A \in ℚ$
31		pcz	$⊢ A \in ℚ \to (A \in ℤ \leftrightarrow \forall p \in ℙ 0 \leq p pCnt A)$
32	30 31	syl	$⊢ ((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \to (A \in ℤ \leftrightarrow \forall p \in ℙ 0 \leq p pCnt A)$
33	29 32	mpbird	$⊢ ((A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \land A \neq 0) \to A \in ℤ$
34		0zd	$⊢ (A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \to 0 \in ℤ$
35	1 33 34	pm2.61ne	$⊢ (A \in ℚ \land N \in ℕ \land A^{N} \in ℤ) \to A \in ℤ$

Metamath Proof Explorer

Theorem qexpz

Proof