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

Theorem prmirredOLD 18395
 Description: The irreducible elements of are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) Obsolete version of prmirred 18392 as of 10-Jun-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
prmirredOLD.1 flds
prmirredOLD.2 Irred
Assertion
Ref Expression
prmirredOLD

Proof of Theorem prmirredOLD
StepHypRef Expression
1 prmirredOLD.2 . . 3 Irred
2 zsubrg 18339 . . . 4 SubRingfld
3 prmirredOLD.1 . . . . 5 flds
43subrgbas 17307 . . . 4 SubRingfld
52, 4ax-mp 5 . . 3
61, 5irredcl 17223 . 2
7 elnn0 10809 . . . . . . 7
8 ax-1 6 . . . . . . . 8
93subrgring 17301 . . . . . . . . . . . 12 SubRingfld
102, 9ax-mp 5 . . . . . . . . . . 11
11 subrgsubg 17304 . . . . . . . . . . . . . 14 SubRingfld SubGrpfld
122, 11ax-mp 5 . . . . . . . . . . . . 13 SubGrpfld
13 cnfld0 18310 . . . . . . . . . . . . . 14 fld
143, 13subg0 16078 . . . . . . . . . . . . 13 SubGrpfld
1512, 14ax-mp 5 . . . . . . . . . . . 12
161, 15irredn0 17222 . . . . . . . . . . 11
1710, 16mpan 670 . . . . . . . . . 10
1817necon2bi 2704 . . . . . . . . 9
1918pm2.21d 106 . . . . . . . 8
208, 19jaoi 379 . . . . . . 7
217, 20sylbi 195 . . . . . 6
22 prmnn 14095 . . . . . . 7
2322a1i 11 . . . . . 6
243, 1prmirredlemOLD 18393 . . . . . . 7
2524a1i 11 . . . . . 6
2621, 23, 25pm5.21ndd 354 . . . . 5
27 nn0re 10816 . . . . . . 7
28 nn0ge0 10833 . . . . . . 7
2927, 28absidd 13233 . . . . . 6
3029eleq1d 2536 . . . . 5
3126, 30bitr4d 256 . . . 4
333, 1prmirredlemOLD 18393 . . . . . 6
3433adantl 466 . . . . 5
35 eqid 2467 . . . . . . . . 9
361, 35, 5irrednegb 17230 . . . . . . . 8
3710, 36mpan 670 . . . . . . 7
38 eqid 2467 . . . . . . . . . . 11 fld fld
393, 38, 35subginv 16079 . . . . . . . . . 10 SubGrpfld fld
4012, 39mpan 670 . . . . . . . . 9 fld
41 zcn 10881 . . . . . . . . . 10
42 cnfldneg 18312 . . . . . . . . . 10 fld
4341, 42syl 16 . . . . . . . . 9 fld
4440, 43eqtr3d 2510 . . . . . . . 8
4544eleq1d 2536 . . . . . . 7
4637, 45bitrd 253 . . . . . 6
4746adantr 465 . . . . 5
48 zre 10880 . . . . . . . 8
4948adantr 465 . . . . . . 7
50 nnnn0 10814 . . . . . . . . . 10
5150nn0ge0d 10867 . . . . . . . . 9
5251adantl 466 . . . . . . . 8
5349le0neg1d 10136 . . . . . . . 8
5452, 53mpbird 232 . . . . . . 7
5549, 54absnidd 13224 . . . . . 6
5655eleq1d 2536 . . . . 5
5734, 47, 563bitr4d 285 . . . 4