# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in ℂ\wedge \Re \left({A}\right)\in \left(0,\frac{\mathrm{\pi }}{2}\right)\right)\to 0<\Re \left(\mathrm{tan}{A}\right)$

### Proof

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