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

Metamath Proof Explorer

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