Proof of Theorem prmirred
Step | Hyp | Ref
| Expression |
1 | | prmirred.i |
. . 3
⊢ 𝐼 =
(Irred‘ℤring) |
2 | | zringbas 19643 |
. . 3
⊢ ℤ =
(Base‘ℤring) |
3 | 1, 2 | irredcl 18527 |
. 2
⊢ (𝐴 ∈ 𝐼 → 𝐴 ∈ ℤ) |
4 | | elnn0 11171 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℕ
∨ 𝐴 =
0)) |
5 | | ax-1 6 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
6 | | zringring 19640 |
. . . . . . . . . . 11
⊢
ℤring ∈ Ring |
7 | | zring0 19647 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℤring) |
8 | 1, 7 | irredn0 18526 |
. . . . . . . . . . 11
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ 𝐼) → 𝐴 ≠ 0) |
9 | 6, 8 | mpan 702 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐼 → 𝐴 ≠ 0) |
10 | 9 | necon2bi 2812 |
. . . . . . . . 9
⊢ (𝐴 = 0 → ¬ 𝐴 ∈ 𝐼) |
11 | 10 | pm2.21d 117 |
. . . . . . . 8
⊢ (𝐴 = 0 → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
12 | 5, 11 | jaoi 393 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∨ 𝐴 = 0) → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
13 | 4, 12 | sylbi 206 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ)) |
14 | | prmnn 15226 |
. . . . . . 7
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℕ) |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ ℙ
→ 𝐴 ∈
ℕ)) |
16 | 1 | prmirredlem 19660 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ ℕ
→ (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ))) |
18 | 13, 15, 17 | pm5.21ndd 368 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |
19 | | nn0re 11178 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
20 | | nn0ge0 11195 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
21 | 19, 20 | absidd 14009 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ (abs‘𝐴) =
𝐴) |
22 | 21 | eleq1d 2672 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ ((abs‘𝐴)
∈ ℙ ↔ 𝐴
∈ ℙ)) |
23 | 18, 22 | bitr4d 270 |
. . . 4
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈
ℙ)) |
24 | 23 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈
ℙ)) |
25 | 1 | prmirredlem 19660 |
. . . . . 6
⊢ (-𝐴 ∈ ℕ → (-𝐴 ∈ 𝐼 ↔ -𝐴 ∈ ℙ)) |
26 | 25 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (-𝐴 ∈ 𝐼 ↔ -𝐴 ∈ ℙ)) |
27 | | eqid 2610 |
. . . . . . . . 9
⊢
(invg‘ℤring) =
(invg‘ℤring) |
28 | 1, 27, 2 | irrednegb 18534 |
. . . . . . . 8
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ 𝐼 ↔
((invg‘ℤring)‘𝐴) ∈ 𝐼)) |
29 | 6, 28 | mpan 702 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔
((invg‘ℤring)‘𝐴) ∈ 𝐼)) |
30 | | zsubrg 19618 |
. . . . . . . . . . 11
⊢ ℤ
∈ (SubRing‘ℂfld) |
31 | | subrgsubg 18609 |
. . . . . . . . . . 11
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubGrp‘ℂfld)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ ℤ
∈ (SubGrp‘ℂfld) |
33 | | df-zring 19638 |
. . . . . . . . . . 11
⊢
ℤring = (ℂfld ↾s
ℤ) |
34 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
35 | 33, 34, 27 | subginv 17424 |
. . . . . . . . . 10
⊢ ((ℤ
∈ (SubGrp‘ℂfld) ∧ 𝐴 ∈ ℤ) →
((invg‘ℂfld)‘𝐴) =
((invg‘ℤring)‘𝐴)) |
36 | 32, 35 | mpan 702 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ →
((invg‘ℂfld)‘𝐴) =
((invg‘ℤring)‘𝐴)) |
37 | | zcn 11259 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
38 | | cnfldneg 19591 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((invg‘ℂfld)‘𝐴) = -𝐴) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ →
((invg‘ℂfld)‘𝐴) = -𝐴) |
40 | 36, 39 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ →
((invg‘ℤring)‘𝐴) = -𝐴) |
41 | 40 | eleq1d 2672 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ →
(((invg‘ℤring)‘𝐴) ∈ 𝐼 ↔ -𝐴 ∈ 𝐼)) |
42 | 29, 41 | bitrd 267 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ -𝐴 ∈ 𝐼)) |
43 | 42 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ∈ 𝐼 ↔ -𝐴 ∈ 𝐼)) |
44 | | zre 11258 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
45 | 44 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 𝐴 ∈
ℝ) |
46 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (-𝐴 ∈ ℕ → -𝐴 ∈
ℕ0) |
47 | 46 | nn0ge0d 11231 |
. . . . . . . . 9
⊢ (-𝐴 ∈ ℕ → 0 ≤
-𝐴) |
48 | 47 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 0 ≤
-𝐴) |
49 | 45 | le0neg1d 10478 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
50 | 48, 49 | mpbird 246 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 𝐴 ≤ 0) |
51 | 45, 50 | absnidd 14000 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) →
(abs‘𝐴) = -𝐴) |
52 | 51 | eleq1d 2672 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) →
((abs‘𝐴) ∈
ℙ ↔ -𝐴 ∈
ℙ)) |
53 | 26, 43, 52 | 3bitr4d 299 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ)) |
54 | 53 | adantrl 748 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ -𝐴 ∈ ℕ)) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ)) |
55 | | elznn0nn 11268 |
. . . 4
⊢ (𝐴 ∈ ℤ ↔ (𝐴 ∈ ℕ0 ∨
(𝐴 ∈ ℝ ∧
-𝐴 ∈
ℕ))) |
56 | 55 | biimpi 205 |
. . 3
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ ℕ0 ∨
(𝐴 ∈ ℝ ∧
-𝐴 ∈
ℕ))) |
57 | 24, 54, 56 | mpjaodan 823 |
. 2
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ)) |
58 | 3, 57 | biadan2 672 |
1
⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈
ℙ)) |