Metamath Proof Explorer

Theorem rtprmirr

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

Ref Expression
Assertion rtprmirr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑃 ↑𝑐 ( 1 / 𝑁 ) ) ∈ ( ℝ ∖ ℚ ) )

Proof

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