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