Metamath Proof Explorer

Theorem m1p1sr

Description: Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996) (New usage is discouraged.)

Ref Expression
Assertion m1p1sr ( -1R +R 1R ) = 0R

Proof

Step Hyp Ref Expression
1 df-m1r ⊢ -1R = [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R
2 df-1r ⊢ 1R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R
3 1 2 oveq12i ⊢ ( -1R +R 1R ) = ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R +R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
4 df-0r ⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
5 1pr ⊢ 1P ∈ P
6 addclpr ⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
7 5 5 6 mp2an ⊢ ( 1P +P 1P ) ∈ P
8 addsrpr ⊢ ( ( ( 1P ∈ P ∧ ( 1P +P 1P ) ∈ P ) ∧ ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R +R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( 1P +P ( 1P +P 1P ) ) , ( ( 1P +P 1P ) +P 1P ) ⟩ ] ~R )
9 5 7 7 5 8 mp4an ⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R +R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( 1P +P ( 1P +P 1P ) ) , ( ( 1P +P 1P ) +P 1P ) ⟩ ] ~R
10 addasspr ⊢ ( ( 1P +P 1P ) +P 1P ) = ( 1P +P ( 1P +P 1P ) )
11 10 oveq2i ⊢ ( 1P +P ( ( 1P +P 1P ) +P 1P ) ) = ( 1P +P ( 1P +P ( 1P +P 1P ) ) )
12 addclpr ⊢ ( ( 1P ∈ P ∧ ( 1P +P 1P ) ∈ P ) → ( 1P +P ( 1P +P 1P ) ) ∈ P )
13 5 7 12 mp2an ⊢ ( 1P +P ( 1P +P 1P ) ) ∈ P
14 addclpr ⊢ ( ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) → ( ( 1P +P 1P ) +P 1P ) ∈ P )
15 7 5 14 mp2an ⊢ ( ( 1P +P 1P ) +P 1P ) ∈ P
16 enreceq ⊢ ( ( ( 1P ∈ P ∧ 1P ∈ P ) ∧ ( ( 1P +P ( 1P +P 1P ) ) ∈ P ∧ ( ( 1P +P 1P ) +P 1P ) ∈ P ) ) → ( [ ⟨ 1P , 1P ⟩ ] ~R = [ ⟨ ( 1P +P ( 1P +P 1P ) ) , ( ( 1P +P 1P ) +P 1P ) ⟩ ] ~R ↔ ( 1P +P ( ( 1P +P 1P ) +P 1P ) ) = ( 1P +P ( 1P +P ( 1P +P 1P ) ) ) ) )
17 5 5 13 15 16 mp4an ⊢ ( [ ⟨ 1P , 1P ⟩ ] ~R = [ ⟨ ( 1P +P ( 1P +P 1P ) ) , ( ( 1P +P 1P ) +P 1P ) ⟩ ] ~R ↔ ( 1P +P ( ( 1P +P 1P ) +P 1P ) ) = ( 1P +P ( 1P +P ( 1P +P 1P ) ) ) )
18 11 17 mpbir ⊢ [ ⟨ 1P , 1P ⟩ ] ~R = [ ⟨ ( 1P +P ( 1P +P 1P ) ) , ( ( 1P +P 1P ) +P 1P ) ⟩ ] ~R
19 9 18 eqtr4i ⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R +R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ 1P , 1P ⟩ ] ~R
20 4 19 eqtr4i ⊢ 0R = ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R +R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
21 3 20 eqtr4i ⊢ ( -1R +R 1R ) = 0R