Description: The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval . (Contributed by David Moews, 28-Feb-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ang.1 | |- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) |
|
| angvald.1 | |- ( ph -> X e. CC ) |
||
| angvald.2 | |- ( ph -> X =/= 0 ) |
||
| angvald.3 | |- ( ph -> Y e. CC ) |
||
| angvald.4 | |- ( ph -> Y =/= 0 ) |
||
| Assertion | angvald | |- ( ph -> ( X F Y ) = ( Im ` ( log ` ( Y / X ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ang.1 | |- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) |
|
| 2 | angvald.1 | |- ( ph -> X e. CC ) |
|
| 3 | angvald.2 | |- ( ph -> X =/= 0 ) |
|
| 4 | angvald.3 | |- ( ph -> Y e. CC ) |
|
| 5 | angvald.4 | |- ( ph -> Y =/= 0 ) |
|
| 6 | 1 | angval | |- ( ( ( X e. CC /\ X =/= 0 ) /\ ( Y e. CC /\ Y =/= 0 ) ) -> ( X F Y ) = ( Im ` ( log ` ( Y / X ) ) ) ) |
| 7 | 2 3 4 5 6 | syl22anc | |- ( ph -> ( X F Y ) = ( Im ` ( log ` ( Y / X ) ) ) ) |