dp2clq

Description: Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dp2clq.a	$⊢ A \in ℕ_{0}$
	dp2clq.b	$⊢ B \in ℚ$
Assertion	dp2clq	Could not format assertion : No typesetting found for \|- _ A B e. QQ with typecode \|-

Step	Hyp	Ref	Expression
1		dp2clq.a	$⊢ A \in ℕ_{0}$
2		dp2clq.b	$⊢ B \in ℚ$
3		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for \|- _ A B = ( A + ( B / ; 1 0 ) ) with typecode \|-
4		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
5	4 1	sselii	$⊢ A \in ℚ$
6		10nn0	$⊢ 10 \in ℕ_{0}$
7	4 6	sselii	$⊢ 10 \in ℚ$
8		0re	$⊢ 0 \in ℝ$
9		10pos	$⊢ 0 < 10$
10	8 9	gtneii	$⊢ 10 \neq 0$
11		qdivcl	$⊢ (B \in ℚ \land 10 \in ℚ \land 10 \neq 0) \to \frac{B}{10} \in ℚ$
12	2 7 10 11	mp3an	$⊢ \frac{B}{10} \in ℚ$
13		qaddcl	$⊢ (A \in ℚ \land \frac{B}{10} \in ℚ) \to A + (\frac{B}{10}) \in ℚ$
14	5 12 13	mp2an	$⊢ A + (\frac{B}{10}) \in ℚ$
15	3 14	eqeltri	Could not format _ A B e. QQ : No typesetting found for \|- _ A B e. QQ with typecode \|-

Metamath Proof Explorer