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 \|-

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 \neq 0$
5		redivcl	$⊢ (B \in ℝ \land 10 \in ℝ \land 10 \neq 0) \to \frac{B}{10} \in ℝ$
6	2 4 5	mp3an23	$⊢ B \in ℝ \to \frac{B}{10} \in ℝ$
7		readdcl	$⊢ (A \in ℝ \land \frac{B}{10} \in ℝ) \to A + (\frac{B}{10}) \in ℝ$
8	6 7	sylan2	$⊢ (A \in ℝ \land B \in ℝ) \to A + (\frac{B}{10}) \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 \|-

Metamath Proof Explorer