# Metamath Proof Explorer

## 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}↔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}↔0\ne 1\right)$
16 12 13 5 15 syl3anc ${⊢}{A}\in ℂ\to \left(0-{{A}}^{2}\ne 1-{{A}}^{2}↔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}=-1{{A}}^{2}$
22 5 mulm1d ${⊢}{A}\in ℂ\to -1{{A}}^{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 syl6eq ${⊢}{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$