Theorem elre0re

Description: Specialized version of 0red without using ax-1cn and ax-cnre . (Contributed by Steven Nguyen, 28-Jan-2023)

	Ref	Expression
Assertion	elre0re	|- ( A e. RR -> 0 e. RR )

Proof

Step	Hyp	Ref	Expression
1		ax-rnegex	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
2		readdcl	|- ( ( A e. RR /\ x e. RR ) -> ( A + x ) e. RR )
3		eleq1	|- ( ( A + x ) = 0 -> ( ( A + x ) e. RR <-> 0 e. RR ) )
4	2 3	syl5ibcom	|- ( ( A e. RR /\ x e. RR ) -> ( ( A + x ) = 0 -> 0 e. RR ) )
5	4	rexlimdva	|- ( A e. RR -> ( E. x e. RR ( A + x ) = 0 -> 0 e. RR ) )
6	1 5	mpd	|- ( A e. RR -> 0 e. RR )