Theorem zs12zodd

Description: A dyadic fraction is either an integer or an odd number divided by a positive power of two. (Contributed by Scott Fenton, 5-Dec-2025)

	Ref	Expression
Assertion	zs12zodd	Could not format assertion : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elzs12	Could not format ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. b e. NN0_s A = ( a /su ( 2s ^su b ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. b e. NN0_s A = ( a /su ( 2s ^su b ) ) ) with typecode |-
2		oveq2	Could not format ( c = 0s -> ( 2s ^su c ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( c = 0s -> ( 2s ^su c ) = ( 2s ^su 0s ) ) with typecode |-
3		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
4		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
5	3 4	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
6	2 5	eqtrdi	Could not format ( c = 0s -> ( 2s ^su c ) = 1s ) : No typesetting found for |- ( c = 0s -> ( 2s ^su c ) = 1s ) with typecode |-
7	6	oveq2d	Could not format ( c = 0s -> ( a /su ( 2s ^su c ) ) = ( a /su 1s ) ) : No typesetting found for |- ( c = 0s -> ( a /su ( 2s ^su c ) ) = ( a /su 1s ) ) with typecode |-
8	7	eleq1d	Could not format ( c = 0s -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su 1s ) e. ZZ_s ) ) : No typesetting found for |- ( c = 0s -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su 1s ) e. ZZ_s ) ) with typecode |-
9	7	eqeq1d	Could not format ( c = 0s -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = 0s -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
10	9	2rexbidv	Could not format ( c = 0s -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = 0s -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
11	8 10	orbi12d	Could not format ( c = 0s -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = 0s -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
12	11	ralbidv	Could not format ( c = 0s -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = 0s -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
13		oveq2	Could not format ( c = w -> ( 2s ^su c ) = ( 2s ^su w ) ) : No typesetting found for |- ( c = w -> ( 2s ^su c ) = ( 2s ^su w ) ) with typecode |-
14	13	oveq2d	Could not format ( c = w -> ( a /su ( 2s ^su c ) ) = ( a /su ( 2s ^su w ) ) ) : No typesetting found for |- ( c = w -> ( a /su ( 2s ^su c ) ) = ( a /su ( 2s ^su w ) ) ) with typecode |-
15	14	eleq1d	Could not format ( c = w -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su ( 2s ^su w ) ) e. ZZ_s ) ) : No typesetting found for |- ( c = w -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su ( 2s ^su w ) ) e. ZZ_s ) ) with typecode |-
16	14	eqeq1d	Could not format ( c = w -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = w -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
17	16	2rexbidv	Could not format ( c = w -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = w -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
18	15 17	orbi12d	Could not format ( c = w -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = w -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
19	18	ralbidv	Could not format ( c = w -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = w -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
20		oveq2	Could not format ( c = ( w +s 1s ) -> ( 2s ^su c ) = ( 2s ^su ( w +s 1s ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( 2s ^su c ) = ( 2s ^su ( w +s 1s ) ) ) with typecode |-
21	20	oveq2d	Could not format ( c = ( w +s 1s ) -> ( a /su ( 2s ^su c ) ) = ( a /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( a /su ( 2s ^su c ) ) = ( a /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
22	21	eleq1d	Could not format ( c = ( w +s 1s ) -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) with typecode |-
23	21	eqeq1d	Could not format ( c = ( w +s 1s ) -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
24	23	2rexbidv	Could not format ( c = ( w +s 1s ) -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
25	22 24	orbi12d	Could not format ( c = ( w +s 1s ) -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
26	25	ralbidv	Could not format ( c = ( w +s 1s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
27		oveq1	Could not format ( a = b -> ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( b /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( a = b -> ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( b /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
28	27	eleq1d	Could not format ( a = b -> ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) : No typesetting found for |- ( a = b -> ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) with typecode |-
29	27	eqeq1d	Could not format ( a = b -> ( ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( a = b -> ( ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
30	29	2rexbidv	Could not format ( a = b -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( a = b -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
31		oveq2	Could not format ( x = p -> ( 2s x.s x ) = ( 2s x.s p ) ) : No typesetting found for |- ( x = p -> ( 2s x.s x ) = ( 2s x.s p ) ) with typecode |-
32	31	oveq1d	Could not format ( x = p -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s p ) +s 1s ) ) : No typesetting found for |- ( x = p -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s p ) +s 1s ) ) with typecode |-
33	32	oveq1d	Could not format ( x = p -> ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) ) : No typesetting found for |- ( x = p -> ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) ) with typecode |-
34	33	eqeq2d	Could not format ( x = p -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( x = p -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
35		oveq2	Could not format ( y = q -> ( 2s ^su y ) = ( 2s ^su q ) ) : No typesetting found for |- ( y = q -> ( 2s ^su y ) = ( 2s ^su q ) ) with typecode |-
36	35	oveq2d	Could not format ( y = q -> ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) : No typesetting found for |- ( y = q -> ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) with typecode |-
37	36	eqeq2d	Could not format ( y = q -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( y = q -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) <-> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
38	34 37	cbvrex2vw	Could not format ( E. x e. ZZ_s E. y e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) : No typesetting found for |- ( E. x e. ZZ_s E. y e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) with typecode |-
39	30 38	bitrdi	Could not format ( a = b -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( a = b -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
40	28 39	orbi12d	Could not format ( a = b -> ( ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( a = b -> ( ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
41	40	cbvralvw	Could not format ( A. a e. ZZ_s ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( A. a e. ZZ_s ( ( a /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
42	26 41	bitrdi	Could not format ( c = ( w +s 1s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( c = ( w +s 1s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
43		oveq2	Could not format ( c = b -> ( 2s ^su c ) = ( 2s ^su b ) ) : No typesetting found for |- ( c = b -> ( 2s ^su c ) = ( 2s ^su b ) ) with typecode |-
44	43	oveq2d	Could not format ( c = b -> ( a /su ( 2s ^su c ) ) = ( a /su ( 2s ^su b ) ) ) : No typesetting found for |- ( c = b -> ( a /su ( 2s ^su c ) ) = ( a /su ( 2s ^su b ) ) ) with typecode |-
45	44	eleq1d	Could not format ( c = b -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su ( 2s ^su b ) ) e. ZZ_s ) ) : No typesetting found for |- ( c = b -> ( ( a /su ( 2s ^su c ) ) e. ZZ_s <-> ( a /su ( 2s ^su b ) ) e. ZZ_s ) ) with typecode |-
46	44	eqeq1d	Could not format ( c = b -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = b -> ( ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
47	46	2rexbidv	Could not format ( c = b -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( c = b -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
48	45 47	orbi12d	Could not format ( c = b -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = b -> ( ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
49	48	ralbidv	Could not format ( c = b -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c = b -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su c ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su c ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> A. a e. ZZ_s ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
50		zno	$$⊢a\in {\mathbb{Z}}_s\to a\in \mathrm{No}$$
51		divs1	$$⊢a\in \mathrm{No}\to a{/}_{\mathrm{su}}{1}_s=a$$
52	50 51	syl	$$⊢a\in {\mathbb{Z}}_s\to a{/}_{\mathrm{su}}{1}_s=a$$
53		id	$$⊢a\in {\mathbb{Z}}_s\to a\in {\mathbb{Z}}_s$$
54	52 53	eqeltrd	$$⊢a\in {\mathbb{Z}}_s\to a{/}_{\mathrm{su}}{1}_s\in {\mathbb{Z}}_s$$
55	54	orcd	Could not format ( a e. ZZ_s -> ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( a e. ZZ_s -> ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
56	55	rgen	Could not format A. a e. ZZ_s ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) : No typesetting found for |- A. a e. ZZ_s ( ( a /su 1s ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su 1s ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) with typecode |-
57		zseo	Could not format ( b e. ZZ_s -> ( E. c e. ZZ_s b = ( 2s x.s c ) \/ E. c e. ZZ_s b = ( ( 2s x.s c ) +s 1s ) ) ) : No typesetting found for |- ( b e. ZZ_s -> ( E. c e. ZZ_s b = ( 2s x.s c ) \/ E. c e. ZZ_s b = ( ( 2s x.s c ) +s 1s ) ) ) with typecode |-
58		oveq1	Could not format ( a = c -> ( a /su ( 2s ^su w ) ) = ( c /su ( 2s ^su w ) ) ) : No typesetting found for |- ( a = c -> ( a /su ( 2s ^su w ) ) = ( c /su ( 2s ^su w ) ) ) with typecode |-
59	58	eleq1d	Could not format ( a = c -> ( ( a /su ( 2s ^su w ) ) e. ZZ_s <-> ( c /su ( 2s ^su w ) ) e. ZZ_s ) ) : No typesetting found for |- ( a = c -> ( ( a /su ( 2s ^su w ) ) e. ZZ_s <-> ( c /su ( 2s ^su w ) ) e. ZZ_s ) ) with typecode |-
60	58	eqeq1d	Could not format ( a = c -> ( ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( a = c -> ( ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
61	60	2rexbidv	Could not format ( a = c -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( a = c -> ( E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
62	59 61	orbi12d	Could not format ( a = c -> ( ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( a = c -> ( ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
63	62	rspcv	Could not format ( c e. ZZ_s -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( c e. ZZ_s -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
64	63	adantl	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
65	33	eqeq2d	Could not format ( x = p -> ( ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( x = p -> ( ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
66	36	eqeq2d	Could not format ( y = q -> ( ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( y = q -> ( ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su y ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
67	65 66	cbvrex2vw	Could not format ( E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) : No typesetting found for |- ( E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) with typecode |-
68	67	orbi2i	Could not format ( ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
69	64 68	imbitrdi	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
70	69	imp	Could not format ( ( ( w e. NN0_s /\ c e. ZZ_s ) /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ c e. ZZ_s ) /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
71	70	an32s	Could not format ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
72		simpl	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to w\in {\mathbb{N}}_{\mathrm{0s}}$$
73		expsp1	Could not format ( ( 2s e. No /\ w e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) = ( ( 2s ^su w ) x.s 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ w e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) = ( ( 2s ^su w ) x.s 2s ) ) with typecode |-
74	3 72 73	sylancr	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) = ( ( 2s ^su w ) x.s 2s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) = ( ( 2s ^su w ) x.s 2s ) ) with typecode |-
75	74	oveq1d	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s ^su ( w +s 1s ) ) x.s c ) = ( ( ( 2s ^su w ) x.s 2s ) x.s c ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s ^su ( w +s 1s ) ) x.s c ) = ( ( ( 2s ^su w ) x.s 2s ) x.s c ) ) with typecode |-
76		expscl	Could not format ( ( 2s e. No /\ w e. NN0_s ) -> ( 2s ^su w ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ w e. NN0_s ) -> ( 2s ^su w ) e. No ) with typecode |-
77	3 72 76	sylancr	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su w ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su w ) e. No ) with typecode |-
78	3	a1i	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> 2s e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> 2s e. No ) with typecode |-
79		zno	$$⊢c\in {\mathbb{Z}}_s\to c\in \mathrm{No}$$
80	79	adantl	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to c\in \mathrm{No}$$
81	77 78 80	mulsassd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su w ) x.s 2s ) x.s c ) = ( ( 2s ^su w ) x.s ( 2s x.s c ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su w ) x.s 2s ) x.s c ) = ( ( 2s ^su w ) x.s ( 2s x.s c ) ) ) with typecode |-
82	75 81	eqtrd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s ^su ( w +s 1s ) ) x.s c ) = ( ( 2s ^su w ) x.s ( 2s x.s c ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s ^su ( w +s 1s ) ) x.s c ) = ( ( 2s ^su w ) x.s ( 2s x.s c ) ) ) with typecode |-
83	82	oveq1d	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su ( w +s 1s ) ) x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s ^su w ) x.s ( 2s x.s c ) ) /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su ( w +s 1s ) ) x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s ^su w ) x.s ( 2s x.s c ) ) /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
84		peano2n0s	$$⊢w\in {\mathbb{N}}_{\mathrm{0s}}\to w{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
85	84	adantr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to w{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
86	80 85	pw2divscan3d	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su ( w +s 1s ) ) x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = c ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su ( w +s 1s ) ) x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = c ) with typecode |-
87	78 80	mulscld	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s x.s c ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s x.s c ) e. No ) with typecode |-
88		expscl	Could not format ( ( 2s e. No /\ ( w +s 1s ) e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ ( w +s 1s ) e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) e. No ) with typecode |-
89	3 85 88	sylancr	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) e. No ) with typecode |-
90		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
91		expsne0	Could not format ( ( 2s e. No /\ 2s =/= 0s /\ ( w +s 1s ) e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) =/= 0s ) : No typesetting found for |- ( ( 2s e. No /\ 2s =/= 0s /\ ( w +s 1s ) e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) =/= 0s ) with typecode |-
92	3 90 85 91	mp3an12i	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) =/= 0s ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) =/= 0s ) with typecode |-
93		pw2recs	Could not format ( ( w +s 1s ) e. NN0_s -> E. x e. No ( ( 2s ^su ( w +s 1s ) ) x.s x ) = 1s ) : No typesetting found for |- ( ( w +s 1s ) e. NN0_s -> E. x e. No ( ( 2s ^su ( w +s 1s ) ) x.s x ) = 1s ) with typecode |-
94	85 93	syl	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> E. x e. No ( ( 2s ^su ( w +s 1s ) ) x.s x ) = 1s ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> E. x e. No ( ( 2s ^su ( w +s 1s ) ) x.s x ) = 1s ) with typecode |-
95	77 87 89 92 94	divsasswd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su w ) x.s ( 2s x.s c ) ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( 2s ^su w ) x.s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su w ) x.s ( 2s x.s c ) ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( 2s ^su w ) x.s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) ) with typecode |-
96	83 86 95	3eqtr3rd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s ^su w ) x.s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) = c ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s ^su w ) x.s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) = c ) with typecode |-
97	87 85	pw2divscld	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. No ) with typecode |-
98	80 97 72	pw2divsmuld	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( c /su ( 2s ^su w ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) <-> ( ( 2s ^su w ) x.s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) = c ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( c /su ( 2s ^su w ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) <-> ( ( 2s ^su w ) x.s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) = c ) ) with typecode |-
99	96 98	mpbird	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( c /su ( 2s ^su w ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( c /su ( 2s ^su w ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
100	99	eqcomd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( c /su ( 2s ^su w ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( c /su ( 2s ^su w ) ) ) with typecode |-
101	100	eleq1d	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( c /su ( 2s ^su w ) ) e. ZZ_s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( c /su ( 2s ^su w ) ) e. ZZ_s ) ) with typecode |-
102	100	eqeq1d	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
103	102	2rexbidv	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
104	101 103	orbi12d	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
105	104	adantlr	Could not format ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( c /su ( 2s ^su w ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( c /su ( 2s ^su w ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
106	71 105	mpbird	Could not format ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
107		oveq1	Could not format ( b = ( 2s x.s c ) -> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( b = ( 2s x.s c ) -> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
108	107	eleq1d	Could not format ( b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) : No typesetting found for |- ( b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) with typecode |-
109	107	eqeq1d	Could not format ( b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
110	109	2rexbidv	Could not format ( b = ( 2s x.s c ) -> ( E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( b = ( 2s x.s c ) -> ( E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
111	108 110	orbi12d	Could not format ( b = ( 2s x.s c ) -> ( ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( b = ( 2s x.s c ) -> ( ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
112	106 111	syl5ibrcom	Could not format ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
113	112	rexlimdva	Could not format ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( E. c e. ZZ_s b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( E. c e. ZZ_s b = ( 2s x.s c ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
114		oveq2	Could not format ( p = c -> ( 2s x.s p ) = ( 2s x.s c ) ) : No typesetting found for |- ( p = c -> ( 2s x.s p ) = ( 2s x.s c ) ) with typecode |-
115	114	oveq1d	Could not format ( p = c -> ( ( 2s x.s p ) +s 1s ) = ( ( 2s x.s c ) +s 1s ) ) : No typesetting found for |- ( p = c -> ( ( 2s x.s p ) +s 1s ) = ( ( 2s x.s c ) +s 1s ) ) with typecode |-
116	115	oveq1d	Could not format ( p = c -> ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) ) : No typesetting found for |- ( p = c -> ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) ) with typecode |-
117	116	eqeq2d	Could not format ( p = c -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( p = c -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
118		oveq2	Could not format ( q = ( w +s 1s ) -> ( 2s ^su q ) = ( 2s ^su ( w +s 1s ) ) ) : No typesetting found for |- ( q = ( w +s 1s ) -> ( 2s ^su q ) = ( 2s ^su ( w +s 1s ) ) ) with typecode |-
119	118	oveq2d	Could not format ( q = ( w +s 1s ) -> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( q = ( w +s 1s ) -> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
120	119	eqeq2d	Could not format ( q = ( w +s 1s ) -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) ) : No typesetting found for |- ( q = ( w +s 1s ) -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) ) with typecode |-
121		simpr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to c\in {\mathbb{Z}}_s$$
122		n0p1nns	$$⊢w\in {\mathbb{N}}_{\mathrm{0s}}\to w{+}_s{1}_s\in {\mathbb{N}}_s$$
123	122	adantr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to w{+}_s{1}_s\in {\mathbb{N}}_s$$
124		eqidd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
125	117 120 121 123 124	2rspcedvdw	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) with typecode |-
126	125	olcd	Could not format ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
127	126	adantlr	Could not format ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
128		oveq1	Could not format ( b = ( ( 2s x.s c ) +s 1s ) -> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) : No typesetting found for |- ( b = ( ( 2s x.s c ) +s 1s ) -> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) ) with typecode |-
129	128	eleq1d	Could not format ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) : No typesetting found for |- ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s ) ) with typecode |-
130	128	eqeq1d	Could not format ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
131	130	2rexbidv	Could not format ( b = ( ( 2s x.s c ) +s 1s ) -> ( E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( b = ( ( 2s x.s c ) +s 1s ) -> ( E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) <-> E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
132	129 131	orbi12d	Could not format ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) <-> ( ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
133	127 132	syl5ibrcom	Could not format ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) /\ c e. ZZ_s ) -> ( b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
134	133	rexlimdva	Could not format ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( E. c e. ZZ_s b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( E. c e. ZZ_s b = ( ( 2s x.s c ) +s 1s ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
135	113 134	jaod	Could not format ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( ( E. c e. ZZ_s b = ( 2s x.s c ) \/ E. c e. ZZ_s b = ( ( 2s x.s c ) +s 1s ) ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( ( E. c e. ZZ_s b = ( 2s x.s c ) \/ E. c e. ZZ_s b = ( ( 2s x.s c ) +s 1s ) ) -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
136	57 135	syl5	Could not format ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( b e. ZZ_s -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> ( b e. ZZ_s -> ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
137	136	ralrimiv	Could not format ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) -> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) with typecode |-
138	137	ex	Could not format ( w e. NN0_s -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( w e. NN0_s -> ( A. a e. ZZ_s ( ( a /su ( 2s ^su w ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su w ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> A. b e. ZZ_s ( ( b /su ( 2s ^su ( w +s 1s ) ) ) e. ZZ_s \/ E. p e. ZZ_s E. q e. NN_s ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) ) ) ) with typecode |-
139	12 19 42 49 56 138	n0sind	Could not format ( b e. NN0_s -> A. a e. ZZ_s ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( b e. NN0_s -> A. a e. ZZ_s ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
140		rsp	Could not format ( A. a e. ZZ_s ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( a e. ZZ_s -> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( A. a e. ZZ_s ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) -> ( a e. ZZ_s -> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
141	139 140	syl	Could not format ( b e. NN0_s -> ( a e. ZZ_s -> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( b e. NN0_s -> ( a e. ZZ_s -> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
142	141	impcom	Could not format ( ( a e. ZZ_s /\ b e. NN0_s ) -> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ b e. NN0_s ) -> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
143		eleq1	Could not format ( A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s <-> ( a /su ( 2s ^su b ) ) e. ZZ_s ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s <-> ( a /su ( 2s ^su b ) ) e. ZZ_s ) ) with typecode |-
144		eqeq1	Could not format ( A = ( a /su ( 2s ^su b ) ) -> ( A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su b ) ) -> ( A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
145	144	2rexbidv	Could not format ( A = ( a /su ( 2s ^su b ) ) -> ( E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su b ) ) -> ( E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) <-> E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
146	143 145	orbi12d	Could not format ( A = ( a /su ( 2s ^su b ) ) -> ( ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su b ) ) -> ( ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) <-> ( ( a /su ( 2s ^su b ) ) e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s ( a /su ( 2s ^su b ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
147	142 146	syl5ibrcom	Could not format ( ( a e. ZZ_s /\ b e. NN0_s ) -> ( A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ b e. NN0_s ) -> ( A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) ) with typecode |-
148	147	rexlimivv	Could not format ( E. a e. ZZ_s E. b e. NN0_s A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( E. a e. ZZ_s E. b e. NN0_s A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-
149	1 148	sylbi	Could not format ( A e. ZZ_s[1/2] -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A e. ZZ_s \/ E. x e. ZZ_s E. y e. NN_s A = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su y ) ) ) ) with typecode |-