Metamath Proof Explorer

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 ⊆ ℂ