Step |
Hyp |
Ref |
Expression |
1 |
|
elzs |
|
2 |
|
nnn0s |
|
3 |
|
n0seo |
Could not format ( y e. NN0_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) : No typesetting found for |- ( y e. NN0_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) with typecode |- |
4 |
2 3
|
syl |
Could not format ( y e. NN_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) : No typesetting found for |- ( y e. NN_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) with typecode |- |
5 |
|
nnn0s |
|
6 |
|
n0seo |
Could not format ( z e. NN0_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( z e. NN0_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
7 |
5 6
|
syl |
Could not format ( z e. NN_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( z e. NN_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
8 |
|
reeanv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) with typecode |- |
9 |
|
n0zs |
|
10 |
9
|
adantr |
|
11 |
|
n0zs |
|
12 |
11
|
adantl |
|
13 |
10 12
|
zsubscld |
|
14 |
|
2sno |
Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |- |
15 |
14
|
a1i |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> 2s e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> 2s e. No ) with typecode |- |
16 |
|
n0sno |
|
17 |
16
|
adantr |
|
18 |
|
n0sno |
|
19 |
18
|
adantl |
|
20 |
15 17 19
|
subsdid |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) with typecode |- |
21 |
20
|
eqcomd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) with typecode |- |
22 |
|
oveq2 |
Could not format ( x = ( w -s t ) -> ( 2s x.s x ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( x = ( w -s t ) -> ( 2s x.s x ) = ( 2s x.s ( w -s t ) ) ) with typecode |- |
23 |
22
|
rspceeqv |
Could not format ( ( ( w -s t ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( ( w -s t ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) with typecode |- |
24 |
13 21 23
|
syl2anc |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) with typecode |- |
25 |
|
oveq12 |
Could not format ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) with typecode |- |
26 |
25
|
eqeq1d |
Could not format ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) with typecode |- |
27 |
26
|
rexbidv |
Could not format ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) with typecode |- |
28 |
24 27
|
syl5ibrcom |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) with typecode |- |
29 |
28
|
rexlimivv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |- |
30 |
8 29
|
sylbir |
Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |- |
31 |
30
|
orcd |
Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
32 |
|
reeanv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) with typecode |- |
33 |
15 17
|
mulscld |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s w ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s w ) e. No ) with typecode |- |
34 |
|
1sno |
|
35 |
34
|
a1i |
|
36 |
15 19
|
mulscld |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s t ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s t ) e. No ) with typecode |- |
37 |
33 35 36
|
addsubsd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) ) with typecode |- |
38 |
21
|
oveq1d |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) with typecode |- |
39 |
37 38
|
eqtrd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) with typecode |- |
40 |
22
|
oveq1d |
Could not format ( x = ( w -s t ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) : No typesetting found for |- ( x = ( w -s t ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) with typecode |- |
41 |
40
|
rspceeqv |
Could not format ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
42 |
13 39 41
|
syl2anc |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
43 |
|
oveq12 |
Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) ) with typecode |- |
44 |
43
|
eqeq1d |
Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
45 |
44
|
rexbidv |
Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
46 |
42 45
|
syl5ibrcom |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
47 |
46
|
rexlimivv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
48 |
32 47
|
sylbir |
Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
49 |
48
|
olcd |
Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
50 |
|
reeanv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
51 |
|
1zs |
|
52 |
51
|
a1i |
|
53 |
13 52
|
zsubscld |
|
54 |
13
|
znod |
|
55 |
15 54 35
|
subsdid |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( ( w -s t ) -s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( ( w -s t ) -s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) ) with typecode |- |
56 |
55
|
oveq1d |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) ) with typecode |- |
57 |
|
mulsrid |
Could not format ( 2s e. No -> ( 2s x.s 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s x.s 1s ) = 2s ) with typecode |- |
58 |
14 57
|
ax-mp |
Could not format ( 2s x.s 1s ) = 2s : No typesetting found for |- ( 2s x.s 1s ) = 2s with typecode |- |
59 |
58
|
oveq2i |
Could not format ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s 2s ) : No typesetting found for |- ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s 2s ) with typecode |- |
60 |
59
|
oveq1i |
Could not format ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) : No typesetting found for |- ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) with typecode |- |
61 |
15 54
|
mulscld |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) e. No ) with typecode |- |
62 |
61 35 15
|
addsubsd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) ) with typecode |- |
63 |
61 35 15
|
addsubsassd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |- |
64 |
62 63
|
eqtr3d |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |- |
65 |
60 64
|
eqtrid |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |- |
66 |
56 65
|
eqtrd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |- |
67 |
|
subscl |
Could not format ( ( 1s e. No /\ 2s e. No ) -> ( 1s -s 2s ) e. No ) : No typesetting found for |- ( ( 1s e. No /\ 2s e. No ) -> ( 1s -s 2s ) e. No ) with typecode |- |
68 |
34 14 67
|
mp2an |
Could not format ( 1s -s 2s ) e. No : No typesetting found for |- ( 1s -s 2s ) e. No with typecode |- |
69 |
|
negnegs |
Could not format ( ( 1s -s 2s ) e. No -> ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) ) : No typesetting found for |- ( ( 1s -s 2s ) e. No -> ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) ) with typecode |- |
70 |
68 69
|
ax-mp |
Could not format ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) : No typesetting found for |- ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) with typecode |- |
71 |
34
|
a1i |
|
72 |
14
|
a1i |
Could not format ( T. -> 2s e. No ) : No typesetting found for |- ( T. -> 2s e. No ) with typecode |- |
73 |
71 72
|
negsubsdi2d |
Could not format ( T. -> ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) ) : No typesetting found for |- ( T. -> ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) ) with typecode |- |
74 |
73
|
mptru |
Could not format ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) : No typesetting found for |- ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) with typecode |- |
75 |
|
1p1e2s |
Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |- |
76 |
|
subadds |
Could not format ( ( 2s e. No /\ 1s e. No /\ 1s e. No ) -> ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ 1s e. No /\ 1s e. No ) -> ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) ) with typecode |- |
77 |
14 34 34 76
|
mp3an |
Could not format ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) : No typesetting found for |- ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) with typecode |- |
78 |
75 77
|
mpbir |
Could not format ( 2s -s 1s ) = 1s : No typesetting found for |- ( 2s -s 1s ) = 1s with typecode |- |
79 |
74 78
|
eqtri |
Could not format ( -us ` ( 1s -s 2s ) ) = 1s : No typesetting found for |- ( -us ` ( 1s -s 2s ) ) = 1s with typecode |- |
80 |
79
|
fveq2i |
Could not format ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( -us ` 1s ) : No typesetting found for |- ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( -us ` 1s ) with typecode |- |
81 |
70 80
|
eqtr3i |
Could not format ( 1s -s 2s ) = ( -us ` 1s ) : No typesetting found for |- ( 1s -s 2s ) = ( -us ` 1s ) with typecode |- |
82 |
81
|
oveq2i |
Could not format ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) : No typesetting found for |- ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) with typecode |- |
83 |
61 35
|
subsvald |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) ) with typecode |- |
84 |
82 83
|
eqtr4id |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) -s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) -s 1s ) ) with typecode |- |
85 |
20
|
oveq1d |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) with typecode |- |
86 |
84 85
|
eqtrd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) with typecode |- |
87 |
33 36 35
|
subsubs4d |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
88 |
66 86 87
|
3eqtrrd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) with typecode |- |
89 |
|
oveq2 |
Could not format ( x = ( ( w -s t ) -s 1s ) -> ( 2s x.s x ) = ( 2s x.s ( ( w -s t ) -s 1s ) ) ) : No typesetting found for |- ( x = ( ( w -s t ) -s 1s ) -> ( 2s x.s x ) = ( 2s x.s ( ( w -s t ) -s 1s ) ) ) with typecode |- |
90 |
89
|
oveq1d |
Could not format ( x = ( ( w -s t ) -s 1s ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) : No typesetting found for |- ( x = ( ( w -s t ) -s 1s ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) with typecode |- |
91 |
90
|
rspceeqv |
Could not format ( ( ( ( w -s t ) -s 1s ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( ( ( w -s t ) -s 1s ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
92 |
53 88 91
|
syl2anc |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
93 |
|
oveq12 |
Could not format ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
94 |
93
|
eqeq1d |
Could not format ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
95 |
94
|
rexbidv |
Could not format ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
96 |
92 95
|
syl5ibrcom |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
97 |
96
|
rexlimivv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
98 |
50 97
|
sylbir |
Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |- |
99 |
98
|
olcd |
Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
100 |
|
reeanv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
101 |
33 35 36 35
|
addsubs4d |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) ) with typecode |- |
102 |
|
subsid |
|
103 |
34 102
|
ax-mp |
|
104 |
103
|
oveq2i |
Could not format ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) : No typesetting found for |- ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) with typecode |- |
105 |
33 36
|
subscld |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) e. No ) with typecode |- |
106 |
105
|
addsridd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) with typecode |- |
107 |
106 21
|
eqtrd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( 2s x.s ( w -s t ) ) ) with typecode |- |
108 |
104 107
|
eqtrid |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( 2s x.s ( w -s t ) ) ) with typecode |- |
109 |
101 108
|
eqtrd |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) with typecode |- |
110 |
22
|
rspceeqv |
Could not format ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) with typecode |- |
111 |
13 109 110
|
syl2anc |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) with typecode |- |
112 |
|
oveq12 |
Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) ) with typecode |- |
113 |
112
|
eqeq1d |
Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) with typecode |- |
114 |
113
|
rexbidv |
Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) with typecode |- |
115 |
111 114
|
syl5ibrcom |
Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) with typecode |- |
116 |
115
|
rexlimivv |
Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |- |
117 |
100 116
|
sylbir |
Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |- |
118 |
117
|
orcd |
Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
119 |
31 49 99 118
|
ccase |
Could not format ( ( ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) /\ ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) /\ ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
120 |
4 7 119
|
syl2an |
Could not format ( ( y e. NN_s /\ z e. NN_s ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y e. NN_s /\ z e. NN_s ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
121 |
|
eqeq1 |
Could not format ( N = ( y -s z ) -> ( N = ( 2s x.s x ) <-> ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( N = ( 2s x.s x ) <-> ( y -s z ) = ( 2s x.s x ) ) ) with typecode |- |
122 |
121
|
rexbidv |
Could not format ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) <-> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) <-> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) with typecode |- |
123 |
|
eqeq1 |
Could not format ( N = ( y -s z ) -> ( N = ( ( 2s x.s x ) +s 1s ) <-> ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( N = ( ( 2s x.s x ) +s 1s ) <-> ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
124 |
123
|
rexbidv |
Could not format ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
125 |
122 124
|
orbi12d |
Could not format ( N = ( y -s z ) -> ( ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) ) with typecode |- |
126 |
120 125
|
syl5ibrcom |
Could not format ( ( y e. NN_s /\ z e. NN_s ) -> ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) ) : No typesetting found for |- ( ( y e. NN_s /\ z e. NN_s ) -> ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) ) with typecode |- |
127 |
126
|
rexlimivv |
Could not format ( E. y e. NN_s E. z e. NN_s N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( E. y e. NN_s E. z e. NN_s N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |
128 |
1 127
|
sylbi |
Could not format ( N e. ZZ_s -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( N e. ZZ_s -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |- |