Theorem dp2clq

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

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

Proof

Step	Hyp	Ref	Expression
1		dp2clq.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp2clq.b	$$⊢B\in \mathbb{Q}$$
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	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Q}$$
5	4 1	sselii	$$⊢A\in \mathbb{Q}$$
6		10nn0	$$⊢10\in {\mathbb{N}}_0$$
7	4 6	sselii	$$⊢10\in \mathbb{Q}$$
8		0re	$$⊢0\in ℝ$$
9		10pos	$$⊢0<10$$
10	8 9	gtneii	$$⊢10\ne 0$$
11		qdivcl	$$⊢\left(B\in \mathbb{Q}\wedge 10\in \mathbb{Q}\wedge 10\ne 0\right)\to \frac{B}{10}\in \mathbb{Q}$$
12	2 7 10 11	mp3an	$$⊢\frac{B}{10}\in \mathbb{Q}$$
13		qaddcl	$$⊢\left(A\in \mathbb{Q}\wedge \frac{B}{10}\in \mathbb{Q}\right)\to A+\left(\frac{B}{10}\right)\in \mathbb{Q}$$
14	5 12 13	mp2an	$$⊢A+\left(\frac{B}{10}\right)\in \mathbb{Q}$$
15	3 14	eqeltri	Could not format _ A B e. QQ : No typesetting found for |- _ A B e. QQ with typecode |-