asinbnd

Description: The arcsine function has range within a vertical strip of the complex plane with real part between -upi / 2 and pi / 2 . (Contributed by Mario Carneiro, 2-Apr-2015)

		Ref	Expression
	Assertion	asinbnd	$⊢ A \in ℂ \to ℜ (arcsin (A)) \in [- \frac{π}{2}, \frac{π}{2}]$

Proof

Step	Hyp	Ref	Expression
1		asinval	$⊢ A \in ℂ \to arcsin (A) = (- i) \log (i A + \sqrt{1 - A^{2}})$
2	1	fveq2d	$⊢ A \in ℂ \to ℜ (arcsin (A)) = ℜ ((- i) \log (i A + \sqrt{1 - A^{2}}))$
3		ax-icn	$⊢ i \in ℂ$
4		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
5	3 4	mpan	$⊢ A \in ℂ \to i A \in ℂ$
6		ax-1cn	$⊢ 1 \in ℂ$
7		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
8		subcl	$⊢ (1 \in ℂ \land A^{2} \in ℂ) \to 1 - A^{2} \in ℂ$
9	6 7 8	sylancr	$⊢ A \in ℂ \to 1 - A^{2} \in ℂ$
10	9	sqrtcld	$⊢ A \in ℂ \to \sqrt{1 - A^{2}} \in ℂ$
11	5 10	addcld	$⊢ A \in ℂ \to i A + \sqrt{1 - A^{2}} \in ℂ$
12		asinlem	$⊢ A \in ℂ \to i A + \sqrt{1 - A^{2}} \neq 0$
13	11 12	logcld	$⊢ A \in ℂ \to \log (i A + \sqrt{1 - A^{2}}) \in ℂ$
14		imre	$⊢ \log (i A + \sqrt{1 - A^{2}}) \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) = ℜ ((- i) \log (i A + \sqrt{1 - A^{2}}))$
15	13 14	syl	$⊢ A \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) = ℜ ((- i) \log (i A + \sqrt{1 - A^{2}}))$
16	2 15	eqtr4d	$⊢ A \in ℂ \to ℜ (arcsin (A)) = ℑ (\log (i A + \sqrt{1 - A^{2}}))$
17		asinlem3	$⊢ A \in ℂ \to 0 \leq ℜ (i A + \sqrt{1 - A^{2}})$
18		argrege0	$⊢ (i A + \sqrt{1 - A^{2}} \in ℂ \land i A + \sqrt{1 - A^{2}} \neq 0 \land 0 \leq ℜ (i A + \sqrt{1 - A^{2}})) \to ℑ (\log (i A + \sqrt{1 - A^{2}})) \in [- \frac{π}{2}, \frac{π}{2}]$
19	11 12 17 18	syl3anc	$⊢ A \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) \in [- \frac{π}{2}, \frac{π}{2}]$
20	16 19	eqeltrd	$⊢ A \in ℂ \to ℜ (arcsin (A)) \in [- \frac{π}{2}, \frac{π}{2}]$

Metamath Proof Explorer

Theorem asinbnd

Proof