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	$⊢ (A \in ℝ \land B \in ℝ) \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 (⟨x, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \in ℝ \leftrightarrow A + ⟨y, 0_{𝑹}⟩ \in ℝ)$
5		oveq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to A + ⟨y, 0_{𝑹}⟩ = A + B$
6	5	eleq1d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (A + ⟨y, 0_{𝑹}⟩ \in ℝ \leftrightarrow A + B \in ℝ)$
7		addresr	$⊢ (x \in 𝑹 \land y \in 𝑹) \to ⟨x, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ = ⟨x +_{𝑹} y, 0_{𝑹}⟩$
8		addclsr	$⊢ (x \in 𝑹 \land y \in 𝑹) \to x +_{𝑹} y \in 𝑹$
9		opelreal	$⊢ ⟨x +_{𝑹} y, 0_{𝑹}⟩ \in ℝ \leftrightarrow x +_{𝑹} y \in 𝑹$
10	8 9	sylibr	$⊢ (x \in 𝑹 \land y \in 𝑹) \to ⟨x +_{𝑹} y, 0_{𝑹}⟩ \in ℝ$
11	7 10	eqeltrd	$⊢ (x \in 𝑹 \land y \in 𝑹) \to ⟨x, 0_{𝑹}⟩ + ⟨y, 0_{𝑹}⟩ \in ℝ$
12	1 2 4 6 11	2gencl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$

Metamath Proof Explorer

Theorem axaddrcl

Proof