Theorem sigarimcd

Description: Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017)

	Ref	Expression
Hypotheses	sigarimcd.sigar	$$⊢G=\left(x\in ℂ,y\in ℂ⟼\Im \left(\bar{x}y\right)\right)$$
	sigarimcd.a	$$⊢\phi \to \left(A\in ℂ\wedge B\in ℂ\right)$$
Assertion	sigarimcd	$$⊢\phi \to AGB\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		sigarimcd.sigar	$$⊢G=\left(x\in ℂ,y\in ℂ⟼\Im \left(\bar{x}y\right)\right)$$
2		sigarimcd.a	$$⊢\phi \to \left(A\in ℂ\wedge B\in ℂ\right)$$
3	1	sigarim	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to AGB\in ℝ$$
4	3	recnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to AGB\in ℂ$$
5	2 4	syl	$$⊢\phi \to AGB\in ℂ$$