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	Could not format assertion : No typesetting found for |- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
2		10re	$$⊢10\in ℝ$$
3		10pos	$$⊢0<10$$
4	2 3	gt0ne0ii	$$⊢10\ne 0$$
5		redivcl	$$⊢\left(B\in ℝ\wedge 10\in ℝ\wedge 10\ne 0\right)\to \frac{B}{10}\in ℝ$$
6	2 4 5	mp3an23	$$⊢B\in ℝ\to \frac{B}{10}\in ℝ$$
7		readdcl	$$⊢\left(A\in ℝ\wedge \frac{B}{10}\in ℝ\right)\to A+\left(\frac{B}{10}\right)\in ℝ$$
8	6 7	sylan2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(\frac{B}{10}\right)\in ℝ$$
9	1 8	eqeltrid	Could not format ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) : No typesetting found for |- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) with typecode |-