Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmirred Structured version   Unicode version

Theorem prmirred 18394
 Description: The irreducible elements of are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
Hypothesis
Ref Expression
prmirred.i Irredring
Assertion
Ref Expression
prmirred

Proof of Theorem prmirred
StepHypRef Expression
1 prmirred.i . . 3 Irredring
2 zringbas 18364 . . 3 ring
31, 2irredcl 17225 . 2
4 elnn0 10809 . . . . . . 7
5 ax-1 6 . . . . . . . 8
6 zringring 18361 . . . . . . . . . . 11 ring
7 zring0 18368 . . . . . . . . . . . 12 ring
81, 7irredn0 17224 . . . . . . . . . . 11 ring
96, 8mpan 670 . . . . . . . . . 10
109necon2bi 2704 . . . . . . . . 9
1110pm2.21d 106 . . . . . . . 8
125, 11jaoi 379 . . . . . . 7
134, 12sylbi 195 . . . . . 6
14 prmnn 14096 . . . . . . 7
1514a1i 11 . . . . . 6
161prmirredlem 18392 . . . . . . 7
1716a1i 11 . . . . . 6
1813, 15, 17pm5.21ndd 354 . . . . 5
19 nn0re 10816 . . . . . . 7
20 nn0ge0 10833 . . . . . . 7
2119, 20absidd 13234 . . . . . 6
2221eleq1d 2536 . . . . 5
2318, 22bitr4d 256 . . . 4
251prmirredlem 18392 . . . . . 6
2625adantl 466 . . . . 5
27 eqid 2467 . . . . . . . . 9 ring ring
281, 27, 2irrednegb 17232 . . . . . . . 8 ring ring
296, 28mpan 670 . . . . . . 7 ring
30 zsubrg 18341 . . . . . . . . . . 11 SubRingfld
31 subrgsubg 17306 . . . . . . . . . . 11 SubRingfld SubGrpfld
3230, 31ax-mp 5 . . . . . . . . . 10 SubGrpfld
33 df-zring 18359 . . . . . . . . . . 11 ring flds
34 eqid 2467 . . . . . . . . . . 11 fld fld
3533, 34, 27subginv 16080 . . . . . . . . . 10 SubGrpfld fld ring
3632, 35mpan 670 . . . . . . . . 9 fld ring
37 zcn 10881 . . . . . . . . . 10
38 cnfldneg 18314 . . . . . . . . . 10 fld
3937, 38syl 16 . . . . . . . . 9 fld
4036, 39eqtr3d 2510 . . . . . . . 8 ring
4140eleq1d 2536 . . . . . . 7 ring
4229, 41bitrd 253 . . . . . 6
4342adantr 465 . . . . 5
44 zre 10880 . . . . . . . 8
4544adantr 465 . . . . . . 7
46 nnnn0 10814 . . . . . . . . . 10
4746nn0ge0d 10867 . . . . . . . . 9
4847adantl 466 . . . . . . . 8
4945le0neg1d 10136 . . . . . . . 8
5048, 49mpbird 232 . . . . . . 7
5145, 50absnidd 13225 . . . . . 6
5251eleq1d 2536 . . . . 5
5326, 43, 523bitr4d 285 . . . 4