Metamath Proof Explorer

Theorem decsplit

Description: Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

Ref Expression
Hypotheses decsplit0.1 
|- A e. NN0
decsplit.2 
|- B e. NN0
decsplit.3 
|- D e. NN0
decsplit.4 
|- M e. NN0
decsplit.5 
|- ( M + 1 ) = N
decsplit.6 
|- ( ( A x. ( ; 1 0 ^ M ) ) + B ) = C
Assertion decsplit 
|- ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ; C D

Proof

Step Hyp Ref Expression
1 decsplit0.1 
 |-  A e. NN0
2 decsplit.2 
 |-  B e. NN0
3 decsplit.3 
 |-  D e. NN0
4 decsplit.4 
 |-  M e. NN0
5 decsplit.5 
 |-  ( M + 1 ) = N
6 decsplit.6 
 |-  ( ( A x. ( ; 1 0 ^ M ) ) + B ) = C
7 10nn0 
 |-  ; 1 0 e. NN0
8 7 4 nn0expcli 
 |-  ( ; 1 0 ^ M ) e. NN0
9 1 8 nn0mulcli 
 |-  ( A x. ( ; 1 0 ^ M ) ) e. NN0
10 7 9 nn0mulcli 
 |-  ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) e. NN0
11 10 nn0cni 
 |-  ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) e. CC
12 7 2 nn0mulcli 
 |-  ( ; 1 0 x. B ) e. NN0
13 12 nn0cni 
 |-  ( ; 1 0 x. B ) e. CC
14 3 nn0cni 
 |-  D e. CC
15 11 13 14 addassi 
 |-  ( ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ; 1 0 x. B ) ) + D ) = ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ( ; 1 0 x. B ) + D ) )
16 7 nn0cni 
 |-  ; 1 0 e. CC
17 9 nn0cni 
 |-  ( A x. ( ; 1 0 ^ M ) ) e. CC
18 2 nn0cni 
 |-  B e. CC
19 16 17 18 adddii 
 |-  ( ; 1 0 x. ( ( A x. ( ; 1 0 ^ M ) ) + B ) ) = ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ; 1 0 x. B ) )
20 6 oveq2i 
 |-  ( ; 1 0 x. ( ( A x. ( ; 1 0 ^ M ) ) + B ) ) = ( ; 1 0 x. C )
21 19 20 eqtr3i 
 |-  ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ; 1 0 x. B ) ) = ( ; 1 0 x. C )
22 21 oveq1i 
 |-  ( ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ; 1 0 x. B ) ) + D ) = ( ( ; 1 0 x. C ) + D )
23 15 22 eqtr3i 
 |-  ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ( ; 1 0 x. B ) + D ) ) = ( ( ; 1 0 x. C ) + D )
24 8 nn0cni 
 |-  ( ; 1 0 ^ M ) e. CC
25 24 16 mulcomi 
 |-  ( ( ; 1 0 ^ M ) x. ; 1 0 ) = ( ; 1 0 x. ( ; 1 0 ^ M ) )
26 7 4 5 25 numexpp1 
 |-  ( ; 1 0 ^ N ) = ( ; 1 0 x. ( ; 1 0 ^ M ) )
27 26 oveq2i 
 |-  ( A x. ( ; 1 0 ^ N ) ) = ( A x. ( ; 1 0 x. ( ; 1 0 ^ M ) ) )
28 1 nn0cni 
 |-  A e. CC
29 28 16 24 mul12i 
 |-  ( A x. ( ; 1 0 x. ( ; 1 0 ^ M ) ) ) = ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) )
30 27 29 eqtri 
 |-  ( A x. ( ; 1 0 ^ N ) ) = ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) )
31 dfdec10 
 |-  ; B D = ( ( ; 1 0 x. B ) + D )
32 30 31 oveq12i 
 |-  ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ( ; 1 0 x. B ) + D ) )
33 dfdec10 
 |-  ; C D = ( ( ; 1 0 x. C ) + D )
34 23 32 33 3eqtr4i 
 |-  ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ; C D