Theorem 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	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , 0R ⟩ )

Proof

Step	Hyp	Ref	Expression
1		0r	⊢ 0R ∈ R
2		addcnsr	⊢ ( ( ( 𝐴 ∈ R ∧ 0R ∈ R ) ∧ ( 𝐵 ∈ R ∧ 0R ∈ R ) ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ )
3	2	an4s	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 0R ∈ R ∧ 0R ∈ R ) ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ )
4	1 1 3	mpanr12	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ )
5		0idsr	⊢ ( 0R ∈ R → ( 0R +R 0R ) = 0R )
6	1 5	ax-mp	⊢ ( 0R +R 0R ) = 0R
7	6	opeq2i	⊢ ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ = ⟨ ( 𝐴 +R 𝐵 ) , 0R ⟩
8	4 7	eqtrdi	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , 0R ⟩ )