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	3	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P \in ℝ$
14	6	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 0 \leq P$
15	11	adantr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \frac{1}{N} \in ℝ$
16	13 14 15	recxpcld	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} \in ℝ$
17	7	ad2antlr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to N \in ℝ$
18		eluz2gt1	$⊢ N \in ℤ_{\geq 2} \to 1 < N$
19	18	ad2antlr	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 1 < N$
20		recgt1i	$⊢ (N \in ℝ \land 1 < N) \to (0 < \frac{1}{N} \land \frac{1}{N} < 1)$
21	20	simprd	$⊢ (N \in ℝ \land 1 < N) \to \frac{1}{N} < 1$
22	17 19 21	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \frac{1}{N} < 1$
23		simpll	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P \in ℙ$
24		prmgt1	$⊢ P \in ℙ \to 1 < P$
25	23 24	syl	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 1 < P$
26		1red	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 1 \in ℝ$
27	13 25 15 26	cxpltd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to (\frac{1}{N} < 1 \leftrightarrow P^{\frac{1}{N}} < P^{1})$
28	22 27	mpbid	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} < P^{1}$
29	13	recnd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P \in ℂ$
30	29	cxp1d	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{1} = P$
31	28 30	breqtrd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} < P$
32	16 31	ltned	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} \neq P$
33	32	neneqd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} = P$
34	29	cxp0d	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{0} = 1$
35	20	simpld	$⊢ (N \in ℝ \land 1 < N) \to 0 < \frac{1}{N}$
36	17 19 35	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 0 < \frac{1}{N}$
37		0red	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 0 \in ℝ$
38	13 25 37 15	cxpltd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to (0 < \frac{1}{N} \leftrightarrow P^{0} < P^{\frac{1}{N}})$
39	36 38	mpbid	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{0} < P^{\frac{1}{N}}$
40	34 39	eqbrtrrd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to 1 < P^{\frac{1}{N}}$
41	26 40	gtned	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} \neq 1$
42	41	neneqd	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} = 1$
43		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))$
44	43	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))$
45	44	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))$
46	33 42 45	mtord	$⊢ ((P \in ℙ \land N \in ℤ_{\geq 2}) \land P^{\frac{1}{N}} \in ℕ) \to \neg P^{\frac{1}{N}} ∥ P$
47		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)$
48	46 47	mpbir	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg (P^{\frac{1}{N}} \in ℕ \land P^{\frac{1}{N}} ∥ P)$
49		prmz	$⊢ P \in ℙ \to P \in ℤ$
50	49	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P \in ℤ$
51		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
52	51	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to N \in ℕ$
53		simp3	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} \in ℕ$
54		zrtdvds	$⊢ (P \in ℤ \land N \in ℕ \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} ∥ P$
55	50 52 53 54	syl3anc	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℕ) \to P^{\frac{1}{N}} ∥ P$
56	55	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℕ \to P^{\frac{1}{N}} ∥ P)$
57	56	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))$
58	48 57	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℕ$
59	1	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
60	59	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to P \in ℝ^{+}$
61	7	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to N \in ℝ$
62	9	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to N \neq 0$
63	61 62	rereccld	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to \frac{1}{N} \in ℝ$
64	60 63	cxpgt0d	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℤ) \to 0 < P^{\frac{1}{N}}$
65	64	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to 0 < P^{\frac{1}{N}})$
66	65	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}}))$
67		elnnz	$⊢ P^{\frac{1}{N}} \in ℕ \leftrightarrow (P^{\frac{1}{N}} \in ℤ \land 0 < P^{\frac{1}{N}})$
68	66 67	syl6ibr	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℤ \to P^{\frac{1}{N}} \in ℕ)$
69	58 68	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℤ$
70	49	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P \in ℤ$
71	51	3ad2ant2	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to N \in ℕ$
72		simp3	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℚ$
73		zrtelqelz	$⊢ (P \in ℤ \land N \in ℕ \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℤ$
74	70 71 72 73	syl3anc	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2} \land P^{\frac{1}{N}} \in ℚ) \to P^{\frac{1}{N}} \in ℤ$
75	74	3expia	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to (P^{\frac{1}{N}} \in ℚ \to P^{\frac{1}{N}} \in ℤ)$
76	69 75	mtod	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to \neg P^{\frac{1}{N}} \in ℚ$
77	12 76	eldifd	$⊢ (P \in ℙ \land N \in ℤ_{\geq 2}) \to P^{\frac{1}{N}} \in (ℝ ∖ ℚ)$

Metamath Proof Explorer

Theorem rtprmirr

Proof