Proof of Theorem tanadd
Step | Hyp | Ref
| Expression |
1 | | addcl 10841 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
2 | 1 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → (𝐴 + 𝐵) ∈ ℂ) |
3 | | simpr3 1198 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘(𝐴 + 𝐵)) ≠ 0) |
4 | | tanval 15722 |
. . 3
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ (cos‘(𝐴 + 𝐵)) ≠ 0) → (tan‘(𝐴 + 𝐵)) = ((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵)))) |
5 | 2, 3, 4 | syl2anc 587 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘(𝐴 + 𝐵)) = ((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵)))) |
6 | | sinadd 15758 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) |
7 | 6 | adantr 484 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) |
8 | | cosadd 15759 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |
9 | 8 | adantr 484 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |
10 | 7, 9 | oveq12d 7253 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵))) = ((((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵))) / (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵))))) |
11 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 𝐴 ∈
ℂ) |
12 | 11 | coscld 15725 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐴) ∈
ℂ) |
13 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 𝐵 ∈
ℂ) |
14 | 13 | coscld 15725 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐵) ∈
ℂ) |
15 | 12, 14 | mulcld 10883 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(cos‘𝐵)) ∈
ℂ) |
16 | | simpr1 1196 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐴) ≠
0) |
17 | 11, 16 | tancld 15726 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐴) ∈
ℂ) |
18 | | simpr2 1197 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐵) ≠
0) |
19 | 13, 18 | tancld 15726 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐵) ∈
ℂ) |
20 | 15, 17, 19 | adddid 10887 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) +
(tan‘𝐵))) =
((((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) +
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵)))) |
21 | 12, 14, 17 | mul32d 11072 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) =
(((cos‘𝐴) ·
(tan‘𝐴)) ·
(cos‘𝐵))) |
22 | | tanval 15722 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
23 | 11, 16, 22 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
24 | 23 | oveq2d 7251 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(tan‘𝐴)) =
((cos‘𝐴) ·
((sin‘𝐴) /
(cos‘𝐴)))) |
25 | 11 | sincld 15724 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(sin‘𝐴) ∈
ℂ) |
26 | 25, 12, 16 | divcan2d 11640 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
((sin‘𝐴) /
(cos‘𝐴))) =
(sin‘𝐴)) |
27 | 24, 26 | eqtrd 2779 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(tan‘𝐴)) =
(sin‘𝐴)) |
28 | 27 | oveq1d 7250 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(tan‘𝐴)) ·
(cos‘𝐵)) =
((sin‘𝐴) ·
(cos‘𝐵))) |
29 | 21, 28 | eqtrd 2779 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) =
((sin‘𝐴) ·
(cos‘𝐵))) |
30 | 12, 14, 19 | mulassd 10886 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵)) =
((cos‘𝐴) ·
((cos‘𝐵) ·
(tan‘𝐵)))) |
31 | | tanval 15722 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧
(cos‘𝐵) ≠ 0)
→ (tan‘𝐵) =
((sin‘𝐵) /
(cos‘𝐵))) |
32 | 13, 18, 31 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐵) =
((sin‘𝐵) /
(cos‘𝐵))) |
33 | 32 | oveq2d 7251 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐵) ·
(tan‘𝐵)) =
((cos‘𝐵) ·
((sin‘𝐵) /
(cos‘𝐵)))) |
34 | 13 | sincld 15724 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(sin‘𝐵) ∈
ℂ) |
35 | 34, 14, 18 | divcan2d 11640 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐵) ·
((sin‘𝐵) /
(cos‘𝐵))) =
(sin‘𝐵)) |
36 | 33, 35 | eqtrd 2779 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐵) ·
(tan‘𝐵)) =
(sin‘𝐵)) |
37 | 36 | oveq2d 7251 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
((cos‘𝐵) ·
(tan‘𝐵))) =
((cos‘𝐴) ·
(sin‘𝐵))) |
38 | 30, 37 | eqtrd 2779 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵)) =
((cos‘𝐴) ·
(sin‘𝐵))) |
39 | 29, 38 | oveq12d 7253 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) +
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵))) =
(((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵)))) |
40 | 20, 39 | eqtrd 2779 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) +
(tan‘𝐵))) =
(((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵)))) |
41 | | 1cnd 10858 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 1 ∈
ℂ) |
42 | 17, 19 | mulcld 10883 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((tan‘𝐴) ·
(tan‘𝐵)) ∈
ℂ) |
43 | 15, 41, 42 | subdid 11318 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) · (1
− ((tan‘𝐴)
· (tan‘𝐵)))) =
((((cos‘𝐴) ·
(cos‘𝐵)) · 1)
− (((cos‘𝐴)
· (cos‘𝐵))
· ((tan‘𝐴)
· (tan‘𝐵))))) |
44 | 15 | mulid1d 10880 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) · 1)
= ((cos‘𝐴) ·
(cos‘𝐵))) |
45 | 12, 14, 17, 19 | mul4d 11074 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) ·
(tan‘𝐵))) =
(((cos‘𝐴) ·
(tan‘𝐴)) ·
((cos‘𝐵) ·
(tan‘𝐵)))) |
46 | 27, 36 | oveq12d 7253 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(tan‘𝐴)) ·
((cos‘𝐵) ·
(tan‘𝐵))) =
((sin‘𝐴) ·
(sin‘𝐵))) |
47 | 45, 46 | eqtrd 2779 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) ·
(tan‘𝐵))) =
((sin‘𝐴) ·
(sin‘𝐵))) |
48 | 44, 47 | oveq12d 7253 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((((cos‘𝐴) ·
(cos‘𝐵)) · 1)
− (((cos‘𝐴)
· (cos‘𝐵))
· ((tan‘𝐴)
· (tan‘𝐵)))) =
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵)))) |
49 | 43, 48 | eqtrd 2779 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) · (1
− ((tan‘𝐴)
· (tan‘𝐵)))) =
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵)))) |
50 | 40, 49 | oveq12d 7253 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) +
(tan‘𝐵))) /
(((cos‘𝐴) ·
(cos‘𝐵)) · (1
− ((tan‘𝐴)
· (tan‘𝐵)))))
= ((((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵))) /
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵))))) |
51 | 17, 19 | addcld 10882 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((tan‘𝐴) +
(tan‘𝐵)) ∈
ℂ) |
52 | | ax-1cn 10817 |
. . . . 5
⊢ 1 ∈
ℂ |
53 | | subcl 11107 |
. . . . 5
⊢ ((1
∈ ℂ ∧ ((tan‘𝐴) · (tan‘𝐵)) ∈ ℂ) → (1 −
((tan‘𝐴) ·
(tan‘𝐵))) ∈
ℂ) |
54 | 52, 42, 53 | sylancr 590 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → (1 −
((tan‘𝐴) ·
(tan‘𝐵))) ∈
ℂ) |
55 | | tanaddlem 15760 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0))
→ ((cos‘(𝐴 +
𝐵)) ≠ 0 ↔
((tan‘𝐴) ·
(tan‘𝐵)) ≠
1)) |
56 | 55 | 3adantr3 1173 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘(𝐴 + 𝐵)) ≠ 0 ↔
((tan‘𝐴) ·
(tan‘𝐵)) ≠
1)) |
57 | 3, 56 | mpbid 235 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((tan‘𝐴) ·
(tan‘𝐵)) ≠
1) |
58 | 57 | necomd 2999 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 1 ≠
((tan‘𝐴) ·
(tan‘𝐵))) |
59 | | subeq0 11134 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ ((tan‘𝐴) · (tan‘𝐵)) ∈ ℂ) → ((1 −
((tan‘𝐴) ·
(tan‘𝐵))) = 0 ↔
1 = ((tan‘𝐴) ·
(tan‘𝐵)))) |
60 | 59 | necon3bid 2988 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ ((tan‘𝐴) · (tan‘𝐵)) ∈ ℂ) → ((1 −
((tan‘𝐴) ·
(tan‘𝐵))) ≠ 0
↔ 1 ≠ ((tan‘𝐴) · (tan‘𝐵)))) |
61 | 52, 42, 60 | sylancr 590 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → ((1 −
((tan‘𝐴) ·
(tan‘𝐵))) ≠ 0
↔ 1 ≠ ((tan‘𝐴) · (tan‘𝐵)))) |
62 | 58, 61 | mpbird 260 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → (1 −
((tan‘𝐴) ·
(tan‘𝐵))) ≠
0) |
63 | 12, 14, 16, 18 | mulne0d 11514 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(cos‘𝐵)) ≠
0) |
64 | 51, 54, 15, 62, 63 | divcan5d 11664 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) +
(tan‘𝐵))) /
(((cos‘𝐴) ·
(cos‘𝐵)) · (1
− ((tan‘𝐴)
· (tan‘𝐵)))))
= (((tan‘𝐴) +
(tan‘𝐵)) / (1 −
((tan‘𝐴) ·
(tan‘𝐵))))) |
65 | 10, 50, 64 | 3eqtr2rd 2786 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((tan‘𝐴) +
(tan‘𝐵)) / (1 −
((tan‘𝐴) ·
(tan‘𝐵)))) =
((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵)))) |
66 | 5, 65 | eqtr4d 2782 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘(𝐴 + 𝐵)) = (((tan‘𝐴) + (tan‘𝐵)) / (1 − ((tan‘𝐴) · (tan‘𝐵))))) |