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}_{𝑹} \cdot_{𝑹} {-1}_{𝑹} = 1_{𝑹}$

Proof

Step	Hyp	Ref	Expression
1		df-m1r	$⊢ {-1}_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
2	1 1	oveq12i	$⊢ {-1}_{𝑹} \cdot_{𝑹} {-1}_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
3		df-1r	$⊢ 1_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
4		1pr	$⊢ 1_{𝑷} \in 𝑷$
5		addclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
6	4 4 5	mp2an	$⊢ 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
7		mulsrpr	$⊢ ((1_{𝑷} \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \land (1_{𝑷} \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷)) \to [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} = [⟨(1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})), (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹}$
8	4 6 4 6 7	mp4an	$⊢ [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} = [⟨(1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})), (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹}$
9		addasspr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})) = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})))$
10		1idpr	$⊢ 1_{𝑷} \in 𝑷 \to 1_{𝑷} \cdot_{𝑷} 1_{𝑷} = 1_{𝑷}$
11	4 10	ax-mp	$⊢ 1_{𝑷} \cdot_{𝑷} 1_{𝑷} = 1_{𝑷}$
12		distrpr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})$
13		mulcompr	$⊢ 1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}$
14	13	oveq1i	$⊢ (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}) = ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})$
15	12 14	eqtr4i	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})$
16	11 15	oveq12i	$⊢ (1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) = 1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}))$
17	16	oveq2i	$⊢ 1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))) = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})))$
18	9 17	eqtr4i	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})) = 1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})))$
19		mulclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to 1_{𝑷} \cdot_{𝑷} 1_{𝑷} \in 𝑷$
20	4 4 19	mp2an	$⊢ 1_{𝑷} \cdot_{𝑷} 1_{𝑷} \in 𝑷$
21		mulclpr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \to (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
22	6 6 21	mp2an	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
23		addclpr	$⊢ (1_{𝑷} \cdot_{𝑷} 1_{𝑷} \in 𝑷 \land (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷) \to (1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷$
24	20 22 23	mp2an	$⊢ (1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷$
25		mulclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \to 1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
26	4 6 25	mp2an	$⊢ 1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
27		mulclpr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷} \in 𝑷$
28	6 4 27	mp2an	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷} \in 𝑷$
29		addclpr	$⊢ (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷 \land (1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷} \in 𝑷) \to (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
30	26 28 29	mp2an	$⊢ (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
31		enreceq	$⊢ ((1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \land ((1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷 \land (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷}) \in 𝑷)) \to ([⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})), (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} \leftrightarrow (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})) = 1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))))$
32	6 4 24 30 31	mp4an	$⊢ [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})), (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} \leftrightarrow (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})) = 1_{𝑷} +_{𝑷} ((1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})))$
33	18 32	mpbir	$⊢ [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(1_{𝑷} \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})), (1_{𝑷} \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹}$
34	8 33	eqtr4i	$⊢ [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
35	3 34	eqtr4i	$⊢ 1_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
36	2 35	eqtr4i	$⊢ {-1}_{𝑹} \cdot_{𝑹} {-1}_{𝑹} = 1_{𝑹}$

Metamath Proof Explorer

Theorem m1m1sr

Proof