asinneg

Description: The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015)

		Ref	Expression
	Assertion	asinneg	$⊢ A \in ℂ \to arcsin (- A) = - arcsin (A)$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
3	1 2	mpan	$⊢ A \in ℂ \to i A \in ℂ$
4		ax-1cn	$⊢ 1 \in ℂ$
5		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
6		subcl	$⊢ (1 \in ℂ \land A^{2} \in ℂ) \to 1 - A^{2} \in ℂ$
7	4 5 6	sylancr	$⊢ A \in ℂ \to 1 - A^{2} \in ℂ$
8	7	sqrtcld	$⊢ A \in ℂ \to \sqrt{1 - A^{2}} \in ℂ$
9	3 8	addcld	$⊢ A \in ℂ \to i A + \sqrt{1 - A^{2}} \in ℂ$
10		asinlem	$⊢ A \in ℂ \to i A + \sqrt{1 - A^{2}} \neq 0$
11	9 10	logcld	$⊢ A \in ℂ \to \log (i A + \sqrt{1 - A^{2}}) \in ℂ$
12		efneg	$⊢ \log (i A + \sqrt{1 - A^{2}}) \in ℂ \to e^{- \log (i A + \sqrt{1 - A^{2}})} = \frac{1}{e^{\log (i A + \sqrt{1 - A^{2}})}}$
13	11 12	syl	$⊢ A \in ℂ \to e^{- \log (i A + \sqrt{1 - A^{2}})} = \frac{1}{e^{\log (i A + \sqrt{1 - A^{2}})}}$
14		eflog	$⊢ (i A + \sqrt{1 - A^{2}} \in ℂ \land i A + \sqrt{1 - A^{2}} \neq 0) \to e^{\log (i A + \sqrt{1 - A^{2}})} = i A + \sqrt{1 - A^{2}}$
15	9 10 14	syl2anc	$⊢ A \in ℂ \to e^{\log (i A + \sqrt{1 - A^{2}})} = i A + \sqrt{1 - A^{2}}$
16	15	oveq2d	$⊢ A \in ℂ \to \frac{1}{e^{\log (i A + \sqrt{1 - A^{2}})}} = \frac{1}{i A + \sqrt{1 - A^{2}}}$
17		asinlem2	$⊢ A \in ℂ \to (i A + \sqrt{1 - A^{2}}) (i (- A) + \sqrt{1 - {(- A)}^{2}}) = 1$
18	4	a1i	$⊢ A \in ℂ \to 1 \in ℂ$
19		negcl	$⊢ A \in ℂ \to - A \in ℂ$
20		mulcl	$⊢ (i \in ℂ \land - A \in ℂ) \to i (- A) \in ℂ$
21	1 19 20	sylancr	$⊢ A \in ℂ \to i (- A) \in ℂ$
22	19	sqcld	$⊢ A \in ℂ \to {(- A)}^{2} \in ℂ$
23		subcl	$⊢ (1 \in ℂ \land {(- A)}^{2} \in ℂ) \to 1 - {(- A)}^{2} \in ℂ$
24	4 22 23	sylancr	$⊢ A \in ℂ \to 1 - {(- A)}^{2} \in ℂ$
25	24	sqrtcld	$⊢ A \in ℂ \to \sqrt{1 - {(- A)}^{2}} \in ℂ$
26	21 25	addcld	$⊢ A \in ℂ \to i (- A) + \sqrt{1 - {(- A)}^{2}} \in ℂ$
27	18 9 26 10	divmuld	$⊢ A \in ℂ \to (\frac{1}{i A + \sqrt{1 - A^{2}}} = i (- A) + \sqrt{1 - {(- A)}^{2}} \leftrightarrow (i A + \sqrt{1 - A^{2}}) (i (- A) + \sqrt{1 - {(- A)}^{2}}) = 1)$
28	17 27	mpbird	$⊢ A \in ℂ \to \frac{1}{i A + \sqrt{1 - A^{2}}} = i (- A) + \sqrt{1 - {(- A)}^{2}}$
29	13 16 28	3eqtrd	$⊢ A \in ℂ \to e^{- \log (i A + \sqrt{1 - A^{2}})} = i (- A) + \sqrt{1 - {(- A)}^{2}}$
30		asinlem	$⊢ - A \in ℂ \to i (- A) + \sqrt{1 - {(- A)}^{2}} \neq 0$
31	19 30	syl	$⊢ A \in ℂ \to i (- A) + \sqrt{1 - {(- A)}^{2}} \neq 0$
32	11	negcld	$⊢ A \in ℂ \to - \log (i A + \sqrt{1 - A^{2}}) \in ℂ$
33	11	imnegd	$⊢ A \in ℂ \to ℑ (- \log (i A + \sqrt{1 - A^{2}})) = - ℑ (\log (i A + \sqrt{1 - A^{2}}))$
34	11	imcld	$⊢ A \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ$
35	34	renegcld	$⊢ A \in ℂ \to - ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ$
36		pire	$⊢ π \in ℝ$
37	36	a1i	$⊢ A \in ℂ \to π \in ℝ$
38	9 10	logimcld	$⊢ A \in ℂ \to (- π < ℑ (\log (i A + \sqrt{1 - A^{2}})) \land ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π)$
39	38	simprd	$⊢ A \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π$
40	9	renegd	$⊢ A \in ℂ \to ℜ (- (i A + \sqrt{1 - A^{2}})) = - ℜ (i A + \sqrt{1 - A^{2}})$
41		asinlem3	$⊢ A \in ℂ \to 0 \leq ℜ (i A + \sqrt{1 - A^{2}})$
42	9	recld	$⊢ A \in ℂ \to ℜ (i A + \sqrt{1 - A^{2}}) \in ℝ$
43	42	le0neg2d	$⊢ A \in ℂ \to (0 \leq ℜ (i A + \sqrt{1 - A^{2}}) \leftrightarrow - ℜ (i A + \sqrt{1 - A^{2}}) \leq 0)$
44	41 43	mpbid	$⊢ A \in ℂ \to - ℜ (i A + \sqrt{1 - A^{2}}) \leq 0$
45	40 44	eqbrtrd	$⊢ A \in ℂ \to ℜ (- (i A + \sqrt{1 - A^{2}})) \leq 0$
46	9	negcld	$⊢ A \in ℂ \to - (i A + \sqrt{1 - A^{2}}) \in ℂ$
47	46	recld	$⊢ A \in ℂ \to ℜ (- (i A + \sqrt{1 - A^{2}})) \in ℝ$
48		0re	$⊢ 0 \in ℝ$
49		lenlt	$⊢ (ℜ (- (i A + \sqrt{1 - A^{2}})) \in ℝ \land 0 \in ℝ) \to (ℜ (- (i A + \sqrt{1 - A^{2}})) \leq 0 \leftrightarrow \neg 0 < ℜ (- (i A + \sqrt{1 - A^{2}})))$
50	47 48 49	sylancl	$⊢ A \in ℂ \to (ℜ (- (i A + \sqrt{1 - A^{2}})) \leq 0 \leftrightarrow \neg 0 < ℜ (- (i A + \sqrt{1 - A^{2}})))$
51	45 50	mpbid	$⊢ A \in ℂ \to \neg 0 < ℜ (- (i A + \sqrt{1 - A^{2}}))$
52		lognegb	$⊢ (i A + \sqrt{1 - A^{2}} \in ℂ \land i A + \sqrt{1 - A^{2}} \neq 0) \to (- (i A + \sqrt{1 - A^{2}}) \in ℝ^{+} \leftrightarrow ℑ (\log (i A + \sqrt{1 - A^{2}})) = π)$
53	9 10 52	syl2anc	$⊢ A \in ℂ \to (- (i A + \sqrt{1 - A^{2}}) \in ℝ^{+} \leftrightarrow ℑ (\log (i A + \sqrt{1 - A^{2}})) = π)$
54		rpgt0	$⊢ - (i A + \sqrt{1 - A^{2}}) \in ℝ^{+} \to 0 < - (i A + \sqrt{1 - A^{2}})$
55		rpre	$⊢ - (i A + \sqrt{1 - A^{2}}) \in ℝ^{+} \to - (i A + \sqrt{1 - A^{2}}) \in ℝ$
56	55	rered	$⊢ - (i A + \sqrt{1 - A^{2}}) \in ℝ^{+} \to ℜ (- (i A + \sqrt{1 - A^{2}})) = - (i A + \sqrt{1 - A^{2}})$
57	54 56	breqtrrd	$⊢ - (i A + \sqrt{1 - A^{2}}) \in ℝ^{+} \to 0 < ℜ (- (i A + \sqrt{1 - A^{2}}))$
58	53 57	biimtrrdi	$⊢ A \in ℂ \to (ℑ (\log (i A + \sqrt{1 - A^{2}})) = π \to 0 < ℜ (- (i A + \sqrt{1 - A^{2}})))$
59	58	necon3bd	$⊢ A \in ℂ \to (\neg 0 < ℜ (- (i A + \sqrt{1 - A^{2}})) \to ℑ (\log (i A + \sqrt{1 - A^{2}})) \neq π)$
60	51 59	mpd	$⊢ A \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) \neq π$
61	60	necomd	$⊢ A \in ℂ \to π \neq ℑ (\log (i A + \sqrt{1 - A^{2}}))$
62	34 37 39 61	leneltd	$⊢ A \in ℂ \to ℑ (\log (i A + \sqrt{1 - A^{2}})) < π$
63		ltneg	$⊢ (ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ \land π \in ℝ) \to (ℑ (\log (i A + \sqrt{1 - A^{2}})) < π \leftrightarrow - π < - ℑ (\log (i A + \sqrt{1 - A^{2}})))$
64	34 36 63	sylancl	$⊢ A \in ℂ \to (ℑ (\log (i A + \sqrt{1 - A^{2}})) < π \leftrightarrow - π < - ℑ (\log (i A + \sqrt{1 - A^{2}})))$
65	62 64	mpbid	$⊢ A \in ℂ \to - π < - ℑ (\log (i A + \sqrt{1 - A^{2}}))$
66	38	simpld	$⊢ A \in ℂ \to - π < ℑ (\log (i A + \sqrt{1 - A^{2}}))$
67	36	renegcli	$⊢ - π \in ℝ$
68		ltle	$⊢ (- π \in ℝ \land ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ) \to (- π < ℑ (\log (i A + \sqrt{1 - A^{2}})) \to - π \leq ℑ (\log (i A + \sqrt{1 - A^{2}})))$
69	67 34 68	sylancr	$⊢ A \in ℂ \to (- π < ℑ (\log (i A + \sqrt{1 - A^{2}})) \to - π \leq ℑ (\log (i A + \sqrt{1 - A^{2}})))$
70	66 69	mpd	$⊢ A \in ℂ \to - π \leq ℑ (\log (i A + \sqrt{1 - A^{2}}))$
71		lenegcon1	$⊢ (π \in ℝ \land ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ) \to (- π \leq ℑ (\log (i A + \sqrt{1 - A^{2}})) \leftrightarrow - ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π)$
72	36 34 71	sylancr	$⊢ A \in ℂ \to (- π \leq ℑ (\log (i A + \sqrt{1 - A^{2}})) \leftrightarrow - ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π)$
73	70 72	mpbid	$⊢ A \in ℂ \to - ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π$
74	67	rexri	$⊢ - π \in ℝ^{*}$
75		elioc2	$⊢ (- π \in ℝ^{*} \land π \in ℝ) \to (- ℑ (\log (i A + \sqrt{1 - A^{2}})) \in (- π, π] \leftrightarrow (- ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ \land - π < - ℑ (\log (i A + \sqrt{1 - A^{2}})) \land - ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π))$
76	74 36 75	mp2an	$⊢ - ℑ (\log (i A + \sqrt{1 - A^{2}})) \in (- π, π] \leftrightarrow (- ℑ (\log (i A + \sqrt{1 - A^{2}})) \in ℝ \land - π < - ℑ (\log (i A + \sqrt{1 - A^{2}})) \land - ℑ (\log (i A + \sqrt{1 - A^{2}})) \leq π)$
77	35 65 73 76	syl3anbrc	$⊢ A \in ℂ \to - ℑ (\log (i A + \sqrt{1 - A^{2}})) \in (- π, π]$
78	33 77	eqeltrd	$⊢ A \in ℂ \to ℑ (- \log (i A + \sqrt{1 - A^{2}})) \in (- π, π]$
79		imf	$⊢ ℑ : ℂ ⟶ ℝ$
80		ffn	$⊢ ℑ : ℂ ⟶ ℝ \to ℑ Fn ℂ$
81		elpreima	$⊢ ℑ Fn ℂ \to (- \log (i A + \sqrt{1 - A^{2}}) \in ℑ^{-1} [(- π, π]] \leftrightarrow (- \log (i A + \sqrt{1 - A^{2}}) \in ℂ \land ℑ (- \log (i A + \sqrt{1 - A^{2}})) \in (- π, π]))$
82	79 80 81	mp2b	$⊢ - \log (i A + \sqrt{1 - A^{2}}) \in ℑ^{-1} [(- π, π]] \leftrightarrow (- \log (i A + \sqrt{1 - A^{2}}) \in ℂ \land ℑ (- \log (i A + \sqrt{1 - A^{2}})) \in (- π, π])$
83	32 78 82	sylanbrc	$⊢ A \in ℂ \to - \log (i A + \sqrt{1 - A^{2}}) \in ℑ^{-1} [(- π, π]]$
84		logrn	$⊢ ran log = ℑ^{-1} [(- π, π]]$
85	83 84	eleqtrrdi	$⊢ A \in ℂ \to - \log (i A + \sqrt{1 - A^{2}}) \in ran log$
86		logeftb	$⊢ (i (- A) + \sqrt{1 - {(- A)}^{2}} \in ℂ \land i (- A) + \sqrt{1 - {(- A)}^{2}} \neq 0 \land - \log (i A + \sqrt{1 - A^{2}}) \in ran log) \to (\log (i (- A) + \sqrt{1 - {(- A)}^{2}}) = - \log (i A + \sqrt{1 - A^{2}}) \leftrightarrow e^{- \log (i A + \sqrt{1 - A^{2}})} = i (- A) + \sqrt{1 - {(- A)}^{2}})$
87	26 31 85 86	syl3anc	$⊢ A \in ℂ \to (\log (i (- A) + \sqrt{1 - {(- A)}^{2}}) = - \log (i A + \sqrt{1 - A^{2}}) \leftrightarrow e^{- \log (i A + \sqrt{1 - A^{2}})} = i (- A) + \sqrt{1 - {(- A)}^{2}})$
88	29 87	mpbird	$⊢ A \in ℂ \to \log (i (- A) + \sqrt{1 - {(- A)}^{2}}) = - \log (i A + \sqrt{1 - A^{2}})$
89	88	oveq2d	$⊢ A \in ℂ \to (- i) \log (i (- A) + \sqrt{1 - {(- A)}^{2}}) = (- i) (- \log (i A + \sqrt{1 - A^{2}}))$
90		negicn	$⊢ - i \in ℂ$
91		mulneg2	$⊢ (- i \in ℂ \land \log (i A + \sqrt{1 - A^{2}}) \in ℂ) \to (- i) (- \log (i A + \sqrt{1 - A^{2}})) = - (- i) \log (i A + \sqrt{1 - A^{2}})$
92	90 11 91	sylancr	$⊢ A \in ℂ \to (- i) (- \log (i A + \sqrt{1 - A^{2}})) = - (- i) \log (i A + \sqrt{1 - A^{2}})$
93	89 92	eqtrd	$⊢ A \in ℂ \to (- i) \log (i (- A) + \sqrt{1 - {(- A)}^{2}}) = - (- i) \log (i A + \sqrt{1 - A^{2}})$
94		asinval	$⊢ - A \in ℂ \to arcsin (- A) = (- i) \log (i (- A) + \sqrt{1 - {(- A)}^{2}})$
95	19 94	syl	$⊢ A \in ℂ \to arcsin (- A) = (- i) \log (i (- A) + \sqrt{1 - {(- A)}^{2}})$
96		asinval	$⊢ A \in ℂ \to arcsin (A) = (- i) \log (i A + \sqrt{1 - A^{2}})$
97	96	negeqd	$⊢ A \in ℂ \to - arcsin (A) = - (- i) \log (i A + \sqrt{1 - A^{2}})$
98	93 95 97	3eqtr4d	$⊢ A \in ℂ \to arcsin (- A) = - arcsin (A)$

Metamath Proof Explorer

Theorem asinneg

Proof