Metamath Proof Explorer

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 syl5eq ⊢ ( 𝐴 ∈ ℂ → ( ( 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 )