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	$⊢ {-1}_{𝑹} +_{𝑹} 1_{𝑹} = 0_{𝑹}$

Proof

Step	Hyp	Ref	Expression
1		df-m1r	$⊢ {-1}_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
2		df-1r	$⊢ 1_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
3	1 2	oveq12i	$⊢ {-1}_{𝑹} +_{𝑹} 1_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
4		df-0r	$⊢ 0_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
5		1pr	$⊢ 1_{𝑷} \in 𝑷$
6		addclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
7	5 5 6	mp2an	$⊢ 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
8		addsrpr	$⊢ ((1_{𝑷} \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \land (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}), (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
9	5 7 7 5 8	mp4an	$⊢ [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}), (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
10		addasspr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷} = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})$
11	10	oveq2i	$⊢ 1_{𝑷} +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}) = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))$
12		addclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \to 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
13	5 7 12	mp2an	$⊢ 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
14		addclpr	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷} \in 𝑷$
15	7 5 14	mp2an	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷} \in 𝑷$
16		enreceq	$⊢ ((1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \land (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷 \land (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷} \in 𝑷)) \to ([⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}), (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow 1_{𝑷} +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}) = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})))$
17	5 5 13 15 16	mp4an	$⊢ [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}), (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow 1_{𝑷} +_{𝑷} ((1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}) = 1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))$
18	11 17	mpbir	$⊢ [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}), (1_{𝑷} +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
19	9 18	eqtr4i	$⊢ [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
20	4 19	eqtr4i	$⊢ 0_{𝑹} = [⟨1_{𝑷}, 1_{𝑷} +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
21	3 20	eqtr4i	$⊢ {-1}_{𝑹} +_{𝑹} 1_{𝑹} = 0_{𝑹}$

Metamath Proof Explorer

Theorem m1p1sr

Proof