addresr

Description: Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	addresr	$⊢ (A \in 𝑹 \land B \in 𝑹) \to ⟨A, 0_{𝑹}⟩ + ⟨B, 0_{𝑹}⟩ = ⟨A +_{𝑹} B, 0_{𝑹}⟩$

Step	Hyp	Ref	Expression
1		0r	$⊢ 0_{𝑹} \in 𝑹$
2		addcnsr	$⊢ ((A \in 𝑹 \land 0_{𝑹} \in 𝑹) \land (B \in 𝑹 \land 0_{𝑹} \in 𝑹)) \to ⟨A, 0_{𝑹}⟩ + ⟨B, 0_{𝑹}⟩ = ⟨A +_{𝑹} B, 0_{𝑹} +_{𝑹} 0_{𝑹}⟩$
3	2	an4s	$⊢ ((A \in 𝑹 \land B \in 𝑹) \land (0_{𝑹} \in 𝑹 \land 0_{𝑹} \in 𝑹)) \to ⟨A, 0_{𝑹}⟩ + ⟨B, 0_{𝑹}⟩ = ⟨A +_{𝑹} B, 0_{𝑹} +_{𝑹} 0_{𝑹}⟩$
4	1 1 3	mpanr12	$⊢ (A \in 𝑹 \land B \in 𝑹) \to ⟨A, 0_{𝑹}⟩ + ⟨B, 0_{𝑹}⟩ = ⟨A +_{𝑹} B, 0_{𝑹} +_{𝑹} 0_{𝑹}⟩$
5		0idsr	$⊢ 0_{𝑹} \in 𝑹 \to 0_{𝑹} +_{𝑹} 0_{𝑹} = 0_{𝑹}$
6	1 5	ax-mp	$⊢ 0_{𝑹} +_{𝑹} 0_{𝑹} = 0_{𝑹}$
7	6	opeq2i	$⊢ ⟨A +_{𝑹} B, 0_{𝑹} +_{𝑹} 0_{𝑹}⟩ = ⟨A +_{𝑹} B, 0_{𝑹}⟩$
8	4 7	eqtrdi	$⊢ (A \in 𝑹 \land B \in 𝑹) \to ⟨A, 0_{𝑹}⟩ + ⟨B, 0_{𝑹}⟩ = ⟨A +_{𝑹} B, 0_{𝑹}⟩$

Metamath Proof Explorer