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	mulid2i	⊢ ( 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 ) ) ) )