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 , y x y
Assertion sigarim A B A G B

Proof

Step Hyp Ref Expression
1 sigar G = x , y x y
2 1 sigarval A B A G B = A B
3 simpl A B A
4 3 cjcld A B A
5 simpr A B B
6 4 5 mulcld A B A B
7 6 imcld A B A B
8 2 7 eqeltrd A B A G B