Theorem asinlem2

Description: The argument to the logarithm in df-asin has the property that replacing A with -u A in the expression gives the reciprocal. (Contributed by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Assertion	asinlem2	$$⊢A\in ℂ\to \left(\mathrm{i}A+\sqrt{1-A^2}\right)\left(\mathrm{i}\left(-A\right)+\sqrt{1-{\left(-A\right)}^2}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
3	1 2	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
4		ax-1cn	$$⊢1\in ℂ$$
5		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
6		subcl	$$⊢\left(1\in ℂ\wedge A^2\in ℂ\right)\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	addcomd	$$⊢A\in ℂ\to \mathrm{i}A+\sqrt{1-A^2}=\sqrt{1-A^2}+\mathrm{i}A$$
10		mulneg2	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
11	1 10	mpan	$$⊢A\in ℂ\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
12		sqneg	$$⊢A\in ℂ\to {\left(-A\right)}^2=A^2$$
13	12	oveq2d	$$⊢A\in ℂ\to 1-{\left(-A\right)}^2=1-A^2$$
14	13	fveq2d	$$⊢A\in ℂ\to \sqrt{1-{\left(-A\right)}^2}=\sqrt{1-A^2}$$
15	11 14	oveq12d	$$⊢A\in ℂ\to \mathrm{i}\left(-A\right)+\sqrt{1-{\left(-A\right)}^2}=-\mathrm{i}A+\sqrt{1-A^2}$$
16	3	negcld	$$⊢A\in ℂ\to -\mathrm{i}A\in ℂ$$
17	16 8	addcomd	$$⊢A\in ℂ\to -\mathrm{i}A+\sqrt{1-A^2}=\sqrt{1-A^2}+\left(-\mathrm{i}A\right)$$
18	8 3	negsubd	$$⊢A\in ℂ\to \sqrt{1-A^2}+\left(-\mathrm{i}A\right)=\sqrt{1-A^2}-\mathrm{i}A$$
19	15 17 18	3eqtrd	$$⊢A\in ℂ\to \mathrm{i}\left(-A\right)+\sqrt{1-{\left(-A\right)}^2}=\sqrt{1-A^2}-\mathrm{i}A$$
20	9 19	oveq12d	$$⊢A\in ℂ\to \left(\mathrm{i}A+\sqrt{1-A^2}\right)\left(\mathrm{i}\left(-A\right)+\sqrt{1-{\left(-A\right)}^2}\right)=\left(\sqrt{1-A^2}+\mathrm{i}A\right)\left(\sqrt{1-A^2}-\mathrm{i}A\right)$$
21	7	sqsqrtd	$$⊢A\in ℂ\to {\sqrt{1-A^2}}^2=1-A^2$$
22		sqmul	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
23	1 22	mpan	$$⊢A\in ℂ\to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
24		i2	$$⊢{\mathrm{i}}^2=-1$$
25	24	oveq1i	$$⊢{\mathrm{i}}^2{A}^2=-1A^2$$
26	5	mulm1d	$$⊢A\in ℂ\to -1A^2=-A^2$$
27	25 26	eqtrid	$$⊢A\in ℂ\to {\mathrm{i}}^2{A}^2=-A^2$$
28	23 27	eqtrd	$$⊢A\in ℂ\to {\mathrm{i}A}^2=-A^2$$
29	21 28	oveq12d	$$⊢A\in ℂ\to {\sqrt{1-A^2}}^2-{\mathrm{i}A}^2=1-A^2-\left(-A^2\right)$$
30		subsq	$$⊢\left(\sqrt{1-A^2}\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to {\sqrt{1-A^2}}^2-{\mathrm{i}A}^2=\left(\sqrt{1-A^2}+\mathrm{i}A\right)\left(\sqrt{1-A^2}-\mathrm{i}A\right)$$
31	8 3 30	syl2anc	$$⊢A\in ℂ\to {\sqrt{1-A^2}}^2-{\mathrm{i}A}^2=\left(\sqrt{1-A^2}+\mathrm{i}A\right)\left(\sqrt{1-A^2}-\mathrm{i}A\right)$$
32	7 5	subnegd	$$⊢A\in ℂ\to 1-A^2-\left(-A^2\right)=1-A^2+A^2$$
33	29 31 32	3eqtr3d	$$⊢A\in ℂ\to \left(\sqrt{1-A^2}+\mathrm{i}A\right)\left(\sqrt{1-A^2}-\mathrm{i}A\right)=1-A^2+A^2$$
34		npcan	$$⊢\left(1\in ℂ\wedge A^2\in ℂ\right)\to 1-A^2+A^2=1$$
35	4 5 34	sylancr	$$⊢A\in ℂ\to 1-A^2+A^2=1$$
36	20 33 35	3eqtrd	$$⊢A\in ℂ\to \left(\mathrm{i}A+\sqrt{1-A^2}\right)\left(\mathrm{i}\left(-A\right)+\sqrt{1-{\left(-A\right)}^2}\right)=1$$