Theorem 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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		2cnd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ∈ ℂ )
2		simprr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℕ )
3	2	nncnd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℂ )
4		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
5	4	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ )
6	5	nnnn0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ0 )
7	3 6	expcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℂ )
8	2	nnne0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ≠ 0 )
9	5	nnzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℤ )
10	3 8 9	expne0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ≠ 0 )
11	1 7 10	divcan4d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) = 2 )
12	7	2timesd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 · ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑞 ↑ 𝑁 ) + ( 𝑞 ↑ 𝑁 ) ) )
13		simpl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
14		simprl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ∈ ℕ )
15		ax-flt	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑞 ∈ ℕ ∧ 𝑞 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( ( 𝑞 ↑ 𝑁 ) + ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) )
16	13 2 2 14 15	syl13anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑞 ↑ 𝑁 ) + ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) )
17	12 16	eqnetrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 · ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) )
18	1 7	mulcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 · ( 𝑞 ↑ 𝑁 ) ) ∈ ℂ )
19	14	nncnd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ∈ ℂ )
20	19 6	expcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 ↑ 𝑁 ) ∈ ℂ )
21		div11	⊢ ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) ∈ ℂ ∧ ( 𝑝 ↑ 𝑁 ) ∈ ℂ ∧ ( ( 𝑞 ↑ 𝑁 ) ∈ ℂ ∧ ( 𝑞 ↑ 𝑁 ) ≠ 0 ) ) → ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) ↔ ( 2 · ( 𝑞 ↑ 𝑁 ) ) = ( 𝑝 ↑ 𝑁 ) ) )
22	18 20 7 10 21	syl112anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) ↔ ( 2 · ( 𝑞 ↑ 𝑁 ) ) = ( 𝑝 ↑ 𝑁 ) ) )
23	22	necon3bid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) ≠ ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) ↔ ( 2 · ( 𝑞 ↑ 𝑁 ) ) ≠ ( 𝑝 ↑ 𝑁 ) ) )
24	17 23	mpbird	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 2 · ( 𝑞 ↑ 𝑁 ) ) / ( 𝑞 ↑ 𝑁 ) ) ≠ ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) )
25	11 24	eqnetrrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ≠ ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) )
26	19 3 8 6	expdivd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑ 𝑁 ) = ( ( 𝑝 ↑ 𝑁 ) / ( 𝑞 ↑ 𝑁 ) ) )
27	25 26	neeqtrrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ≠ ( ( 𝑝 / 𝑞 ) ↑ 𝑁 ) )
28	19 3 8	divcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℂ )
29	14	nnne0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ≠ 0 )
30	19 3 29 8	divne0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ≠ 0 )
31	28 30 9	cxpexpzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) = ( ( 𝑝 / 𝑞 ) ↑ 𝑁 ) )
32	27 31	neeqtrrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ≠ ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) )
33		2re	⊢ 2 ∈ ℝ
34	33	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 2 ∈ ℝ )
35		0le2	⊢ 0 ≤ 2
36	35	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 0 ≤ 2 )
37	14	nnrpd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑝 ∈ ℝ+ )
38	2	nnrpd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℝ+ )
39	37 38	rpdivcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ+ )
40	39	rpred	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
41	39	rpge0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 0 ≤ ( 𝑝 / 𝑞 ) )
42	5	nnred	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
43	40 41 42	recxpcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ∈ ℝ )
44	40 41 42	cxpge0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 0 ≤ ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) )
45	5	nnrpd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℝ+ )
46	45	rpreccld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / 𝑁 ) ∈ ℝ+ )
47	34 36 43 44 46	recxpf1lem	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 = ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↔ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) ) )
48	47	necon3bid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 ≠ ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↔ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) ) )
49	32 48	mpbid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) )
50	5	nnrecred	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / 𝑁 ) ∈ ℝ )
51	50	recnd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / 𝑁 ) ∈ ℂ )
52	28 51	cxpcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℂ )
53	28 30 51	cxpne0d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ≠ 0 )
54	52 53 9	cxpexpzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑𝑐 𝑁 ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) )
55		cxpcom	⊢ ( ( ( 𝑝 / 𝑞 ) ∈ ℝ+ ∧ ( 1 / 𝑁 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑𝑐 𝑁 ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) )
56	39 50 42 55	syl3anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑𝑐 𝑁 ) = ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) )
57		cxproot	⊢ ( ( ( 𝑝 / 𝑞 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = ( 𝑝 / 𝑞 ) )
58	28 5 57	syl2anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = ( 𝑝 / 𝑞 ) )
59	54 56 58	3eqtr3d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝑝 / 𝑞 ) ↑𝑐 𝑁 ) ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
60	49 59	neeqtrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ≠ ( 𝑝 / 𝑞 ) )
61	60	neneqd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑝 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
62	61	ralrimivva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ℕ ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
63		ralnex2	⊢ ( ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ℕ ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) ↔ ¬ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
64	62 63	sylib	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
65		2rp	⊢ 2 ∈ ℝ+
66	65	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℝ+ )
67	4	nnrecred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 / 𝑁 ) ∈ ℝ )
68	66 67	cxpgt0d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 0 < ( 2 ↑𝑐 ( 1 / 𝑁 ) ) )
69	68	biantrud	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ↔ ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ∧ 0 < ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ) ) )
70		elpqb	⊢ ( ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ∧ 0 < ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ) ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) )
71	69 70	bitrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) = ( 𝑝 / 𝑞 ) ) )
72	64 71	mtbird	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ¬ ( 2 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ℚ )