This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 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 ⟩ )