**Description:** The number 4 is real. (Contributed by NM, 27-May-1999)

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

Assertion | 4re | $${\u22a2}4\in \mathbb{R}$$ |

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

1 | df-4 | $${\u22a2}4=3+1$$ | |

2 | 3re | $${\u22a2}3\in \mathbb{R}$$ | |

3 | 1re | $${\u22a2}1\in \mathbb{R}$$ | |

4 | 2 3 | readdcli | $${\u22a2}3+1\in \mathbb{R}$$ |

5 | 1 4 | eqeltri | $${\u22a2}4\in \mathbb{R}$$ |