1sr

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

		Ref	Expression
	Assertion	1sr	$⊢ 1_{𝑹} \in 𝑹$

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

Metamath Proof Explorer