Step |
Hyp |
Ref |
Expression |
1 |
|
sqdeccom12.a |
⊢ 𝐴 ∈ ℕ0 |
2 |
|
sqdeccom12.b |
⊢ 𝐵 ∈ ℕ0 |
3 |
|
sq3deccom12.c |
⊢ 𝐶 ∈ ℕ0 |
4 |
|
sq3deccom12.d |
⊢ ( 𝐴 + 𝐶 ) = 𝐷 |
5 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
6 |
|
eqid |
⊢ ; 𝐶 0 = ; 𝐶 0 |
7 |
|
eqid |
⊢ ; 𝐴 𝐵 = ; 𝐴 𝐵 |
8 |
1
|
nn0cni |
⊢ 𝐴 ∈ ℂ |
9 |
3
|
nn0cni |
⊢ 𝐶 ∈ ℂ |
10 |
8 9 4
|
addcomli |
⊢ ( 𝐶 + 𝐴 ) = 𝐷 |
11 |
2
|
nn0cni |
⊢ 𝐵 ∈ ℂ |
12 |
11
|
addid2i |
⊢ ( 0 + 𝐵 ) = 𝐵 |
13 |
3 5 1 2 6 7 10 12
|
decadd |
⊢ ( ; 𝐶 0 + ; 𝐴 𝐵 ) = ; 𝐷 𝐵 |
14 |
1 2
|
deccl |
⊢ ; 𝐴 𝐵 ∈ ℕ0 |
15 |
14
|
nn0cni |
⊢ ; 𝐴 𝐵 ∈ ℂ |
16 |
15
|
addid2i |
⊢ ( 0 + ; 𝐴 𝐵 ) = ; 𝐴 𝐵 |
17 |
3 5 14 6 16
|
decaddi |
⊢ ( ; 𝐶 0 + ; 𝐴 𝐵 ) = ; 𝐶 ; 𝐴 𝐵 |
18 |
13 17
|
eqtr3i |
⊢ ; 𝐷 𝐵 = ; 𝐶 ; 𝐴 𝐵 |
19 |
18 18
|
oveq12i |
⊢ ( ; 𝐷 𝐵 · ; 𝐷 𝐵 ) = ( ; 𝐶 ; 𝐴 𝐵 · ; 𝐶 ; 𝐴 𝐵 ) |
20 |
19
|
oveq2i |
⊢ ( ( ; ; 𝐴 𝐵 𝐶 · ; ; 𝐴 𝐵 𝐶 ) − ( ; 𝐷 𝐵 · ; 𝐷 𝐵 ) ) = ( ( ; ; 𝐴 𝐵 𝐶 · ; ; 𝐴 𝐵 𝐶 ) − ( ; 𝐶 ; 𝐴 𝐵 · ; 𝐶 ; 𝐴 𝐵 ) ) |
21 |
14 3
|
sqdeccom12 |
⊢ ( ( ; ; 𝐴 𝐵 𝐶 · ; ; 𝐴 𝐵 𝐶 ) − ( ; 𝐶 ; 𝐴 𝐵 · ; 𝐶 ; 𝐴 𝐵 ) ) = ( ; 9 9 · ( ( ; 𝐴 𝐵 · ; 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) ) |
22 |
20 21
|
eqtri |
⊢ ( ( ; ; 𝐴 𝐵 𝐶 · ; ; 𝐴 𝐵 𝐶 ) − ( ; 𝐷 𝐵 · ; 𝐷 𝐵 ) ) = ( ; 9 9 · ( ( ; 𝐴 𝐵 · ; 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) ) |