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
|
eqtr2id |
|- ( 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
|
eqtr2id |
|- ( A e. NN -> ( ; A 9 + 1 ) = ; ( A + 1 ) 0 ) |