acoscos

Description: The arccosine function is an inverse to cos . (Contributed by Mario Carneiro, 2-Apr-2015)

		Ref	Expression
	Assertion	acoscos	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to arccos (\cos A) = A$

Proof

Step	Hyp	Ref	Expression
1		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
2	1	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to \cos A \in ℂ$
3		acosval	$⊢ \cos A \in ℂ \to arccos (\cos A) = (\frac{π}{2}) - arcsin (\cos A)$
4	2 3	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to arccos (\cos A) = (\frac{π}{2}) - arcsin (\cos A)$
5		picn	$⊢ π \in ℂ$
6		halfcl	$⊢ π \in ℂ \to \frac{π}{2} \in ℂ$
7	5 6	ax-mp	$⊢ \frac{π}{2} \in ℂ$
8		simpl	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to A \in ℂ$
9		nncan	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) = A$
10	7 8 9	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) = A$
11	10	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to \cos ((\frac{π}{2}) - ((\frac{π}{2}) - A)) = \cos A$
12		subcl	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ) \to (\frac{π}{2}) - A \in ℂ$
13	7 8 12	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - A \in ℂ$
14		coshalfpim	$⊢ (\frac{π}{2}) - A \in ℂ \to \cos ((\frac{π}{2}) - ((\frac{π}{2}) - A)) = \sin ((\frac{π}{2}) - A)$
15	13 14	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to \cos ((\frac{π}{2}) - ((\frac{π}{2}) - A)) = \sin ((\frac{π}{2}) - A)$
16	11 15	eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to \cos A = \sin ((\frac{π}{2}) - A)$
17	16	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to arcsin (\cos A) = arcsin (\sin ((\frac{π}{2}) - A))$
18		halfpire	$⊢ \frac{π}{2} \in ℝ$
19	18	recni	$⊢ \frac{π}{2} \in ℂ$
20		resub	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ) \to ℜ ((\frac{π}{2}) - A) = ℜ (\frac{π}{2}) - ℜ (A)$
21	19 8 20	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ℜ ((\frac{π}{2}) - A) = ℜ (\frac{π}{2}) - ℜ (A)$
22		rere	$⊢ \frac{π}{2} \in ℝ \to ℜ (\frac{π}{2}) = \frac{π}{2}$
23	18 22	ax-mp	$⊢ ℜ (\frac{π}{2}) = \frac{π}{2}$
24	23	oveq1i	$⊢ ℜ (\frac{π}{2}) - ℜ (A) = (\frac{π}{2}) - ℜ (A)$
25	21 24	eqtrdi	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ℜ ((\frac{π}{2}) - A) = (\frac{π}{2}) - ℜ (A)$
26		recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$
27	26	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ℜ (A) \in ℝ$
28		resubcl	$⊢ (\frac{π}{2} \in ℝ \land ℜ (A) \in ℝ) \to (\frac{π}{2}) - ℜ (A) \in ℝ$
29	18 27 28	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - ℜ (A) \in ℝ$
30	18	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to \frac{π}{2} \in ℝ$
31		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
32	31	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to - \frac{π}{2} \in ℝ$
33		eliooord	$⊢ ℜ (A) \in (0, π) \to (0 < ℜ (A) \land ℜ (A) < π)$
34	33	adantl	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (0 < ℜ (A) \land ℜ (A) < π)$
35	34	simprd	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ℜ (A) < π$
36	19 19	subnegi	$⊢ (\frac{π}{2}) - (- \frac{π}{2}) = (\frac{π}{2}) + (\frac{π}{2})$
37		pidiv2halves	$⊢ (\frac{π}{2}) + (\frac{π}{2}) = π$
38	36 37	eqtri	$⊢ (\frac{π}{2}) - (- \frac{π}{2}) = π$
39	35 38	breqtrrdi	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ℜ (A) < (\frac{π}{2}) - (- \frac{π}{2})$
40	27 30 32 39	ltsub13d	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to - \frac{π}{2} < (\frac{π}{2}) - ℜ (A)$
41	34	simpld	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to 0 < ℜ (A)$
42		ltsubpos	$⊢ (ℜ (A) \in ℝ \land \frac{π}{2} \in ℝ) \to (0 < ℜ (A) \leftrightarrow (\frac{π}{2}) - ℜ (A) < \frac{π}{2})$
43	27 18 42	sylancl	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (0 < ℜ (A) \leftrightarrow (\frac{π}{2}) - ℜ (A) < \frac{π}{2})$
44	41 43	mpbid	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - ℜ (A) < \frac{π}{2}$
45	31	rexri	$⊢ - \frac{π}{2} \in ℝ^{*}$
46	18	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
47		elioo2	$⊢ (- \frac{π}{2} \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to ((\frac{π}{2}) - ℜ (A) \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow ((\frac{π}{2}) - ℜ (A) \in ℝ \land - \frac{π}{2} < (\frac{π}{2}) - ℜ (A) \land (\frac{π}{2}) - ℜ (A) < \frac{π}{2}))$
48	45 46 47	mp2an	$⊢ (\frac{π}{2}) - ℜ (A) \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow ((\frac{π}{2}) - ℜ (A) \in ℝ \land - \frac{π}{2} < (\frac{π}{2}) - ℜ (A) \land (\frac{π}{2}) - ℜ (A) < \frac{π}{2})$
49	29 40 44 48	syl3anbrc	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})$
50	25 49	eqeltrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ℜ ((\frac{π}{2}) - A) \in (- \frac{π}{2}, \frac{π}{2})$
51		asinsin	$⊢ ((\frac{π}{2}) - A \in ℂ \land ℜ ((\frac{π}{2}) - A) \in (- \frac{π}{2}, \frac{π}{2})) \to arcsin (\sin ((\frac{π}{2}) - A)) = (\frac{π}{2}) - A$
52	13 50 51	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to arcsin (\sin ((\frac{π}{2}) - A)) = (\frac{π}{2}) - A$
53	17 52	eqtr2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - A = arcsin (\cos A)$
54		asincl	$⊢ \cos A \in ℂ \to arcsin (\cos A) \in ℂ$
55	2 54	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to arcsin (\cos A) \in ℂ$
56		subsub23	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ \land arcsin (\cos A) \in ℂ) \to ((\frac{π}{2}) - A = arcsin (\cos A) \leftrightarrow (\frac{π}{2}) - arcsin (\cos A) = A)$
57	19 8 55 56	mp3an2i	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to ((\frac{π}{2}) - A = arcsin (\cos A) \leftrightarrow (\frac{π}{2}) - arcsin (\cos A) = A)$
58	53 57	mpbid	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to (\frac{π}{2}) - arcsin (\cos A) = A$
59	4 58	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, π)) \to arccos (\cos A) = A$

Metamath Proof Explorer

Theorem acoscos

Proof