tanregt0

Description: The real part of the tangent of a complex number with real part in the open interval ( 0 (,) ( _pi / 2 ) ) is positive. (Contributed by Mario Carneiro, 5-Apr-2015)

		Ref	Expression
	Assertion	tanregt0	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < ℜ (\tan A)$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$
3	2	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (A) \in ℝ$
4	3	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (A) \in ℂ$
5	3	rered	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (ℜ (A)) = ℜ (A)$
6		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
7	6	rexri	$⊢ - \frac{π}{2} \in ℝ^{*}$
8		0re	$⊢ 0 \in ℝ$
9		pirp	$⊢ π \in ℝ^{+}$
10		rphalfcl	$⊢ π \in ℝ^{+} \to \frac{π}{2} \in ℝ^{+}$
11		rpgt0	$⊢ \frac{π}{2} \in ℝ^{+} \to 0 < \frac{π}{2}$
12	9 10 11	mp2b	$⊢ 0 < \frac{π}{2}$
13		halfpire	$⊢ \frac{π}{2} \in ℝ$
14		lt0neg2	$⊢ \frac{π}{2} \in ℝ \to (0 < \frac{π}{2} \leftrightarrow - \frac{π}{2} < 0)$
15	13 14	ax-mp	$⊢ 0 < \frac{π}{2} \leftrightarrow - \frac{π}{2} < 0$
16	12 15	mpbi	$⊢ - \frac{π}{2} < 0$
17	6 8 16	ltleii	$⊢ - \frac{π}{2} \leq 0$
18		iooss1	$⊢ (- \frac{π}{2} \in ℝ^{*} \land - \frac{π}{2} \leq 0) \to (0, \frac{π}{2}) \subseteq (- \frac{π}{2}, \frac{π}{2})$
19	7 17 18	mp2an	$⊢ (0, \frac{π}{2}) \subseteq (- \frac{π}{2}, \frac{π}{2})$
20		simpr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (A) \in (0, \frac{π}{2})$
21	19 20	sseldi	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})$
22	5 21	eqeltrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (ℜ (A)) \in (- \frac{π}{2}, \frac{π}{2})$
23		cosne0	$⊢ (ℜ (A) \in ℂ \land ℜ (ℜ (A)) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ℜ (A) \neq 0$
24	4 22 23	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \cos ℜ (A) \neq 0$
25	4 24	tancld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) \in ℂ$
26		ax-icn	$⊢ i \in ℂ$
27		imcl	$⊢ A \in ℂ \to ℑ (A) \in ℝ$
28	27	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (A) \in ℝ$
29	28	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (A) \in ℂ$
30		mulcl	$⊢ (i \in ℂ \land ℑ (A) \in ℂ) \to i ℑ (A) \in ℂ$
31	26 29 30	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to i ℑ (A) \in ℂ$
32		rpcoshcl	$⊢ ℑ (A) \in ℝ \to \cos i ℑ (A) \in ℝ^{+}$
33	28 32	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \cos i ℑ (A) \in ℝ^{+}$
34	33	rpne0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \cos i ℑ (A) \neq 0$
35	31 34	tancld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan i ℑ (A) \in ℂ$
36	25 35	mulcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) \tan i ℑ (A) \in ℂ$
37		subcl	$⊢ (1 \in ℂ \land \tan ℜ (A) \tan i ℑ (A) \in ℂ) \to 1 - \tan ℜ (A) \tan i ℑ (A) \in ℂ$
38	1 36 37	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 - \tan ℜ (A) \tan i ℑ (A) \in ℂ$
39		replim	$⊢ A \in ℂ \to A = ℜ (A) + i ℑ (A)$
40	39	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to A = ℜ (A) + i ℑ (A)$
41	40	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \cos A = \cos (ℜ (A) + i ℑ (A))$
42		cosne0	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A \neq 0$
43	21 42	syldan	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \cos A \neq 0$
44	41 43	eqnetrrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \cos (ℜ (A) + i ℑ (A)) \neq 0$
45		tanaddlem	$⊢ ((ℜ (A) \in ℂ \land i ℑ (A) \in ℂ) \land (\cos ℜ (A) \neq 0 \land \cos i ℑ (A) \neq 0)) \to (\cos (ℜ (A) + i ℑ (A)) \neq 0 \leftrightarrow \tan ℜ (A) \tan i ℑ (A) \neq 1)$
46	4 31 24 34 45	syl22anc	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (\cos (ℜ (A) + i ℑ (A)) \neq 0 \leftrightarrow \tan ℜ (A) \tan i ℑ (A) \neq 1)$
47	44 46	mpbid	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) \tan i ℑ (A) \neq 1$
48	47	necomd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 \neq \tan ℜ (A) \tan i ℑ (A)$
49		subeq0	$⊢ (1 \in ℂ \land \tan ℜ (A) \tan i ℑ (A) \in ℂ) \to (1 - \tan ℜ (A) \tan i ℑ (A) = 0 \leftrightarrow 1 = \tan ℜ (A) \tan i ℑ (A))$
50	49	necon3bid	$⊢ (1 \in ℂ \land \tan ℜ (A) \tan i ℑ (A) \in ℂ) \to (1 - \tan ℜ (A) \tan i ℑ (A) \neq 0 \leftrightarrow 1 \neq \tan ℜ (A) \tan i ℑ (A))$
51	1 36 50	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (1 - \tan ℜ (A) \tan i ℑ (A) \neq 0 \leftrightarrow 1 \neq \tan ℜ (A) \tan i ℑ (A))$
52	48 51	mpbird	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 - \tan ℜ (A) \tan i ℑ (A) \neq 0$
53	38 52	absrpcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \|1 - \tan ℜ (A) \tan i ℑ (A)\| \in ℝ^{+}$
54		2z	$⊢ 2 \in ℤ$
55		rpexpcl	$⊢ (\|1 - \tan ℜ (A) \tan i ℑ (A)\| \in ℝ^{+} \land 2 \in ℤ) \to {\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2} \in ℝ^{+}$
56	53 54 55	sylancl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2} \in ℝ^{+}$
57	56	rprecred	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}} \in ℝ$
58	38	cjcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \overline{1 - \tan ℜ (A) \tan i ℑ (A)} \in ℂ$
59	25 35	addcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) + \tan i ℑ (A) \in ℂ$
60	58 59	mulcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A)) \in ℂ$
61	60	recld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))) \in ℝ$
62	56	rpreccld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}} \in ℝ^{+}$
63	62	rpgt0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < \frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}$
64	3 24	retancld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) \in ℝ$
65		1re	$⊢ 1 \in ℝ$
66		retanhcl	$⊢ ℑ (A) \in ℝ \to \frac{\tan i ℑ (A)}{i} \in ℝ$
67	28 66	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan i ℑ (A)}{i} \in ℝ$
68	67	resqcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {(\frac{\tan i ℑ (A)}{i})}^{2} \in ℝ$
69		resubcl	$⊢ (1 \in ℝ \land {(\frac{\tan i ℑ (A)}{i})}^{2} \in ℝ) \to 1 - {(\frac{\tan i ℑ (A)}{i})}^{2} \in ℝ$
70	65 68 69	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 - {(\frac{\tan i ℑ (A)}{i})}^{2} \in ℝ$
71		tanrpcl	$⊢ ℜ (A) \in (0, \frac{π}{2}) \to \tan ℜ (A) \in ℝ^{+}$
72	71	adantl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) \in ℝ^{+}$
73	72	rpgt0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < \tan ℜ (A)$
74		absresq	$⊢ \frac{\tan i ℑ (A)}{i} \in ℝ \to {\|\frac{\tan i ℑ (A)}{i}\|}^{2} = {(\frac{\tan i ℑ (A)}{i})}^{2}$
75	67 74	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|\frac{\tan i ℑ (A)}{i}\|}^{2} = {(\frac{\tan i ℑ (A)}{i})}^{2}$
76		tanhbnd	$⊢ ℑ (A) \in ℝ \to \frac{\tan i ℑ (A)}{i} \in (- 1, 1)$
77	28 76	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan i ℑ (A)}{i} \in (- 1, 1)$
78		eliooord	$⊢ \frac{\tan i ℑ (A)}{i} \in (- 1, 1) \to (- 1 < \frac{\tan i ℑ (A)}{i} \land \frac{\tan i ℑ (A)}{i} < 1)$
79	77 78	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (- 1 < \frac{\tan i ℑ (A)}{i} \land \frac{\tan i ℑ (A)}{i} < 1)$
80		abslt	$⊢ (\frac{\tan i ℑ (A)}{i} \in ℝ \land 1 \in ℝ) \to (\|\frac{\tan i ℑ (A)}{i}\| < 1 \leftrightarrow (- 1 < \frac{\tan i ℑ (A)}{i} \land \frac{\tan i ℑ (A)}{i} < 1))$
81	67 65 80	sylancl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (\|\frac{\tan i ℑ (A)}{i}\| < 1 \leftrightarrow (- 1 < \frac{\tan i ℑ (A)}{i} \land \frac{\tan i ℑ (A)}{i} < 1))$
82	79 81	mpbird	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \|\frac{\tan i ℑ (A)}{i}\| < 1$
83	67	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan i ℑ (A)}{i} \in ℂ$
84	83	abscld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \|\frac{\tan i ℑ (A)}{i}\| \in ℝ$
85	65	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 \in ℝ$
86	83	absge0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 \leq \|\frac{\tan i ℑ (A)}{i}\|$
87		0le1	$⊢ 0 \leq 1$
88	87	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 \leq 1$
89	84 85 86 88	lt2sqd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (\|\frac{\tan i ℑ (A)}{i}\| < 1 \leftrightarrow {\|\frac{\tan i ℑ (A)}{i}\|}^{2} < 1^{2})$
90	82 89	mpbid	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|\frac{\tan i ℑ (A)}{i}\|}^{2} < 1^{2}$
91		sq1	$⊢ 1^{2} = 1$
92	90 91	breqtrdi	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|\frac{\tan i ℑ (A)}{i}\|}^{2} < 1$
93	75 92	eqbrtrrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {(\frac{\tan i ℑ (A)}{i})}^{2} < 1$
94		posdif	$⊢ ({(\frac{\tan i ℑ (A)}{i})}^{2} \in ℝ \land 1 \in ℝ) \to ({(\frac{\tan i ℑ (A)}{i})}^{2} < 1 \leftrightarrow 0 < 1 - {(\frac{\tan i ℑ (A)}{i})}^{2})$
95	68 65 94	sylancl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ({(\frac{\tan i ℑ (A)}{i})}^{2} < 1 \leftrightarrow 0 < 1 - {(\frac{\tan i ℑ (A)}{i})}^{2})$
96	93 95	mpbid	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < 1 - {(\frac{\tan i ℑ (A)}{i})}^{2}$
97	64 70 73 96	mulgt0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < \tan ℜ (A) (1 - {(\frac{\tan i ℑ (A)}{i})}^{2})$
98	38	recjd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) = ℜ (1 - \tan ℜ (A) \tan i ℑ (A))$
99		resub	$⊢ (1 \in ℂ \land \tan ℜ (A) \tan i ℑ (A) \in ℂ) \to ℜ (1 - \tan ℜ (A) \tan i ℑ (A)) = ℜ (1) - ℜ (\tan ℜ (A) \tan i ℑ (A))$
100	1 36 99	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (1 - \tan ℜ (A) \tan i ℑ (A)) = ℜ (1) - ℜ (\tan ℜ (A) \tan i ℑ (A))$
101		re1	$⊢ ℜ (1) = 1$
102	101	oveq1i	$⊢ ℜ (1) - ℜ (\tan ℜ (A) \tan i ℑ (A)) = 1 - ℜ (\tan ℜ (A) \tan i ℑ (A))$
103	64 35	remul2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan ℜ (A) \tan i ℑ (A)) = \tan ℜ (A) ℜ (\tan i ℑ (A))$
104		negicn	$⊢ - i \in ℂ$
105	104	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - i \in ℂ$
106		ine0	$⊢ i \neq 0$
107	26 106	negne0i	$⊢ - i \neq 0$
108	107	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - i \neq 0$
109	35 105 108	divcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan i ℑ (A)}{- i} \in ℂ$
110		imre	$⊢ \frac{\tan i ℑ (A)}{- i} \in ℂ \to ℑ (\frac{\tan i ℑ (A)}{- i}) = ℜ ((- i) (\frac{\tan i ℑ (A)}{- i}))$
111	109 110	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\frac{\tan i ℑ (A)}{- i}) = ℜ ((- i) (\frac{\tan i ℑ (A)}{- i}))$
112	26	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to i \in ℂ$
113	106	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to i \neq 0$
114	35 112 113	divneg2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - \frac{\tan i ℑ (A)}{i} = \frac{\tan i ℑ (A)}{- i}$
115	67	renegcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - \frac{\tan i ℑ (A)}{i} \in ℝ$
116	114 115	eqeltrrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan i ℑ (A)}{- i} \in ℝ$
117	116	reim0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\frac{\tan i ℑ (A)}{- i}) = 0$
118	35 105 108	divcan2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (- i) (\frac{\tan i ℑ (A)}{- i}) = \tan i ℑ (A)$
119	118	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ ((- i) (\frac{\tan i ℑ (A)}{- i})) = ℜ (\tan i ℑ (A))$
120	111 117 119	3eqtr3rd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan i ℑ (A)) = 0$
121	120	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) ℜ (\tan i ℑ (A)) = \tan ℜ (A) \cdot 0$
122	25	mul01d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) \cdot 0 = 0$
123	103 121 122	3eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan ℜ (A) \tan i ℑ (A)) = 0$
124	123	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 - ℜ (\tan ℜ (A) \tan i ℑ (A)) = 1 - 0$
125		1m0e1	$⊢ 1 - 0 = 1$
126	124 125	syl6eq	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 - ℜ (\tan ℜ (A) \tan i ℑ (A)) = 1$
127	102 126	syl5eq	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (1) - ℜ (\tan ℜ (A) \tan i ℑ (A)) = 1$
128	98 100 127	3eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) = 1$
129	35 112 113	divcan2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to i (\frac{\tan i ℑ (A)}{i}) = \tan i ℑ (A)$
130	129	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) + i (\frac{\tan i ℑ (A)}{i}) = \tan ℜ (A) + \tan i ℑ (A)$
131	130	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan ℜ (A) + i (\frac{\tan i ℑ (A)}{i})) = ℜ (\tan ℜ (A) + \tan i ℑ (A))$
132	64 67	crred	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan ℜ (A) + i (\frac{\tan i ℑ (A)}{i})) = \tan ℜ (A)$
133	131 132	eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan ℜ (A) + \tan i ℑ (A)) = \tan ℜ (A)$
134	128 133	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℜ (\tan ℜ (A) + \tan i ℑ (A)) = 1 \tan ℜ (A)$
135		mulcom	$⊢ (1 \in ℂ \land \tan ℜ (A) \in ℂ) \to 1 \tan ℜ (A) = \tan ℜ (A) \cdot 1$
136	1 25 135	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 \tan ℜ (A) = \tan ℜ (A) \cdot 1$
137	134 136	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℜ (\tan ℜ (A) + \tan i ℑ (A)) = \tan ℜ (A) \cdot 1$
138	25 83 83	mulassd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}) (\frac{\tan i ℑ (A)}{i}) = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}) (\frac{\tan i ℑ (A)}{i})$
139	38	imcjd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) = - ℑ (1 - \tan ℜ (A) \tan i ℑ (A))$
140		imsub	$⊢ (1 \in ℂ \land \tan ℜ (A) \tan i ℑ (A) \in ℂ) \to ℑ (1 - \tan ℜ (A) \tan i ℑ (A)) = ℑ (1) - ℑ (\tan ℜ (A) \tan i ℑ (A))$
141	1 36 140	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (1 - \tan ℜ (A) \tan i ℑ (A)) = ℑ (1) - ℑ (\tan ℜ (A) \tan i ℑ (A))$
142		im1	$⊢ ℑ (1) = 0$
143	142	oveq1i	$⊢ ℑ (1) - ℑ (\tan ℜ (A) \tan i ℑ (A)) = 0 - ℑ (\tan ℜ (A) \tan i ℑ (A))$
144		df-neg	$⊢ - ℑ (\tan ℜ (A) \tan i ℑ (A)) = 0 - ℑ (\tan ℜ (A) \tan i ℑ (A))$
145	143 144	eqtr4i	$⊢ ℑ (1) - ℑ (\tan ℜ (A) \tan i ℑ (A)) = - ℑ (\tan ℜ (A) \tan i ℑ (A))$
146	64 35	immul2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan ℜ (A) \tan i ℑ (A)) = \tan ℜ (A) ℑ (\tan i ℑ (A))$
147		imval	$⊢ \tan i ℑ (A) \in ℂ \to ℑ (\tan i ℑ (A)) = ℜ (\frac{\tan i ℑ (A)}{i})$
148	35 147	syl	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan i ℑ (A)) = ℜ (\frac{\tan i ℑ (A)}{i})$
149	67	rered	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\frac{\tan i ℑ (A)}{i}) = \frac{\tan i ℑ (A)}{i}$
150	148 149	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan i ℑ (A)) = \frac{\tan i ℑ (A)}{i}$
151	150	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) ℑ (\tan i ℑ (A)) = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
152	146 151	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan ℜ (A) \tan i ℑ (A)) = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
153	152	negeqd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - ℑ (\tan ℜ (A) \tan i ℑ (A)) = - \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
154	145 153	syl5eq	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (1) - ℑ (\tan ℜ (A) \tan i ℑ (A)) = - \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
155	141 154	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (1 - \tan ℜ (A) \tan i ℑ (A)) = - \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
156	155	negeqd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - ℑ (1 - \tan ℜ (A) \tan i ℑ (A)) = - (- \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}))$
157	64 67	remulcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}) \in ℝ$
158	157	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}) \in ℂ$
159	158	negnegd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to - (- \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})) = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
160	139 156 159	3eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i})$
161	130	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan ℜ (A) + i (\frac{\tan i ℑ (A)}{i})) = ℑ (\tan ℜ (A) + \tan i ℑ (A))$
162	64 67	crimd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan ℜ (A) + i (\frac{\tan i ℑ (A)}{i})) = \frac{\tan i ℑ (A)}{i}$
163	161 162	eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\tan ℜ (A) + \tan i ℑ (A)) = \frac{\tan i ℑ (A)}{i}$
164	160 163	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℑ (\tan ℜ (A) + \tan i ℑ (A)) = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}) (\frac{\tan i ℑ (A)}{i})$
165	83	sqvald	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {(\frac{\tan i ℑ (A)}{i})}^{2} = (\frac{\tan i ℑ (A)}{i}) (\frac{\tan i ℑ (A)}{i})$
166	165	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) {(\frac{\tan i ℑ (A)}{i})}^{2} = \tan ℜ (A) (\frac{\tan i ℑ (A)}{i}) (\frac{\tan i ℑ (A)}{i})$
167	138 164 166	3eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℑ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℑ (\tan ℜ (A) + \tan i ℑ (A)) = \tan ℜ (A) {(\frac{\tan i ℑ (A)}{i})}^{2}$
168	137 167	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℜ (\tan ℜ (A) + \tan i ℑ (A)) - ℑ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℑ (\tan ℜ (A) + \tan i ℑ (A)) = \tan ℜ (A) \cdot 1 - \tan ℜ (A) {(\frac{\tan i ℑ (A)}{i})}^{2}$
169	58 59	remuld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))) = ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℜ (\tan ℜ (A) + \tan i ℑ (A)) - ℑ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)}) ℑ (\tan ℜ (A) + \tan i ℑ (A))$
170	1	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 1 \in ℂ$
171	83	sqcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {(\frac{\tan i ℑ (A)}{i})}^{2} \in ℂ$
172	25 170 171	subdid	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan ℜ (A) (1 - {(\frac{\tan i ℑ (A)}{i})}^{2}) = \tan ℜ (A) \cdot 1 - \tan ℜ (A) {(\frac{\tan i ℑ (A)}{i})}^{2}$
173	168 169 172	3eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))) = \tan ℜ (A) (1 - {(\frac{\tan i ℑ (A)}{i})}^{2})$
174	97 173	breqtrrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A)))$
175	57 61 63 174	mulgt0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < (\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A)))$
176	40	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan A = \tan (ℜ (A) + i ℑ (A))$
177		tanadd	$⊢ ((ℜ (A) \in ℂ \land i ℑ (A) \in ℂ) \land (\cos ℜ (A) \neq 0 \land \cos i ℑ (A) \neq 0 \land \cos (ℜ (A) + i ℑ (A)) \neq 0)) \to \tan (ℜ (A) + i ℑ (A)) = \frac{\tan ℜ (A) + \tan i ℑ (A)}{1 - \tan ℜ (A) \tan i ℑ (A)}$
178	4 31 24 34 44 177	syl23anc	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan (ℜ (A) + i ℑ (A)) = \frac{\tan ℜ (A) + \tan i ℑ (A)}{1 - \tan ℜ (A) \tan i ℑ (A)}$
179		recval	$⊢ (1 - \tan ℜ (A) \tan i ℑ (A) \in ℂ \land 1 - \tan ℜ (A) \tan i ℑ (A) \neq 0) \to \frac{1}{1 - \tan ℜ (A) \tan i ℑ (A)} = \frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)}}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}$
180	38 52 179	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{1}{1 - \tan ℜ (A) \tan i ℑ (A)} = \frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)}}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}$
181	180	oveq1d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to (\frac{1}{1 - \tan ℜ (A) \tan i ℑ (A)}) (\tan ℜ (A) + \tan i ℑ (A)) = (\frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)}}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) (\tan ℜ (A) + \tan i ℑ (A))$
182	59 38 52	divrec2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan ℜ (A) + \tan i ℑ (A)}{1 - \tan ℜ (A) \tan i ℑ (A)} = (\frac{1}{1 - \tan ℜ (A) \tan i ℑ (A)}) (\tan ℜ (A) + \tan i ℑ (A))$
183	38	abscld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \|1 - \tan ℜ (A) \tan i ℑ (A)\| \in ℝ$
184	183	resqcld	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2} \in ℝ$
185	184	recnd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2} \in ℂ$
186	56	rpne0d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to {\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2} \neq 0$
187	58 59 185 186	div23d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}} = (\frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)}}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) (\tan ℜ (A) + \tan i ℑ (A))$
188	181 182 187	3eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\tan ℜ (A) + \tan i ℑ (A)}{1 - \tan ℜ (A) \tan i ℑ (A)} = \frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}$
189	176 178 188	3eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan A = \frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}$
190	60 185 186	divrec2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \frac{\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}} = (\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) \overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))$
191	189 190	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to \tan A = (\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) \overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))$
192	191	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan A) = ℜ ((\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) \overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A)))$
193	57 60	remul2d	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ ((\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) \overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A))) = (\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A)))$
194	192 193	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to ℜ (\tan A) = (\frac{1}{{\|1 - \tan ℜ (A) \tan i ℑ (A)\|}^{2}}) ℜ (\overline{1 - \tan ℜ (A) \tan i ℑ (A)} (\tan ℜ (A) + \tan i ℑ (A)))$
195	175 194	breqtrrd	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < ℜ (\tan A)$

Metamath Proof Explorer

Theorem tanregt0

Proof