Mathbox for Saveliy Skresanov < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sigarls Structured version   Unicode version

Theorem sigarls 37899
 Description: Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
Hypothesis
Ref Expression
sigar
Assertion
Ref Expression
sigarls
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem sigarls
StepHypRef Expression
1 simp1 1005 . . . . . 6
21cjcld 13227 . . . . 5
3 simp2 1006 . . . . 5
4 simpr 462 . . . . . . 7
54recnd 9658 . . . . . 6
653adant1 1023 . . . . 5
72, 3, 6mulassd 9655 . . . 4
87fveq2d 5876 . . 3
9 simp3 1007 . . . . 5
102, 3mulcld 9652 . . . . 5
119, 10immul2d 13259 . . . 4
1210, 6mulcomd 9653 . . . . 5
1312fveq2d 5876 . . . 4
14 imcl 13142 . . . . . . 7
1514recnd 9658 . . . . . 6
1610, 15syl 17 . . . . 5
1716, 6mulcomd 9653 . . . 4
1811, 13, 173eqtr4d 2471 . . 3
198, 18eqtr3d 2463 . 2
20 simpl 458 . . . . 5
2120, 5mulcld 9652 . . . 4