itgocn

Description: All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

		Ref	Expression
	Assertion	itgocn	$⊢ IntgOver (S) \subseteq ℂ$

Step	Hyp	Ref	Expression
1		df-itgo	$⊢ IntgOver = (a \in 𝒫 ℂ ⟼ \{b \in ℂ \| \exists c \in Poly (a) (c (b) = 0 \land coeff (c) (\deg (c)) = 1)\})$
2	1	dmmptss	$⊢ dom IntgOver \subseteq 𝒫 ℂ$
3	2	sseli	$⊢ S \in dom IntgOver \to S \in 𝒫 ℂ$
4		cnex	$⊢ ℂ \in V$
5	4	elpw2	$⊢ S \in 𝒫 ℂ \leftrightarrow S \subseteq ℂ$
6		itgoval	$⊢ S \subseteq ℂ \to IntgOver (S) = \{a \in ℂ \| \exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\}$
7		ssrab2	$⊢ \{a \in ℂ \| \exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\} \subseteq ℂ$
8	6 7	eqsstrdi	$⊢ S \subseteq ℂ \to IntgOver (S) \subseteq ℂ$
9	5 8	sylbi	$⊢ S \in 𝒫 ℂ \to IntgOver (S) \subseteq ℂ$
10	3 9	syl	$⊢ S \in dom IntgOver \to IntgOver (S) \subseteq ℂ$
11		ndmfv	$⊢ \neg S \in dom IntgOver \to IntgOver (S) = \emptyset$
12		0ss	$⊢ \emptyset \subseteq ℂ$
13	11 12	eqsstrdi	$⊢ \neg S \in dom IntgOver \to IntgOver (S) \subseteq ℂ$
14	10 13	pm2.61i	$⊢ IntgOver (S) \subseteq ℂ$

Metamath Proof Explorer