Metamath Proof Explorer


Theorem ren0

Description: The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion ren0
|- RR =/= (/)

Proof

Step Hyp Ref Expression
1 0re
 |-  0 e. RR
2 1 ne0ii
 |-  RR =/= (/)