Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Saveliy Skresanov
Ceva's theorem
sigarim
Next ⟩
sigarac
Metamath Proof Explorer
Ascii
Unicode
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
∈
ℝ