Description: Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dp2clq.a | |- A e. NN0 |
|
| dp2clq.b | |- B e. QQ |
||
| Assertion | dp2clq | |- _ A B e. QQ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dp2clq.a | |- A e. NN0 |
|
| 2 | dp2clq.b | |- B e. QQ |
|
| 3 | df-dp2 | |- _ A B = ( A + ( B / ; 1 0 ) ) |
|
| 4 | nn0ssq | |- NN0 C_ QQ |
|
| 5 | 4 1 | sselii | |- A e. QQ |
| 6 | 10nn0 | |- ; 1 0 e. NN0 |
|
| 7 | 4 6 | sselii | |- ; 1 0 e. QQ |
| 8 | 0re | |- 0 e. RR |
|
| 9 | 10pos | |- 0 < ; 1 0 |
|
| 10 | 8 9 | gtneii | |- ; 1 0 =/= 0 |
| 11 | qdivcl | |- ( ( B e. QQ /\ ; 1 0 e. QQ /\ ; 1 0 =/= 0 ) -> ( B / ; 1 0 ) e. QQ ) |
|
| 12 | 2 7 10 11 | mp3an | |- ( B / ; 1 0 ) e. QQ |
| 13 | qaddcl | |- ( ( A e. QQ /\ ( B / ; 1 0 ) e. QQ ) -> ( A + ( B / ; 1 0 ) ) e. QQ ) |
|
| 14 | 5 12 13 | mp2an | |- ( A + ( B / ; 1 0 ) ) e. QQ |
| 15 | 3 14 | eqeltri | |- _ A B e. QQ |