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