asinlem3

Description: The argument to the logarithm in df-asin has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015)

		Ref	Expression
	Assertion	asinlem3	$⊢ A \in ℂ \to 0 \leq ℜ (i A + \sqrt{1 - A^{2}})$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ A \in ℂ \to 0 \in ℝ$
2		imcl	$⊢ A \in ℂ \to ℑ (A) \in ℝ$
3		ax-icn	$⊢ i \in ℂ$
4		negcl	$⊢ A \in ℂ \to - A \in ℂ$
5	4	adantr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to - A \in ℂ$
6		mulcl	$⊢ (i \in ℂ \land - A \in ℂ) \to i (- A) \in ℂ$
7	3 5 6	sylancr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to i (- A) \in ℂ$
8		ax-1cn	$⊢ 1 \in ℂ$
9	5	sqcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to {(- A)}^{2} \in ℂ$
10		subcl	$⊢ (1 \in ℂ \land {(- A)}^{2} \in ℂ) \to 1 - {(- A)}^{2} \in ℂ$
11	8 9 10	sylancr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 1 - {(- A)}^{2} \in ℂ$
12	11	sqrtcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \sqrt{1 - {(- A)}^{2}} \in ℂ$
13	7 12	addcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to i (- A) + \sqrt{1 - {(- A)}^{2}} \in ℂ$
14		asinlem	$⊢ - A \in ℂ \to i (- A) + \sqrt{1 - {(- A)}^{2}} \neq 0$
15	5 14	syl	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to i (- A) + \sqrt{1 - {(- A)}^{2}} \neq 0$
16	13 15	absrpcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \|i (- A) + \sqrt{1 - {(- A)}^{2}}\| \in ℝ^{+}$
17		2z	$⊢ 2 \in ℤ$
18		rpexpcl	$⊢ (\|i (- A) + \sqrt{1 - {(- A)}^{2}}\| \in ℝ^{+} \land 2 \in ℤ) \to {\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2} \in ℝ^{+}$
19	16 17 18	sylancl	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to {\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2} \in ℝ^{+}$
20	19	rprecred	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}} \in ℝ$
21	13	cjcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \overline{i (- A) + \sqrt{1 - {(- A)}^{2}}} \in ℂ$
22	21	recld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℜ (\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}) \in ℝ$
23	19	rpreccld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}} \in ℝ^{+}$
24	23	rpge0d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 0 \leq \frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}$
25		imneg	$⊢ A \in ℂ \to ℑ (- A) = - ℑ (A)$
26	25	adantr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℑ (- A) = - ℑ (A)$
27	2	le0neg2d	$⊢ A \in ℂ \to (0 \leq ℑ (A) \leftrightarrow - ℑ (A) \leq 0)$
28	27	biimpa	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to - ℑ (A) \leq 0$
29	26 28	eqbrtrd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℑ (- A) \leq 0$
30		asinlem3a	$⊢ (- A \in ℂ \land ℑ (- A) \leq 0) \to 0 \leq ℜ (i (- A) + \sqrt{1 - {(- A)}^{2}})$
31	5 29 30	syl2anc	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 0 \leq ℜ (i (- A) + \sqrt{1 - {(- A)}^{2}})$
32	13	recjd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℜ (\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}) = ℜ (i (- A) + \sqrt{1 - {(- A)}^{2}})$
33	31 32	breqtrrd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 0 \leq ℜ (\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}})$
34	20 22 24 33	mulge0d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 0 \leq (\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) ℜ (\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}})$
35		recval	$⊢ (i (- A) + \sqrt{1 - {(- A)}^{2}} \in ℂ \land i (- A) + \sqrt{1 - {(- A)}^{2}} \neq 0) \to \frac{1}{i (- A) + \sqrt{1 - {(- A)}^{2}}} = \frac{\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}$
36	13 15 35	syl2anc	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \frac{1}{i (- A) + \sqrt{1 - {(- A)}^{2}}} = \frac{\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}$
37		asinlem2	$⊢ A \in ℂ \to (i A + \sqrt{1 - A^{2}}) (i (- A) + \sqrt{1 - {(- A)}^{2}}) = 1$
38	37	adantr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to (i A + \sqrt{1 - A^{2}}) (i (- A) + \sqrt{1 - {(- A)}^{2}}) = 1$
39	38	eqcomd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 1 = (i A + \sqrt{1 - A^{2}}) (i (- A) + \sqrt{1 - {(- A)}^{2}})$
40		1cnd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 1 \in ℂ$
41		simpl	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to A \in ℂ$
42		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
43	3 41 42	sylancr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to i A \in ℂ$
44		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
45	44	adantr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to A^{2} \in ℂ$
46		subcl	$⊢ (1 \in ℂ \land A^{2} \in ℂ) \to 1 - A^{2} \in ℂ$
47	8 45 46	sylancr	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 1 - A^{2} \in ℂ$
48	47	sqrtcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \sqrt{1 - A^{2}} \in ℂ$
49	43 48	addcld	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to i A + \sqrt{1 - A^{2}} \in ℂ$
50	40 49 13 15	divmul3d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to (\frac{1}{i (- A) + \sqrt{1 - {(- A)}^{2}}} = i A + \sqrt{1 - A^{2}} \leftrightarrow 1 = (i A + \sqrt{1 - A^{2}}) (i (- A) + \sqrt{1 - {(- A)}^{2}}))$
51	39 50	mpbird	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \frac{1}{i (- A) + \sqrt{1 - {(- A)}^{2}}} = i A + \sqrt{1 - A^{2}}$
52	19	rpcnd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to {\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2} \in ℂ$
53	19	rpne0d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to {\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2} \neq 0$
54	21 52 53	divrec2d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to \frac{\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}} = (\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) \overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}$
55	36 51 54	3eqtr3d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to i A + \sqrt{1 - A^{2}} = (\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) \overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}$
56	55	fveq2d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℜ (i A + \sqrt{1 - A^{2}}) = ℜ ((\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) \overline{i (- A) + \sqrt{1 - {(- A)}^{2}}})$
57	20 21	remul2d	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℜ ((\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) \overline{i (- A) + \sqrt{1 - {(- A)}^{2}}}) = (\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) ℜ (\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}})$
58	56 57	eqtrd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to ℜ (i A + \sqrt{1 - A^{2}}) = (\frac{1}{{\|i (- A) + \sqrt{1 - {(- A)}^{2}}\|}^{2}}) ℜ (\overline{i (- A) + \sqrt{1 - {(- A)}^{2}}})$
59	34 58	breqtrrd	$⊢ (A \in ℂ \land 0 \leq ℑ (A)) \to 0 \leq ℜ (i A + \sqrt{1 - A^{2}})$
60		asinlem3a	$⊢ (A \in ℂ \land ℑ (A) \leq 0) \to 0 \leq ℜ (i A + \sqrt{1 - A^{2}})$
61	1 2 59 60	lecasei	$⊢ A \in ℂ \to 0 \leq ℜ (i A + \sqrt{1 - A^{2}})$

Metamath Proof Explorer

Theorem asinlem3

Proof