rtprmirr

Description: The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023)

		Ref	Expression
	Assertion	rtprmirr	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \in (ℝ ∖ ℚ)$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2	1	adantr	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P \in ℕ$
3	2	nnred	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P \in ℝ$
4		0red	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 0 \in ℝ$
5	2	nngt0d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 0 < P$
6	4 3 5	ltled	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 0 \leq P$
7		eluzelre	$⊢ N \in ℤ_{\geq 2} \to N \in ℝ$
8	7	adantl	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to N \in ℝ$
9		eluz2n0	$⊢ N \in ℤ_{\geq 2} \to N \neq 0$
10	9	adantl	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to N \neq 0$
11	8 10	rereccld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \frac{1}{N} \in ℝ$
12	3 6 11	recxpcld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \in ℝ$
13		eluz2gt1	$⊢ N \in ℤ_{\geq 2} \to 1 < N$
14		recgt1i	$⊢ (N \in ℝ \land 1 < N) \to (0 < \frac{1}{N} \land \frac{1}{N} < 1)$
15	7 13 14	syl2anc	$⊢ N \in ℤ_{\geq 2} \to (0 < \frac{1}{N} \land \frac{1}{N} < 1)$
16	15	simprd	$⊢ N \in ℤ_{\geq 2} \to \frac{1}{N} < 1$
17	16	adantl	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \frac{1}{N} < 1$
18		prmgt1	$⊢ P \in ℙ \to 1 < P$
19	18	adantr	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 1 < P$
20		1red	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 1 \in ℝ$
21	3 19 11 20	cxpltd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (\frac{1}{N} < 1 \leftrightarrow P^{\frac{1}{N}} < P^{1})$
22	17 21	mpbid	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} < P^{1}$
23	2	nncnd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P \in ℂ$
24	23	cxp1d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{1} = P$
25	22 24	breqtrd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} < P$
26	12 25	ltned	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \neq P$
27	26	neneqd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} = P$
28	27	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} = P$
29	23	cxp0d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{0} = 1$
30	15	simpld	$⊢ N \in ℤ_{\geq 2} \to 0 < \frac{1}{N}$
31	30	adantl	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 0 < \frac{1}{N}$
32	3 19 4 11	cxpltd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (0 < \frac{1}{N} \leftrightarrow P^{0} < P^{\frac{1}{N}})$
33	31 32	mpbid	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{0} < P^{\frac{1}{N}}$
34	29 33	eqbrtrrd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 1 < P^{\frac{1}{N}}$
35	20 34	gtned	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \neq 1$
36	35	neneqd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} = 1$
37	36	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} = 1$
38		dvdsprime	$⊢ (P \in ℙ \land P^{\frac{1}{N}} \in ℕ) \to (P^{\frac{1}{N}} ∥ P \leftrightarrow (P^{\frac{1}{N}} = P \lor P^{\frac{1}{N}} = 1))$
39	38	adantlr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to (P^{\frac{1}{N}} ∥ P \leftrightarrow (P^{\frac{1}{N}} = P \lor P^{\frac{1}{N}} = 1))$
40	39	biimpd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to (P^{\frac{1}{N}} ∥ P \to (P^{\frac{1}{N}} = P \lor P^{\frac{1}{N}} = 1))$
41	28 37 40	mtord	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} ∥ P$
42		nan	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg (P^{\frac{1}{N}} \in ℕ \land P^{\frac{1}{N}} ∥ P)) \leftrightarrow (((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} ∥ P)$
43	41 42	mpbir	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg (P^{\frac{1}{N}} \in ℕ \land P^{\frac{1}{N}} ∥ P)$
44		prmz	$⊢ P \in ℙ \to P \in ℤ$
45	44	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P \in ℤ$
46		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
47	46	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to N \in ℕ$
48		simp3	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} \in ℕ$
49		zrtdvds	$⊢ (P \in ℤ \land N \in ℕ \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} ∥ P$
50	45 47 48 49	syl3anc	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} ∥ P$
51	50	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℕ \to P^{\frac{1}{N}} ∥ P)$
52	51	ancld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℕ \to (P^{\frac{1}{N}} \in ℕ \land P^{\frac{1}{N}} ∥ P))$
53	43 52	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℕ$
54	1	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
55	54	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to P \in ℝ^{+}$
56	7	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to N \in ℝ$
57	9	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to N \neq 0$
58	56 57	rereccld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to \frac{1}{N} \in ℝ$
59	55 58	cxpgt0d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to 0 < P^{\frac{1}{N}}$
60	59	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to 0 < P^{\frac{1}{N}})$
61	60	ancld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to (P^{\frac{1}{N}} \in ℤ \land 0 < P^{\frac{1}{N}}))$
62		elnnz	$⊢ P^{\frac{1}{N}} \in ℕ \leftrightarrow (P^{\frac{1}{N}} \in ℤ \land 0 < P^{\frac{1}{N}})$
63	61 62	imbitrrdi	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to P^{\frac{1}{N}} \in ℕ)$
64	53 63	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℤ$
65	44	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P \in ℤ$
66	46	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to N \in ℕ$
67		simp3	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℚ$
68		zrtelqelz	$⊢ (P \in ℤ \land N \in ℕ \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℤ$
69	65 66 67 68	syl3anc	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℤ$
70	69	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℚ \to P^{\frac{1}{N}} \in ℤ)$
71	64 70	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℚ$
72	12 71	eldifd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \in (ℝ ∖ ℚ)$

Metamath Proof Explorer

Theorem rtprmirr

Proof