This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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