Metamath Proof Explorer


Theorem dp2clq

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

Ref Expression
Hypotheses dp2clq.a A0
dp2clq.b B
Assertion dp2clq Could not format assertion : No typesetting found for |- _ A B e. QQ with typecode |-

Proof

Step Hyp Ref Expression
1 dp2clq.a A0
2 dp2clq.b B
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
5 4 1 sselii A
6 10nn0 100
7 4 6 sselii 10
8 0re 0
9 10pos 0<10
10 8 9 gtneii 100
11 qdivcl B10100B10
12 2 7 10 11 mp3an B10
13 qaddcl AB10A+B10
14 5 12 13 mp2an A+B10
15 3 14 eqeltri Could not format _ A B e. QQ : No typesetting found for |- _ A B e. QQ with typecode |-