Proof of Theorem tanadd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addcl 11238 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | 
| 2 | 1 | adantr 480 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → (𝐴 + 𝐵) ∈ ℂ) | 
| 3 |  | simpr3 1196 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘(𝐴 + 𝐵)) ≠ 0) | 
| 4 |  | tanval 16165 | . . 3
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ (cos‘(𝐴 + 𝐵)) ≠ 0) → (tan‘(𝐴 + 𝐵)) = ((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵)))) | 
| 5 | 2, 3, 4 | syl2anc 584 | . 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘(𝐴 + 𝐵)) = ((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵)))) | 
| 6 |  | sinadd 16201 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) | 
| 7 | 6 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) | 
| 8 |  | cosadd 16202 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) | 
| 10 | 7, 9 | oveq12d 7450 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵))) = ((((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵))) / (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵))))) | 
| 11 |  | simpll 766 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 𝐴 ∈
ℂ) | 
| 12 | 11 | coscld 16168 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐴) ∈
ℂ) | 
| 13 |  | simplr 768 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 𝐵 ∈
ℂ) | 
| 14 | 13 | coscld 16168 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐵) ∈
ℂ) | 
| 15 | 12, 14 | mulcld 11282 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(cos‘𝐵)) ∈
ℂ) | 
| 16 |  | simpr1 1194 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐴) ≠
0) | 
| 17 | 11, 16 | tancld 16169 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐴) ∈
ℂ) | 
| 18 |  | simpr2 1195 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(cos‘𝐵) ≠
0) | 
| 19 | 13, 18 | tancld 16169 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐵) ∈
ℂ) | 
| 20 | 15, 17, 19 | adddid 11286 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) +
(tan‘𝐵))) =
((((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) +
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵)))) | 
| 21 | 12, 14, 17 | mul32d 11472 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) =
(((cos‘𝐴) ·
(tan‘𝐴)) ·
(cos‘𝐵))) | 
| 22 |  | tanval 16165 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) | 
| 23 | 11, 16, 22 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) | 
| 24 | 23 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(tan‘𝐴)) =
((cos‘𝐴) ·
((sin‘𝐴) /
(cos‘𝐴)))) | 
| 25 | 11 | sincld 16167 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(sin‘𝐴) ∈
ℂ) | 
| 26 | 25, 12, 16 | divcan2d 12046 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
((sin‘𝐴) /
(cos‘𝐴))) =
(sin‘𝐴)) | 
| 27 | 24, 26 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(tan‘𝐴)) =
(sin‘𝐴)) | 
| 28 | 27 | oveq1d 7447 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(tan‘𝐴)) ·
(cos‘𝐵)) =
((sin‘𝐴) ·
(cos‘𝐵))) | 
| 29 | 21, 28 | eqtrd 2776 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) =
((sin‘𝐴) ·
(cos‘𝐵))) | 
| 30 | 12, 14, 19 | mulassd 11285 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵)) =
((cos‘𝐴) ·
((cos‘𝐵) ·
(tan‘𝐵)))) | 
| 31 |  | tanval 16165 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧
(cos‘𝐵) ≠ 0)
→ (tan‘𝐵) =
((sin‘𝐵) /
(cos‘𝐵))) | 
| 32 | 13, 18, 31 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘𝐵) =
((sin‘𝐵) /
(cos‘𝐵))) | 
| 33 | 32 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐵) ·
(tan‘𝐵)) =
((cos‘𝐵) ·
((sin‘𝐵) /
(cos‘𝐵)))) | 
| 34 | 13 | sincld 16167 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(sin‘𝐵) ∈
ℂ) | 
| 35 | 34, 14, 18 | divcan2d 12046 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐵) ·
((sin‘𝐵) /
(cos‘𝐵))) =
(sin‘𝐵)) | 
| 36 | 33, 35 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐵) ·
(tan‘𝐵)) =
(sin‘𝐵)) | 
| 37 | 36 | oveq2d 7448 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
((cos‘𝐵) ·
(tan‘𝐵))) =
((cos‘𝐴) ·
(sin‘𝐵))) | 
| 38 | 30, 37 | eqtrd 2776 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵)) =
((cos‘𝐴) ·
(sin‘𝐵))) | 
| 39 | 29, 38 | oveq12d 7450 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐴)) +
(((cos‘𝐴) ·
(cos‘𝐵)) ·
(tan‘𝐵))) =
(((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵)))) | 
| 40 | 20, 39 | eqtrd 2776 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) +
(tan‘𝐵))) =
(((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵)))) | 
| 41 |  | 1cnd 11257 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 1 ∈
ℂ) | 
| 42 | 17, 19 | mulcld 11282 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((tan‘𝐴) ·
(tan‘𝐵)) ∈
ℂ) | 
| 43 | 15, 41, 42 | subdid 11720 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) · (1
− ((tan‘𝐴)
· (tan‘𝐵)))) =
((((cos‘𝐴) ·
(cos‘𝐵)) · 1)
− (((cos‘𝐴)
· (cos‘𝐵))
· ((tan‘𝐴)
· (tan‘𝐵))))) | 
| 44 | 15 | mulridd 11279 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) · 1)
= ((cos‘𝐴) ·
(cos‘𝐵))) | 
| 45 | 12, 14, 17, 19 | mul4d 11474 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) ·
(tan‘𝐵))) =
(((cos‘𝐴) ·
(tan‘𝐴)) ·
((cos‘𝐵) ·
(tan‘𝐵)))) | 
| 46 | 27, 36 | oveq12d 7450 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(tan‘𝐴)) ·
((cos‘𝐵) ·
(tan‘𝐵))) =
((sin‘𝐴) ·
(sin‘𝐵))) | 
| 47 | 45, 46 | eqtrd 2776 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) ·
((tan‘𝐴) ·
(tan‘𝐵))) =
((sin‘𝐴) ·
(sin‘𝐵))) | 
| 48 | 44, 47 | oveq12d 7450 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((((cos‘𝐴) ·
(cos‘𝐵)) · 1)
− (((cos‘𝐴)
· (cos‘𝐵))
· ((tan‘𝐴)
· (tan‘𝐵)))) =
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵)))) | 
| 49 | 43, 48 | eqtrd 2776 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((cos‘𝐴) ·
(cos‘𝐵)) · (1
− ((tan‘𝐴)
· (tan‘𝐵)))) =
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵)))) | 
| 50 | 40, 49 | oveq12d 7450 | . . 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 11281 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((tan‘𝐴) +
(tan‘𝐵)) ∈
ℂ) | 
| 52 |  | ax-1cn 11214 | . . . . 5
⊢ 1 ∈
ℂ | 
| 53 |  | subcl 11508 | . . . . 5
⊢ ((1
∈ ℂ ∧ ((tan‘𝐴) · (tan‘𝐵)) ∈ ℂ) → (1 −
((tan‘𝐴) ·
(tan‘𝐵))) ∈
ℂ) | 
| 54 | 52, 42, 53 | sylancr 587 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → (1 −
((tan‘𝐴) ·
(tan‘𝐵))) ∈
ℂ) | 
| 55 |  | tanaddlem 16203 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0))
→ ((cos‘(𝐴 +
𝐵)) ≠ 0 ↔
((tan‘𝐴) ·
(tan‘𝐵)) ≠
1)) | 
| 56 | 55 | 3adantr3 1171 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘(𝐴 + 𝐵)) ≠ 0 ↔
((tan‘𝐴) ·
(tan‘𝐵)) ≠
1)) | 
| 57 | 3, 56 | mpbid 232 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((tan‘𝐴) ·
(tan‘𝐵)) ≠
1) | 
| 58 | 57 | necomd 2995 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → 1 ≠
((tan‘𝐴) ·
(tan‘𝐵))) | 
| 59 |  | subeq0 11536 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ ((tan‘𝐴) · (tan‘𝐵)) ∈ ℂ) → ((1 −
((tan‘𝐴) ·
(tan‘𝐵))) = 0 ↔
1 = ((tan‘𝐴) ·
(tan‘𝐵)))) | 
| 60 | 59 | necon3bid 2984 | . . . . . 6
⊢ ((1
∈ ℂ ∧ ((tan‘𝐴) · (tan‘𝐵)) ∈ ℂ) → ((1 −
((tan‘𝐴) ·
(tan‘𝐵))) ≠ 0
↔ 1 ≠ ((tan‘𝐴) · (tan‘𝐵)))) | 
| 61 | 52, 42, 60 | sylancr 587 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → ((1 −
((tan‘𝐴) ·
(tan‘𝐵))) ≠ 0
↔ 1 ≠ ((tan‘𝐴) · (tan‘𝐵)))) | 
| 62 | 58, 61 | mpbird 257 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) → (1 −
((tan‘𝐴) ·
(tan‘𝐵))) ≠
0) | 
| 63 | 12, 14, 16, 18 | mulne0d 11916 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
((cos‘𝐴) ·
(cos‘𝐵)) ≠
0) | 
| 64 | 51, 54, 15, 62, 63 | divcan5d 12070 | . . 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 2783 | . 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(((tan‘𝐴) +
(tan‘𝐵)) / (1 −
((tan‘𝐴) ·
(tan‘𝐵)))) =
((sin‘(𝐴 + 𝐵)) / (cos‘(𝐴 + 𝐵)))) | 
| 66 | 5, 65 | eqtr4d 2779 | 1
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((cos‘𝐴) ≠ 0 ∧
(cos‘𝐵) ≠ 0 ∧
(cos‘(𝐴 + 𝐵)) ≠ 0)) →
(tan‘(𝐴 + 𝐵)) = (((tan‘𝐴) + (tan‘𝐵)) / (1 − ((tan‘𝐴) · (tan‘𝐵))))) |