sigarim

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

		Ref	Expression
	Hypothesis	sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
	Assertion	sigarim	$⊢ (A \in ℂ \land B \in ℂ) \to A G B \in ℝ$

Step	Hyp	Ref	Expression
1		sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
2	1	sigarval	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = ℑ (\overline{A} B)$
3		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
4	3	cjcld	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} \in ℂ$
5		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
6	4 5	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} B \in ℂ$
7	6	imcld	$⊢ (A \in ℂ \land B \in ℂ) \to ℑ (\overline{A} B) \in ℝ$
8	2 7	eqeltrd	$⊢ (A \in ℂ \land B \in ℂ) \to A G B \in ℝ$

Metamath Proof Explorer