Description: The irreducible elements of ZZ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | prmirred.i | |
|
Assertion | prmirred | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmirred.i | |
|
2 | zringbas | |
|
3 | 1 2 | irredcl | |
4 | elnn0 | |
|
5 | zringring | |
|
6 | zring0 | |
|
7 | 1 6 | irredn0 | |
8 | 5 7 | mpan | |
9 | 8 | necon2bi | |
10 | 9 | pm2.21d | |
11 | 10 | jao1i | |
12 | 4 11 | sylbi | |
13 | prmnn | |
|
14 | 13 | a1i | |
15 | 1 | prmirredlem | |
16 | 15 | a1i | |
17 | 12 14 16 | pm5.21ndd | |
18 | nn0re | |
|
19 | nn0ge0 | |
|
20 | 18 19 | absidd | |
21 | 20 | eleq1d | |
22 | 17 21 | bitr4d | |
23 | 22 | adantl | |
24 | 1 | prmirredlem | |
25 | 24 | adantl | |
26 | eqid | |
|
27 | 1 26 2 | irrednegb | |
28 | 5 27 | mpan | |
29 | zsubrg | |
|
30 | subrgsubg | |
|
31 | 29 30 | ax-mp | |
32 | df-zring | |
|
33 | eqid | |
|
34 | 32 33 26 | subginv | |
35 | 31 34 | mpan | |
36 | zcn | |
|
37 | cnfldneg | |
|
38 | 36 37 | syl | |
39 | 35 38 | eqtr3d | |
40 | 39 | eleq1d | |
41 | 28 40 | bitrd | |
42 | 41 | adantr | |
43 | zre | |
|
44 | 43 | adantr | |
45 | nnnn0 | |
|
46 | 45 | nn0ge0d | |
47 | 46 | adantl | |
48 | 44 | le0neg1d | |
49 | 47 48 | mpbird | |
50 | 44 49 | absnidd | |
51 | 50 | eleq1d | |
52 | 25 42 51 | 3bitr4d | |
53 | 52 | adantrl | |
54 | elznn0nn | |
|
55 | 54 | biimpi | |
56 | 23 53 55 | mpjaodan | |
57 | 3 56 | biadanii | |