MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmirredlem Structured version   Visualization version   GIF version

Theorem prmirredlem 20694
Description: A positive integer is irreducible over iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
Hypothesis
Ref Expression
prmirred.i 𝐼 = (Irred‘ℤring)
Assertion
Ref Expression
prmirredlem (𝐴 ∈ ℕ → (𝐴𝐼𝐴 ∈ ℙ))

Proof of Theorem prmirredlem
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zringring 20673 . . . . . 6 ring ∈ Ring
2 prmirred.i . . . . . . 7 𝐼 = (Irred‘ℤring)
3 zring1 20681 . . . . . . 7 1 = (1r‘ℤring)
42, 3irredn1 19948 . . . . . 6 ((ℤring ∈ Ring ∧ 𝐴𝐼) → 𝐴 ≠ 1)
51, 4mpan 687 . . . . 5 (𝐴𝐼𝐴 ≠ 1)
65anim2i 617 . . . 4 ((𝐴 ∈ ℕ ∧ 𝐴𝐼) → (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1))
7 eluz2b3 12662 . . . 4 (𝐴 ∈ (ℤ‘2) ↔ (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1))
86, 7sylibr 233 . . 3 ((𝐴 ∈ ℕ ∧ 𝐴𝐼) → 𝐴 ∈ (ℤ‘2))
9 nnz 12342 . . . . . . . 8 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
109ad2antrl 725 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦 ∈ ℤ)
11 simprr 770 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝐴)
12 nnne0 12007 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ≠ 0)
1312ad2antrl 725 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦 ≠ 0)
14 nnz 12342 . . . . . . . . . 10 (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
1514ad2antrr 723 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴 ∈ ℤ)
16 dvdsval2 15966 . . . . . . . . 9 ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝐴 ∈ ℤ) → (𝑦𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ))
1710, 13, 15, 16syl3anc 1370 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ))
1811, 17mpbid 231 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝐴 / 𝑦) ∈ ℤ)
1915zcnd 12427 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴 ∈ ℂ)
20 nncn 11981 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
2120ad2antrl 725 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦 ∈ ℂ)
2219, 21, 13divcan2d 11753 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 · (𝐴 / 𝑦)) = 𝐴)
23 simplr 766 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴𝐼)
2422, 23eqeltrd 2839 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼)
25 zringbas 20676 . . . . . . . 8 ℤ = (Base‘ℤring)
26 eqid 2738 . . . . . . . 8 (Unit‘ℤring) = (Unit‘ℤring)
27 zringmulr 20679 . . . . . . . 8 · = (.r‘ℤring)
282, 25, 26, 27irredmul 19951 . . . . . . 7 ((𝑦 ∈ ℤ ∧ (𝐴 / 𝑦) ∈ ℤ ∧ (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) → (𝑦 ∈ (Unit‘ℤring) ∨ (𝐴 / 𝑦) ∈ (Unit‘ℤring)))
2910, 18, 24, 28syl3anc 1370 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 ∈ (Unit‘ℤring) ∨ (𝐴 / 𝑦) ∈ (Unit‘ℤring)))
30 zringunit 20688 . . . . . . . . . 10 (𝑦 ∈ (Unit‘ℤring) ↔ (𝑦 ∈ ℤ ∧ (abs‘𝑦) = 1))
3130baib 536 . . . . . . . . 9 (𝑦 ∈ ℤ → (𝑦 ∈ (Unit‘ℤring) ↔ (abs‘𝑦) = 1))
3210, 31syl 17 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 ∈ (Unit‘ℤring) ↔ (abs‘𝑦) = 1))
33 nnnn0 12240 . . . . . . . . . . 11 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
34 nn0re 12242 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
35 nn0ge0 12258 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0 → 0 ≤ 𝑦)
3634, 35absidd 15134 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → (abs‘𝑦) = 𝑦)
3733, 36syl 17 . . . . . . . . . 10 (𝑦 ∈ ℕ → (abs‘𝑦) = 𝑦)
3837ad2antrl 725 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (abs‘𝑦) = 𝑦)
3938eqeq1d 2740 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((abs‘𝑦) = 1 ↔ 𝑦 = 1))
4032, 39bitrd 278 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 ∈ (Unit‘ℤring) ↔ 𝑦 = 1))
41 zringunit 20688 . . . . . . . . . 10 ((𝐴 / 𝑦) ∈ (Unit‘ℤring) ↔ ((𝐴 / 𝑦) ∈ ℤ ∧ (abs‘(𝐴 / 𝑦)) = 1))
4241baib 536 . . . . . . . . 9 ((𝐴 / 𝑦) ∈ ℤ → ((𝐴 / 𝑦) ∈ (Unit‘ℤring) ↔ (abs‘(𝐴 / 𝑦)) = 1))
4318, 42syl 17 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring) ↔ (abs‘(𝐴 / 𝑦)) = 1))
44 nnre 11980 . . . . . . . . . . . . 13 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
4544ad2antrr 723 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴 ∈ ℝ)
46 simprl 768 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦 ∈ ℕ)
4745, 46nndivred 12027 . . . . . . . . . . 11 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝐴 / 𝑦) ∈ ℝ)
48 nnnn0 12240 . . . . . . . . . . . . . 14 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
49 nn0ge0 12258 . . . . . . . . . . . . . 14 (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
5048, 49syl 17 . . . . . . . . . . . . 13 (𝐴 ∈ ℕ → 0 ≤ 𝐴)
5150ad2antrr 723 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 0 ≤ 𝐴)
5246nnred 11988 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦 ∈ ℝ)
53 nngt0 12004 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 < 𝑦)
5453ad2antrl 725 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 0 < 𝑦)
55 divge0 11844 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → 0 ≤ (𝐴 / 𝑦))
5645, 51, 52, 54, 55syl22anc 836 . . . . . . . . . . 11 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 0 ≤ (𝐴 / 𝑦))
5747, 56absidd 15134 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (abs‘(𝐴 / 𝑦)) = (𝐴 / 𝑦))
5857eqeq1d 2740 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ (𝐴 / 𝑦) = 1))
59 1cnd 10970 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → 1 ∈ ℂ)
6019, 21, 59, 13divmuld 11773 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((𝐴 / 𝑦) = 1 ↔ (𝑦 · 1) = 𝐴))
6121mulid1d 10992 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 · 1) = 𝑦)
6261eqeq1d 2740 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((𝑦 · 1) = 𝐴𝑦 = 𝐴))
6358, 60, 623bitrd 305 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ 𝑦 = 𝐴))
6443, 63bitrd 278 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring) ↔ 𝑦 = 𝐴))
6540, 64orbi12d 916 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → ((𝑦 ∈ (Unit‘ℤring) ∨ (𝐴 / 𝑦) ∈ (Unit‘ℤring)) ↔ (𝑦 = 1 ∨ 𝑦 = 𝐴)))
6629, 65mpbid 231 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦 = 1 ∨ 𝑦 = 𝐴))
6766expr 457 . . . 4 (((𝐴 ∈ ℕ ∧ 𝐴𝐼) ∧ 𝑦 ∈ ℕ) → (𝑦𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))
6867ralrimiva 3103 . . 3 ((𝐴 ∈ ℕ ∧ 𝐴𝐼) → ∀𝑦 ∈ ℕ (𝑦𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))
69 isprm2 16387 . . 3 (𝐴 ∈ ℙ ↔ (𝐴 ∈ (ℤ‘2) ∧ ∀𝑦 ∈ ℕ (𝑦𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))))
708, 68, 69sylanbrc 583 . 2 ((𝐴 ∈ ℕ ∧ 𝐴𝐼) → 𝐴 ∈ ℙ)
71 prmz 16380 . . . 4 (𝐴 ∈ ℙ → 𝐴 ∈ ℤ)
72 1nprm 16384 . . . . 5 ¬ 1 ∈ ℙ
73 zringunit 20688 . . . . . 6 (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1))
74 prmnn 16379 . . . . . . . . . 10 (𝐴 ∈ ℙ → 𝐴 ∈ ℕ)
75 nn0re 12242 . . . . . . . . . . 11 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
7675, 49absidd 15134 . . . . . . . . . 10 (𝐴 ∈ ℕ0 → (abs‘𝐴) = 𝐴)
7774, 48, 763syl 18 . . . . . . . . 9 (𝐴 ∈ ℙ → (abs‘𝐴) = 𝐴)
78 id 22 . . . . . . . . 9 (𝐴 ∈ ℙ → 𝐴 ∈ ℙ)
7977, 78eqeltrd 2839 . . . . . . . 8 (𝐴 ∈ ℙ → (abs‘𝐴) ∈ ℙ)
80 eleq1 2826 . . . . . . . 8 ((abs‘𝐴) = 1 → ((abs‘𝐴) ∈ ℙ ↔ 1 ∈ ℙ))
8179, 80syl5ibcom 244 . . . . . . 7 (𝐴 ∈ ℙ → ((abs‘𝐴) = 1 → 1 ∈ ℙ))
8281adantld 491 . . . . . 6 (𝐴 ∈ ℙ → ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 1 ∈ ℙ))
8373, 82syl5bi 241 . . . . 5 (𝐴 ∈ ℙ → (𝐴 ∈ (Unit‘ℤring) → 1 ∈ ℙ))
8472, 83mtoi 198 . . . 4 (𝐴 ∈ ℙ → ¬ 𝐴 ∈ (Unit‘ℤring))
85 dvdsmul1 15987 . . . . . . . . . . 11 ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∥ (𝑥 · 𝑦))
8685ad2antlr 724 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ (𝑥 · 𝑦))
87 simpr 485 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) = 𝐴)
8886, 87breqtrd 5100 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥𝐴)
89 simplrl 774 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℤ)
9071ad2antrr 723 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℤ)
91 absdvdsb 15984 . . . . . . . . . 10 ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑥𝐴 ↔ (abs‘𝑥) ∥ 𝐴))
9289, 90, 91syl2anc 584 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥𝐴 ↔ (abs‘𝑥) ∥ 𝐴))
9388, 92mpbid 231 . . . . . . . 8 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∥ 𝐴)
94 breq1 5077 . . . . . . . . . 10 (𝑦 = (abs‘𝑥) → (𝑦𝐴 ↔ (abs‘𝑥) ∥ 𝐴))
95 eqeq1 2742 . . . . . . . . . . 11 (𝑦 = (abs‘𝑥) → (𝑦 = 1 ↔ (abs‘𝑥) = 1))
96 eqeq1 2742 . . . . . . . . . . 11 (𝑦 = (abs‘𝑥) → (𝑦 = 𝐴 ↔ (abs‘𝑥) = 𝐴))
9795, 96orbi12d 916 . . . . . . . . . 10 (𝑦 = (abs‘𝑥) → ((𝑦 = 1 ∨ 𝑦 = 𝐴) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))
9894, 97imbi12d 345 . . . . . . . . 9 (𝑦 = (abs‘𝑥) → ((𝑦𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)) ↔ ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))))
9969simprbi 497 . . . . . . . . . 10 (𝐴 ∈ ℙ → ∀𝑦 ∈ ℕ (𝑦𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))
10099ad2antrr 723 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ∀𝑦 ∈ ℕ (𝑦𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))
10189zcnd 12427 . . . . . . . . . . . 12 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℂ)
10274ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℕ)
103102nnne0d 12023 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ≠ 0)
104 simplrr 775 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℤ)
105104zcnd 12427 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℂ)
106105mul02d 11173 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (0 · 𝑦) = 0)
107103, 87, 1063netr4d 3021 . . . . . . . . . . . . 13 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) ≠ (0 · 𝑦))
108 oveq1 7282 . . . . . . . . . . . . . 14 (𝑥 = 0 → (𝑥 · 𝑦) = (0 · 𝑦))
109108necon3i 2976 . . . . . . . . . . . . 13 ((𝑥 · 𝑦) ≠ (0 · 𝑦) → 𝑥 ≠ 0)
110107, 109syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ≠ 0)
111101, 110absne0d 15159 . . . . . . . . . . 11 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ≠ 0)
112111neneqd 2948 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ¬ (abs‘𝑥) = 0)
113 nn0abscl 15024 . . . . . . . . . . . . 13 (𝑥 ∈ ℤ → (abs‘𝑥) ∈ ℕ0)
11489, 113syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℕ0)
115 elnn0 12235 . . . . . . . . . . . 12 ((abs‘𝑥) ∈ ℕ0 ↔ ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0))
116114, 115sylib 217 . . . . . . . . . . 11 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0))
117116ord 861 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (¬ (abs‘𝑥) ∈ ℕ → (abs‘𝑥) = 0))
118112, 117mt3d 148 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℕ)
11998, 100, 118rspcdva 3562 . . . . . . . 8 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))
12093, 119mpd 15 . . . . . . 7 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))
121 zringunit 20688 . . . . . . . . . 10 (𝑥 ∈ (Unit‘ℤring) ↔ (𝑥 ∈ ℤ ∧ (abs‘𝑥) = 1))
122121baib 536 . . . . . . . . 9 (𝑥 ∈ ℤ → (𝑥 ∈ (Unit‘ℤring) ↔ (abs‘𝑥) = 1))
12389, 122syl 17 . . . . . . . 8 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring) ↔ (abs‘𝑥) = 1))
124104, 31syl 17 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑦 ∈ (Unit‘ℤring) ↔ (abs‘𝑦) = 1))
125105abscld 15148 . . . . . . . . . . 11 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℝ)
126125recnd 11003 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℂ)
127 1cnd 10970 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 1 ∈ ℂ)
128101abscld 15148 . . . . . . . . . . 11 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℝ)
129128recnd 11003 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℂ)
130126, 127, 129, 111mulcand 11608 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑦) = 1))
13187fveq2d 6778 . . . . . . . . . . . 12 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = (abs‘𝐴))
132101, 105absmuld 15166 . . . . . . . . . . . 12 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = ((abs‘𝑥) · (abs‘𝑦)))
13377ad2antrr 723 . . . . . . . . . . . 12 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝐴) = 𝐴)
134131, 132, 1333eqtr3d 2786 . . . . . . . . . . 11 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · (abs‘𝑦)) = 𝐴)
135129mulid1d 10992 . . . . . . . . . . 11 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · 1) = (abs‘𝑥))
136134, 135eqeq12d 2754 . . . . . . . . . 10 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ 𝐴 = (abs‘𝑥)))
137 eqcom 2745 . . . . . . . . . 10 (𝐴 = (abs‘𝑥) ↔ (abs‘𝑥) = 𝐴)
138136, 137bitrdi 287 . . . . . . . . 9 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑥) = 𝐴))
139124, 130, 1383bitr2d 307 . . . . . . . 8 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑦 ∈ (Unit‘ℤring) ↔ (abs‘𝑥) = 𝐴))
140123, 139orbi12d 916 . . . . . . 7 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((𝑥 ∈ (Unit‘ℤring) ∨ 𝑦 ∈ (Unit‘ℤring)) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))
141120, 140mpbird 256 . . . . . 6 (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring) ∨ 𝑦 ∈ (Unit‘ℤring)))
142141ex 413 . . . . 5 ((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring) ∨ 𝑦 ∈ (Unit‘ℤring))))
143142ralrimivva 3123 . . . 4 (𝐴 ∈ ℙ → ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring) ∨ 𝑦 ∈ (Unit‘ℤring))))
14425, 26, 2, 27isirred2 19943 . . . 4 (𝐴𝐼 ↔ (𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈ (Unit‘ℤring) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring) ∨ 𝑦 ∈ (Unit‘ℤring)))))
14571, 84, 143, 144syl3anbrc 1342 . . 3 (𝐴 ∈ ℙ → 𝐴𝐼)
146145adantl 482 . 2 ((𝐴 ∈ ℕ ∧ 𝐴 ∈ ℙ) → 𝐴𝐼)
14770, 146impbida 798 1 (𝐴 ∈ ℕ → (𝐴𝐼𝐴 ∈ ℙ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1539  wcel 2106  wne 2943  wral 3064   class class class wbr 5074  cfv 6433  (class class class)co 7275  cc 10869  cr 10870  0cc0 10871  1c1 10872   · cmul 10876   < clt 11009  cle 11010   / cdiv 11632  cn 11973  2c2 12028  0cn0 12233  cz 12319  cuz 12582  abscabs 14945  cdvds 15963  cprime 16376  Ringcrg 19783  Unitcui 19881  Irredcir 19882  ringczring 20670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-tpos 8042  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-rp 12731  df-fz 13240  df-seq 13722  df-exp 13783  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-dvds 15964  df-prm 16377  df-gz 16631  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-0g 17152  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-grp 18580  df-minusg 18581  df-subg 18752  df-cmn 19388  df-mgp 19721  df-ur 19738  df-ring 19785  df-cring 19786  df-oppr 19862  df-dvdsr 19883  df-unit 19884  df-irred 19885  df-invr 19914  df-dvr 19925  df-drng 19993  df-subrg 20022  df-cnfld 20598  df-zring 20671
This theorem is referenced by:  dfprm2  20695  prmirred  20696
  Copyright terms: Public domain W3C validator