| Step |
Hyp |
Ref |
Expression |
| 1 |
|
0sno |
Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |- |
| 2 |
1
|
a1i |
Could not format ( ( ( A e. No /\ 0s 0s e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s 0s e. No ) with typecode |- |
| 3 |
|
simpll |
Could not format ( ( ( A e. No /\ 0s A e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s A e. No ) with typecode |- |
| 4 |
|
simprl |
Could not format ( ( ( A e. No /\ 0s B e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s B e. No ) with typecode |- |
| 5 |
|
simplr |
Could not format ( ( ( A e. No /\ 0s 0s 0s
|
| 6 |
|
simprr |
Could not format ( ( ( A e. No /\ 0s 0s 0s
|
| 7 |
2 3 2 4 5 6
|
sltmuld |
Could not format ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) ( ( 0s x.s B ) -s ( 0s x.s 0s ) )
|
| 8 |
|
muls02 |
Could not format ( B e. No -> ( 0s x.s B ) = 0s ) : No typesetting found for |- ( B e. No -> ( 0s x.s B ) = 0s ) with typecode |- |
| 9 |
4 8
|
syl |
Could not format ( ( ( A e. No /\ 0s ( 0s x.s B ) = 0s ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( 0s x.s B ) = 0s ) with typecode |- |
| 10 |
|
muls02 |
Could not format ( 0s e. No -> ( 0s x.s 0s ) = 0s ) : No typesetting found for |- ( 0s e. No -> ( 0s x.s 0s ) = 0s ) with typecode |- |
| 11 |
1 10
|
ax-mp |
Could not format ( 0s x.s 0s ) = 0s : No typesetting found for |- ( 0s x.s 0s ) = 0s with typecode |- |
| 12 |
11
|
a1i |
Could not format ( ( ( A e. No /\ 0s ( 0s x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( 0s x.s 0s ) = 0s ) with typecode |- |
| 13 |
9 12
|
oveq12d |
Could not format ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) = ( 0s -s 0s ) ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) = ( 0s -s 0s ) ) with typecode |- |
| 14 |
|
subsid |
Could not format ( 0s e. No -> ( 0s -s 0s ) = 0s ) : No typesetting found for |- ( 0s e. No -> ( 0s -s 0s ) = 0s ) with typecode |- |
| 15 |
1 14
|
ax-mp |
Could not format ( 0s -s 0s ) = 0s : No typesetting found for |- ( 0s -s 0s ) = 0s with typecode |- |
| 16 |
13 15
|
eqtrdi |
Could not format ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) = 0s ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( ( 0s x.s B ) -s ( 0s x.s 0s ) ) = 0s ) with typecode |- |
| 17 |
|
muls01 |
Could not format ( A e. No -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |- |
| 18 |
3 17
|
syl |
Could not format ( ( ( A e. No /\ 0s ( A x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( A x.s 0s ) = 0s ) with typecode |- |
| 19 |
18
|
oveq2d |
Could not format ( ( ( A e. No /\ 0s ( ( A x.s B ) -s ( A x.s 0s ) ) = ( ( A x.s B ) -s 0s ) ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( ( A x.s B ) -s ( A x.s 0s ) ) = ( ( A x.s B ) -s 0s ) ) with typecode |- |
| 20 |
|
mulscl |
Could not format ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No ) with typecode |- |
| 21 |
20
|
ad2ant2r |
Could not format ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) with typecode |- |
| 22 |
|
subsid1 |
Could not format ( ( A x.s B ) e. No -> ( ( A x.s B ) -s 0s ) = ( A x.s B ) ) : No typesetting found for |- ( ( A x.s B ) e. No -> ( ( A x.s B ) -s 0s ) = ( A x.s B ) ) with typecode |- |
| 23 |
21 22
|
syl |
Could not format ( ( ( A e. No /\ 0s ( ( A x.s B ) -s 0s ) = ( A x.s B ) ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( ( A x.s B ) -s 0s ) = ( A x.s B ) ) with typecode |- |
| 24 |
19 23
|
eqtrd |
Could not format ( ( ( A e. No /\ 0s ( ( A x.s B ) -s ( A x.s 0s ) ) = ( A x.s B ) ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( ( A x.s B ) -s ( A x.s 0s ) ) = ( A x.s B ) ) with typecode |- |
| 25 |
7 16 24
|
3brtr3d |
Could not format ( ( ( A e. No /\ 0s 0s 0s
|