Metamath Proof Explorer


Theorem 1sr

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

Ref Expression
Assertion 1sr 1RR

Proof

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