Description: The absolute value of the imaginary part of a non-real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | absimnre.1 | |- ( ph -> A e. CC ) |
|
| absimnre.2 | |- ( ph -> -. A e. RR ) |
||
| Assertion | absimnre | |- ( ph -> ( abs ` ( Im ` A ) ) e. RR+ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | absimnre.1 | |- ( ph -> A e. CC ) |
|
| 2 | absimnre.2 | |- ( ph -> -. A e. RR ) |
|
| 3 | 1 | imcld | |- ( ph -> ( Im ` A ) e. RR ) |
| 4 | 3 | recnd | |- ( ph -> ( Im ` A ) e. CC ) |
| 5 | reim0b | |- ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) ) |
|
| 6 | 1 5 | syl | |- ( ph -> ( A e. RR <-> ( Im ` A ) = 0 ) ) |
| 7 | 2 6 | mtbid | |- ( ph -> -. ( Im ` A ) = 0 ) |
| 8 | 7 | neqned | |- ( ph -> ( Im ` A ) =/= 0 ) |
| 9 | 4 8 | absrpcld | |- ( ph -> ( abs ` ( Im ` A ) ) e. RR+ ) |