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 ( 𝐴 ∈ ℕ → ( 𝐴 9 + 1 ) = ( 𝐴 + 1 ) 0 )

Proof

Step Hyp Ref Expression
1 df-dec ⊢ ( 𝐴 + 1 ) 0 = ( ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) + 0 )
2 9nn ⊢ 9 ∈ ℕ
3 peano2nn ⊢ ( 9 ∈ ℕ → ( 9 + 1 ) ∈ ℕ )
4 2 3 ax-mp ⊢ ( 9 + 1 ) ∈ ℕ
5 4 a1i ⊢ ( 𝐴 ∈ ℕ → ( 9 + 1 ) ∈ ℕ )
6 peano2nn ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )
7 5 6 nnmulcld ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) ∈ ℕ )
8 7 nncnd ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) ∈ ℂ )
9 8 addid1d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) + 0 ) = ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) )
10 4 nncni ⊢ ( 9 + 1 ) ∈ ℂ
11 10 a1i ⊢ ( 𝐴 ∈ ℕ → ( 9 + 1 ) ∈ ℂ )
12 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
13 1cnd ⊢ ( 𝐴 ∈ ℕ → 1 ∈ ℂ )
14 11 12 13 adddid ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) = ( ( ( 9 + 1 ) · 𝐴 ) + ( ( 9 + 1 ) · 1 ) ) )
15 11 mulid1d ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · 1 ) = ( 9 + 1 ) )
16 15 oveq2d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 9 + 1 ) · 𝐴 ) + ( ( 9 + 1 ) · 1 ) ) = ( ( ( 9 + 1 ) · 𝐴 ) + ( 9 + 1 ) ) )
17 df-dec ⊢ 𝐴 9 = ( ( ( 9 + 1 ) · 𝐴 ) + 9 )
18 17 oveq1i ⊢ ( 𝐴 9 + 1 ) = ( ( ( ( 9 + 1 ) · 𝐴 ) + 9 ) + 1 )
19 id ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ )
20 5 19 nnmulcld ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · 𝐴 ) ∈ ℕ )
21 20 nncnd ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · 𝐴 ) ∈ ℂ )
22 2 nncni ⊢ 9 ∈ ℂ
23 22 a1i ⊢ ( 𝐴 ∈ ℕ → 9 ∈ ℂ )
24 21 23 13 addassd ⊢ ( 𝐴 ∈ ℕ → ( ( ( ( 9 + 1 ) · 𝐴 ) + 9 ) + 1 ) = ( ( ( 9 + 1 ) · 𝐴 ) + ( 9 + 1 ) ) )
25 18 24 syl5req ⊢ ( 𝐴 ∈ ℕ → ( ( ( 9 + 1 ) · 𝐴 ) + ( 9 + 1 ) ) = ( 𝐴 9 + 1 ) )
26 16 25 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 9 + 1 ) · 𝐴 ) + ( ( 9 + 1 ) · 1 ) ) = ( 𝐴 9 + 1 ) )
27 14 26 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) = ( 𝐴 9 + 1 ) )
28 9 27 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 9 + 1 ) · ( 𝐴 + 1 ) ) + 0 ) = ( 𝐴 9 + 1 ) )
29 1 28 syl5req ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 9 + 1 ) = ( 𝐴 + 1 ) 0 )