Metamath Proof Explorer

Theorem asinlem3a

Description: Lemma for asinlem3 . (Contributed by Mario Carneiro, 1-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
3 2 renegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → - ( ℑ ‘ 𝐴 ) ∈ ℝ )
4 ax-1cn ⊢ 1 ∈ ℂ
5 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
7 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
8 4 6 7 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
9 8 sqrtcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
10 9 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ )
11 1 le0neg1d ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) ≤ 0 ↔ 0 ≤ - ( ℑ ‘ 𝐴 ) ) )
12 11 biimpa ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ - ( ℑ ‘ 𝐴 ) )
13 8 sqrtrege0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
14 3 10 12 13 addge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ ( - ( ℑ ‘ 𝐴 ) + ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
15 ax-icn ⊢ i ∈ ℂ
16 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → 𝐴 ∈ ℂ )
17 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
18 15 16 17 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( i · 𝐴 ) ∈ ℂ )
19 18 9 readdd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( ( ℜ ‘ ( i · 𝐴 ) ) + ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
20 negicn ⊢ - i ∈ ℂ
21 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
22 20 16 21 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( - i · 𝐴 ) ∈ ℂ )
23 22 renegd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ - ( - i · 𝐴 ) ) = - ( ℜ ‘ ( - i · 𝐴 ) ) )
24 15 negnegi ⊢ - - i = i
25 24 oveq1i ⊢ ( - - i · 𝐴 ) = ( i · 𝐴 )
26 mulneg1 ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - - i · 𝐴 ) = - ( - i · 𝐴 ) )
27 20 16 26 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( - - i · 𝐴 ) = - ( - i · 𝐴 ) )
28 25 27 eqtr3id ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( i · 𝐴 ) = - ( - i · 𝐴 ) )
29 28 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ - ( - i · 𝐴 ) ) )
30 imre ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ℜ ‘ ( - i · 𝐴 ) ) )
31 30 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℑ ‘ 𝐴 ) = ( ℜ ‘ ( - i · 𝐴 ) ) )
32 31 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → - ( ℑ ‘ 𝐴 ) = - ( ℜ ‘ ( - i · 𝐴 ) ) )
33 23 29 32 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ ( i · 𝐴 ) ) = - ( ℑ ‘ 𝐴 ) )
34 33 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ( ℜ ‘ ( i · 𝐴 ) ) + ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( - ( ℑ ‘ 𝐴 ) + ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
35 19 34 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( - ( ℑ ‘ 𝐴 ) + ( ℜ ‘ ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
36 14 35 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )