Metamath Proof Explorer

Theorem tanaddlem

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 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A + B ≠ 0 ↔ tan ⁡ A ⁢ tan ⁡ B ≠ 1

Proof

Step Hyp Ref Expression
1 coscl ⊢ A ∈ ℂ → cos ⁡ A ∈ ℂ
2 1 ad2antrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ∈ ℂ
3 coscl ⊢ B ∈ ℂ → cos ⁡ B ∈ ℂ
4 3 ad2antlr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ B ∈ ℂ
5 2 4 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ⁢ cos ⁡ B ∈ ℂ
6 sincl ⊢ A ∈ ℂ → sin ⁡ A ∈ ℂ
7 6 ad2antrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → sin ⁡ A ∈ ℂ
8 sincl ⊢ B ∈ ℂ → sin ⁡ B ∈ ℂ
9 8 ad2antlr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → sin ⁡ B ∈ ℂ
10 7 9 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → sin ⁡ A ⁢ sin ⁡ B ∈ ℂ
11 5 10 subeq0ad ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ⁢ cos ⁡ B − sin ⁡ A ⁢ sin ⁡ B = 0 ↔ cos ⁡ A ⁢ cos ⁡ B = sin ⁡ A ⁢ sin ⁡ B
12 cosadd ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B = cos ⁡ A ⁢ cos ⁡ B − sin ⁡ A ⁢ sin ⁡ B
13 12 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A + B = cos ⁡ A ⁢ cos ⁡ B − sin ⁡ A ⁢ sin ⁡ B
14 13 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A + B = 0 ↔ cos ⁡ A ⁢ cos ⁡ B − sin ⁡ A ⁢ sin ⁡ B = 0
15 tanval ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → tan ⁡ A = sin ⁡ A cos ⁡ A
16 15 ad2ant2r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → tan ⁡ A = sin ⁡ A cos ⁡ A
17 tanval ⊢ B ∈ ℂ ∧ cos ⁡ B ≠ 0 → tan ⁡ B = sin ⁡ B cos ⁡ B
18 17 ad2ant2l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → tan ⁡ B = sin ⁡ B cos ⁡ B
19 16 18 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → tan ⁡ A ⁢ tan ⁡ B = sin ⁡ A cos ⁡ A ⁢ sin ⁡ B cos ⁡ B
20 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ≠ 0
21 simprr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ B ≠ 0
22 7 2 9 4 20 21 divmuldivd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → sin ⁡ A cos ⁡ A ⁢ sin ⁡ B cos ⁡ B = sin ⁡ A ⁢ sin ⁡ B cos ⁡ A ⁢ cos ⁡ B
23 19 22 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → tan ⁡ A ⁢ tan ⁡ B = sin ⁡ A ⁢ sin ⁡ B cos ⁡ A ⁢ cos ⁡ B
24 23 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → tan ⁡ A ⁢ tan ⁡ B = 1 ↔ sin ⁡ A ⁢ sin ⁡ B cos ⁡ A ⁢ cos ⁡ B = 1
25 1cnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → 1 ∈ ℂ
26 2 4 20 21 mulne0d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ⁢ cos ⁡ B ≠ 0
27 10 5 25 26 divmuld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → sin ⁡ A ⁢ sin ⁡ B cos ⁡ A ⁢ cos ⁡ B = 1 ↔ cos ⁡ A ⁢ cos ⁡ B ⋅ 1 = sin ⁡ A ⁢ sin ⁡ B
28 5 mulid1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ⁢ cos ⁡ B ⋅ 1 = cos ⁡ A ⁢ cos ⁡ B
29 28 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A ⁢ cos ⁡ B ⋅ 1 = sin ⁡ A ⁢ sin ⁡ B ↔ cos ⁡ A ⁢ cos ⁡ B = sin ⁡ A ⁢ sin ⁡ B
30 24 27 29 3bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → tan ⁡ A ⁢ tan ⁡ B = 1 ↔ cos ⁡ A ⁢ cos ⁡ B = sin ⁡ A ⁢ sin ⁡ B
31 11 14 30 3bitr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A + B = 0 ↔ tan ⁡ A ⁢ tan ⁡ B = 1
32 31 necon3bid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ cos ⁡ A ≠ 0 ∧ cos ⁡ B ≠ 0 → cos ⁡ A + B ≠ 0 ↔ tan ⁡ A ⁢ tan ⁡ B ≠ 1