Metamath Proof Explorer

Theorem tanval

Description: Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Assertion tanval ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$

Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {A}\in ℂ$
2 coscl ${⊢}{A}\in ℂ\to \mathrm{cos}{A}\in ℂ$
3 2 anim1i ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \left(\mathrm{cos}{A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)$
4 eldifsn ${⊢}\mathrm{cos}{A}\in \left(ℂ\setminus \left\{0\right\}\right)↔\left(\mathrm{cos}{A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)$
5 3 4 sylibr ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{cos}{A}\in \left(ℂ\setminus \left\{0\right\}\right)$
6 cosf ${⊢}\mathrm{cos}:ℂ⟶ℂ$
7 ffn ${⊢}\mathrm{cos}:ℂ⟶ℂ\to \mathrm{cos}Fnℂ$
8 elpreima ${⊢}\mathrm{cos}Fnℂ\to \left({A}\in {\mathrm{cos}}^{-1}\left[ℂ\setminus \left\{0\right\}\right]↔\left({A}\in ℂ\wedge \mathrm{cos}{A}\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)$
9 6 7 8 mp2b ${⊢}{A}\in {\mathrm{cos}}^{-1}\left[ℂ\setminus \left\{0\right\}\right]↔\left({A}\in ℂ\wedge \mathrm{cos}{A}\in \left(ℂ\setminus \left\{0\right\}\right)\right)$
10 1 5 9 sylanbrc ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to {A}\in {\mathrm{cos}}^{-1}\left[ℂ\setminus \left\{0\right\}\right]$
11 fveq2 ${⊢}{x}={A}\to \mathrm{sin}{x}=\mathrm{sin}{A}$
12 fveq2 ${⊢}{x}={A}\to \mathrm{cos}{x}=\mathrm{cos}{A}$
13 11 12 oveq12d ${⊢}{x}={A}\to \frac{\mathrm{sin}{x}}{\mathrm{cos}{x}}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$
14 df-tan ${⊢}\mathrm{tan}=\left({x}\in {\mathrm{cos}}^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\mathrm{sin}{x}}{\mathrm{cos}{x}}\right)$
15 ovex ${⊢}\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}\in \mathrm{V}$
16 13 14 15 fvmpt ${⊢}{A}\in {\mathrm{cos}}^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \mathrm{tan}{A}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$
17 10 16 syl ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$