**Description:** The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999)

Ref | Expression | ||
---|---|---|---|

Hypothesis | recl.1 | $${\u22a2}{A}\in \u2102$$ | |

Assertion | imcli | $${\u22a2}\Im \left({A}\right)\in \mathbb{R}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | recl.1 | $${\u22a2}{A}\in \u2102$$ | |

2 | imcl | $${\u22a2}{A}\in \u2102\to \Im \left({A}\right)\in \mathbb{R}$$ | |

3 | 1 2 | ax-mp | $${\u22a2}\Im \left({A}\right)\in \mathbb{R}$$ |