Metamath Proof Explorer

Theorem sigarim

Description: Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017)

Ref Expression
Hypothesis sigar 
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
Assertion sigarim 
|- ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. RR )

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 1 sigarval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
3 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
4 3 cjcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` A ) e. CC )
5 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
6 4 5 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) x. B ) e. CC )
7 6 imcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( ( * ` A ) x. B ) ) e. RR )
8 2 7 eqeltrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. RR )