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 
|- ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) e. ( RR \ QQ ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 1 adantr 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> P e. NN )
3 2 nnred 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> P e. RR )
4 0red 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 0 e. RR )
5 2 nngt0d 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 0 < P )
6 4 3 5 ltled 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 0 <_ P )
7 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
8 7 adantl 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> N e. RR )
9 eluz2n0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N =/= 0 )
10 9 adantl 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> N =/= 0 )
11 8 10 rereccld 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( 1 / N ) e. RR )
12 3 6 11 recxpcld 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) e. RR )
13 3 adantr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> P e. RR )
14 6 adantr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 0 <_ P )
15 11 adantr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( 1 / N ) e. RR )
16 13 14 15 recxpcld 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) e. RR )
17 7 ad2antlr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> N e. RR )
18 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
19 18 ad2antlr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 1 < N )
20 recgt1i 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 0 < ( 1 / N ) /\ ( 1 / N ) < 1 ) )
21 20 simprd 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 / N ) < 1 )
22 17 19 21 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( 1 / N ) < 1 )
23 simpll 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> P e. Prime )
24 prmgt1 
 |-  ( P e. Prime -> 1 < P )
25 23 24 syl 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 1 < P )
26 1red 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 1 e. RR )
27 13 25 15 26 cxpltd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( ( 1 / N ) < 1 <-> ( P ^c ( 1 / N ) ) < ( P ^c 1 ) ) )
28 22 27 mpbid 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) < ( P ^c 1 ) )
29 13 recnd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> P e. CC )
30 29 cxp1d 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c 1 ) = P )
31 28 30 breqtrd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) < P )
32 16 31 ltned 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) =/= P )
33 32 neneqd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) = P )
34 29 cxp0d 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c 0 ) = 1 )
35 20 simpld 
 |-  ( ( N e. RR /\ 1 < N ) -> 0 < ( 1 / N ) )
36 17 19 35 syl2anc 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 0 < ( 1 / N ) )
37 0red 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 0 e. RR )
38 13 25 37 15 cxpltd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( 0 < ( 1 / N ) <-> ( P ^c 0 ) < ( P ^c ( 1 / N ) ) ) )
39 36 38 mpbid 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c 0 ) < ( P ^c ( 1 / N ) ) )
40 34 39 eqbrtrrd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> 1 < ( P ^c ( 1 / N ) ) )
41 26 40 gtned 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) =/= 1 )
42 41 neneqd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) = 1 )
43 dvdsprime 
 |-  ( ( P e. Prime /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( ( P ^c ( 1 / N ) ) || P <-> ( ( P ^c ( 1 / N ) ) = P \/ ( P ^c ( 1 / N ) ) = 1 ) ) )
44 43 adantlr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( ( P ^c ( 1 / N ) ) || P <-> ( ( P ^c ( 1 / N ) ) = P \/ ( P ^c ( 1 / N ) ) = 1 ) ) )
45 44 biimpd 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( ( P ^c ( 1 / N ) ) || P -> ( ( P ^c ( 1 / N ) ) = P \/ ( P ^c ( 1 / N ) ) = 1 ) ) )
46 33 42 45 mtord 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) || P )
47 nan 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( ( P ^c ( 1 / N ) ) e. NN /\ ( P ^c ( 1 / N ) ) || P ) ) <-> ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) || P ) )
48 46 47 mpbir 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( ( P ^c ( 1 / N ) ) e. NN /\ ( P ^c ( 1 / N ) ) || P ) )
49 prmz 
 |-  ( P e. Prime -> P e. ZZ )
50 49 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> P e. ZZ )
51 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
52 51 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> N e. NN )
53 simp3 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) e. NN )
54 zrtdvds 
 |-  ( ( P e. ZZ /\ N e. NN /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) || P )
55 50 52 53 54 syl3anc 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) || P )
56 55 3expia 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. NN -> ( P ^c ( 1 / N ) ) || P ) )
57 56 ancld 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. NN -> ( ( P ^c ( 1 / N ) ) e. NN /\ ( P ^c ( 1 / N ) ) || P ) ) )
58 48 57 mtod 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) e. NN )
59 1 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
60 59 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> P e. RR+ )
61 7 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> N e. RR )
62 9 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> N =/= 0 )
63 61 62 rereccld 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> ( 1 / N ) e. RR )
64 60 63 cxpgt0d 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> 0 < ( P ^c ( 1 / N ) ) )
65 64 3expia 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. ZZ -> 0 < ( P ^c ( 1 / N ) ) ) )
66 65 ancld 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. ZZ -> ( ( P ^c ( 1 / N ) ) e. ZZ /\ 0 < ( P ^c ( 1 / N ) ) ) ) )
67 elnnz 
 |-  ( ( P ^c ( 1 / N ) ) e. NN <-> ( ( P ^c ( 1 / N ) ) e. ZZ /\ 0 < ( P ^c ( 1 / N ) ) ) )
68 66 67 syl6ibr 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. ZZ -> ( P ^c ( 1 / N ) ) e. NN ) )
69 58 68 mtod 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) e. ZZ )
70 49 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. QQ ) -> P e. ZZ )
71 51 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. QQ ) -> N e. NN )
72 simp3 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. QQ ) -> ( P ^c ( 1 / N ) ) e. QQ )
73 zrtelqelz 
 |-  ( ( P e. ZZ /\ N e. NN /\ ( P ^c ( 1 / N ) ) e. QQ ) -> ( P ^c ( 1 / N ) ) e. ZZ )
74 70 71 72 73 syl3anc 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. QQ ) -> ( P ^c ( 1 / N ) ) e. ZZ )
75 74 3expia 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. QQ -> ( P ^c ( 1 / N ) ) e. ZZ ) )
76 69 75 mtod 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) e. QQ )
77 12 76 eldifd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) e. ( RR \ QQ ) )