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