This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( 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 ‘ 𝐴 ) ∈ ℙ ) )