Metamath Proof Explorer

Theorem prmirredlem

Description: A positive integer is irreducible over ZZ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypothesis prmirred.i 
|- I = ( Irred ` ZZring )
Assertion prmirredlem 
|- ( A e. NN -> ( A e. I <-> A e. Prime ) )

Proof

Step Hyp Ref Expression
1 prmirred.i 
 |-  I = ( Irred ` ZZring )
2 zringring 
 |-  ZZring e. Ring
3 zring1 
 |-  1 = ( 1r ` ZZring )
4 1 3 irredn1 
 |-  ( ( ZZring e. Ring /\ A e. I ) -> A =/= 1 )
5 2 4 mpan 
 |-  ( A e. I -> A =/= 1 )
6 5 anim2i 
 |-  ( ( A e. NN /\ A e. I ) -> ( A e. NN /\ A =/= 1 ) )
7 eluz2b3 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ A =/= 1 ) )
8 6 7 sylibr 
 |-  ( ( A e. NN /\ A e. I ) -> A e. ( ZZ>= ` 2 ) )
9 nnz 
 |-  ( y e. NN -> y e. ZZ )
10 9 ad2antrl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> y e. ZZ )
11 simprr 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> y || A )
12 nnne0 
 |-  ( y e. NN -> y =/= 0 )
13 12 ad2antrl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> y =/= 0 )
14 nnz 
 |-  ( A e. NN -> A e. ZZ )
15 14 ad2antrr 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> A e. ZZ )
16 dvdsval2 
 |-  ( ( y e. ZZ /\ y =/= 0 /\ A e. ZZ ) -> ( y || A <-> ( A / y ) e. ZZ ) )
17 10 13 15 16 syl3anc 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y || A <-> ( A / y ) e. ZZ ) )
18 11 17 mpbid 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( A / y ) e. ZZ )
19 15 zcnd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> A e. CC )
20 nncn 
 |-  ( y e. NN -> y e. CC )
21 20 ad2antrl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> y e. CC )
22 19 21 13 divcan2d 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y x. ( A / y ) ) = A )
23 simplr 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> A e. I )
24 22 23 eqeltrd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y x. ( A / y ) ) e. I )
25 zringbas 
 |-  ZZ = ( Base ` ZZring )
26 eqid 
 |-  ( Unit ` ZZring ) = ( Unit ` ZZring )
27 zringmulr 
 |-  x. = ( .r ` ZZring )
28 1 25 26 27 irredmul 
 |-  ( ( y e. ZZ /\ ( A / y ) e. ZZ /\ ( y x. ( A / y ) ) e. I ) -> ( y e. ( Unit ` ZZring ) \/ ( A / y ) e. ( Unit ` ZZring ) ) )
29 10 18 24 28 syl3anc 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y e. ( Unit ` ZZring ) \/ ( A / y ) e. ( Unit ` ZZring ) ) )
30 zringunit 
 |-  ( y e. ( Unit ` ZZring ) <-> ( y e. ZZ /\ ( abs ` y ) = 1 ) )
31 30 baib 
 |-  ( y e. ZZ -> ( y e. ( Unit ` ZZring ) <-> ( abs ` y ) = 1 ) )
32 10 31 syl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y e. ( Unit ` ZZring ) <-> ( abs ` y ) = 1 ) )
33 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
34 nn0re 
 |-  ( y e. NN0 -> y e. RR )
35 nn0ge0 
 |-  ( y e. NN0 -> 0 <_ y )
36 34 35 absidd 
 |-  ( y e. NN0 -> ( abs ` y ) = y )
37 33 36 syl 
 |-  ( y e. NN -> ( abs ` y ) = y )
38 37 ad2antrl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( abs ` y ) = y )
39 38 eqeq1d 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( abs ` y ) = 1 <-> y = 1 ) )
40 32 39 bitrd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y e. ( Unit ` ZZring ) <-> y = 1 ) )
41 zringunit 
 |-  ( ( A / y ) e. ( Unit ` ZZring ) <-> ( ( A / y ) e. ZZ /\ ( abs ` ( A / y ) ) = 1 ) )
42 41 baib 
 |-  ( ( A / y ) e. ZZ -> ( ( A / y ) e. ( Unit ` ZZring ) <-> ( abs ` ( A / y ) ) = 1 ) )
43 18 42 syl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( A / y ) e. ( Unit ` ZZring ) <-> ( abs ` ( A / y ) ) = 1 ) )
44 nnre 
 |-  ( A e. NN -> A e. RR )
45 44 ad2antrr 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> A e. RR )
46 simprl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> y e. NN )
47 45 46 nndivred 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( A / y ) e. RR )
48 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
49 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
50 48 49 syl 
 |-  ( A e. NN -> 0 <_ A )
51 50 ad2antrr 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> 0 <_ A )
52 46 nnred 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> y e. RR )
53 nngt0 
 |-  ( y e. NN -> 0 < y )
54 53 ad2antrl 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> 0 < y )
55 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( y e. RR /\ 0 < y ) ) -> 0 <_ ( A / y ) )
56 45 51 52 54 55 syl22anc 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> 0 <_ ( A / y ) )
57 47 56 absidd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( abs ` ( A / y ) ) = ( A / y ) )
58 57 eqeq1d 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( abs ` ( A / y ) ) = 1 <-> ( A / y ) = 1 ) )
59 1cnd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> 1 e. CC )
60 19 21 59 13 divmuld 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( A / y ) = 1 <-> ( y x. 1 ) = A ) )
61 21 mulid1d 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y x. 1 ) = y )
62 61 eqeq1d 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( y x. 1 ) = A <-> y = A ) )
63 58 60 62 3bitrd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( abs ` ( A / y ) ) = 1 <-> y = A ) )
64 43 63 bitrd 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( A / y ) e. ( Unit ` ZZring ) <-> y = A ) )
65 40 64 orbi12d 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( ( y e. ( Unit ` ZZring ) \/ ( A / y ) e. ( Unit ` ZZring ) ) <-> ( y = 1 \/ y = A ) ) )
66 29 65 mpbid 
 |-  ( ( ( A e. NN /\ A e. I ) /\ ( y e. NN /\ y || A ) ) -> ( y = 1 \/ y = A ) )
67 66 expr 
 |-  ( ( ( A e. NN /\ A e. I ) /\ y e. NN ) -> ( y || A -> ( y = 1 \/ y = A ) ) )
68 67 ralrimiva 
 |-  ( ( A e. NN /\ A e. I ) -> A. y e. NN ( y || A -> ( y = 1 \/ y = A ) ) )
69 isprm2 
 |-  ( A e. Prime <-> ( A e. ( ZZ>= ` 2 ) /\ A. y e. NN ( y || A -> ( y = 1 \/ y = A ) ) ) )
70 8 68 69 sylanbrc 
 |-  ( ( A e. NN /\ A e. I ) -> A e. Prime )
71 prmz 
 |-  ( A e. Prime -> A e. ZZ )
72 1nprm 
 |-  -. 1 e. Prime
73 zringunit 
 |-  ( A e. ( Unit ` ZZring ) <-> ( A e. ZZ /\ ( abs ` A ) = 1 ) )
74 prmnn 
 |-  ( A e. Prime -> A e. NN )
75 nn0re 
 |-  ( A e. NN0 -> A e. RR )
76 75 49 absidd 
 |-  ( A e. NN0 -> ( abs ` A ) = A )
77 74 48 76 3syl 
 |-  ( A e. Prime -> ( abs ` A ) = A )
78 id 
 |-  ( A e. Prime -> A e. Prime )
79 77 78 eqeltrd 
 |-  ( A e. Prime -> ( abs ` A ) e. Prime )
80 eleq1 
 |-  ( ( abs ` A ) = 1 -> ( ( abs ` A ) e. Prime <-> 1 e. Prime ) )
81 79 80 syl5ibcom 
 |-  ( A e. Prime -> ( ( abs ` A ) = 1 -> 1 e. Prime ) )
82 81 adantld 
 |-  ( A e. Prime -> ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> 1 e. Prime ) )
83 73 82 syl5bi 
 |-  ( A e. Prime -> ( A e. ( Unit ` ZZring ) -> 1 e. Prime ) )
84 72 83 mtoi 
 |-  ( A e. Prime -> -. A e. ( Unit ` ZZring ) )
85 dvdsmul1 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> x || ( x x. y ) )
86 85 ad2antlr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> x || ( x x. y ) )
87 simpr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( x x. y ) = A )
88 86 87 breqtrd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> x || A )
89 simplrl 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> x e. ZZ )
90 71 ad2antrr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> A e. ZZ )
91 absdvdsb 
 |-  ( ( x e. ZZ /\ A e. ZZ ) -> ( x || A <-> ( abs ` x ) || A ) )
92 89 90 91 syl2anc 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( x || A <-> ( abs ` x ) || A ) )
93 88 92 mpbid 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` x ) || A )
94 breq1 
 |-  ( y = ( abs ` x ) -> ( y || A <-> ( abs ` x ) || A ) )
95 eqeq1 
 |-  ( y = ( abs ` x ) -> ( y = 1 <-> ( abs ` x ) = 1 ) )
96 eqeq1 
 |-  ( y = ( abs ` x ) -> ( y = A <-> ( abs ` x ) = A ) )
97 95 96 orbi12d 
 |-  ( y = ( abs ` x ) -> ( ( y = 1 \/ y = A ) <-> ( ( abs ` x ) = 1 \/ ( abs ` x ) = A ) ) )
98 94 97 imbi12d 
 |-  ( y = ( abs ` x ) -> ( ( y || A -> ( y = 1 \/ y = A ) ) <-> ( ( abs ` x ) || A -> ( ( abs ` x ) = 1 \/ ( abs ` x ) = A ) ) ) )
99 69 simprbi 
 |-  ( A e. Prime -> A. y e. NN ( y || A -> ( y = 1 \/ y = A ) ) )
100 99 ad2antrr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> A. y e. NN ( y || A -> ( y = 1 \/ y = A ) ) )
101 89 zcnd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> x e. CC )
102 74 ad2antrr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> A e. NN )
103 102 nnne0d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> A =/= 0 )
104 simplrr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> y e. ZZ )
105 104 zcnd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> y e. CC )
106 105 mul02d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( 0 x. y ) = 0 )
107 103 87 106 3netr4d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( x x. y ) =/= ( 0 x. y ) )
108 oveq1 
 |-  ( x = 0 -> ( x x. y ) = ( 0 x. y ) )
109 108 necon3i 
 |-  ( ( x x. y ) =/= ( 0 x. y ) -> x =/= 0 )
110 107 109 syl 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> x =/= 0 )
111 101 110 absne0d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` x ) =/= 0 )
112 111 neneqd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> -. ( abs ` x ) = 0 )
113 nn0abscl 
 |-  ( x e. ZZ -> ( abs ` x ) e. NN0 )
114 89 113 syl 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` x ) e. NN0 )
115 elnn0 
 |-  ( ( abs ` x ) e. NN0 <-> ( ( abs ` x ) e. NN \/ ( abs ` x ) = 0 ) )
116 114 115 sylib 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( abs ` x ) e. NN \/ ( abs ` x ) = 0 ) )
117 116 ord 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( -. ( abs ` x ) e. NN -> ( abs ` x ) = 0 ) )
118 112 117 mt3d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` x ) e. NN )
119 98 100 118 rspcdva 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( abs ` x ) || A -> ( ( abs ` x ) = 1 \/ ( abs ` x ) = A ) ) )
120 93 119 mpd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( abs ` x ) = 1 \/ ( abs ` x ) = A ) )
121 zringunit 
 |-  ( x e. ( Unit ` ZZring ) <-> ( x e. ZZ /\ ( abs ` x ) = 1 ) )
122 121 baib 
 |-  ( x e. ZZ -> ( x e. ( Unit ` ZZring ) <-> ( abs ` x ) = 1 ) )
123 89 122 syl 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( x e. ( Unit ` ZZring ) <-> ( abs ` x ) = 1 ) )
124 104 31 syl 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( y e. ( Unit ` ZZring ) <-> ( abs ` y ) = 1 ) )
125 105 abscld 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` y ) e. RR )
126 125 recnd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` y ) e. CC )
127 1cnd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> 1 e. CC )
128 101 abscld 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` x ) e. RR )
129 128 recnd 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` x ) e. CC )
130 126 127 129 111 mulcand 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( ( abs ` x ) x. ( abs ` y ) ) = ( ( abs ` x ) x. 1 ) <-> ( abs ` y ) = 1 ) )
131 87 fveq2d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` ( x x. y ) ) = ( abs ` A ) )
132 101 105 absmuld 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
133 77 ad2antrr 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( abs ` A ) = A )
134 131 132 133 3eqtr3d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( abs ` x ) x. ( abs ` y ) ) = A )
135 129 mulid1d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( abs ` x ) x. 1 ) = ( abs ` x ) )
136 134 135 eqeq12d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( ( abs ` x ) x. ( abs ` y ) ) = ( ( abs ` x ) x. 1 ) <-> A = ( abs ` x ) ) )
137 eqcom 
 |-  ( A = ( abs ` x ) <-> ( abs ` x ) = A )
138 136 137 bitrdi 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( ( abs ` x ) x. ( abs ` y ) ) = ( ( abs ` x ) x. 1 ) <-> ( abs ` x ) = A ) )
139 124 130 138 3bitr2d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( y e. ( Unit ` ZZring ) <-> ( abs ` x ) = A ) )
140 123 139 orbi12d 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( ( x e. ( Unit ` ZZring ) \/ y e. ( Unit ` ZZring ) ) <-> ( ( abs ` x ) = 1 \/ ( abs ` x ) = A ) ) )
141 120 140 mpbird 
 |-  ( ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) /\ ( x x. y ) = A ) -> ( x e. ( Unit ` ZZring ) \/ y e. ( Unit ` ZZring ) ) )
142 141 ex 
 |-  ( ( A e. Prime /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. y ) = A -> ( x e. ( Unit ` ZZring ) \/ y e. ( Unit ` ZZring ) ) ) )
143 142 ralrimivva 
 |-  ( A e. Prime -> A. x e. ZZ A. y e. ZZ ( ( x x. y ) = A -> ( x e. ( Unit ` ZZring ) \/ y e. ( Unit ` ZZring ) ) ) )
144 25 26 1 27 isirred2 
 |-  ( A e. I <-> ( A e. ZZ /\ -. A e. ( Unit ` ZZring ) /\ A. x e. ZZ A. y e. ZZ ( ( x x. y ) = A -> ( x e. ( Unit ` ZZring ) \/ y e. ( Unit ` ZZring ) ) ) ) )
145 71 84 143 144 syl3anbrc 
 |-  ( A e. Prime -> A e. I )
146 145 adantl 
 |-  ( ( A e. NN /\ A e. Prime ) -> A e. I )
147 70 146 impbida 
 |-  ( A e. NN -> ( A e. I <-> A e. Prime ) )