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	mulridd	\|- ( ( ( 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	biimtrid	\|- ( 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	mulridd	\|- ( ( ( 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 ) )

Metamath Proof Explorer

Theorem prmirredlem

Proof