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 N 2 P 1 N

Proof

Step Hyp Ref Expression
1 prmnn P P
2 1 adantr P N 2 P
3 2 nnred P N 2 P
4 0red P N 2 0
5 2 nngt0d P N 2 0 < P
6 4 3 5 ltled P N 2 0 P
7 eluzelre N 2 N
8 7 adantl P N 2 N
9 eluz2n0 N 2 N 0
10 9 adantl P N 2 N 0
11 8 10 rereccld P N 2 1 N
12 3 6 11 recxpcld P N 2 P 1 N
13 eluz2gt1 N 2 1 < N
14 recgt1i N 1 < N 0 < 1 N 1 N < 1
15 7 13 14 syl2anc N 2 0 < 1 N 1 N < 1
16 15 simprd N 2 1 N < 1
17 16 adantl P N 2 1 N < 1
18 1 nnred P P
19 18 adantr P N 2 P
20 prmgt1 P 1 < P
21 20 adantr P N 2 1 < P
22 1red P N 2 1
23 19 21 11 22 cxpltd P N 2 1 N < 1 P 1 N < P 1
24 17 23 mpbid P N 2 P 1 N < P 1
25 2 nncnd P N 2 P
26 25 cxp1d P N 2 P 1 = P
27 24 26 breqtrd P N 2 P 1 N < P
28 12 27 ltned P N 2 P 1 N P
29 28 neneqd P N 2 ¬ P 1 N = P
30 29 adantr P N 2 P 1 N ¬ P 1 N = P
31 25 cxp0d P N 2 P 0 = 1
32 15 simpld N 2 0 < 1 N
33 32 adantl P N 2 0 < 1 N
34 19 21 4 11 cxpltd P N 2 0 < 1 N P 0 < P 1 N
35 33 34 mpbid P N 2 P 0 < P 1 N
36 31 35 eqbrtrrd P N 2 1 < P 1 N
37 22 36 gtned P N 2 P 1 N 1
38 37 neneqd P N 2 ¬ P 1 N = 1
39 38 adantr P N 2 P 1 N ¬ P 1 N = 1
40 dvdsprime P P 1 N P 1 N P P 1 N = P P 1 N = 1
41 40 adantlr P N 2 P 1 N P 1 N P P 1 N = P P 1 N = 1
42 41 biimpd P N 2 P 1 N P 1 N P P 1 N = P P 1 N = 1
43 30 39 42 mtord P N 2 P 1 N ¬ P 1 N P
44 nan P N 2 ¬ P 1 N P 1 N P P N 2 P 1 N ¬ P 1 N P
45 43 44 mpbir P N 2 ¬ P 1 N P 1 N P
46 prmz P P
47 eluz2nn N 2 N
48 zrtdvds P N P 1 N P 1 N P
49 46 47 48 syl3an12 P N 2 P 1 N P 1 N P
50 49 3expia P N 2 P 1 N P 1 N P
51 50 ancld P N 2 P 1 N P 1 N P 1 N P
52 45 51 mtod P N 2 ¬ P 1 N
53 1 nnrpd P P +
54 53 3ad2ant1 P N 2 P 1 N P +
55 7 3ad2ant2 P N 2 P 1 N N
56 9 3ad2ant2 P N 2 P 1 N N 0
57 55 56 rereccld P N 2 P 1 N 1 N
58 54 57 cxpgt0d P N 2 P 1 N 0 < P 1 N
59 58 3expia P N 2 P 1 N 0 < P 1 N
60 59 ancld P N 2 P 1 N P 1 N 0 < P 1 N
61 elnnz P 1 N P 1 N 0 < P 1 N
62 60 61 imbitrrdi P N 2 P 1 N P 1 N
63 52 62 mtod P N 2 ¬ P 1 N
64 zrtelqelz P N P 1 N P 1 N
65 46 47 64 syl3an12 P N 2 P 1 N P 1 N
66 65 3expia P N 2 P 1 N P 1 N
67 63 66 mtod P N 2 ¬ P 1 N
68 12 67 eldifd P N 2 P 1 N