Metamath Proof Explorer


Theorem prmirred

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 I=Irredring
Assertion prmirred AIAA

Proof

Step Hyp Ref Expression
1 prmirred.i I=Irredring
2 zringbas =Basering
3 1 2 irredcl AIA
4 elnn0 A0AA=0
5 zringring ringRing
6 zring0 0=0ring
7 1 6 irredn0 ringRingAIA0
8 5 7 mpan AIA0
9 8 necon2bi A=0¬AI
10 9 pm2.21d A=0AIA
11 10 jao1i AA=0AIA
12 4 11 sylbi A0AIA
13 prmnn AA
14 13 a1i A0AA
15 1 prmirredlem AAIA
16 15 a1i A0AAIA
17 12 14 16 pm5.21ndd A0AIA
18 nn0re A0A
19 nn0ge0 A00A
20 18 19 absidd A0A=A
21 20 eleq1d A0AA
22 17 21 bitr4d A0AIA
23 22 adantl AA0AIA
24 1 prmirredlem AAIA
25 24 adantl AAAIA
26 eqid invgring=invgring
27 1 26 2 irrednegb ringRingAAIinvgringAI
28 5 27 mpan AAIinvgringAI
29 zsubrg SubRingfld
30 subrgsubg SubRingfldSubGrpfld
31 29 30 ax-mp SubGrpfld
32 df-zring ring=fld𝑠
33 eqid invgfld=invgfld
34 32 33 26 subginv SubGrpfldAinvgfldA=invgringA
35 31 34 mpan AinvgfldA=invgringA
36 zcn AA
37 cnfldneg AinvgfldA=A
38 36 37 syl AinvgfldA=A
39 35 38 eqtr3d AinvgringA=A
40 39 eleq1d AinvgringAIAI
41 28 40 bitrd AAIAI
42 41 adantr AAAIAI
43 zre AA
44 43 adantr AAA
45 nnnn0 AA0
46 45 nn0ge0d A0A
47 46 adantl AA0A
48 44 le0neg1d AAA00A
49 47 48 mpbird AAA0
50 44 49 absnidd AAA=A
51 50 eleq1d AAAA
52 25 42 51 3bitr4d AAAIA
53 52 adantrl AAAAIA
54 elznn0nn AA0AA
55 54 biimpi AA0AA
56 23 53 55 mpjaodan AAIA
57 3 56 biadanii AIAA