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

Metamath Proof Explorer

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