Step |
Hyp |
Ref |
Expression |
1 |
|
numsucc.1 |
|- Y e. NN0 |
2 |
|
numsucc.2 |
|- T = ( Y + 1 ) |
3 |
|
numsucc.3 |
|- A e. NN0 |
4 |
|
numsucc.4 |
|- ( A + 1 ) = B |
5 |
|
numsucc.5 |
|- N = ( ( T x. A ) + Y ) |
6 |
|
1nn0 |
|- 1 e. NN0 |
7 |
1 6
|
nn0addcli |
|- ( Y + 1 ) e. NN0 |
8 |
2 7
|
eqeltri |
|- T e. NN0 |
9 |
8
|
nn0cni |
|- T e. CC |
10 |
9
|
mulid1i |
|- ( T x. 1 ) = T |
11 |
10
|
oveq2i |
|- ( ( T x. A ) + ( T x. 1 ) ) = ( ( T x. A ) + T ) |
12 |
3
|
nn0cni |
|- A e. CC |
13 |
|
ax-1cn |
|- 1 e. CC |
14 |
9 12 13
|
adddii |
|- ( T x. ( A + 1 ) ) = ( ( T x. A ) + ( T x. 1 ) ) |
15 |
2
|
eqcomi |
|- ( Y + 1 ) = T |
16 |
8 3 1 15 5
|
numsuc |
|- ( N + 1 ) = ( ( T x. A ) + T ) |
17 |
11 14 16
|
3eqtr4ri |
|- ( N + 1 ) = ( T x. ( A + 1 ) ) |
18 |
4
|
oveq2i |
|- ( T x. ( A + 1 ) ) = ( T x. B ) |
19 |
3 6
|
nn0addcli |
|- ( A + 1 ) e. NN0 |
20 |
4 19
|
eqeltrri |
|- B e. NN0 |
21 |
8 20
|
num0u |
|- ( T x. B ) = ( ( T x. B ) + 0 ) |
22 |
17 18 21
|
3eqtri |
|- ( N + 1 ) = ( ( T x. B ) + 0 ) |