Theorem z12zsodd

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	z12zsodd	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		elz12s	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		2no	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	50	divs1d	$$⊢a\in {\mathbb{Z}}_s\to a{/}_{\mathrm{su}}{1}_s=a$$
52		id	$$⊢a\in {\mathbb{Z}}_s\to a\in {\mathbb{Z}}_s$$
53	51 52	eqeltrd	$$⊢a\in {\mathbb{Z}}_s\to a{/}_{\mathrm{su}}{1}_s\in {\mathbb{Z}}_s$$
54	53	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 |-
55	54	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 |-
56		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 |-
57		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 |-
58	57	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 |-
59	57	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 |-
60	59	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 |-
61	58 60	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 |-
62	61	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 |-
63	62	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 |-
64	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 |-
65	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 |-
66	64 65	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 |-
67	66	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 |-
68	63 67	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 |-
69	68	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 |-
70	69	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 |-
71		simpl	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to w\in {\mathbb{N}}_{\mathrm{0s}}$$
72		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 |-
73	3 71 72	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 |-
74	73	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 |-
75		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 |-
76	3 71 75	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 |-
77	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 |-
78		zno	$$⊢c\in {\mathbb{Z}}_s\to c\in \mathrm{No}$$
79	78	adantl	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to c\in \mathrm{No}$$
80	76 77 79	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 |-
81	74 80	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 |-
82	81	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 |-
83		peano2n0s	$$⊢w\in {\mathbb{N}}_{\mathrm{0s}}\to w{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
84	83	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}}$$
85	79 84	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 |-
86	77 79	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 |-
87		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 |-
88	3 84 87	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 |-
89		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
90		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 |-
91	3 89 84 90	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 |-
92		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 |-
93	84 92	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 |-
94	76 86 88 91 93	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 |-
95	82 85 94	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 |-
96	86 84	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 |-
97	79 96 71	pw2divmulsd	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 |-
98	95 97	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 |-
99	98	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 |-
100	99	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 |-
101	99	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 |-
102	101	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 |-
103	100 102	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 |-
104	103	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 |-
105	70 104	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 |-
106		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 |-
107	106	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 |-
108	106	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 |-
109	108	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 |-
110	107 109	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 |-
111	105 110	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 |-
112	111	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 |-
113		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 |-
114	113	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 |-
115	114	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 |-
116	115	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 |-
117		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 |-
118	117	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 |-
119	118	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 |-
120		simpr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to c\in {\mathbb{Z}}_s$$
121		n0p1nns	$$⊢w\in {\mathbb{N}}_{\mathrm{0s}}\to w{+}_s{1}_s\in {\mathbb{N}}_s$$
122	121	adantr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge c\in {\mathbb{Z}}_s\right)\to w{+}_s{1}_s\in {\mathbb{N}}_s$$
123		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 |-
124	116 119 120 122 123	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 |-
125	124	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 |-
126	125	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 |-
127		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 |-
128	127	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 |-
129	127	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 |-
130	129	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 |-
131	128 130	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 |-
132	126 131	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 |-
133	132	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 |-
134	112 133	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 |-
135	56 134	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 |-
136	135	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 |-
137	136	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 |-
138	12 19 42 49 55 137	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 |-
139		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 |-
140	138 139	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 |-
141	140	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 |-
142		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 |-
143		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 |-
144	143	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 |-
145	142 144	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 |-
146	141 145	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 |-
147	146	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 |-
148	1 147	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 |-