Proof of Theorem zringunit
| Step | Hyp | Ref
| Expression |
| 1 | | zringbas 21464 |
. . . 4
⊢ ℤ =
(Base‘ℤring) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Unit‘ℤring) =
(Unit‘ℤring) |
| 3 | 1, 2 | unitcl 20375 |
. . 3
⊢ (𝐴 ∈
(Unit‘ℤring) → 𝐴 ∈ ℤ) |
| 4 | | zsubrg 21438 |
. . . . . . 7
⊢ ℤ
∈ (SubRing‘ℂfld) |
| 5 | | zgz 16971 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ[i]) |
| 6 | 5 | ssriv 3987 |
. . . . . . 7
⊢ ℤ
⊆ ℤ[i] |
| 7 | | gzsubrg 21439 |
. . . . . . . 8
⊢
ℤ[i] ∈ (SubRing‘ℂfld) |
| 8 | | eqid 2737 |
. . . . . . . . 9
⊢
(ℂfld ↾s ℤ[i]) =
(ℂfld ↾s ℤ[i]) |
| 9 | 8 | subsubrg 20598 |
. . . . . . . 8
⊢
(ℤ[i] ∈ (SubRing‘ℂfld) → (ℤ
∈ (SubRing‘(ℂfld ↾s ℤ[i]))
↔ (ℤ ∈ (SubRing‘ℂfld) ∧ ℤ
⊆ ℤ[i]))) |
| 10 | 7, 9 | ax-mp 5 |
. . . . . . 7
⊢ (ℤ
∈ (SubRing‘(ℂfld ↾s ℤ[i]))
↔ (ℤ ∈ (SubRing‘ℂfld) ∧ ℤ
⊆ ℤ[i])) |
| 11 | 4, 6, 10 | mpbir2an 711 |
. . . . . 6
⊢ ℤ
∈ (SubRing‘(ℂfld ↾s
ℤ[i])) |
| 12 | | df-zring 21458 |
. . . . . . . 8
⊢
ℤring = (ℂfld ↾s
ℤ) |
| 13 | | ressabs 17294 |
. . . . . . . . 9
⊢
((ℤ[i] ∈ (SubRing‘ℂfld) ∧ ℤ
⊆ ℤ[i]) → ((ℂfld ↾s
ℤ[i]) ↾s ℤ) = (ℂfld
↾s ℤ)) |
| 14 | 7, 6, 13 | mp2an 692 |
. . . . . . . 8
⊢
((ℂfld ↾s ℤ[i])
↾s ℤ) = (ℂfld ↾s
ℤ) |
| 15 | 12, 14 | eqtr4i 2768 |
. . . . . . 7
⊢
ℤring = ((ℂfld ↾s
ℤ[i]) ↾s ℤ) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(Unit‘(ℂfld ↾s ℤ[i])) =
(Unit‘(ℂfld ↾s
ℤ[i])) |
| 17 | 15, 16, 2 | subrguss 20587 |
. . . . . 6
⊢ (ℤ
∈ (SubRing‘(ℂfld ↾s ℤ[i]))
→ (Unit‘ℤring) ⊆
(Unit‘(ℂfld ↾s
ℤ[i]))) |
| 18 | 11, 17 | ax-mp 5 |
. . . . 5
⊢
(Unit‘ℤring) ⊆
(Unit‘(ℂfld ↾s
ℤ[i])) |
| 19 | 18 | sseli 3979 |
. . . 4
⊢ (𝐴 ∈
(Unit‘ℤring) → 𝐴 ∈ (Unit‘(ℂfld
↾s ℤ[i]))) |
| 20 | 8 | gzrngunit 21451 |
. . . . 5
⊢ (𝐴 ∈
(Unit‘(ℂfld ↾s ℤ[i])) ↔
(𝐴 ∈ ℤ[i] ∧
(abs‘𝐴) =
1)) |
| 21 | 20 | simprbi 496 |
. . . 4
⊢ (𝐴 ∈
(Unit‘(ℂfld ↾s ℤ[i])) →
(abs‘𝐴) =
1) |
| 22 | 19, 21 | syl 17 |
. . 3
⊢ (𝐴 ∈
(Unit‘ℤring) → (abs‘𝐴) = 1) |
| 23 | 3, 22 | jca 511 |
. 2
⊢ (𝐴 ∈
(Unit‘ℤring) → (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) |
| 24 | | zcn 12618 |
. . . . 5
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
| 25 | 24 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
𝐴 ∈
ℂ) |
| 26 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
(abs‘𝐴) =
1) |
| 27 | | ax-1ne0 11224 |
. . . . . . 7
⊢ 1 ≠
0 |
| 28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) → 1
≠ 0) |
| 29 | 26, 28 | eqnetrd 3008 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
(abs‘𝐴) ≠
0) |
| 30 | | fveq2 6906 |
. . . . . . 7
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
| 31 | | abs0 15324 |
. . . . . . 7
⊢
(abs‘0) = 0 |
| 32 | 30, 31 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
| 33 | 32 | necon3i 2973 |
. . . . 5
⊢
((abs‘𝐴) ≠
0 → 𝐴 ≠
0) |
| 34 | 29, 33 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
𝐴 ≠ 0) |
| 35 | | eldifsn 4786 |
. . . 4
⊢ (𝐴 ∈ (ℂ ∖ {0})
↔ (𝐴 ∈ ℂ
∧ 𝐴 ≠
0)) |
| 36 | 25, 34, 35 | sylanbrc 583 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
𝐴 ∈ (ℂ ∖
{0})) |
| 37 | | simpl 482 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
𝐴 ∈
ℤ) |
| 38 | | cnfldinv 21415 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((invr‘ℂfld)‘𝐴) = (1 / 𝐴)) |
| 39 | 25, 34, 38 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((invr‘ℂfld)‘𝐴) = (1 / 𝐴)) |
| 40 | | zre 12617 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 41 | 40 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
𝐴 ∈
ℝ) |
| 42 | | absresq 15341 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
((abs‘𝐴)↑2) =
(𝐴↑2)) |
| 43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
(𝐴↑2)) |
| 44 | 26 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
(1↑2)) |
| 45 | | sq1 14234 |
. . . . . . . 8
⊢
(1↑2) = 1 |
| 46 | 44, 45 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
1) |
| 47 | 25 | sqvald 14183 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
(𝐴↑2) = (𝐴 · 𝐴)) |
| 48 | 43, 46, 47 | 3eqtr3rd 2786 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
(𝐴 · 𝐴) = 1) |
| 49 | | 1cnd 11256 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) → 1
∈ ℂ) |
| 50 | 49, 25, 25, 34 | divmuld 12065 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((1 / 𝐴) = 𝐴 ↔ (𝐴 · 𝐴) = 1)) |
| 51 | 48, 50 | mpbird 257 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
(1 / 𝐴) = 𝐴) |
| 52 | 39, 51 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((invr‘ℂfld)‘𝐴) = 𝐴) |
| 53 | 52, 37 | eqeltrd 2841 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
((invr‘ℂfld)‘𝐴) ∈ ℤ) |
| 54 | | cnfldbas 21368 |
. . . . . 6
⊢ ℂ =
(Base‘ℂfld) |
| 55 | | cnfld0 21405 |
. . . . . 6
⊢ 0 =
(0g‘ℂfld) |
| 56 | | cndrng 21411 |
. . . . . 6
⊢
ℂfld ∈ DivRing |
| 57 | 54, 55, 56 | drngui 20735 |
. . . . 5
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
| 58 | | eqid 2737 |
. . . . 5
⊢
(invr‘ℂfld) =
(invr‘ℂfld) |
| 59 | 12, 57, 2, 58 | subrgunit 20590 |
. . . 4
⊢ (ℤ
∈ (SubRing‘ℂfld) → (𝐴 ∈ (Unit‘ℤring)
↔ (𝐴 ∈ (ℂ
∖ {0}) ∧ 𝐴 ∈
ℤ ∧ ((invr‘ℂfld)‘𝐴) ∈
ℤ))) |
| 60 | 4, 59 | ax-mp 5 |
. . 3
⊢ (𝐴 ∈
(Unit‘ℤring) ↔ (𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐴 ∈ ℤ ∧
((invr‘ℂfld)‘𝐴) ∈ ℤ)) |
| 61 | 36, 37, 53, 60 | syl3anbrc 1344 |
. 2
⊢ ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) →
𝐴 ∈
(Unit‘ℤring)) |
| 62 | 23, 61 | impbii 209 |
1
⊢ (𝐴 ∈
(Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) |