This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 Could not format assertion : No typesetting found for |- ( A e. NN -> ( ; A 9 + 1 ) = ; ( A + 1 ) 0 ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-dec Could not format ; ( A + 1 ) 0 = ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 ) : No typesetting found for |- ; ( A + 1 ) 0 = ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 ) with typecode |-
2 9nn ⊢ 9 ∈ ℕ
3 peano2nn ⊢ 9 ∈ ℕ → 9 + 1 ∈ ℕ
4 2 3 ax-mp ⊢ 9 + 1 ∈ ℕ
5 4 a1i ⊢ A ∈ ℕ → 9 + 1 ∈ ℕ
6 peano2nn ⊢ A ∈ ℕ → A + 1 ∈ ℕ
7 5 6 nnmulcld ⊢ A ∈ ℕ → 9 + 1 ⁢ A + 1 ∈ ℕ
8 7 nncnd ⊢ A ∈ ℕ → 9 + 1 ⁢ A + 1 ∈ ℂ
9 8 addridd ⊢ A ∈ ℕ → 9 + 1 ⁢ A + 1 + 0 = 9 + 1 ⁢ A + 1
10 4 nncni ⊢ 9 + 1 ∈ ℂ
11 10 a1i ⊢ A ∈ ℕ → 9 + 1 ∈ ℂ
12 nncn ⊢ A ∈ ℕ → A ∈ ℂ
13 1cnd ⊢ A ∈ ℕ → 1 ∈ ℂ
14 11 12 13 adddid ⊢ A ∈ ℕ → 9 + 1 ⁢ A + 1 = 9 + 1 ⁢ A + 9 + 1 ⋅ 1
15 11 mulridd ⊢ A ∈ ℕ → 9 + 1 ⋅ 1 = 9 + 1
16 15 oveq2d ⊢ A ∈ ℕ → 9 + 1 ⁢ A + 9 + 1 ⋅ 1 = 9 + 1 ⁢ A + 9 + 1
17 df-dec Could not format ; A 9 = ( ( ( 9 + 1 ) x. A ) + 9 ) : No typesetting found for |- ; A 9 = ( ( ( 9 + 1 ) x. A ) + 9 ) with typecode |-
18 17 oveq1i Could not format ( ; A 9 + 1 ) = ( ( ( ( 9 + 1 ) x. A ) + 9 ) + 1 ) : No typesetting found for |- ( ; A 9 + 1 ) = ( ( ( ( 9 + 1 ) x. A ) + 9 ) + 1 ) with typecode |-
19 id ⊢ A ∈ ℕ → A ∈ ℕ
20 5 19 nnmulcld ⊢ A ∈ ℕ → 9 + 1 ⁢ A ∈ ℕ
21 20 nncnd ⊢ A ∈ ℕ → 9 + 1 ⁢ A ∈ ℂ
22 2 nncni ⊢ 9 ∈ ℂ
23 22 a1i ⊢ A ∈ ℕ → 9 ∈ ℂ
24 21 23 13 addassd ⊢ A ∈ ℕ → 9 + 1 ⁢ A + 9 + 1 = 9 + 1 ⁢ A + 9 + 1
25 18 24 eqtr2id Could not format ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( 9 + 1 ) ) = ( ; A 9 + 1 ) ) : No typesetting found for |- ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( 9 + 1 ) ) = ( ; A 9 + 1 ) ) with typecode |-
26 16 25 eqtrd Could not format ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( ( 9 + 1 ) x. 1 ) ) = ( ; A 9 + 1 ) ) : No typesetting found for |- ( A e. NN -> ( ( ( 9 + 1 ) x. A ) + ( ( 9 + 1 ) x. 1 ) ) = ( ; A 9 + 1 ) ) with typecode |-
27 14 26 eqtrd Could not format ( A e. NN -> ( ( 9 + 1 ) x. ( A + 1 ) ) = ( ; A 9 + 1 ) ) : No typesetting found for |- ( A e. NN -> ( ( 9 + 1 ) x. ( A + 1 ) ) = ( ; A 9 + 1 ) ) with typecode |-
28 9 27 eqtrd Could not format ( A e. NN -> ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 ) = ( ; A 9 + 1 ) ) : No typesetting found for |- ( A e. NN -> ( ( ( 9 + 1 ) x. ( A + 1 ) ) + 0 ) = ( ; A 9 + 1 ) ) with typecode |-
29 1 28 eqtr2id Could not format ( A e. NN -> ( ; A 9 + 1 ) = ; ( A + 1 ) 0 ) : No typesetting found for |- ( A e. NN -> ( ; A 9 + 1 ) = ; ( A + 1 ) 0 ) with typecode |-