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

Theorem prmirred 19003
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.)
Hypothesis
Ref Expression
prmirred.i  |-  I  =  (Irred ` ring )
Assertion
Ref Expression
prmirred  |-  ( A  e.  I  <->  ( A  e.  ZZ  /\  ( abs `  A )  e.  Prime ) )

Proof of Theorem prmirred
StepHypRef Expression
1 prmirred.i . . 3  |-  I  =  (Irred ` ring )
2 zringbas 18982 . . 3  |-  ZZ  =  ( Base ` ring )
31, 2irredcl 17870 . 2  |-  ( A  e.  I  ->  A  e.  ZZ )
4 elnn0 10817 . . . . . . 7  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
5 ax-1 6 . . . . . . . 8  |-  ( A  e.  NN  ->  ( A  e.  I  ->  A  e.  NN ) )
6 zringring 18979 . . . . . . . . . . 11  |-ring  e.  Ring
7 zring0 18986 . . . . . . . . . . . 12  |-  0  =  ( 0g ` ring )
81, 7irredn0 17869 . . . . . . . . . . 11  |-  ( (ring  e. 
Ring  /\  A  e.  I
)  ->  A  =/=  0 )
96, 8mpan 674 . . . . . . . . . 10  |-  ( A  e.  I  ->  A  =/=  0 )
109necon2bi 2626 . . . . . . . . 9  |-  ( A  =  0  ->  -.  A  e.  I )
1110pm2.21d 109 . . . . . . . 8  |-  ( A  =  0  ->  ( A  e.  I  ->  A  e.  NN ) )
125, 11jaoi 380 . . . . . . 7  |-  ( ( A  e.  NN  \/  A  =  0 )  ->  ( A  e.  I  ->  A  e.  NN ) )
134, 12sylbi 198 . . . . . 6  |-  ( A  e.  NN0  ->  ( A  e.  I  ->  A  e.  NN ) )
14 prmnn 14563 . . . . . . 7  |-  ( A  e.  Prime  ->  A  e.  NN )
1514a1i 11 . . . . . 6  |-  ( A  e.  NN0  ->  ( A  e.  Prime  ->  A  e.  NN ) )
161prmirredlem 19001 . . . . . . 7  |-  ( A  e.  NN  ->  ( A  e.  I  <->  A  e.  Prime ) )
1716a1i 11 . . . . . 6  |-  ( A  e.  NN0  ->  ( A  e.  NN  ->  ( A  e.  I  <->  A  e.  Prime ) ) )
1813, 15, 17pm5.21ndd 355 . . . . 5  |-  ( A  e.  NN0  ->  ( A  e.  I  <->  A  e.  Prime ) )
19 nn0re 10824 . . . . . . 7  |-  ( A  e.  NN0  ->  A  e.  RR )
20 nn0ge0 10841 . . . . . . 7  |-  ( A  e.  NN0  ->  0  <_  A )
2119, 20absidd 13423 . . . . . 6  |-  ( A  e.  NN0  ->  ( abs `  A )  =  A )
2221eleq1d 2485 . . . . 5  |-  ( A  e.  NN0  ->  ( ( abs `  A )  e.  Prime  <->  A  e.  Prime ) )
2318, 22bitr4d 259 . . . 4  |-  ( A  e.  NN0  ->  ( A  e.  I  <->  ( abs `  A )  e.  Prime ) )
2423adantl 467 . . 3  |-  ( ( A  e.  ZZ  /\  A  e.  NN0 )  -> 
( A  e.  I  <->  ( abs `  A )  e.  Prime ) )
251prmirredlem 19001 . . . . . 6  |-  ( -u A  e.  NN  ->  (
-u A  e.  I  <->  -u A  e.  Prime )
)
2625adantl 467 . . . . 5  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  ( -u A  e.  I  <->  -u A  e.  Prime ) )
27 eqid 2423 . . . . . . . . 9  |-  ( invg ` ring )  =  ( invg ` ring )
281, 27, 2irrednegb 17877 . . . . . . . 8  |-  ( (ring  e. 
Ring  /\  A  e.  ZZ )  ->  ( A  e.  I  <->  ( ( invg ` ring ) `  A )  e.  I ) )
296, 28mpan 674 . . . . . . 7  |-  ( A  e.  ZZ  ->  ( A  e.  I  <->  ( ( invg ` ring ) `  A )  e.  I ) )
30 zsubrg 18959 . . . . . . . . . . 11  |-  ZZ  e.  (SubRing ` fld )
31 subrgsubg 17952 . . . . . . . . . . 11  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubGrp ` fld ) )
3230, 31ax-mp 5 . . . . . . . . . 10  |-  ZZ  e.  (SubGrp ` fld )
33 df-zring 18977 . . . . . . . . . . 11  |-ring  =  (flds  ZZ )
34 eqid 2423 . . . . . . . . . . 11  |-  ( invg ` fld )  =  ( invg ` fld )
3533, 34, 27subginv 16762 . . . . . . . . . 10  |-  ( ( ZZ  e.  (SubGrp ` fld )  /\  A  e.  ZZ )  ->  ( ( invg ` fld ) `  A )  =  ( ( invg ` ring ) `  A ) )
3632, 35mpan 674 . . . . . . . . 9  |-  ( A  e.  ZZ  ->  (
( invg ` fld ) `  A )  =  ( ( invg ` ring ) `  A ) )
37 zcn 10888 . . . . . . . . . 10  |-  ( A  e.  ZZ  ->  A  e.  CC )
38 cnfldneg 18932 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
( invg ` fld ) `  A )  =  -u A )
3937, 38syl 17 . . . . . . . . 9  |-  ( A  e.  ZZ  ->  (
( invg ` fld ) `  A )  =  -u A )
4036, 39eqtr3d 2459 . . . . . . . 8  |-  ( A  e.  ZZ  ->  (
( invg ` ring ) `  A )  =  -u A )
4140eleq1d 2485 . . . . . . 7  |-  ( A  e.  ZZ  ->  (
( ( invg ` ring ) `  A )  e.  I  <->  -u A  e.  I
) )
4229, 41bitrd 256 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  e.  I  <->  -u A  e.  I ) )
4342adantr 466 . . . . 5  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  ( A  e.  I  <->  -u A  e.  I
) )
44 zre 10887 . . . . . . . 8  |-  ( A  e.  ZZ  ->  A  e.  RR )
4544adantr 466 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  A  e.  RR )
46 nnnn0 10822 . . . . . . . . . 10  |-  ( -u A  e.  NN  ->  -u A  e.  NN0 )
4746nn0ge0d 10874 . . . . . . . . 9  |-  ( -u A  e.  NN  ->  0  <_  -u A )
4847adantl 467 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  0  <_  -u A
)
4945le0neg1d 10131 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  ( A  <_ 
0  <->  0  <_  -u A
) )
5048, 49mpbird 235 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  A  <_  0
)
5145, 50absnidd 13414 . . . . . 6  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  ( abs `  A
)  =  -u A
)
5251eleq1d 2485 . . . . 5  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  ( ( abs `  A )  e.  Prime  <->  -u A  e.  Prime ) )
5326, 43, 523bitr4d 288 . . . 4  |-  ( ( A  e.  ZZ  /\  -u A  e.  NN )  ->  ( A  e.  I  <->  ( abs `  A
)  e.  Prime )
)
5453adantrl 720 . . 3  |-  ( ( A  e.  ZZ  /\  ( A  e.  RR  /\  -u A  e.  NN ) )  ->  ( A  e.  I  <->  ( abs `  A )  e.  Prime ) )
55 elznn0nn 10897 . . . 4  |-  ( A  e.  ZZ  <->  ( A  e.  NN0  \/  ( A  e.  RR  /\  -u A  e.  NN ) ) )
5655biimpi 197 . . 3  |-  ( A  e.  ZZ  ->  ( A  e.  NN0  \/  ( A  e.  RR  /\  -u A  e.  NN ) ) )
5724, 54, 56mpjaodan 793 . 2  |-  ( A  e.  ZZ  ->  ( A  e.  I  <->  ( abs `  A )  e.  Prime ) )
583, 57biadan2 646 1  |-  ( A  e.  I  <->  ( A  e.  ZZ  /\  ( abs `  A )  e.  Prime ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2594   class class class wbr 4361   ` cfv 5539   CCcc 9483   RRcr 9484   0cc0 9485    <_ cle 9622   -ucneg 9807   NNcn 10555   NN0cn0 10815   ZZcz 10883   abscabs 13236   Primecprime 14560   invgcminusg 16608  SubGrpcsubg 16749   Ringcrg 17718  Irredcir 17806  SubRingcsubrg 17942  ℂfldccnfld 18908  ℤringzring 18976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563  ax-addf 9564  ax-mulf 9565
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-tpos 6923  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-sup 7904  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-4 10616  df-5 10617  df-6 10618  df-7 10619  df-8 10620  df-9 10621  df-10 10622  df-n0 10816  df-z 10884  df-dec 10998  df-uz 11106  df-rp 11249  df-fz 11731  df-seq 12159  df-exp 12218  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-dvds 14244  df-prm 14561  df-gz 14812  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-ress 15066  df-plusg 15141  df-mulr 15142  df-starv 15143  df-tset 15147  df-ple 15148  df-ds 15150  df-unif 15151  df-0g 15278  df-mgm 16426  df-sgrp 16465  df-mnd 16475  df-grp 16611  df-minusg 16612  df-subg 16752  df-cmn 17370  df-mgp 17662  df-ur 17674  df-ring 17720  df-cring 17721  df-oppr 17789  df-dvdsr 17807  df-unit 17808  df-irred 17809  df-invr 17838  df-dvr 17849  df-drng 17915  df-subrg 17944  df-cnfld 18909  df-zring 18977
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator