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 i A + 1 A 2 0

Proof

Step Hyp Ref Expression
1 ax-icn i
2 mulcl i A i A
3 1 2 mpan A i A
4 ax-1cn 1
5 sqcl A A 2
6 subcl 1 A 2 1 A 2
7 4 5 6 sylancr A 1 A 2
8 7 sqrtcld A 1 A 2
9 3 8 subnegd A i A 1 A 2 = i A + 1 A 2
10 8 negcld A 1 A 2
11 0ne1 0 1
12 0cnd A 0
13 1cnd A 1
14 subcan2 0 1 A 2 0 A 2 = 1 A 2 0 = 1
15 14 necon3bid 0 1 A 2 0 A 2 1 A 2 0 1
16 12 13 5 15 syl3anc A 0 A 2 1 A 2 0 1
17 11 16 mpbiri A 0 A 2 1 A 2
18 sqmul i A i A 2 = i 2 A 2
19 1 18 mpan A i A 2 = i 2 A 2
20 i2 i 2 = 1
21 20 oveq1i i 2 A 2 = -1 A 2
22 5 mulm1d A -1 A 2 = A 2
23 21 22 syl5eq A i 2 A 2 = A 2
24 19 23 eqtrd A i A 2 = A 2
25 df-neg A 2 = 0 A 2
26 24 25 syl6eq A i A 2 = 0 A 2
27 sqneg 1 A 2 1 A 2 2 = 1 A 2 2
28 8 27 syl A 1 A 2 2 = 1 A 2 2
29 7 sqsqrtd A 1 A 2 2 = 1 A 2
30 28 29 eqtrd A 1 A 2 2 = 1 A 2
31 17 26 30 3netr4d A i A 2 1 A 2 2
32 oveq1 i A = 1 A 2 i A 2 = 1 A 2 2
33 32 necon3i i A 2 1 A 2 2 i A 1 A 2
34 31 33 syl A i A 1 A 2
35 3 10 34 subne0d A i A 1 A 2 0
36 9 35 eqnetrrd A i A + 1 A 2 0