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

Metamath Proof Explorer

Theorem sincosq1eq

Description: Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008)

Ref Expression
Assertion sincosq1eq ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( sin ‘ ( 𝐴 · ( π / 2 ) ) ) = ( cos ‘ ( 𝐵 · ( π / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 2cn ⊢ 2 ∈ ℂ
3 2ne0 ⊢ 2 ≠ 0
4 1 2 3 divcli ⊢ ( π / 2 ) ∈ ℂ
5 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( π / 2 ) ∈ ℂ ) → ( 𝐴 · ( π / 2 ) ) ∈ ℂ )
6 4 5 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( π / 2 ) ) ∈ ℂ )
7 coshalfpim ⊢ ( ( 𝐴 · ( π / 2 ) ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) ) = ( sin ‘ ( 𝐴 · ( π / 2 ) ) ) )
8 6 7 syl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) ) = ( sin ‘ ( 𝐴 · ( π / 2 ) ) ) )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( cos ‘ ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) ) = ( sin ‘ ( 𝐴 · ( π / 2 ) ) ) )
10 adddir ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( π / 2 ) ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( π / 2 ) ) = ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) )
11 4 10 mp3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( π / 2 ) ) = ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) )
12 11 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( ( 𝐴 + 𝐵 ) · ( π / 2 ) ) = ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) )
13 oveq1 ⊢ ( ( 𝐴 + 𝐵 ) = 1 → ( ( 𝐴 + 𝐵 ) · ( π / 2 ) ) = ( 1 · ( π / 2 ) ) )
14 4 mullidi ⊢ ( 1 · ( π / 2 ) ) = ( π / 2 )
15 13 14 eqtrdi ⊢ ( ( 𝐴 + 𝐵 ) = 1 → ( ( 𝐴 + 𝐵 ) · ( π / 2 ) ) = ( π / 2 ) )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( ( 𝐴 + 𝐵 ) · ( π / 2 ) ) = ( π / 2 ) )
17 12 16 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) = ( π / 2 ) )
18 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ ( π / 2 ) ∈ ℂ ) → ( 𝐵 · ( π / 2 ) ) ∈ ℂ )
19 4 18 mpan2 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · ( π / 2 ) ) ∈ ℂ )
20 subadd ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ ( 𝐴 · ( π / 2 ) ) ∈ ℂ ∧ ( 𝐵 · ( π / 2 ) ) ∈ ℂ ) → ( ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) = ( 𝐵 · ( π / 2 ) ) ↔ ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) = ( π / 2 ) ) )
21 4 6 19 20 mp3an3an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) = ( 𝐵 · ( π / 2 ) ) ↔ ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) = ( π / 2 ) ) )
22 21 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) = ( 𝐵 · ( π / 2 ) ) ↔ ( ( 𝐴 · ( π / 2 ) ) + ( 𝐵 · ( π / 2 ) ) ) = ( π / 2 ) ) )
23 17 22 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) = ( 𝐵 · ( π / 2 ) ) )
24 23 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( cos ‘ ( ( π / 2 ) − ( 𝐴 · ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐵 · ( π / 2 ) ) ) )
25 9 24 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) = 1 ) → ( sin ‘ ( 𝐴 · ( π / 2 ) ) ) = ( cos ‘ ( 𝐵 · ( π / 2 ) ) ) )