This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 +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 ⊢ 1R ∈ R