Theorem asinlem

Description: The argument to the logarithm in df-asin is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	asinlem	$$⊢A\in ℂ\to \mathrm{i}A+\sqrt{1-A^2}\ne 0$$

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	subnegd	$$⊢A\in ℂ\to \mathrm{i}A-\left(-\sqrt{1-A^2}\right)=\mathrm{i}A+\sqrt{1-A^2}$$
10	8	negcld	$$⊢A\in ℂ\to -\sqrt{1-A^2}\in ℂ$$
11		0ne1	$$⊢0\ne 1$$
12		0cnd	$$⊢A\in ℂ\to 0\in ℂ$$
13		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
14		subcan2	$$⊢\left(0\in ℂ\wedge 1\in ℂ\wedge A^2\in ℂ\right)\to \left(0-A^2=1-A^2\leftrightarrow 0=1\right)$$
15	14	necon3bid	$$⊢\left(0\in ℂ\wedge 1\in ℂ\wedge A^2\in ℂ\right)\to \left(0-A^2\ne 1-A^2\leftrightarrow 0\ne 1\right)$$
16	12 13 5 15	syl3anc	$$⊢A\in ℂ\to \left(0-A^2\ne 1-A^2\leftrightarrow 0\ne 1\right)$$
17	11 16	mpbiri	$$⊢A\in ℂ\to 0-A^2\ne 1-A^2$$
18		sqmul	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
19	1 18	mpan	$$⊢A\in ℂ\to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
20		i2	$$⊢{\mathrm{i}}^2=-1$$
21	20	oveq1i	$$⊢{\mathrm{i}}^2{A}^2=-1A^2$$
22	5	mulm1d	$$⊢A\in ℂ\to -1A^2=-A^2$$
23	21 22	syl5eq	$$⊢A\in ℂ\to {\mathrm{i}}^2{A}^2=-A^2$$
24	19 23	eqtrd	$$⊢A\in ℂ\to {\mathrm{i}A}^2=-A^2$$
25		df-neg	$$⊢-A^2=0-A^2$$
26	24 25	eqtrdi	$$⊢A\in ℂ\to {\mathrm{i}A}^2=0-A^2$$
27		sqneg	$$⊢\sqrt{1-A^2}\in ℂ\to {\left(-\sqrt{1-A^2}\right)}^2={\sqrt{1-A^2}}^2$$
28	8 27	syl	$$⊢A\in ℂ\to {\left(-\sqrt{1-A^2}\right)}^2={\sqrt{1-A^2}}^2$$
29	7	sqsqrtd	$$⊢A\in ℂ\to {\sqrt{1-A^2}}^2=1-A^2$$
30	28 29	eqtrd	$$⊢A\in ℂ\to {\left(-\sqrt{1-A^2}\right)}^2=1-A^2$$
31	17 26 30	3netr4d	$$⊢A\in ℂ\to {\mathrm{i}A}^2\ne {\left(-\sqrt{1-A^2}\right)}^2$$
32		oveq1	$$⊢\mathrm{i}A=-\sqrt{1-A^2}\to {\mathrm{i}A}^2={\left(-\sqrt{1-A^2}\right)}^2$$
33	32	necon3i	$$⊢{\mathrm{i}A}^2\ne {\left(-\sqrt{1-A^2}\right)}^2\to \mathrm{i}A\ne -\sqrt{1-A^2}$$
34	31 33	syl	$$⊢A\in ℂ\to \mathrm{i}A\ne -\sqrt{1-A^2}$$
35	3 10 34	subne0d	$$⊢A\in ℂ\to \mathrm{i}A-\left(-\sqrt{1-A^2}\right)\ne 0$$
36	9 35	eqnetrrd	$$⊢A\in ℂ\to \mathrm{i}A+\sqrt{1-A^2}\ne 0$$