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 = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
	sigarimcd.a	|- ( ph -> ( A e. CC /\ B e. CC ) )
Assertion	sigarimcd	|- ( ph -> ( A G B ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		sigarimcd.sigar	|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2		sigarimcd.a	|- ( ph -> ( A e. CC /\ B e. CC ) )
3	1	sigarim	|- ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. RR )
4	3	recnd	|- ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. CC )
5	2 4	syl	|- ( ph -> ( A G B ) e. CC )