Step |
Hyp |
Ref |
Expression |
1 |
|
numsucc.1 |
⊢ 𝑌 ∈ ℕ0 |
2 |
|
numsucc.2 |
⊢ 𝑇 = ( 𝑌 + 1 ) |
3 |
|
numsucc.3 |
⊢ 𝐴 ∈ ℕ0 |
4 |
|
numsucc.4 |
⊢ ( 𝐴 + 1 ) = 𝐵 |
5 |
|
numsucc.5 |
⊢ 𝑁 = ( ( 𝑇 · 𝐴 ) + 𝑌 ) |
6 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
7 |
1 6
|
nn0addcli |
⊢ ( 𝑌 + 1 ) ∈ ℕ0 |
8 |
2 7
|
eqeltri |
⊢ 𝑇 ∈ ℕ0 |
9 |
8
|
nn0cni |
⊢ 𝑇 ∈ ℂ |
10 |
9
|
mulid1i |
⊢ ( 𝑇 · 1 ) = 𝑇 |
11 |
10
|
oveq2i |
⊢ ( ( 𝑇 · 𝐴 ) + ( 𝑇 · 1 ) ) = ( ( 𝑇 · 𝐴 ) + 𝑇 ) |
12 |
3
|
nn0cni |
⊢ 𝐴 ∈ ℂ |
13 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
14 |
9 12 13
|
adddii |
⊢ ( 𝑇 · ( 𝐴 + 1 ) ) = ( ( 𝑇 · 𝐴 ) + ( 𝑇 · 1 ) ) |
15 |
2
|
eqcomi |
⊢ ( 𝑌 + 1 ) = 𝑇 |
16 |
8 3 1 15 5
|
numsuc |
⊢ ( 𝑁 + 1 ) = ( ( 𝑇 · 𝐴 ) + 𝑇 ) |
17 |
11 14 16
|
3eqtr4ri |
⊢ ( 𝑁 + 1 ) = ( 𝑇 · ( 𝐴 + 1 ) ) |
18 |
4
|
oveq2i |
⊢ ( 𝑇 · ( 𝐴 + 1 ) ) = ( 𝑇 · 𝐵 ) |
19 |
3 6
|
nn0addcli |
⊢ ( 𝐴 + 1 ) ∈ ℕ0 |
20 |
4 19
|
eqeltrri |
⊢ 𝐵 ∈ ℕ0 |
21 |
8 20
|
num0u |
⊢ ( 𝑇 · 𝐵 ) = ( ( 𝑇 · 𝐵 ) + 0 ) |
22 |
17 18 21
|
3eqtri |
⊢ ( 𝑁 + 1 ) = ( ( 𝑇 · 𝐵 ) + 0 ) |