# Metamath Proof Explorer

Description: A useful intermediate step in tanadd when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion tanaddlem ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{cos}\left({A}+{B}\right)\ne 0↔\mathrm{tan}{A}\mathrm{tan}{B}\ne 1\right)$

### Proof

Step Hyp Ref Expression
1 coscl ${⊢}{A}\in ℂ\to \mathrm{cos}{A}\in ℂ$
2 1 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{A}\in ℂ$
3 coscl ${⊢}{B}\in ℂ\to \mathrm{cos}{B}\in ℂ$
4 3 ad2antlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{B}\in ℂ$
5 2 4 mulcld ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{A}\mathrm{cos}{B}\in ℂ$
6 sincl ${⊢}{A}\in ℂ\to \mathrm{sin}{A}\in ℂ$
7 6 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{sin}{A}\in ℂ$
8 sincl ${⊢}{B}\in ℂ\to \mathrm{sin}{B}\in ℂ$
9 8 ad2antlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{sin}{B}\in ℂ$
10 7 9 mulcld ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{sin}{A}\mathrm{sin}{B}\in ℂ$
11 5 10 subeq0ad ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{cos}{A}\mathrm{cos}{B}-\mathrm{sin}{A}\mathrm{sin}{B}=0↔\mathrm{cos}{A}\mathrm{cos}{B}=\mathrm{sin}{A}\mathrm{sin}{B}\right)$
12 cosadd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{cos}\left({A}+{B}\right)=\mathrm{cos}{A}\mathrm{cos}{B}-\mathrm{sin}{A}\mathrm{sin}{B}$
13 12 adantr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}\left({A}+{B}\right)=\mathrm{cos}{A}\mathrm{cos}{B}-\mathrm{sin}{A}\mathrm{sin}{B}$
14 13 eqeq1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{cos}\left({A}+{B}\right)=0↔\mathrm{cos}{A}\mathrm{cos}{B}-\mathrm{sin}{A}\mathrm{sin}{B}=0\right)$
15 tanval ${⊢}\left({A}\in ℂ\wedge \mathrm{cos}{A}\ne 0\right)\to \mathrm{tan}{A}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$
16 15 ad2ant2r ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{tan}{A}=\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}$
17 tanval ${⊢}\left({B}\in ℂ\wedge \mathrm{cos}{B}\ne 0\right)\to \mathrm{tan}{B}=\frac{\mathrm{sin}{B}}{\mathrm{cos}{B}}$
18 17 ad2ant2l ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{tan}{B}=\frac{\mathrm{sin}{B}}{\mathrm{cos}{B}}$
19 16 18 oveq12d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{tan}{A}\mathrm{tan}{B}=\left(\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}\right)\left(\frac{\mathrm{sin}{B}}{\mathrm{cos}{B}}\right)$
20 simprl ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{A}\ne 0$
21 simprr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{B}\ne 0$
22 7 2 9 4 20 21 divmuldivd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\frac{\mathrm{sin}{A}}{\mathrm{cos}{A}}\right)\left(\frac{\mathrm{sin}{B}}{\mathrm{cos}{B}}\right)=\frac{\mathrm{sin}{A}\mathrm{sin}{B}}{\mathrm{cos}{A}\mathrm{cos}{B}}$
23 19 22 eqtrd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{tan}{A}\mathrm{tan}{B}=\frac{\mathrm{sin}{A}\mathrm{sin}{B}}{\mathrm{cos}{A}\mathrm{cos}{B}}$
24 23 eqeq1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{tan}{A}\mathrm{tan}{B}=1↔\frac{\mathrm{sin}{A}\mathrm{sin}{B}}{\mathrm{cos}{A}\mathrm{cos}{B}}=1\right)$
25 1cnd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to 1\in ℂ$
26 2 4 20 21 mulne0d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{A}\mathrm{cos}{B}\ne 0$
27 10 5 25 26 divmuld ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\frac{\mathrm{sin}{A}\mathrm{sin}{B}}{\mathrm{cos}{A}\mathrm{cos}{B}}=1↔\mathrm{cos}{A}\mathrm{cos}{B}\cdot 1=\mathrm{sin}{A}\mathrm{sin}{B}\right)$
28 5 mulid1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \mathrm{cos}{A}\mathrm{cos}{B}\cdot 1=\mathrm{cos}{A}\mathrm{cos}{B}$
29 28 eqeq1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{cos}{A}\mathrm{cos}{B}\cdot 1=\mathrm{sin}{A}\mathrm{sin}{B}↔\mathrm{cos}{A}\mathrm{cos}{B}=\mathrm{sin}{A}\mathrm{sin}{B}\right)$
30 24 27 29 3bitrd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{tan}{A}\mathrm{tan}{B}=1↔\mathrm{cos}{A}\mathrm{cos}{B}=\mathrm{sin}{A}\mathrm{sin}{B}\right)$
31 11 14 30 3bitr4d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{cos}\left({A}+{B}\right)=0↔\mathrm{tan}{A}\mathrm{tan}{B}=1\right)$
32 31 necon3bid ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left(\mathrm{cos}{A}\ne 0\wedge \mathrm{cos}{B}\ne 0\right)\right)\to \left(\mathrm{cos}\left({A}+{B}\right)\ne 0↔\mathrm{tan}{A}\mathrm{tan}{B}\ne 1\right)$