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

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	addcomd	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) )
10		mulneg2	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
11	1 10	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
12		sqneg	⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
13	12	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( 1 − ( - 𝐴 ↑ 2 ) ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
14	13	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
15	11 14	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) = ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
16	3	negcld	⊢ ( 𝐴 ∈ ℂ → - ( i · 𝐴 ) ∈ ℂ )
17	16 8	addcomd	⊢ ( 𝐴 ∈ ℂ → ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + - ( i · 𝐴 ) ) )
18	8 3	negsubd	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + - ( i · 𝐴 ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) )
19	15 17 18	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) = ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) )
20	9 19	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) · ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) ) )
21	7	sqsqrtd	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
22		sqmul	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
23	1 22	mpan	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
24		i2	⊢ ( i ↑ 2 ) = - 1
25	24	oveq1i	⊢ ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
26	5	mulm1d	⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
27	25 26	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
28	23 27	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
29	21 28	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 1 − ( 𝐴 ↑ 2 ) ) − - ( 𝐴 ↑ 2 ) ) )
30		subsq	⊢ ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) · ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) ) )
31	8 3 30	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) · ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) ) )
32	7 5	subnegd	⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( 𝐴 ↑ 2 ) ) − - ( 𝐴 ↑ 2 ) ) = ( ( 1 − ( 𝐴 ↑ 2 ) ) + ( 𝐴 ↑ 2 ) ) )
33	29 31 32	3eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) + ( i · 𝐴 ) ) · ( ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) − ( i · 𝐴 ) ) ) = ( ( 1 − ( 𝐴 ↑ 2 ) ) + ( 𝐴 ↑ 2 ) ) )
34		npcan	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 1 − ( 𝐴 ↑ 2 ) ) + ( 𝐴 ↑ 2 ) ) = 1 )
35	4 5 34	sylancr	⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( 𝐴 ↑ 2 ) ) + ( 𝐴 ↑ 2 ) ) = 1 )
36	20 33 35	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = 1 )