Theorem dp2cl

Description: Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015)

	Ref	Expression
Assertion	dp2cl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → _ 𝐴 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		df-dp2	⊢ _ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / ; 1 0 ) )
2		10re	⊢ ; 1 0 ∈ ℝ
3		10pos	⊢ 0 < ; 1 0
4	2 3	gt0ne0ii	⊢ ; 1 0 ≠ 0
5		redivcl	⊢ ( ( 𝐵 ∈ ℝ ∧ ; 1 0 ∈ ℝ ∧ ; 1 0 ≠ 0 ) → ( 𝐵 / ; 1 0 ) ∈ ℝ )
6	2 4 5	mp3an23	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 / ; 1 0 ) ∈ ℝ )
7		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 / ; 1 0 ) ∈ ℝ ) → ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ )
8	6 7	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ )
9	1 8	eqeltrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → _ 𝐴 𝐵 ∈ ℝ )