Metamath Proof Explorer

Theorem asinlem3a

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

Ref Expression
Assertion asinlem3a ⊢ A ∈ ℂ ∧ ℑ ⁡ A ≤ 0 → 0 ≤ ℜ ⁡ i ⁢ A + 1 − A 2

Proof

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