This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ↔ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ≠ 1 ) )

Proof

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