Metamath Proof Explorer

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 ⊢ φ → A ∈ ℂ
tanhalfpim.1 ⊢ φ → sin ⁡ A ≠ 0
Assertion tanhalfpim ⊢ φ → tan ⁡ π 2 − A = cos ⁡ A sin ⁡ A

Proof

Step Hyp Ref Expression
1 tanhalfpim.a ⊢ φ → A ∈ ℂ
2 tanhalfpim.1 ⊢ φ → sin ⁡ A ≠ 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 − A ∈ ℂ
9 coshalfpim ⊢ A ∈ ℂ → cos ⁡ π 2 − A = sin ⁡ A
10 1 9 syl ⊢ φ → cos ⁡ π 2 − A = sin ⁡ A
11 10 2 eqnetrd ⊢ φ → cos ⁡ π 2 − A ≠ 0
12 tanval ⊢ π 2 − A ∈ ℂ ∧ cos ⁡ π 2 − A ≠ 0 → tan ⁡ π 2 − A = sin ⁡ π 2 − A cos ⁡ π 2 − A
13 8 11 12 syl2anc ⊢ φ → tan ⁡ π 2 − A = sin ⁡ π 2 − A cos ⁡ π 2 − A
14 sinhalfpim ⊢ A ∈ ℂ → sin ⁡ π 2 − A = cos ⁡ A
15 14 9 oveq12d ⊢ A ∈ ℂ → sin ⁡ π 2 − A cos ⁡ π 2 − A = cos ⁡ A sin ⁡ A
16 1 15 syl ⊢ φ → sin ⁡ π 2 − A cos ⁡ π 2 − A = cos ⁡ A sin ⁡ A
17 13 16 eqtrd ⊢ φ → tan ⁡ π 2 − A = cos ⁡ A sin ⁡ A