Theorem addclsr

Description: Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addclsr	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) ∈ R )

Proof

Step	Hyp	Ref	Expression
1		df-nr	⊢ R = ( ( P × P ) / ~R )
2		oveq1	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
3	2	eleq1d	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ↔ ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ) )
4		oveq2	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 +R 𝐵 ) )
5	4	eleq1d	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ↔ ( 𝐴 +R 𝐵 ) ∈ ( ( P × P ) / ~R ) ) )
6		addsrpr	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R )
7		addclpr	⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 +P 𝑧 ) ∈ P )
8		addclpr	⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 +P 𝑤 ) ∈ P )
9	7 8	anim12i	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) )
10	9	an4s	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) )
11		opelxpi	⊢ ( ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) → ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ∈ ( P × P ) )
12		enrex	⊢ ~R ∈ V
13	12	ecelqsi	⊢ ( ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ∈ ( P × P ) → [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
14	10 11 13	3syl	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
15	6 14	eqeltrd	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) )
16	1 3 5 15	2ecoptocl	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) ∈ ( ( P × P ) / ~R ) )
17	16 1	eleqtrrdi	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) ∈ R )