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