Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Stefan O'Rear
Algebraic integers I
itgocn
Next ⟩
cnsrexpcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
itgocn
Description:
All integral elements are complex numbers.
(Contributed by
Stefan O'Rear
, 27-Nov-2014)
Ref
Expression
Assertion
itgocn
⊢
IntgOver
⁡
S
⊆
ℂ
Proof
Step
Hyp
Ref
Expression
1
df-itgo
⊢
IntgOver
=
a
∈
𝒫
ℂ
⟼
b
∈
ℂ
|
∃
c
∈
Poly
⁡
a
c
⁡
b
=
0
∧
coeff
⁡
c
⁡
deg
⁡
c
=
1
2
1
dmmptss
⊢
dom
⁡
IntgOver
⊆
𝒫
ℂ
3
2
sseli
⊢
S
∈
dom
⁡
IntgOver
→
S
∈
𝒫
ℂ
4
cnex
⊢
ℂ
∈
V
5
4
elpw2
⊢
S
∈
𝒫
ℂ
↔
S
⊆
ℂ
6
itgoval
⊢
S
⊆
ℂ
→
IntgOver
⁡
S
=
a
∈
ℂ
|
∃
b
∈
Poly
⁡
S
b
⁡
a
=
0
∧
coeff
⁡
b
⁡
deg
⁡
b
=
1
7
ssrab2
⊢
a
∈
ℂ
|
∃
b
∈
Poly
⁡
S
b
⁡
a
=
0
∧
coeff
⁡
b
⁡
deg
⁡
b
=
1
⊆
ℂ
8
6
7
eqsstrdi
⊢
S
⊆
ℂ
→
IntgOver
⁡
S
⊆
ℂ
9
5
8
sylbi
⊢
S
∈
𝒫
ℂ
→
IntgOver
⁡
S
⊆
ℂ
10
3
9
syl
⊢
S
∈
dom
⁡
IntgOver
→
IntgOver
⁡
S
⊆
ℂ
11
ndmfv
⊢
¬
S
∈
dom
⁡
IntgOver
→
IntgOver
⁡
S
=
∅
12
0ss
⊢
∅
⊆
ℂ
13
11
12
eqsstrdi
⊢
¬
S
∈
dom
⁡
IntgOver
→
IntgOver
⁡
S
⊆
ℂ
14
10
13
pm2.61i
⊢
IntgOver
⁡
S
⊆
ℂ