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\in \mathbb{N}$$
3		peano2nn	$$⊢9\in \mathbb{N}\to 9+1\in \mathbb{N}$$
4	2 3	ax-mp	$$⊢9+1\in \mathbb{N}$$
5	4	a1i	$$⊢A\in \mathbb{N}\to 9+1\in \mathbb{N}$$
6		peano2nn	$$⊢A\in \mathbb{N}\to A+1\in \mathbb{N}$$
7	5 6	nnmulcld	$$⊢A\in \mathbb{N}\to \left(9+1\right)\left(A+1\right)\in \mathbb{N}$$
8	7	nncnd	$$⊢A\in \mathbb{N}\to \left(9+1\right)\left(A+1\right)\in ℂ$$
9	8	addid1d	$$⊢A\in \mathbb{N}\to \left(9+1\right)\left(A+1\right)+0=\left(9+1\right)\left(A+1\right)$$
10	4	nncni	$$⊢9+1\in ℂ$$
11	10	a1i	$$⊢A\in \mathbb{N}\to 9+1\in ℂ$$
12		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
13		1cnd	$$⊢A\in \mathbb{N}\to 1\in ℂ$$
14	11 12 13	adddid	$$⊢A\in \mathbb{N}\to \left(9+1\right)\left(A+1\right)=\left(9+1\right)A+\left(9+1\right)\cdot 1$$
15	11	mulid1d	$$⊢A\in \mathbb{N}\to \left(9+1\right)\cdot 1=9+1$$
16	15	oveq2d	$$⊢A\in \mathbb{N}\to \left(9+1\right)A+\left(9+1\right)\cdot 1=\left(9+1\right)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\in \mathbb{N}\to A\in \mathbb{N}$$
20	5 19	nnmulcld	$$⊢A\in \mathbb{N}\to \left(9+1\right)A\in \mathbb{N}$$
21	20	nncnd	$$⊢A\in \mathbb{N}\to \left(9+1\right)A\in ℂ$$
22	2	nncni	$$⊢9\in ℂ$$
23	22	a1i	$$⊢A\in \mathbb{N}\to 9\in ℂ$$
24	21 23 13	addassd	$$⊢A\in \mathbb{N}\to \left(9+1\right)A+9+1=\left(9+1\right)A+9+1$$
25	18 24	syl5req	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	syl5req	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 |-