Metamath Proof Explorer

Theorem deccarry

Description: Add 1 to a 2 digit number with carry. This is a special case of decsucc , but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g., by applying this theorem three times we get ( ; ; 9 9 9 + 1 ) = ; ; ; 1 0 0 0 . (Contributed by AV, 4-Aug-2020) (Revised by ML, 8-Aug-2020) (Proof shortened by AV, 10-Sep-2021)

Ref Expression
Assertion deccarry 
|- ( A e. NN -> ( ; A 9 + 1 ) = ; ( A + 1 ) 0 )

Proof

Step Hyp Ref Expression
1 df-dec 
 |-  ; ( A + 1 ) 0 = ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 )
2 9nn 
 |-  9 e. NN
3 peano2nn 
 |-  ( 9 e. NN -> ( 9 + 1 ) e. NN )
4 2 3 ax-mp 
 |-  ( 9 + 1 ) e. NN
5 4 a1i 
 |-  ( A e. NN -> ( 9 + 1 ) e. NN )
6 peano2nn 
 |-  ( A e. NN -> ( A + 1 ) e. NN )
7 5 6 nnmulcld 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. ( A + 1 ) ) e. NN )
8 7 nncnd 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. ( A + 1 ) ) e. CC )
9 8 addid1d 
 |-  ( A e. NN -> ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 ) = ( ( 9 + 1 ) x. ( A + 1 ) ) )
10 4 nncni 
 |-  ( 9 + 1 ) e. CC
11 10 a1i 
 |-  ( A e. NN -> ( 9 + 1 ) e. CC )
12 nncn 
 |-  ( A e. NN -> A e. CC )
13 1cnd 
 |-  ( A e. NN -> 1 e. CC )
14 11 12 13 adddid 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. ( A + 1 ) ) = ( ( ( 9 + 1 ) x. A ) + ( ( 9 + 1 ) x. 1 ) ) )
15 11 mulid1d 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. 1 ) = ( 9 + 1 ) )
16 15 oveq2d 
 |-  ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( ( 9 + 1 ) x. 1 ) ) = ( ( ( 9 + 1 ) x. A ) + ( 9 + 1 ) ) )
17 df-dec 
 |-  ; A 9 = ( ( ( 9 + 1 ) x. A ) + 9 )
18 17 oveq1i 
 |-  ( ; A 9 + 1 ) = ( ( ( ( 9 + 1 ) x. A ) + 9 ) + 1 )
19 id 
 |-  ( A e. NN -> A e. NN )
20 5 19 nnmulcld 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. A ) e. NN )
21 20 nncnd 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. A ) e. CC )
22 2 nncni 
 |-  9 e. CC
23 22 a1i 
 |-  ( A e. NN -> 9 e. CC )
24 21 23 13 addassd 
 |-  ( A e. NN -> ( ( ( ( 9 + 1 ) x. A ) + 9 ) + 1 ) = ( ( ( 9 + 1 ) x. A ) + ( 9 + 1 ) ) )
25 18 24 syl5req 
 |-  ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( 9 + 1 ) ) = ( ; A 9 + 1 ) )
26 16 25 eqtrd 
 |-  ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( ( 9 + 1 ) x. 1 ) ) = ( ; A 9 + 1 ) )
27 14 26 eqtrd 
 |-  ( A e. NN -> ( ( 9 + 1 ) x. ( A + 1 ) ) = ( ; A 9 + 1 ) )
28 9 27 eqtrd 
 |-  ( A e. NN -> ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 ) = ( ; A 9 + 1 ) )
29 1 28 syl5req 
 |-  ( A e. NN -> ( ; A 9 + 1 ) = ; ( A + 1 ) 0 )