Metamath Proof Explorer


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 0RR
2 addcnsr ( ( ( 𝐴R ∧ 0RR ) ∧ ( 𝐵R ∧ 0RR ) ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ )
3 2 an4s ( ( ( 𝐴R𝐵R ) ∧ ( 0RR ∧ 0RR ) ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ )
4 1 1 3 mpanr12 ( ( 𝐴R𝐵R ) → ( ⟨ 𝐴 , 0R ⟩ + ⟨ 𝐵 , 0R ⟩ ) = ⟨ ( 𝐴 +R 𝐵 ) , ( 0R +R 0R ) ⟩ )
5 0idsr ( 0RR → ( 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 ⟩ )