Theorem m1r

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

	Ref	Expression
Assertion	m1r	⊢ -1R ∈ R

Proof

Step	Hyp	Ref	Expression
1		1pr	⊢ 1P ∈ P
2		addclpr	⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
3	1 1 2	mp2an	⊢ ( 1P +P 1P ) ∈ P
4		opelxpi	⊢ ( ( 1P ∈ P ∧ ( 1P +P 1P ) ∈ P ) → ⟨ 1P , ( 1P +P 1P ) ⟩ ∈ ( P × P ) )
5	1 3 4	mp2an	⊢ ⟨ 1P , ( 1P +P 1P ) ⟩ ∈ ( P × P )
6		enrex	⊢ ~R ∈ V
7	6	ecelqsi	⊢ ( ⟨ 1P , ( 1P +P 1P ) ⟩ ∈ ( P × P ) → [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
8	5 7	ax-mp	⊢ [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R ∈ ( ( P × P ) / ~R )
9		df-m1r	⊢ -1R = [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R
10		df-nr	⊢ R = ( ( P × P ) / ~R )
11	8 9 10	3eltr4i	⊢ -1R ∈ R