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	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
4		ax-1cn	⊢ 1 ∈ ℂ
5		sqcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
6		subcl	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
7	4 5 6	sylancr	⊢ ( 𝐴 ∈ ℂ → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
8	7	sqrtcld	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
9	3 8	subnegd	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) − - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
10	8	negcld	⊢ ( 𝐴 ∈ ℂ → - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
11		0ne1	⊢ 0 ≠ 1
12		0cnd	⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℂ )
13		1cnd	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
14		subcan2	⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 0 − ( 𝐴 ↑ 2 ) ) = ( 1 − ( 𝐴 ↑ 2 ) ) ↔ 0 = 1 ) )
15	14	necon3bid	⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 0 − ( 𝐴 ↑ 2 ) ) ≠ ( 1 − ( 𝐴 ↑ 2 ) ) ↔ 0 ≠ 1 ) )
16	12 13 5 15	syl3anc	⊢ ( 𝐴 ∈ ℂ → ( ( 0 − ( 𝐴 ↑ 2 ) ) ≠ ( 1 − ( 𝐴 ↑ 2 ) ) ↔ 0 ≠ 1 ) )
17	11 16	mpbiri	⊢ ( 𝐴 ∈ ℂ → ( 0 − ( 𝐴 ↑ 2 ) ) ≠ ( 1 − ( 𝐴 ↑ 2 ) ) )
18		sqmul	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
19	1 18	mpan	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
20		i2	⊢ ( i ↑ 2 ) = - 1
21	20	oveq1i	⊢ ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
22	5	mulm1d	⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
23	21 22	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
24	19 23	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
25		df-neg	⊢ - ( 𝐴 ↑ 2 ) = ( 0 − ( 𝐴 ↑ 2 ) )
26	24 25	eqtrdi	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = ( 0 − ( 𝐴 ↑ 2 ) ) )
27		sqneg	⊢ ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ → ( - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) )
28	8 27	syl	⊢ ( 𝐴 ∈ ℂ → ( - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) )
29	7	sqsqrtd	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
30	28 29	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
31	17 26 30	3netr4d	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) ≠ ( - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) )
32		oveq1	⊢ ( ( i · 𝐴 ) = - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) → ( ( i · 𝐴 ) ↑ 2 ) = ( - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) )
33	32	necon3i	⊢ ( ( ( i · 𝐴 ) ↑ 2 ) ≠ ( - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) → ( i · 𝐴 ) ≠ - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
34	31 33	syl	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ≠ - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
35	3 10 34	subne0d	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) − - ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
36	9 35	eqnetrrd	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )