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	⊢ 𝐼 = ( Irred ‘ ℤring )
Assertion	prmirred	⊢ ( 𝐴 ∈ 𝐼 ↔ ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) ∈ ℙ ) )

Proof

Step	Hyp	Ref	Expression
1		prmirred.i	⊢ 𝐼 = ( Irred ‘ ℤring )
2		zringbas	⊢ ℤ = ( Base ‘ ℤring )
3	1 2	irredcl	⊢ ( 𝐴 ∈ 𝐼 → 𝐴 ∈ ℤ )
4		elnn0	⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
5		zringring	⊢ ℤring ∈ Ring
6		zring0	⊢ 0 = ( 0g ‘ ℤring )
7	1 6	irredn0	⊢ ( ( ℤring ∈ Ring ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ≠ 0 )
8	5 7	mpan	⊢ ( 𝐴 ∈ 𝐼 → 𝐴 ≠ 0 )
9	8	necon2bi	⊢ ( 𝐴 = 0 → ¬ 𝐴 ∈ 𝐼 )
10	9	pm2.21d	⊢ ( 𝐴 = 0 → ( 𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ ) )
11	10	jao1i	⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → ( 𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ ) )
12	4 11	sylbi	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ ) )
13		prmnn	⊢ ( 𝐴 ∈ ℙ → 𝐴 ∈ ℕ )
14	13	a1i	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℙ → 𝐴 ∈ ℕ ) )
15	1	prmirredlem	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ ) )
16	15	a1i	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℕ → ( 𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ ) ) )
17	12 14 16	pm5.21ndd	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ ) )
18		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
19		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
20	18 19	absidd	⊢ ( 𝐴 ∈ ℕ0 → ( abs ‘ 𝐴 ) = 𝐴 )
21	20	eleq1d	⊢ ( 𝐴 ∈ ℕ0 → ( ( abs ‘ 𝐴 ) ∈ ℙ ↔ 𝐴 ∈ ℙ ) )
22	17 21	bitr4d	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ 𝐼 ↔ ( abs ‘ 𝐴 ) ∈ ℙ ) )
23	22	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ∈ 𝐼 ↔ ( abs ‘ 𝐴 ) ∈ ℙ ) )
24	1	prmirredlem	⊢ ( - 𝐴 ∈ ℕ → ( - 𝐴 ∈ 𝐼 ↔ - 𝐴 ∈ ℙ ) )
25	24	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → ( - 𝐴 ∈ 𝐼 ↔ - 𝐴 ∈ ℙ ) )
26		eqid	⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
27	1 26 2	irrednegb	⊢ ( ( ℤring ∈ Ring ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ 𝐼 ↔ ( ( invg ‘ ℤring ) ‘ 𝐴 ) ∈ 𝐼 ) )
28	5 27	mpan	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ∈ 𝐼 ↔ ( ( invg ‘ ℤring ) ‘ 𝐴 ) ∈ 𝐼 ) )
29		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
30		subrgsubg	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
31	29 30	ax-mp	⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
32		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
33		eqid	⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
34	32 33 26	subginv	⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ ℤ ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = ( ( invg ‘ ℤring ) ‘ 𝐴 ) )
35	31 34	mpan	⊢ ( 𝐴 ∈ ℤ → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = ( ( invg ‘ ℤring ) ‘ 𝐴 ) )
36		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
37		cnfldneg	⊢ ( 𝐴 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
38	36 37	syl	⊢ ( 𝐴 ∈ ℤ → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
39	35 38	eqtr3d	⊢ ( 𝐴 ∈ ℤ → ( ( invg ‘ ℤring ) ‘ 𝐴 ) = - 𝐴 )
40	39	eleq1d	⊢ ( 𝐴 ∈ ℤ → ( ( ( invg ‘ ℤring ) ‘ 𝐴 ) ∈ 𝐼 ↔ - 𝐴 ∈ 𝐼 ) )
41	28 40	bitrd	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ∈ 𝐼 ↔ - 𝐴 ∈ 𝐼 ) )
42	41	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → ( 𝐴 ∈ 𝐼 ↔ - 𝐴 ∈ 𝐼 ) )
43		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
44	43	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → 𝐴 ∈ ℝ )
45		nnnn0	⊢ ( - 𝐴 ∈ ℕ → - 𝐴 ∈ ℕ0 )
46	45	nn0ge0d	⊢ ( - 𝐴 ∈ ℕ → 0 ≤ - 𝐴 )
47	46	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → 0 ≤ - 𝐴 )
48	44	le0neg1d	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → ( 𝐴 ≤ 0 ↔ 0 ≤ - 𝐴 ) )
49	47 48	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → 𝐴 ≤ 0 )
50	44 49	absnidd	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → ( abs ‘ 𝐴 ) = - 𝐴 )
51	50	eleq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → ( ( abs ‘ 𝐴 ) ∈ ℙ ↔ - 𝐴 ∈ ℙ ) )
52	25 42 51	3bitr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝐴 ∈ ℕ ) → ( 𝐴 ∈ 𝐼 ↔ ( abs ‘ 𝐴 ) ∈ ℙ ) )
53	52	adantrl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 ∈ ℝ ∧ - 𝐴 ∈ ℕ ) ) → ( 𝐴 ∈ 𝐼 ↔ ( abs ‘ 𝐴 ) ∈ ℙ ) )
54		elznn0nn	⊢ ( 𝐴 ∈ ℤ ↔ ( 𝐴 ∈ ℕ0 ∨ ( 𝐴 ∈ ℝ ∧ - 𝐴 ∈ ℕ ) ) )
55	54	biimpi	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ∈ ℕ0 ∨ ( 𝐴 ∈ ℝ ∧ - 𝐴 ∈ ℕ ) ) )
56	23 53 55	mpjaodan	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ∈ 𝐼 ↔ ( abs ‘ 𝐴 ) ∈ ℙ ) )
57	3 56	biadanii	⊢ ( 𝐴 ∈ 𝐼 ↔ ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) ∈ ℙ ) )