Theorem 0r

Description: The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	0r	$$⊢0_{𝑹}\in 𝑹$$

Proof

Step	Hyp	Ref	Expression
1		1pr	$$⊢1_{𝑷}\in 𝑷$$
2		opelxpi	$$⊢\left(1_{𝑷}\in 𝑷\wedge 1_{𝑷}\in 𝑷\right)\to ⟨1_{𝑷},1_{𝑷}⟩\in \left(𝑷\times 𝑷\right)$$
3	1 1 2	mp2an	$$⊢⟨1_{𝑷},1_{𝑷}⟩\in \left(𝑷\times 𝑷\right)$$
4		enrex	$$⊢{~}_{𝑹}\in \mathrm{V}$$
5	4	ecelqsi	$$⊢⟨1_{𝑷},1_{𝑷}⟩\in \left(𝑷\times 𝑷\right)\to \left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}\in \left(\left(𝑷\times 𝑷\right)/{~}_{𝑹}\right)$$
6	3 5	ax-mp	$$⊢\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}\in \left(\left(𝑷\times 𝑷\right)/{~}_{𝑹}\right)$$
7		df-0r	$$⊢0_{𝑹}=\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}$$
8		df-nr	$$⊢𝑹=\left(𝑷\times 𝑷\right)/{~}_{𝑹}$$
9	6 7 8	3eltr4i	$$⊢0_{𝑹}\in 𝑹$$