Proof of Theorem prmirred
Step | Hyp | Ref
| Expression |
1 | | prmirred.i |
. . 3
⊢ 𝐼 =
(Irred‘ℤring) |
2 | | zringbas 20395 |
. . 3
⊢ ℤ =
(Base‘ℤring) |
3 | 1, 2 | irredcl 19676 |
. 2
⊢ (𝐴 ∈ 𝐼 → 𝐴 ∈ ℤ) |
4 | | elnn0 12057 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℕ
∨ 𝐴 =
0)) |
5 | | zringring 20392 |
. . . . . . . . . . 11
⊢
ℤring ∈ Ring |
6 | | zring0 20399 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℤring) |
7 | 1, 6 | irredn0 19675 |
. . . . . . . . . . 11
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ 𝐼) → 𝐴 ≠ 0) |
8 | 5, 7 | mpan 690 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐼 → 𝐴 ≠ 0) |
9 | 8 | necon2bi 2962 |
. . . . . . . . 9
⊢ (𝐴 = 0 → ¬ 𝐴 ∈ 𝐼) |
10 | 9 | pm2.21d 121 |
. . . . . . . 8
⊢ (𝐴 = 0 → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
11 | 10 | jao1i 858 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∨ 𝐴 = 0) → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
12 | 4, 11 | sylbi 220 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
13 | | prmnn 16194 |
. . . . . . 7
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℕ) |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ ℙ
→ 𝐴 ∈
ℕ)) |
15 | 1 | prmirredlem 20413 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ ℕ
→ (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ))) |
17 | 12, 14, 16 | pm5.21ndd 384 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |
18 | | nn0re 12064 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
19 | | nn0ge0 12080 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
20 | 18, 19 | absidd 14951 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (abs‘𝐴) =
𝐴) |
21 | 20 | eleq1d 2815 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ ((abs‘𝐴)
∈ ℙ ↔ 𝐴
∈ ℙ)) |
22 | 17, 21 | bitr4d 285 |
. . . 4
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈
ℙ)) |
23 | 22 | adantl 485 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈
ℙ)) |
24 | 1 | prmirredlem 20413 |
. . . . . 6
⊢ (-𝐴 ∈ ℕ → (-𝐴 ∈ 𝐼 ↔ -𝐴 ∈ ℙ)) |
25 | 24 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (-𝐴 ∈ 𝐼 ↔ -𝐴 ∈ ℙ)) |
26 | | eqid 2736 |
. . . . . . . . 9
⊢
(invg‘ℤring) =
(invg‘ℤring) |
27 | 1, 26, 2 | irrednegb 19683 |
. . . . . . . 8
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ 𝐼 ↔
((invg‘ℤring)‘𝐴) ∈ 𝐼)) |
28 | 5, 27 | mpan 690 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔
((invg‘ℤring)‘𝐴) ∈ 𝐼)) |
29 | | zsubrg 20370 |
. . . . . . . . . . 11
⊢ ℤ
∈ (SubRing‘ℂfld) |
30 | | subrgsubg 19760 |
. . . . . . . . . . 11
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubGrp‘ℂfld)) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . 10
⊢ ℤ
∈ (SubGrp‘ℂfld) |
32 | | df-zring 20390 |
. . . . . . . . . . 11
⊢
ℤring = (ℂfld ↾s
ℤ) |
33 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
34 | 32, 33, 26 | subginv 18504 |
. . . . . . . . . 10
⊢ ((ℤ
∈ (SubGrp‘ℂfld) ∧ 𝐴 ∈ ℤ) →
((invg‘ℂfld)‘𝐴) =
((invg‘ℤring)‘𝐴)) |
35 | 31, 34 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ →
((invg‘ℂfld)‘𝐴) =
((invg‘ℤring)‘𝐴)) |
36 | | zcn 12146 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
37 | | cnfldneg 20343 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((invg‘ℂfld)‘𝐴) = -𝐴) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ →
((invg‘ℂfld)‘𝐴) = -𝐴) |
39 | 35, 38 | eqtr3d 2773 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ →
((invg‘ℤring)‘𝐴) = -𝐴) |
40 | 39 | eleq1d 2815 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ →
(((invg‘ℤring)‘𝐴) ∈ 𝐼 ↔ -𝐴 ∈ 𝐼)) |
41 | 28, 40 | bitrd 282 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ -𝐴 ∈ 𝐼)) |
42 | 41 | adantr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ∈ 𝐼 ↔ -𝐴 ∈ 𝐼)) |
43 | | zre 12145 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
44 | 43 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 𝐴 ∈
ℝ) |
45 | | nnnn0 12062 |
. . . . . . . . . 10
⊢ (-𝐴 ∈ ℕ → -𝐴 ∈
ℕ0) |
46 | 45 | nn0ge0d 12118 |
. . . . . . . . 9
⊢ (-𝐴 ∈ ℕ → 0 ≤
-𝐴) |
47 | 46 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 0 ≤
-𝐴) |
48 | 44 | le0neg1d 11368 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
49 | 47, 48 | mpbird 260 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 𝐴 ≤ 0) |
50 | 44, 49 | absnidd 14942 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) →
(abs‘𝐴) = -𝐴) |
51 | 50 | eleq1d 2815 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) →
((abs‘𝐴) ∈
ℙ ↔ -𝐴 ∈
ℙ)) |
52 | 25, 42, 51 | 3bitr4d 314 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ)) |
53 | 52 | adantrl 716 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ -𝐴 ∈ ℕ)) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ)) |
54 | | elznn0nn 12155 |
. . . 4
⊢ (𝐴 ∈ ℤ ↔ (𝐴 ∈ ℕ0 ∨
(𝐴 ∈ ℝ ∧
-𝐴 ∈
ℕ))) |
55 | 54 | biimpi 219 |
. . 3
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ ℕ0 ∨
(𝐴 ∈ ℝ ∧
-𝐴 ∈
ℕ))) |
56 | 23, 53, 55 | mpjaodan 959 |
. 2
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ)) |
57 | 3, 56 | biadanii 822 |
1
⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈
ℙ)) |