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 = ( Irred ` ZZring )
Assertion prmirred 
|- ( A e. I <-> ( A e. ZZ /\ ( abs ` A ) e. Prime ) )

Proof

Step Hyp Ref Expression
1 prmirred.i 
 |-  I = ( Irred ` ZZring )
2 zringbas 
 |-  ZZ = ( Base ` ZZring )
3 1 2 irredcl 
 |-  ( A e. I -> A e. ZZ )
4 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
5 zringring 
 |-  ZZring e. Ring
6 zring0 
 |-  0 = ( 0g ` ZZring )
7 1 6 irredn0 
 |-  ( ( ZZring e. Ring /\ A e. I ) -> A =/= 0 )
8 5 7 mpan 
 |-  ( A e. I -> A =/= 0 )
9 8 necon2bi 
 |-  ( A = 0 -> -. A e. I )
10 9 pm2.21d 
 |-  ( A = 0 -> ( A e. I -> A e. NN ) )
11 10 jao1i 
 |-  ( ( A e. NN \/ A = 0 ) -> ( A e. I -> A e. NN ) )
12 4 11 sylbi 
 |-  ( A e. NN0 -> ( A e. I -> A e. NN ) )
13 prmnn 
 |-  ( A e. Prime -> A e. NN )
14 13 a1i 
 |-  ( A e. NN0 -> ( A e. Prime -> A e. NN ) )
15 1 prmirredlem 
 |-  ( A e. NN -> ( A e. I <-> A e. Prime ) )
16 15 a1i 
 |-  ( A e. NN0 -> ( A e. NN -> ( A e. I <-> A e. Prime ) ) )
17 12 14 16 pm5.21ndd 
 |-  ( A e. NN0 -> ( A e. I <-> A e. Prime ) )
18 nn0re 
 |-  ( A e. NN0 -> A e. RR )
19 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
20 18 19 absidd 
 |-  ( A e. NN0 -> ( abs ` A ) = A )
21 20 eleq1d 
 |-  ( A e. NN0 -> ( ( abs ` A ) e. Prime <-> A e. Prime ) )
22 17 21 bitr4d 
 |-  ( A e. NN0 -> ( A e. I <-> ( abs ` A ) e. Prime ) )
23 22 adantl 
 |-  ( ( A e. ZZ /\ A e. NN0 ) -> ( A e. I <-> ( abs ` A ) e. Prime ) )
24 1 prmirredlem 
 |-  ( -u A e. NN -> ( -u A e. I <-> -u A e. Prime ) )
25 24 adantl 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> ( -u A e. I <-> -u A e. Prime ) )
26 eqid 
 |-  ( invg ` ZZring ) = ( invg ` ZZring )
27 1 26 2 irrednegb 
 |-  ( ( ZZring e. Ring /\ A e. ZZ ) -> ( A e. I <-> ( ( invg ` ZZring ) ` A ) e. I ) )
28 5 27 mpan 
 |-  ( A e. ZZ -> ( A e. I <-> ( ( invg ` ZZring ) ` A ) e. I ) )
29 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
30 subrgsubg 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) )
31 29 30 ax-mp 
 |-  ZZ e. ( SubGrp ` CCfld )
32 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
33 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
34 32 33 26 subginv 
 |-  ( ( ZZ e. ( SubGrp ` CCfld ) /\ A e. ZZ ) -> ( ( invg ` CCfld ) ` A ) = ( ( invg ` ZZring ) ` A ) )
35 31 34 mpan 
 |-  ( A e. ZZ -> ( ( invg ` CCfld ) ` A ) = ( ( invg ` ZZring ) ` A ) )
36 zcn 
 |-  ( A e. ZZ -> A e. CC )
37 cnfldneg 
 |-  ( A e. CC -> ( ( invg ` CCfld ) ` A ) = -u A )
38 36 37 syl 
 |-  ( A e. ZZ -> ( ( invg ` CCfld ) ` A ) = -u A )
39 35 38 eqtr3d 
 |-  ( A e. ZZ -> ( ( invg ` ZZring ) ` A ) = -u A )
40 39 eleq1d 
 |-  ( A e. ZZ -> ( ( ( invg ` ZZring ) ` A ) e. I <-> -u A e. I ) )
41 28 40 bitrd 
 |-  ( A e. ZZ -> ( A e. I <-> -u A e. I ) )
42 41 adantr 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> ( A e. I <-> -u A e. I ) )
43 zre 
 |-  ( A e. ZZ -> A e. RR )
44 43 adantr 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> A e. RR )
45 nnnn0 
 |-  ( -u A e. NN -> -u A e. NN0 )
46 45 nn0ge0d 
 |-  ( -u A e. NN -> 0 <_ -u A )
47 46 adantl 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> 0 <_ -u A )
48 44 le0neg1d 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> ( A <_ 0 <-> 0 <_ -u A ) )
49 47 48 mpbird 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> A <_ 0 )
50 44 49 absnidd 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> ( abs ` A ) = -u A )
51 50 eleq1d 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> ( ( abs ` A ) e. Prime <-> -u A e. Prime ) )
52 25 42 51 3bitr4d 
 |-  ( ( A e. ZZ /\ -u A e. NN ) -> ( A e. I <-> ( abs ` A ) e. Prime ) )
53 52 adantrl 
 |-  ( ( A e. ZZ /\ ( A e. RR /\ -u A e. NN ) ) -> ( A e. I <-> ( abs ` A ) e. Prime ) )
54 elznn0nn 
 |-  ( A e. ZZ <-> ( A e. NN0 \/ ( A e. RR /\ -u A e. NN ) ) )
55 54 biimpi 
 |-  ( A e. ZZ -> ( A e. NN0 \/ ( A e. RR /\ -u A e. NN ) ) )
56 23 53 55 mpjaodan 
 |-  ( A e. ZZ -> ( A e. I <-> ( abs ` A ) e. Prime ) )
57 3 56 biadanii 
 |-  ( A e. I <-> ( A e. ZZ /\ ( abs ` A ) e. Prime ) )