**Description:** An integer is an extended real number. (Contributed by Glauco
Siliprandi, 2-Jan-2022)

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

Hypothesis | zxrd.1 | $${\u22a2}{\phi}\to {A}\in \mathbb{Z}$$ | |

Assertion | zxrd | $${\u22a2}{\phi}\to {A}\in {\mathbb{R}}^{*}$$ |

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

1 | zxrd.1 | $${\u22a2}{\phi}\to {A}\in \mathbb{Z}$$ | |

2 | 1 | zred | $${\u22a2}{\phi}\to {A}\in \mathbb{R}$$ |

3 | 2 | rexrd | $${\u22a2}{\phi}\to {A}\in {\mathbb{R}}^{*}$$ |