# Metamath Proof Explorer

## Theorem tanval2

Description: Express the tangent function directly in terms of exp . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion tanval2 ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}\left({\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\right)}$

### Proof

Step Hyp Ref Expression
1 tanval ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$
2 2cn ${⊢}2\in ℂ$
3 ax-icn ${⊢}\mathrm{i}\in ℂ$
4 2 3 mulcomi ${⊢}2\mathrm{i}=\mathrm{i}\cdot 2$
5 4 oveq2i ${⊢}\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}\cdot 2}$
6 sinval ${⊢}{A}\in ℂ\to \mathrm{sin}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}$
7 6 adantr ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{sin}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2\mathrm{i}}$
8 simpl ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {A}\in ℂ$
9 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge {A}\in ℂ\right)\to \mathrm{i}{A}\in ℂ$
10 3 8 9 sylancr ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{i}{A}\in ℂ$
11 efcl ${⊢}\mathrm{i}{A}\in ℂ\to {\mathrm{e}}^{\mathrm{i}{A}}\in ℂ$
12 10 11 syl ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}{A}}\in ℂ$
13 negicn ${⊢}-\mathrm{i}\in ℂ$
14 mulcl ${⊢}\left(-\mathrm{i}\in ℂ\wedge {A}\in ℂ\right)\to \left(-\mathrm{i}\right){A}\in ℂ$
15 13 8 14 sylancr ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \left(-\mathrm{i}\right){A}\in ℂ$
16 efcl ${⊢}\left(-\mathrm{i}\right){A}\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\in ℂ$
17 15 16 syl ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\in ℂ$
18 12 17 subcld ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\in ℂ$
19 3 a1i ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{i}\in ℂ$
20 2 a1i ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to 2\in ℂ$
21 ine0 ${⊢}\mathrm{i}\ne 0$
22 21 a1i ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{i}\ne 0$
23 2ne0 ${⊢}2\ne 0$
24 23 a1i ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to 2\ne 0$
25 18 19 20 22 24 divdiv1d ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{2}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}\cdot 2}$
26 5 7 25 3eqtr4a ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{sin}{A}=\frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{2}$
27 cosval ${⊢}{A}\in ℂ\to \mathrm{cos}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}$
28 27 adantr ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{cos}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}$
29 26 28 oveq12d ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}=\frac{\frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{2}}{\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}}$
30 1 29 eqtrd ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{\frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{2}}{\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}}$
31 18 19 22 divcld ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}\in ℂ$
32 12 17 addcld ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\in ℂ$
33 simpr ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{cos}{A}\ne 0$
34 28 33 eqnetrrd ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}\ne 0$
35 32 20 24 diveq0ad ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \left(\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}=0↔{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}=0\right)$
36 35 necon3bid ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \left(\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}\ne 0↔{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\ne 0\right)$
37 34 36 mpbid ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\ne 0$
38 31 32 20 37 24 divcan7d ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \frac{\frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{2}}{\frac{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{2}}=\frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}$
39 18 19 32 22 37 divdiv1d ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \frac{\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}}}{{\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}\left({\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\right)}$
40 30 38 39 3eqtrd ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{{\mathrm{e}}^{\mathrm{i}{A}}-{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{\mathrm{i}\left({\mathrm{e}}^{\mathrm{i}{A}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}\right)}$