reasinsin

Description: The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015)

		Ref	Expression
	Assertion	reasinsin	$⊢ A \in [- \frac{π}{2}, \frac{π}{2}] \to arcsin (\sin A) = A$

Proof

Step	Hyp	Ref	Expression
1		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
2	1	rexri	$⊢ - \frac{π}{2} \in ℝ^{*}$
3		halfpire	$⊢ \frac{π}{2} \in ℝ$
4	3	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
5		pirp	$⊢ π \in ℝ^{+}$
6		rphalfcl	$⊢ π \in ℝ^{+} \to \frac{π}{2} \in ℝ^{+}$
7	5 6	ax-mp	$⊢ \frac{π}{2} \in ℝ^{+}$
8		rpgt0	$⊢ \frac{π}{2} \in ℝ^{+} \to 0 < \frac{π}{2}$
9	7 8	ax-mp	$⊢ 0 < \frac{π}{2}$
10		lt0neg2	$⊢ \frac{π}{2} \in ℝ \to (0 < \frac{π}{2} \leftrightarrow - \frac{π}{2} < 0)$
11	3 10	ax-mp	$⊢ 0 < \frac{π}{2} \leftrightarrow - \frac{π}{2} < 0$
12	9 11	mpbi	$⊢ - \frac{π}{2} < 0$
13		0re	$⊢ 0 \in ℝ$
14	1 13 3	lttri	$⊢ (- \frac{π}{2} < 0 \land 0 < \frac{π}{2}) \to - \frac{π}{2} < \frac{π}{2}$
15	12 9 14	mp2an	$⊢ - \frac{π}{2} < \frac{π}{2}$
16	1 3 15	ltleii	$⊢ - \frac{π}{2} \leq \frac{π}{2}$
17		prunioo	$⊢ (- \frac{π}{2} \in ℝ^{} \land \frac{π}{2} \in ℝ^{} \land - \frac{π}{2} \leq \frac{π}{2}) \to (- \frac{π}{2}, \frac{π}{2}) \cup \{- \frac{π}{2}, \frac{π}{2}\} = [- \frac{π}{2}, \frac{π}{2}]$
18	2 4 16 17	mp3an	$⊢ (- \frac{π}{2}, \frac{π}{2}) \cup \{- \frac{π}{2}, \frac{π}{2}\} = [- \frac{π}{2}, \frac{π}{2}]$
19	18	eleq2i	$⊢ A \in ((- \frac{π}{2}, \frac{π}{2}) \cup \{- \frac{π}{2}, \frac{π}{2}\}) \leftrightarrow A \in [- \frac{π}{2}, \frac{π}{2}]$
20		elun	$⊢ A \in ((- \frac{π}{2}, \frac{π}{2}) \cup \{- \frac{π}{2}, \frac{π}{2}\}) \leftrightarrow (A \in (- \frac{π}{2}, \frac{π}{2}) \lor A \in \{- \frac{π}{2}, \frac{π}{2}\})$
21	19 20	bitr3i	$⊢ A \in [- \frac{π}{2}, \frac{π}{2}] \leftrightarrow (A \in (- \frac{π}{2}, \frac{π}{2}) \lor A \in \{- \frac{π}{2}, \frac{π}{2}\})$
22		elioore	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A \in ℝ$
23	22	recnd	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A \in ℂ$
24	22	rered	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to ℜ (A) = A$
25		id	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A \in (- \frac{π}{2}, \frac{π}{2})$
26	24 25	eqeltrd	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})$
27		asinsin	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to arcsin (\sin A) = A$
28	23 26 27	syl2anc	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to arcsin (\sin A) = A$
29		elpri	$⊢ A \in \{- \frac{π}{2}, \frac{π}{2}\} \to (A = - \frac{π}{2} \lor A = \frac{π}{2})$
30		ax-1cn	$⊢ 1 \in ℂ$
31		asinneg	$⊢ 1 \in ℂ \to arcsin (- 1) = - arcsin (1)$
32	30 31	ax-mp	$⊢ arcsin (- 1) = - arcsin (1)$
33		asin1	$⊢ arcsin (1) = \frac{π}{2}$
34	33	negeqi	$⊢ - arcsin (1) = - \frac{π}{2}$
35	32 34	eqtri	$⊢ arcsin (- 1) = - \frac{π}{2}$
36		fveq2	$⊢ A = - \frac{π}{2} \to \sin A = \sin (- \frac{π}{2})$
37	3	recni	$⊢ \frac{π}{2} \in ℂ$
38		sinneg	$⊢ \frac{π}{2} \in ℂ \to \sin (- \frac{π}{2}) = - \sin (\frac{π}{2})$
39	37 38	ax-mp	$⊢ \sin (- \frac{π}{2}) = - \sin (\frac{π}{2})$
40		sinhalfpi	$⊢ \sin (\frac{π}{2}) = 1$
41	40	negeqi	$⊢ - \sin (\frac{π}{2}) = - 1$
42	39 41	eqtri	$⊢ \sin (- \frac{π}{2}) = - 1$
43	36 42	eqtrdi	$⊢ A = - \frac{π}{2} \to \sin A = - 1$
44	43	fveq2d	$⊢ A = - \frac{π}{2} \to arcsin (\sin A) = arcsin (- 1)$
45		id	$⊢ A = - \frac{π}{2} \to A = - \frac{π}{2}$
46	35 44 45	3eqtr4a	$⊢ A = - \frac{π}{2} \to arcsin (\sin A) = A$
47		fveq2	$⊢ A = \frac{π}{2} \to \sin A = \sin (\frac{π}{2})$
48	47 40	eqtrdi	$⊢ A = \frac{π}{2} \to \sin A = 1$
49	48	fveq2d	$⊢ A = \frac{π}{2} \to arcsin (\sin A) = arcsin (1)$
50		id	$⊢ A = \frac{π}{2} \to A = \frac{π}{2}$
51	33 49 50	3eqtr4a	$⊢ A = \frac{π}{2} \to arcsin (\sin A) = A$
52	46 51	jaoi	$⊢ (A = - \frac{π}{2} \lor A = \frac{π}{2}) \to arcsin (\sin A) = A$
53	29 52	syl	$⊢ A \in \{- \frac{π}{2}, \frac{π}{2}\} \to arcsin (\sin A) = A$
54	28 53	jaoi	$⊢ (A \in (- \frac{π}{2}, \frac{π}{2}) \lor A \in \{- \frac{π}{2}, \frac{π}{2}\}) \to arcsin (\sin A) = A$
55	21 54	sylbi	$⊢ A \in [- \frac{π}{2}, \frac{π}{2}] \to arcsin (\sin A) = A$

Metamath Proof Explorer

Theorem reasinsin

Proof