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 ⊢ 𝐼 = ( Irred ‘ ℤring )
Assertion prmirredlem ( 𝐴 ∈ ℕ → ( 𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ ) )

Proof

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