m1m1sr

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

		Ref	Expression
	Assertion	m1m1sr	⊢ ( -1_R ·_R -1_R ) = 1_R

Proof

Step	Hyp	Ref	Expression
1		df-m1r	⊢ -1_R = [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R
2	1 1	oveq12i	⊢ ( -1_R ·_R -1_R ) = ( [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ·_R [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R )
3		df-1r	⊢ 1_R = [ ⟨ ( 1_P +_P 1_P ) , 1_P ⟩ ] ~_R
4		1pr	⊢ 1_P ∈ P
5		addclpr	⊢ ( ( 1_P ∈ P ∧ 1_P ∈ P ) → ( 1_P +_P 1_P ) ∈ P )
6	4 4 5	mp2an	⊢ ( 1_P +_P 1_P ) ∈ P
7		mulsrpr	⊢ ( ( ( 1_P ∈ P ∧ ( 1_P +_P 1_P ) ∈ P ) ∧ ( 1_P ∈ P ∧ ( 1_P +_P 1_P ) ∈ P ) ) → ( [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ·_R [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ) = [ ⟨ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) , ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ⟩ ] ~_R )
8	4 6 4 6 7	mp4an	⊢ ( [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ·_R [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ) = [ ⟨ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) , ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ⟩ ] ~_R
9		addasspr	⊢ ( ( 1_P +_P 1_P ) +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ) = ( 1_P +_P ( 1_P +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ) )
10		1idpr	⊢ ( 1_P ∈ P → ( 1_P ·_P 1_P ) = 1_P )
11	4 10	ax-mp	⊢ ( 1_P ·_P 1_P ) = 1_P
12		distrpr	⊢ ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) = ( ( ( 1_P +_P 1_P ) ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) )
13		mulcompr	⊢ ( 1_P ·_P ( 1_P +_P 1_P ) ) = ( ( 1_P +_P 1_P ) ·_P 1_P )
14	13	oveq1i	⊢ ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) = ( ( ( 1_P +_P 1_P ) ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) )
15	12 14	eqtr4i	⊢ ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) = ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) )
16	11 15	oveq12i	⊢ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) = ( 1_P +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) )
17	16	oveq2i	⊢ ( 1_P +_P ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) ) = ( 1_P +_P ( 1_P +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ) )
18	9 17	eqtr4i	⊢ ( ( 1_P +_P 1_P ) +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ) = ( 1_P +_P ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) )
19		mulclpr	⊢ ( ( 1_P ∈ P ∧ 1_P ∈ P ) → ( 1_P ·_P 1_P ) ∈ P )
20	4 4 19	mp2an	⊢ ( 1_P ·_P 1_P ) ∈ P
21		mulclpr	⊢ ( ( ( 1_P +_P 1_P ) ∈ P ∧ ( 1_P +_P 1_P ) ∈ P ) → ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ∈ P )
22	6 6 21	mp2an	⊢ ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ∈ P
23		addclpr	⊢ ( ( ( 1_P ·_P 1_P ) ∈ P ∧ ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ∈ P ) → ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) ∈ P )
24	20 22 23	mp2an	⊢ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) ∈ P
25		mulclpr	⊢ ( ( 1_P ∈ P ∧ ( 1_P +_P 1_P ) ∈ P ) → ( 1_P ·_P ( 1_P +_P 1_P ) ) ∈ P )
26	4 6 25	mp2an	⊢ ( 1_P ·_P ( 1_P +_P 1_P ) ) ∈ P
27		mulclpr	⊢ ( ( ( 1_P +_P 1_P ) ∈ P ∧ 1_P ∈ P ) → ( ( 1_P +_P 1_P ) ·_P 1_P ) ∈ P )
28	6 4 27	mp2an	⊢ ( ( 1_P +_P 1_P ) ·_P 1_P ) ∈ P
29		addclpr	⊢ ( ( ( 1_P ·_P ( 1_P +_P 1_P ) ) ∈ P ∧ ( ( 1_P +_P 1_P ) ·_P 1_P ) ∈ P ) → ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ∈ P )
30	26 28 29	mp2an	⊢ ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ∈ P
31		enreceq	⊢ ( ( ( ( 1_P +_P 1_P ) ∈ P ∧ 1_P ∈ P ) ∧ ( ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) ∈ P ∧ ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ∈ P ) ) → ( [ ⟨ ( 1_P +_P 1_P ) , 1_P ⟩ ] ~_R = [ ⟨ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) , ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ⟩ ] ~_R ↔ ( ( 1_P +_P 1_P ) +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ) = ( 1_P +_P ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) ) ) )
32	6 4 24 30 31	mp4an	⊢ ( [ ⟨ ( 1_P +_P 1_P ) , 1_P ⟩ ] ~_R = [ ⟨ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) , ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ⟩ ] ~_R ↔ ( ( 1_P +_P 1_P ) +_P ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ) = ( 1_P +_P ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) ) )
33	18 32	mpbir	⊢ [ ⟨ ( 1_P +_P 1_P ) , 1_P ⟩ ] ~_R = [ ⟨ ( ( 1_P ·_P 1_P ) +_P ( ( 1_P +_P 1_P ) ·_P ( 1_P +_P 1_P ) ) ) , ( ( 1_P ·_P ( 1_P +_P 1_P ) ) +_P ( ( 1_P +_P 1_P ) ·_P 1_P ) ) ⟩ ] ~_R
34	8 33	eqtr4i	⊢ ( [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ·_R [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ) = [ ⟨ ( 1_P +_P 1_P ) , 1_P ⟩ ] ~_R
35	3 34	eqtr4i	⊢ 1_R = ( [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R ·_R [ ⟨ 1_P , ( 1_P +_P 1_P ) ⟩ ] ~_R )
36	2 35	eqtr4i	⊢ ( -1_R ·_R -1_R ) = 1_R

Metamath Proof Explorer

Theorem m1m1sr

Proof