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