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 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A + B = 1 → sin ⁡ A ⁢ π 2 = cos ⁡ B ⁢ π 2

Proof

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