nrt2irr

Description: The N -th root of 2 is irrational for N greater than 2 . For N = 2 , see sqrt2irr . This short and rather elegant proof has the minor disadvantage that it refers to ax-flt , which is still to be formalized. For a proof not requiring ax-flt , see rtprmirr . (Contributed by Prof. Loof Lirpa, 1-Apr-2025) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	nrt2irr	$⊢ N \in ℤ_{\geq 3} \to \neg 2^{\frac{1}{N}} \in ℚ$

Proof

Step	Hyp	Ref	Expression
1		2cnd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 \in ℂ$
2		simprr	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q \in ℕ$
3	2	nncnd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q \in ℂ$
4		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
5	4	adantr	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to N \in ℕ$
6	5	nnnn0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to N \in ℕ_{0}$
7	3 6	expcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q^{N} \in ℂ$
8	2	nnne0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q \neq 0$
9	5	nnzd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to N \in ℤ$
10	3 8 9	expne0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q^{N} \neq 0$
11	1 7 10	divcan4d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{2 q^{N}}{q^{N}} = 2$
12	7	2timesd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 q^{N} = q^{N} + q^{N}$
13		simpl	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to N \in ℤ_{\geq 3}$
14		simprl	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to p \in ℕ$
15		ax-flt	$⊢ (N \in ℤ_{\geq 3} \land (q \in ℕ \land q \in ℕ \land p \in ℕ)) \to q^{N} + q^{N} \neq p^{N}$
16	13 2 2 14 15	syl13anc	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q^{N} + q^{N} \neq p^{N}$
17	12 16	eqnetrd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 q^{N} \neq p^{N}$
18	1 7	mulcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 q^{N} \in ℂ$
19	14	nncnd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to p \in ℂ$
20	19 6	expcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to p^{N} \in ℂ$
21		div11	$⊢ (2 q^{N} \in ℂ \land p^{N} \in ℂ \land (q^{N} \in ℂ \land q^{N} \neq 0)) \to (\frac{2 q^{N}}{q^{N}} = \frac{p^{N}}{q^{N}} \leftrightarrow 2 q^{N} = p^{N})$
22	18 20 7 10 21	syl112anc	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to (\frac{2 q^{N}}{q^{N}} = \frac{p^{N}}{q^{N}} \leftrightarrow 2 q^{N} = p^{N})$
23	22	necon3bid	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to (\frac{2 q^{N}}{q^{N}} \neq \frac{p^{N}}{q^{N}} \leftrightarrow 2 q^{N} \neq p^{N})$
24	17 23	mpbird	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{2 q^{N}}{q^{N}} \neq \frac{p^{N}}{q^{N}}$
25	11 24	eqnetrrd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 \neq \frac{p^{N}}{q^{N}}$
26	19 3 8 6	expdivd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {(\frac{p}{q})}^{N} = \frac{p^{N}}{q^{N}}$
27	25 26	neeqtrrd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 \neq {(\frac{p}{q})}^{N}$
28	19 3 8	divcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{p}{q} \in ℂ$
29	14	nnne0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to p \neq 0$
30	19 3 29 8	divne0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{p}{q} \neq 0$
31	28 30 9	cxpexpzd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {(\frac{p}{q})}^{N} = {(\frac{p}{q})}^{N}$
32	27 31	neeqtrrd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 \neq {(\frac{p}{q})}^{N}$
33		2re	$⊢ 2 \in ℝ$
34	33	a1i	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2 \in ℝ$
35		0le2	$⊢ 0 \leq 2$
36	35	a1i	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 0 \leq 2$
37	14	nnrpd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to p \in ℝ^{+}$
38	2	nnrpd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to q \in ℝ^{+}$
39	37 38	rpdivcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{p}{q} \in ℝ^{+}$
40	39	rpred	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{p}{q} \in ℝ$
41	39	rpge0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 0 \leq \frac{p}{q}$
42	5	nnred	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to N \in ℝ$
43	40 41 42	recxpcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {(\frac{p}{q})}^{N} \in ℝ$
44	40 41 42	cxpge0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 0 \leq {(\frac{p}{q})}^{N}$
45	5	nnrpd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to N \in ℝ^{+}$
46	45	rpreccld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{1}{N} \in ℝ^{+}$
47	34 36 43 44 46	recxpf1lem	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to (2 = {(\frac{p}{q})}^{N} \leftrightarrow 2^{\frac{1}{N}} = {({(\frac{p}{q})}^{N})}^{\frac{1}{N}})$
48	47	necon3bid	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to (2 \neq {(\frac{p}{q})}^{N} \leftrightarrow 2^{\frac{1}{N}} \neq {({(\frac{p}{q})}^{N})}^{\frac{1}{N}})$
49	32 48	mpbid	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2^{\frac{1}{N}} \neq {({(\frac{p}{q})}^{N})}^{\frac{1}{N}}$
50	5	nnrecred	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{1}{N} \in ℝ$
51	50	recnd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \frac{1}{N} \in ℂ$
52	28 51	cxpcld	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {(\frac{p}{q})}^{\frac{1}{N}} \in ℂ$
53	28 30 51	cxpne0d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {(\frac{p}{q})}^{\frac{1}{N}} \neq 0$
54	52 53 9	cxpexpzd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {({(\frac{p}{q})}^{\frac{1}{N}})}^{N} = {({(\frac{p}{q})}^{\frac{1}{N}})}^{N}$
55		cxpcom	$⊢ (\frac{p}{q} \in ℝ^{+} \land \frac{1}{N} \in ℝ \land N \in ℝ) \to {({(\frac{p}{q})}^{\frac{1}{N}})}^{N} = {({(\frac{p}{q})}^{N})}^{\frac{1}{N}}$
56	39 50 42 55	syl3anc	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {({(\frac{p}{q})}^{\frac{1}{N}})}^{N} = {({(\frac{p}{q})}^{N})}^{\frac{1}{N}}$
57		cxproot	$⊢ (\frac{p}{q} \in ℂ \land N \in ℕ) \to {({(\frac{p}{q})}^{\frac{1}{N}})}^{N} = \frac{p}{q}$
58	28 5 57	syl2anc	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {({(\frac{p}{q})}^{\frac{1}{N}})}^{N} = \frac{p}{q}$
59	54 56 58	3eqtr3d	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to {({(\frac{p}{q})}^{N})}^{\frac{1}{N}} = \frac{p}{q}$
60	49 59	neeqtrd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to 2^{\frac{1}{N}} \neq \frac{p}{q}$
61	60	neneqd	$⊢ (N \in ℤ_{\geq 3} \land (p \in ℕ \land q \in ℕ)) \to \neg 2^{\frac{1}{N}} = \frac{p}{q}$
62	61	ralrimivva	$⊢ N \in ℤ_{\geq 3} \to \forall p \in ℕ \forall q \in ℕ \neg 2^{\frac{1}{N}} = \frac{p}{q}$
63		ralnex2	$⊢ \forall p \in ℕ \forall q \in ℕ \neg 2^{\frac{1}{N}} = \frac{p}{q} \leftrightarrow \neg \exists p \in ℕ \exists q \in ℕ 2^{\frac{1}{N}} = \frac{p}{q}$
64	62 63	sylib	$⊢ N \in ℤ_{\geq 3} \to \neg \exists p \in ℕ \exists q \in ℕ 2^{\frac{1}{N}} = \frac{p}{q}$
65		2rp	$⊢ 2 \in ℝ^{+}$
66	65	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℝ^{+}$
67	4	nnrecred	$⊢ N \in ℤ_{\geq 3} \to \frac{1}{N} \in ℝ$
68	66 67	cxpgt0d	$⊢ N \in ℤ_{\geq 3} \to 0 < 2^{\frac{1}{N}}$
69	68	biantrud	$⊢ N \in ℤ_{\geq 3} \to (2^{\frac{1}{N}} \in ℚ \leftrightarrow (2^{\frac{1}{N}} \in ℚ \land 0 < 2^{\frac{1}{N}}))$
70		elpqb	$⊢ (2^{\frac{1}{N}} \in ℚ \land 0 < 2^{\frac{1}{N}}) \leftrightarrow \exists p \in ℕ \exists q \in ℕ 2^{\frac{1}{N}} = \frac{p}{q}$
71	69 70	bitrdi	$⊢ N \in ℤ_{\geq 3} \to (2^{\frac{1}{N}} \in ℚ \leftrightarrow \exists p \in ℕ \exists q \in ℕ 2^{\frac{1}{N}} = \frac{p}{q})$
72	64 71	mtbird	$⊢ N \in ℤ_{\geq 3} \to \neg 2^{\frac{1}{N}} \in ℚ$

Metamath Proof Explorer

Theorem nrt2irr

Proof