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 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
14 recgt1i 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 0 < ( 1 / N ) /\ ( 1 / N ) < 1 ) )
15 7 13 14 syl2anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 0 < ( 1 / N ) /\ ( 1 / N ) < 1 ) )
16 15 simprd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) < 1 )
17 16 adantl 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( 1 / N ) < 1 )
18 1 nnred 
 |-  ( P e. Prime -> P e. RR )
19 18 adantr 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> P e. RR )
20 prmgt1 
 |-  ( P e. Prime -> 1 < P )
21 20 adantr 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 1 < P )
22 1red 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
23 19 21 11 22 cxpltd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( 1 / N ) < 1 <-> ( P ^c ( 1 / N ) ) < ( P ^c 1 ) ) )
24 17 23 mpbid 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) < ( P ^c 1 ) )
25 2 nncnd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> P e. CC )
26 25 cxp1d 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c 1 ) = P )
27 24 26 breqtrd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) < P )
28 12 27 ltned 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) =/= P )
29 28 neneqd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) = P )
30 29 adantr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) = P )
31 25 cxp0d 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c 0 ) = 1 )
32 15 simpld 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 < ( 1 / N ) )
33 32 adantl 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 0 < ( 1 / N ) )
34 19 21 4 11 cxpltd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( 0 < ( 1 / N ) <-> ( P ^c 0 ) < ( P ^c ( 1 / N ) ) ) )
35 33 34 mpbid 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c 0 ) < ( P ^c ( 1 / N ) ) )
36 31 35 eqbrtrrd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> 1 < ( P ^c ( 1 / N ) ) )
37 22 36 gtned 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) =/= 1 )
38 37 neneqd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) = 1 )
39 38 adantr 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) = 1 )
40 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 ) ) )
41 40 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 ) ) )
42 41 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 ) ) )
43 30 39 42 mtord 
 |-  ( ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> -. ( P ^c ( 1 / N ) ) || P )
44 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 ) )
45 43 44 mpbir 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( ( P ^c ( 1 / N ) ) e. NN /\ ( P ^c ( 1 / N ) ) || P ) )
46 prmz 
 |-  ( P e. Prime -> P e. ZZ )
47 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
48 zrtdvds 
 |-  ( ( P e. ZZ /\ N e. NN /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) || P )
49 46 47 48 syl3an12 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. NN ) -> ( P ^c ( 1 / N ) ) || P )
50 49 3expia 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. NN -> ( P ^c ( 1 / N ) ) || P ) )
51 50 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 ) ) )
52 45 51 mtod 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) e. NN )
53 1 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
54 53 3ad2ant1 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> P e. RR+ )
55 7 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> N e. RR )
56 9 3ad2ant2 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> N =/= 0 )
57 55 56 rereccld 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> ( 1 / N ) e. RR )
58 54 57 cxpgt0d 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. ZZ ) -> 0 < ( P ^c ( 1 / N ) ) )
59 58 3expia 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. ZZ -> 0 < ( P ^c ( 1 / N ) ) ) )
60 59 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 ) ) ) ) )
61 elnnz 
 |-  ( ( P ^c ( 1 / N ) ) e. NN <-> ( ( P ^c ( 1 / N ) ) e. ZZ /\ 0 < ( P ^c ( 1 / N ) ) ) )
62 60 61 imbitrrdi 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. ZZ -> ( P ^c ( 1 / N ) ) e. NN ) )
63 52 62 mtod 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) e. ZZ )
64 zrtelqelz 
 |-  ( ( P e. ZZ /\ N e. NN /\ ( P ^c ( 1 / N ) ) e. QQ ) -> ( P ^c ( 1 / N ) ) e. ZZ )
65 46 47 64 syl3an12 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) /\ ( P ^c ( 1 / N ) ) e. QQ ) -> ( P ^c ( 1 / N ) ) e. ZZ )
66 65 3expia 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( ( P ^c ( 1 / N ) ) e. QQ -> ( P ^c ( 1 / N ) ) e. ZZ ) )
67 63 66 mtod 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> -. ( P ^c ( 1 / N ) ) e. QQ )
68 12 67 eldifd 
 |-  ( ( P e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( P ^c ( 1 / N ) ) e. ( RR \ QQ ) )