Theorem acosbnd

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

	Ref	Expression
Assertion	acosbnd	$$⊢A\in ℂ\to \Re \left(arccos\left(A\right)\right)\in \left[0,\mathrm{\pi }\right]$$

Proof

Step	Hyp	Ref	Expression
1		acosval	$$⊢A\in ℂ\to arccos\left(A\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)$$
2	1	fveq2d	$$⊢A\in ℂ\to \Re \left(arccos\left(A\right)\right)=\Re \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)$$
3		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
4	3	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
5		asincl	$$⊢A\in ℂ\to arcsin\left(A\right)\in ℂ$$
6		resub	$$⊢\left(\frac{\mathrm{\pi }}{2}\in ℂ\wedge arcsin\left(A\right)\in ℂ\right)\to \Re \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=\Re \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)$$
7	4 5 6	sylancr	$$⊢A\in ℂ\to \Re \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=\Re \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)$$
8		rere	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \Re \left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
9	3 8	ax-mp	$$⊢\Re \left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
10	9	oveq1i	$$⊢\Re \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)=\left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)$$
11	7 10	eqtrdi	$$⊢A\in ℂ\to \Re \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=\left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)$$
12	2 11	eqtrd	$$⊢A\in ℂ\to \Re \left(arccos\left(A\right)\right)=\left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)$$
13	5	recld	$$⊢A\in ℂ\to \Re \left(arcsin\left(A\right)\right)\in ℝ$$
14		resubcl	$$⊢\left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge \Re \left(arcsin\left(A\right)\right)\in ℝ\right)\to \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\in ℝ$$
15	3 13 14	sylancr	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\in ℝ$$
16		asinbnd	$$⊢A\in ℂ\to \Re \left(arcsin\left(A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
17		neghalfpire	$$⊢-\frac{\mathrm{\pi }}{2}\in ℝ$$
18	17 3	elicc2i	$$⊢\Re \left(arcsin\left(A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\leftrightarrow \left(\Re \left(arcsin\left(A\right)\right)\in ℝ\wedge -\frac{\mathrm{\pi }}{2}\le \Re \left(arcsin\left(A\right)\right)\wedge \Re \left(arcsin\left(A\right)\right)\le \frac{\mathrm{\pi }}{2}\right)$$
19	16 18	sylib	$$⊢A\in ℂ\to \left(\Re \left(arcsin\left(A\right)\right)\in ℝ\wedge -\frac{\mathrm{\pi }}{2}\le \Re \left(arcsin\left(A\right)\right)\wedge \Re \left(arcsin\left(A\right)\right)\le \frac{\mathrm{\pi }}{2}\right)$$
20	19	simp3d	$$⊢A\in ℂ\to \Re \left(arcsin\left(A\right)\right)\le \frac{\mathrm{\pi }}{2}$$
21		subge0	$$⊢\left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge \Re \left(arcsin\left(A\right)\right)\in ℝ\right)\to \left(0\le \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\leftrightarrow \Re \left(arcsin\left(A\right)\right)\le \frac{\mathrm{\pi }}{2}\right)$$
22	3 13 21	sylancr	$$⊢A\in ℂ\to \left(0\le \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\leftrightarrow \Re \left(arcsin\left(A\right)\right)\le \frac{\mathrm{\pi }}{2}\right)$$
23	20 22	mpbird	$$⊢A\in ℂ\to 0\le \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)$$
24	3	a1i	$$⊢A\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℝ$$
25		pire	$$⊢\mathrm{\pi }\in ℝ$$
26	25	a1i	$$⊢A\in ℂ\to \mathrm{\pi }\in ℝ$$
27	25	recni	$$⊢\mathrm{\pi }\in ℂ$$
28	17	recni	$$⊢-\frac{\mathrm{\pi }}{2}\in ℂ$$
29	27 4	negsubi	$$⊢\mathrm{\pi }+\left(-\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{2}\right)$$
30		pidiv2halves	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }$$
31	27 4 4 30	subaddrii	$$⊢\mathrm{\pi }-\left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
32	29 31	eqtri	$$⊢\mathrm{\pi }+\left(-\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
33	4 27 28 32	subaddrii	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }=-\frac{\mathrm{\pi }}{2}$$
34	19	simp2d	$$⊢A\in ℂ\to -\frac{\mathrm{\pi }}{2}\le \Re \left(arcsin\left(A\right)\right)$$
35	33 34	eqbrtrid	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }\le \Re \left(arcsin\left(A\right)\right)$$
36	24 26 13 35	subled	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\le \mathrm{\pi }$$
37		0re	$$⊢0\in ℝ$$
38	37 25	elicc2i	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\in \left[0,\mathrm{\pi }\right]\leftrightarrow \left(\left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\in ℝ\wedge 0\le \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\wedge \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\le \mathrm{\pi }\right)$$
39	15 23 36 38	syl3anbrc	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-\Re \left(arcsin\left(A\right)\right)\in \left[0,\mathrm{\pi }\right]$$
40	12 39	eqeltrd	$$⊢A\in ℂ\to \Re \left(arccos\left(A\right)\right)\in \left[0,\mathrm{\pi }\right]$$