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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elreal	⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
2		elreal	⊢ ( 𝐵 ∈ ℝ ↔ ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐵 )
3		oveq1	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) = ( 𝐴 + ⟨ 𝑦 , 0R ⟩ ) )
4	3	eleq1d	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ ↔ ( 𝐴 + ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ ) )
5		oveq2	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 + ⟨ 𝑦 , 0R ⟩ ) = ( 𝐴 + 𝐵 ) )
6	5	eleq1d	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 𝐴 + ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ ↔ ( 𝐴 + 𝐵 ) ∈ ℝ ) )
7		addresr	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) = ⟨ ( 𝑥 +R 𝑦 ) , 0R ⟩ )
8		addclsr	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( 𝑥 +R 𝑦 ) ∈ R )
9		opelreal	⊢ ( ⟨ ( 𝑥 +R 𝑦 ) , 0R ⟩ ∈ ℝ ↔ ( 𝑥 +R 𝑦 ) ∈ R )
10	8 9	sylibr	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ⟨ ( 𝑥 +R 𝑦 ) , 0R ⟩ ∈ ℝ )
11	7 10	eqeltrd	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ + ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ )
12	1 2 4 6 11	2gencl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )