This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0re

Description: The number 0 is real. Remark: the first step could also be ax-icn . See also 0reALT . (Contributed by Eric Schmidt, 21-May-2007) (Revised by Scott Fenton, 3-Jan-2013) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022)

Ref Expression
Assertion 0re 
|- 0 e. RR

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 cnre 
 |-  ( 1 e. CC -> E. x e. RR E. y e. RR 1 = ( x + ( _i x. y ) ) )
3 ax-rnegex 
 |-  ( x e. RR -> E. z e. RR ( x + z ) = 0 )
4 readdcl 
 |-  ( ( x e. RR /\ z e. RR ) -> ( x + z ) e. RR )
5 eleq1 
 |-  ( ( x + z ) = 0 -> ( ( x + z ) e. RR <-> 0 e. RR ) )
6 4 5 syl5ibcom 
 |-  ( ( x e. RR /\ z e. RR ) -> ( ( x + z ) = 0 -> 0 e. RR ) )
7 6 rexlimdva 
 |-  ( x e. RR -> ( E. z e. RR ( x + z ) = 0 -> 0 e. RR ) )
8 3 7 mpd 
 |-  ( x e. RR -> 0 e. RR )
9 8 adantr 
 |-  ( ( x e. RR /\ E. y e. RR 1 = ( x + ( _i x. y ) ) ) -> 0 e. RR )
10 9 rexlimiva 
 |-  ( E. x e. RR E. y e. RR 1 = ( x + ( _i x. y ) ) -> 0 e. RR )
11 1 2 10 mp2b 
 |-  0 e. RR