Metamath Proof Explorer

Theorem asinlem3

Description: The argument to the logarithm in df-asin has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion asinlem3 ( 𝐴 ∈ ℂ → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 0red ⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℝ )
2 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
3 ax-icn ⊢ i ∈ ℂ
4 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → - 𝐴 ∈ ℂ )
6 mulcl ⊢ ( ( i ∈ ℂ ∧ - 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) ∈ ℂ )
7 3 5 6 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( i · - 𝐴 ) ∈ ℂ )
8 ax-1cn ⊢ 1 ∈ ℂ
9 5 sqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( - 𝐴 ↑ 2 ) ∈ ℂ )
10 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( - 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( - 𝐴 ↑ 2 ) ) ∈ ℂ )
11 8 9 10 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 1 − ( - 𝐴 ↑ 2 ) ) ∈ ℂ )
12 11 sqrtcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ∈ ℂ )
13 7 12 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
14 asinlem ⊢ ( - 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
15 5 14 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
16 13 15 absrpcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ∈ ℝ+ )
17 2z ⊢ 2 ∈ ℤ
18 rpexpcl ⊢ ( ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ∈ ℝ+ )
19 16 17 18 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ∈ ℝ+ )
20 19 rprecred ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) ∈ ℝ )
21 13 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ )
22 21 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℜ ‘ ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ )
23 19 rpreccld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) ∈ ℝ+ )
24 23 rpge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) )
25 imneg ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ - 𝐴 ) = - ( ℑ ‘ 𝐴 ) )
26 25 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ - 𝐴 ) = - ( ℑ ‘ 𝐴 ) )
27 2 le0neg2d ⊢ ( 𝐴 ∈ ℂ → ( 0 ≤ ( ℑ ‘ 𝐴 ) ↔ - ( ℑ ‘ 𝐴 ) ≤ 0 ) )
28 27 biimpa ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → - ( ℑ ‘ 𝐴 ) ≤ 0 )
29 26 28 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ - 𝐴 ) ≤ 0 )
30 asinlem3a ⊢ ( ( - 𝐴 ∈ ℂ ∧ ( ℑ ‘ - 𝐴 ) ≤ 0 ) → 0 ≤ ( ℜ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) )
31 5 29 30 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) )
32 13 recjd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℜ ‘ ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) = ( ℜ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) )
33 31 32 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) )
34 20 22 24 33 mulge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ℜ ‘ ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) ) )
35 recval ⊢ ( ( ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ≠ 0 ) → ( 1 / ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = ( ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) )
36 13 15 35 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 1 / ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = ( ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) )
37 asinlem2 ⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = 1 )
38 37 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = 1 )
39 38 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 1 = ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) )
40 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 1 ∈ ℂ )
41 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
42 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
43 3 41 42 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( i · 𝐴 ) ∈ ℂ )
44 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
45 44 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
46 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
47 8 45 46 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
48 47 sqrtcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
49 43 48 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
50 40 49 13 15 divmul3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( 1 / ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ↔ 1 = ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) )
51 39 50 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( 1 / ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
52 19 rpcnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ∈ ℂ )
53 19 rpne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ≠ 0 )
54 21 52 53 divrec2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) = ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) )
55 36 51 54 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) = ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) )
56 55 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( ℜ ‘ ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) ) )
57 20 21 remul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) ) = ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ℜ ‘ ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) ) )
58 56 57 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( ( 1 / ( ( abs ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ↑ 2 ) ) · ( ℜ ‘ ( ∗ ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) ) )
59 34 58 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ≤ ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
60 asinlem3a ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
61 1 2 59 60 lecasei ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )