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 ( 𝐴 ↑ 𝑁 ) ) ∈ ℕ₀ )
14	5 6 12 13	syl12anc	⊢ ( ( ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) ∧ 𝐴 ≠ 0 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝐴 ↑ 𝑁 ) ) ∈ ℕ₀ )
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	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → 𝐴 ∈ ℤ )

Metamath Proof Explorer

Theorem qexpz

Proof