Description: Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dp20u.1 | |- A e. NN0 |
|
| Assertion | dp20u | |- _ A 0 = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dp20u.1 | |- A e. NN0 |
|
| 2 | df-dp2 | |- _ A 0 = ( A + ( 0 / ; 1 0 ) ) |
|
| 3 | 10nn0 | |- ; 1 0 e. NN0 |
|
| 4 | 3 | nn0rei | |- ; 1 0 e. RR |
| 5 | 4 | recni | |- ; 1 0 e. CC |
| 6 | 0re | |- 0 e. RR |
|
| 7 | 10pos | |- 0 < ; 1 0 |
|
| 8 | 6 7 | gtneii | |- ; 1 0 =/= 0 |
| 9 | div0 | |- ( ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) -> ( 0 / ; 1 0 ) = 0 ) |
|
| 10 | 5 8 9 | mp2an | |- ( 0 / ; 1 0 ) = 0 |
| 11 | 10 | oveq2i | |- ( A + ( 0 / ; 1 0 ) ) = ( A + 0 ) |
| 12 | 1 | nn0cni | |- A e. CC |
| 13 | 12 | addridi | |- ( A + 0 ) = A |
| 14 | 2 11 13 | 3eqtri | |- _ A 0 = A |