# Metamath Proof Explorer

## Theorem angneg

Description: Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 ${⊢}{F}=\left({x}\in \left(ℂ\setminus \left\{0\right\}\right),{y}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\mathrm{log}\left(\frac{{y}}{{x}}\right)\right)\right)$
Assertion angneg ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(-{A}\right){F}\left(-{B}\right)={A}{F}{B}$

### Proof

Step Hyp Ref Expression
1 ang.1 ${⊢}{F}=\left({x}\in \left(ℂ\setminus \left\{0\right\}\right),{y}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\mathrm{log}\left(\frac{{y}}{{x}}\right)\right)\right)$
2 mulm1 ${⊢}{A}\in ℂ\to -1{A}=-{A}$
3 2 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to -1{A}=-{A}$
4 mulm1 ${⊢}{B}\in ℂ\to -1{B}=-{B}$
5 4 ad2antrl ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to -1{B}=-{B}$
6 3 5 oveq12d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to -1{A}{F}-1{B}=\left(-{A}\right){F}\left(-{B}\right)$
7 neg1cn ${⊢}-1\in ℂ$
8 neg1ne0 ${⊢}-1\ne 0$
9 7 8 pm3.2i ${⊢}\left(-1\in ℂ\wedge -1\ne 0\right)$
10 1 angcan ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left(-1\in ℂ\wedge -1\ne 0\right)\right)\to -1{A}{F}-1{B}={A}{F}{B}$
11 9 10 mp3an3 ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to -1{A}{F}-1{B}={A}{F}{B}$
12 6 11 eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(-{A}\right){F}\left(-{B}\right)={A}{F}{B}$