Theorem tanhalfpim

Description: The tangent of _pi / 2 minus a number is the cotangent, here represented by cos A / sin A . (Contributed by SN, 2-Sep-2025)

	Ref	Expression
Hypotheses	tanhalfpim.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	tanhalfpim.1	⊢ ( 𝜑 → ( sin ‘ 𝐴 ) ≠ 0 )
Assertion	tanhalfpim	⊢ ( 𝜑 → ( tan ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tanhalfpim.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		tanhalfpim.1	⊢ ( 𝜑 → ( sin ‘ 𝐴 ) ≠ 0 )
3		picn	⊢ π ∈ ℂ
4		2cn	⊢ 2 ∈ ℂ
5		2ne0	⊢ 2 ≠ 0
6	3 4 5	divcli	⊢ ( π / 2 ) ∈ ℂ
7	6	a1i	⊢ ( 𝜑 → ( π / 2 ) ∈ ℂ )
8	7 1	subcld	⊢ ( 𝜑 → ( ( π / 2 ) − 𝐴 ) ∈ ℂ )
9		coshalfpim	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )
10	1 9	syl	⊢ ( 𝜑 → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )
11	10 2	eqnetrd	⊢ ( 𝜑 → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) ≠ 0 )
12		tanval	⊢ ( ( ( ( π / 2 ) − 𝐴 ) ∈ ℂ ∧ ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) ≠ 0 ) → ( tan ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) / ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) ) )
13	8 11 12	syl2anc	⊢ ( 𝜑 → ( tan ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) / ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) ) )
14		sinhalfpim	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )
15	14 9	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) / ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
16	1 15	syl	⊢ ( 𝜑 → ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) / ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
17	13 16	eqtrd	⊢ ( 𝜑 → ( tan ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )