Step |
Hyp |
Ref |
Expression |
1 |
|
sqdeccom12.a |
|- A e. NN0 |
2 |
|
sqdeccom12.b |
|- B e. NN0 |
3 |
|
sq3deccom12.c |
|- C e. NN0 |
4 |
|
sq3deccom12.d |
|- ( A + C ) = D |
5 |
|
0nn0 |
|- 0 e. NN0 |
6 |
|
eqid |
|- ; C 0 = ; C 0 |
7 |
|
eqid |
|- ; A B = ; A B |
8 |
1
|
nn0cni |
|- A e. CC |
9 |
3
|
nn0cni |
|- C e. CC |
10 |
8 9 4
|
addcomli |
|- ( C + A ) = D |
11 |
2
|
nn0cni |
|- B e. CC |
12 |
11
|
addid2i |
|- ( 0 + B ) = B |
13 |
3 5 1 2 6 7 10 12
|
decadd |
|- ( ; C 0 + ; A B ) = ; D B |
14 |
1 2
|
deccl |
|- ; A B e. NN0 |
15 |
14
|
nn0cni |
|- ; A B e. CC |
16 |
15
|
addid2i |
|- ( 0 + ; A B ) = ; A B |
17 |
3 5 14 6 16
|
decaddi |
|- ( ; C 0 + ; A B ) = ; C ; A B |
18 |
13 17
|
eqtr3i |
|- ; D B = ; C ; A B |
19 |
18 18
|
oveq12i |
|- ( ; D B x. ; D B ) = ( ; C ; A B x. ; C ; A B ) |
20 |
19
|
oveq2i |
|- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ( ; ; A B C x. ; ; A B C ) - ( ; C ; A B x. ; C ; A B ) ) |
21 |
14 3
|
sqdeccom12 |
|- ( ( ; ; A B C x. ; ; A B C ) - ( ; C ; A B x. ; C ; A B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) ) |
22 |
20 21
|
eqtri |
|- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) ) |