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

Theorem sigarmf 37439
 Description: Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
Hypothesis
Ref Expression
sigar
Assertion
Ref Expression
sigarmf
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem sigarmf
StepHypRef Expression
1 cjsub 13131 . . . . . . 7
21oveq1d 6293 . . . . . 6
323adant2 1016 . . . . 5
4 simp1 997 . . . . . . 7
54cjcld 13178 . . . . . 6
6 simp3 999 . . . . . . 7
76cjcld 13178 . . . . . 6
8 simp2 998 . . . . . 6
95, 7, 8subdird 10054 . . . . 5
103, 9eqtrd 2443 . . . 4
1110fveq2d 5853 . . 3
125, 8mulcld 9646 . . . 4
137, 8mulcld 9646 . . . 4
1412, 13imsubd 13199 . . 3
1511, 14eqtrd 2443 . 2
164, 6subcld 9967 . . 3
17 sigar . . . 4
1817sigarval 37435 . . 3
1916, 8, 18syl2anc 659 . 2
2017sigarval 37435 . . . 4