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	1	nnred	$⊢ P \in ℙ \to P \in ℝ$
19	18	adantr	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P \in ℝ$
20		prmgt1	$⊢ P \in ℙ \to 1 < P$
21	20	adantr	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 1 < P$
22		1red	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 1 \in ℝ$
23	19 21 11 22	cxpltd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (\frac{1}{N} < 1 \leftrightarrow P^{\frac{1}{N}} < P^{1})$
24	17 23	mpbid	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} < P^{1}$
25	2	nncnd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P \in ℂ$
26	25	cxp1d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{1} = P$
27	24 26	breqtrd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} < P$
28	12 27	ltned	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \neq P$
29	28	neneqd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} = P$
30	29	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} = P$
31	25	cxp0d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{0} = 1$
32	15	simpld	$⊢ N \in ℤ_{\geq 2} \to 0 < \frac{1}{N}$
33	32	adantl	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 0 < \frac{1}{N}$
34	19 21 4 11	cxpltd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (0 < \frac{1}{N} \leftrightarrow P^{0} < P^{\frac{1}{N}})$
35	33 34	mpbid	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{0} < P^{\frac{1}{N}}$
36	31 35	eqbrtrrd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to 1 < P^{\frac{1}{N}}$
37	22 36	gtned	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \neq 1$
38	37	neneqd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} = 1$
39	38	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} = 1$
40		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))$
41	40	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))$
42	41	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))$
43	30 39 42	mtord	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} ∥ P$
44		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)$
45	43 44	mpbir	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg (P^{\frac{1}{N}} \in ℕ \land P^{\frac{1}{N}} ∥ P)$
46		prmz	$⊢ P \in ℙ \to P \in ℤ$
47		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
48		zrtdvds	$⊢ (P \in ℤ \land N \in ℕ \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} ∥ P$
49	46 47 48	syl3an12	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} ∥ P$
50	49	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℕ \to P^{\frac{1}{N}} ∥ P)$
51	50	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))$
52	45 51	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℕ$
53	1	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
54	53	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to P \in ℝ^{+}$
55	7	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to N \in ℝ$
56	9	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to N \neq 0$
57	55 56	rereccld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to \frac{1}{N} \in ℝ$
58	54 57	cxpgt0d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to 0 < P^{\frac{1}{N}}$
59	58	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to 0 < P^{\frac{1}{N}})$
60	59	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}}))$
61		elnnz	$⊢ P^{\frac{1}{N}} \in ℕ \leftrightarrow (P^{\frac{1}{N}} \in ℤ \land 0 < P^{\frac{1}{N}})$
62	60 61	imbitrrdi	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to P^{\frac{1}{N}} \in ℕ)$
63	52 62	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℤ$
64		zrtelqelz	$⊢ (P \in ℤ \land N \in ℕ \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℤ$
65	46 47 64	syl3an12	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℤ$
66	65	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℚ \to P^{\frac{1}{N}} \in ℤ)$
67	63 66	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℚ$
68	12 67	eldifd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \in (ℝ ∖ ℚ)$

Metamath Proof Explorer

Theorem rtprmirr

Proof