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

Theorem prmirred 16780
 Description: The irreducible elements of are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.)
Hypotheses
Ref Expression
prmirred.1 flds
prmirred.2 Irred
Assertion
Ref Expression
prmirred

Proof of Theorem prmirred
StepHypRef Expression
1 prmirred.2 . . 3 Irred
2 zsubrg 16757 . . . 4 SubRingfld
3 prmirred.1 . . . . 5 flds
43subrgbas 15882 . . . 4 SubRingfld
52, 4ax-mp 5 . . 3
61, 5irredcl 15814 . 2
7 elnn0 10228 . . . . . . 7
8 ax-1 6 . . . . . . . 8
93subrgrng 15876 . . . . . . . . . . . 12 SubRingfld
102, 9ax-mp 5 . . . . . . . . . . 11
11 subrgsubg 15879 . . . . . . . . . . . . . 14 SubRingfld SubGrpfld
122, 11ax-mp 5 . . . . . . . . . . . . 13 SubGrpfld
13 cnfld0 16730 . . . . . . . . . . . . . 14 fld
143, 13subg0 14955 . . . . . . . . . . . . 13 SubGrpfld
1512, 14ax-mp 5 . . . . . . . . . . . 12
161, 15irredn0 15813 . . . . . . . . . . 11
1710, 16mpan 653 . . . . . . . . . 10
1817necon2bi 2652 . . . . . . . . 9
1918pm2.21d 101 . . . . . . . 8
208, 19jaoi 370 . . . . . . 7
217, 20sylbi 189 . . . . . 6
22 prmnn 13087 . . . . . . 7
2322a1i 11 . . . . . 6
243, 1prmirredlem 16778 . . . . . . 7
2524a1i 11 . . . . . 6
2621, 23, 25pm5.21ndd 345 . . . . 5
27 nn0re 10235 . . . . . . 7
28 nn0ge0 10252 . . . . . . 7
2927, 28absidd 12230 . . . . . 6
3029eleq1d 2504 . . . . 5
3126, 30bitr4d 249 . . . 4
333, 1prmirredlem 16778 . . . . . 6
3433adantl 454 . . . . 5
35 eqid 2438 . . . . . . . . 9
361, 35, 5irrednegb 15821 . . . . . . . 8
3710, 36mpan 653 . . . . . . 7
38 eqid 2438 . . . . . . . . . . 11 fld fld
393, 38, 35subginv 14956 . . . . . . . . . 10 SubGrpfld fld
4012, 39mpan 653 . . . . . . . . 9 fld
41 zcn 10292 . . . . . . . . . 10
42 cnfldneg 16732 . . . . . . . . . 10 fld
4341, 42syl 16 . . . . . . . . 9 fld
4440, 43eqtr3d 2472 . . . . . . . 8
4544eleq1d 2504 . . . . . . 7
4637, 45bitrd 246 . . . . . 6
4746adantr 453 . . . . 5
48 zre 10291 . . . . . . . 8
4948adantr 453 . . . . . . 7
50 nnnn0 10233 . . . . . . . . . 10
5150nn0ge0d 10282 . . . . . . . . 9
5251adantl 454 . . . . . . . 8
5349le0neg1d 9603 . . . . . . . 8
5452, 53mpbird 225 . . . . . . 7
5549, 54absnidd 12221 . . . . . 6
5655eleq1d 2504 . . . . 5
5734, 47, 563bitr4d 278 . . . 4