Description: Split a decimal number into two parts. Base case: N = 0 . (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | decsplit0.1 | |- A e. NN0 |
|
| Assertion | decsplit0 | |- ( ( A x. ( ; 1 0 ^ 0 ) ) + 0 ) = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | decsplit0.1 | |- A e. NN0 |
|
| 2 | 1 | decsplit0b | |- ( ( A x. ( ; 1 0 ^ 0 ) ) + 0 ) = ( A + 0 ) |
| 3 | 1 | nn0cni | |- A e. CC |
| 4 | 3 | addid1i | |- ( A + 0 ) = A |
| 5 | 2 4 | eqtri | |- ( ( A x. ( ; 1 0 ^ 0 ) ) + 0 ) = A |