Metamath Proof Explorer


Theorem decsplit1

Description: Split a decimal number into two parts. Base case: N = 1 . (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

Ref Expression
Hypothesis decsplit0.1 A0
Assertion decsplit1 Could not format assertion : No typesetting found for |- ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B with typecode |-

Proof

Step Hyp Ref Expression
1 decsplit0.1 A0
2 10nn0 100
3 2 numexp1 101=10
4 3 oveq2i A101=A10
5 2 nn0cni 10
6 1 nn0cni A
7 5 6 mulcomi 10A=A10
8 4 7 eqtr4i A101=10A
9 8 oveq1i A101+B=10A+B
10 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
11 9 10 eqtr4i Could not format ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B : No typesetting found for |- ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B with typecode |-