Step |
Hyp |
Ref |
Expression |
1 |
|
numma.1 |
⊢ 𝑇 ∈ ℕ0 |
2 |
|
numma.2 |
⊢ 𝐴 ∈ ℕ0 |
3 |
|
numma.3 |
⊢ 𝐵 ∈ ℕ0 |
4 |
|
numma.4 |
⊢ 𝐶 ∈ ℕ0 |
5 |
|
numma.5 |
⊢ 𝐷 ∈ ℕ0 |
6 |
|
numma.6 |
⊢ 𝑀 = ( ( 𝑇 · 𝐴 ) + 𝐵 ) |
7 |
|
numma.7 |
⊢ 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 ) |
8 |
|
numadd.8 |
⊢ ( 𝐴 + 𝐶 ) = 𝐸 |
9 |
|
numadd.9 |
⊢ ( 𝐵 + 𝐷 ) = 𝐹 |
10 |
1 2 3
|
numcl |
⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0 |
11 |
6 10
|
eqeltri |
⊢ 𝑀 ∈ ℕ0 |
12 |
11
|
nn0cni |
⊢ 𝑀 ∈ ℂ |
13 |
12
|
mulid1i |
⊢ ( 𝑀 · 1 ) = 𝑀 |
14 |
13
|
oveq1i |
⊢ ( ( 𝑀 · 1 ) + 𝑁 ) = ( 𝑀 + 𝑁 ) |
15 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
16 |
2
|
nn0cni |
⊢ 𝐴 ∈ ℂ |
17 |
16
|
mulid1i |
⊢ ( 𝐴 · 1 ) = 𝐴 |
18 |
17
|
oveq1i |
⊢ ( ( 𝐴 · 1 ) + 𝐶 ) = ( 𝐴 + 𝐶 ) |
19 |
18 8
|
eqtri |
⊢ ( ( 𝐴 · 1 ) + 𝐶 ) = 𝐸 |
20 |
3
|
nn0cni |
⊢ 𝐵 ∈ ℂ |
21 |
20
|
mulid1i |
⊢ ( 𝐵 · 1 ) = 𝐵 |
22 |
21
|
oveq1i |
⊢ ( ( 𝐵 · 1 ) + 𝐷 ) = ( 𝐵 + 𝐷 ) |
23 |
22 9
|
eqtri |
⊢ ( ( 𝐵 · 1 ) + 𝐷 ) = 𝐹 |
24 |
1 2 3 4 5 6 7 15 19 23
|
numma |
⊢ ( ( 𝑀 · 1 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 ) |
25 |
14 24
|
eqtr3i |
⊢ ( 𝑀 + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 ) |