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 ) ) ) ) ) )