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