asinsinlem

		Ref	Expression
	Assertion	asinsinlem	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 0 < ℜ (e^{i A})$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		simpl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to A \in ℂ$
3		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
4	1 2 3	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i A \in ℂ$
5	4	recld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (i A) \in ℝ$
6	5	reefcld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{ℜ (i A)} \in ℝ$
7		simpr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})$
8		neghalfpirx	$⊢ - \frac{π}{2} \in ℝ^{*}$
9		halfpire	$⊢ \frac{π}{2} \in ℝ$
10	9	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
11		elioo2	$⊢ (- \frac{π}{2} \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (ℜ (A) \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (ℜ (A) \in ℝ \land - \frac{π}{2} < ℜ (A) \land ℜ (A) < \frac{π}{2}))$
12	8 10 11	mp2an	$⊢ ℜ (A) \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (ℜ (A) \in ℝ \land - \frac{π}{2} < ℜ (A) \land ℜ (A) < \frac{π}{2})$
13	7 12	sylib	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (ℜ (A) \in ℝ \land - \frac{π}{2} < ℜ (A) \land ℜ (A) < \frac{π}{2})$
14	13	simp1d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (A) \in ℝ$
15	14	recoscld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ℜ (A) \in ℝ$
16		efgt0	$⊢ ℜ (i A) \in ℝ \to 0 < e^{ℜ (i A)}$
17	5 16	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 0 < e^{ℜ (i A)}$
18		cosq14gt0	$⊢ ℜ (A) \in (- \frac{π}{2}, \frac{π}{2}) \to 0 < \cos ℜ (A)$
19	18	adantl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 0 < \cos ℜ (A)$
20	6 15 17 19	mulgt0d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 0 < e^{ℜ (i A)} \cos ℜ (A)$
21		efeul	$⊢ i A \in ℂ \to e^{i A} = e^{ℜ (i A)} (\cos ℑ (i A) + i \sin ℑ (i A))$
22	4 21	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i A} = e^{ℜ (i A)} (\cos ℑ (i A) + i \sin ℑ (i A))$
23	22	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (e^{i A}) = ℜ (e^{ℜ (i A)} (\cos ℑ (i A) + i \sin ℑ (i A)))$
24	4	imcld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℑ (i A) \in ℝ$
25	24	recoscld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ℑ (i A) \in ℝ$
26	25	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ℑ (i A) \in ℂ$
27	24	resincld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \sin ℑ (i A) \in ℝ$
28	27	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \sin ℑ (i A) \in ℂ$
29		mulcl	$⊢ (i \in ℂ \land \sin ℑ (i A) \in ℂ) \to i \sin ℑ (i A) \in ℂ$
30	1 28 29	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \sin ℑ (i A) \in ℂ$
31	26 30	addcld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ℑ (i A) + i \sin ℑ (i A) \in ℂ$
32	6 31	remul2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (e^{ℜ (i A)} (\cos ℑ (i A) + i \sin ℑ (i A))) = e^{ℜ (i A)} ℜ (\cos ℑ (i A) + i \sin ℑ (i A))$
33	25 27	crred	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (\cos ℑ (i A) + i \sin ℑ (i A)) = \cos ℑ (i A)$
34		imre	$⊢ i A \in ℂ \to ℑ (i A) = ℜ ((- i) i A)$
35	4 34	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℑ (i A) = ℜ ((- i) i A)$
36	1 1	mulneg1i	$⊢ (- i) i = - i i$
37		ixi	$⊢ i i = - 1$
38	37	negeqi	$⊢ - i i = - -1$
39		negneg1e1	$⊢ - -1 = 1$
40	36 38 39	3eqtri	$⊢ (- i) i = 1$
41	40	oveq1i	$⊢ (- i) i A = 1 A$
42		negicn	$⊢ - i \in ℂ$
43	42	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - i \in ℂ$
44	1	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \in ℂ$
45	43 44 2	mulassd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (- i) i A = (- i) i A$
46		mullid	$⊢ A \in ℂ \to 1 A = A$
47	46	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 1 A = A$
48	41 45 47	3eqtr3a	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (- i) i A = A$
49	48	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ ((- i) i A) = ℜ (A)$
50	35 49	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℑ (i A) = ℜ (A)$
51	50	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ℑ (i A) = \cos ℜ (A)$
52	33 51	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (\cos ℑ (i A) + i \sin ℑ (i A)) = \cos ℜ (A)$
53	52	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{ℜ (i A)} ℜ (\cos ℑ (i A) + i \sin ℑ (i A)) = e^{ℜ (i A)} \cos ℜ (A)$
54	23 32 53	3eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (e^{i A}) = e^{ℜ (i A)} \cos ℜ (A)$
55	20 54	breqtrrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 0 < ℜ (e^{i A})$

Metamath Proof Explorer

Theorem asinsinlem

Proof