Theorem axaddrcl

Description: Closure law for addition in the real subfield of complex numbers. Axiom 5 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl be used later. Instead, in most cases use readdcl . (Contributed by NM, 31-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	axaddrcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elreal	$$⊢A\in ℝ\leftrightarrow \exists x\in 𝑹⟨x,0_{𝑹}⟩=A$$
2		elreal	$$⊢B\in ℝ\leftrightarrow \exists y\in 𝑹⟨y,0_{𝑹}⟩=B$$
3		oveq1	$$⊢⟨x,0_{𝑹}⟩=A\to ⟨x,0_{𝑹}⟩+⟨y,0_{𝑹}⟩=A+⟨y,0_{𝑹}⟩$$
4	3	eleq1d	$$⊢⟨x,0_{𝑹}⟩=A\to \left(⟨x,0_{𝑹}⟩+⟨y,0_{𝑹}⟩\in ℝ\leftrightarrow A+⟨y,0_{𝑹}⟩\in ℝ\right)$$
5		oveq2	$$⊢⟨y,0_{𝑹}⟩=B\to A+⟨y,0_{𝑹}⟩=A+B$$
6	5	eleq1d	$$⊢⟨y,0_{𝑹}⟩=B\to \left(A+⟨y,0_{𝑹}⟩\in ℝ\leftrightarrow A+B\in ℝ\right)$$
7		addresr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to ⟨x,0_{𝑹}⟩+⟨y,0_{𝑹}⟩=⟨x{+}_{𝑹}y,0_{𝑹}⟩$$
8		addclsr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to x{+}_{𝑹}y\in 𝑹$$
9		opelreal	$$⊢⟨x{+}_{𝑹}y,0_{𝑹}⟩\in ℝ\leftrightarrow x{+}_{𝑹}y\in 𝑹$$
10	8 9	sylibr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to ⟨x{+}_{𝑹}y,0_{𝑹}⟩\in ℝ$$
11	7 10	eqeltrd	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to ⟨x,0_{𝑹}⟩+⟨y,0_{𝑹}⟩\in ℝ$$
12	1 2 4 6 11	2gencl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B\in ℝ$$