Theorem asinlem3a

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

	Ref	Expression
Assertion	asinlem3a	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to 0\le \Re \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Im \left(A\right)\in ℝ$$
3	2	renegcld	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to -\Im \left(A\right)\in ℝ$$
4		ax-1cn	$$⊢1\in ℂ$$
5		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
6	5	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to A^2\in ℂ$$
7		subcl	$$⊢\left(1\in ℂ\wedge A^2\in ℂ\right)\to 1-A^2\in ℂ$$
8	4 6 7	sylancr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to 1-A^2\in ℂ$$
9	8	sqrtcld	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \sqrt{1-A^2}\in ℂ$$
10	9	recld	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(\sqrt{1-A^2}\right)\in ℝ$$
11	1	le0neg1d	$$⊢A\in ℂ\to \left(\Im \left(A\right)\le 0\leftrightarrow 0\le -\Im \left(A\right)\right)$$
12	11	biimpa	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to 0\le -\Im \left(A\right)$$
13	8	sqrtrege0d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to 0\le \Re \left(\sqrt{1-A^2}\right)$$
14	3 10 12 13	addge0d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to 0\le -\Im \left(A\right)+\Re \left(\sqrt{1-A^2}\right)$$
15		ax-icn	$$⊢\mathrm{i}\in ℂ$$
16		simpl	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to A\in ℂ$$
17		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
18	15 16 17	sylancr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \mathrm{i}A\in ℂ$$
19	18 9	readdd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(\mathrm{i}A+\sqrt{1-A^2}\right)=\Re \left(\mathrm{i}A\right)+\Re \left(\sqrt{1-A^2}\right)$$
20		negicn	$$⊢-\mathrm{i}\in ℂ$$
21		mulcl	$$⊢\left(-\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left(-\mathrm{i}\right)A\in ℂ$$
22	20 16 21	sylancr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \left(-\mathrm{i}\right)A\in ℂ$$
23	22	renegd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(-\left(-\mathrm{i}\right)A\right)=-\Re \left(\left(-\mathrm{i}\right)A\right)$$
24	15	negnegi	$$⊢-\left(-\mathrm{i}\right)=\mathrm{i}$$
25	24	oveq1i	$$⊢\left(-\left(-\mathrm{i}\right)\right)A=\mathrm{i}A$$
26		mulneg1	$$⊢\left(-\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left(-\left(-\mathrm{i}\right)\right)A=-\left(-\mathrm{i}\right)A$$
27	20 16 26	sylancr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \left(-\left(-\mathrm{i}\right)\right)A=-\left(-\mathrm{i}\right)A$$
28	25 27	eqtr3id	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \mathrm{i}A=-\left(-\mathrm{i}\right)A$$
29	28	fveq2d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(\mathrm{i}A\right)=\Re \left(-\left(-\mathrm{i}\right)A\right)$$
30		imre	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$
31	30	adantr	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Im \left(A\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$
32	31	negeqd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to -\Im \left(A\right)=-\Re \left(\left(-\mathrm{i}\right)A\right)$$
33	23 29 32	3eqtr4d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(\mathrm{i}A\right)=-\Im \left(A\right)$$
34	33	oveq1d	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(\mathrm{i}A\right)+\Re \left(\sqrt{1-A^2}\right)=-\Im \left(A\right)+\Re \left(\sqrt{1-A^2}\right)$$
35	19 34	eqtrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to \Re \left(\mathrm{i}A+\sqrt{1-A^2}\right)=-\Im \left(A\right)+\Re \left(\sqrt{1-A^2}\right)$$
36	14 35	breqtrrd	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\le 0\right)\to 0\le \Re \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$