Theorem zs12ge0

Description: An expression for non-negative dyadic rationals. (Contributed by Scott Fenton, 8-Nov-2025)

	Ref	Expression
Assertion	zs12ge0	Could not format assertion : No typesetting found for |- ( ( A e. No /\ 0s <_s A ) -> ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y

Proof

Step	Hyp	Ref	Expression
1		simprl	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> z e. ZZ_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> z e. ZZ_s ) with typecode |-
2		simpllr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> 0s <_s A ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> 0s <_s A ) with typecode |-
3		simprr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> A = ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> A = ( z /su ( 2s ^su p ) ) ) with typecode |-
4	2 3	breqtrd	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> 0s <_s ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> 0s <_s ( z /su ( 2s ^su p ) ) ) with typecode |-
5	1	znod	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> z e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> z e. No ) with typecode |-
6		simplr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> p e. NN0_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> p e. NN0_s ) with typecode |-
7	5 6	pw2ge0divsd	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> ( 0s <_s z <-> 0s <_s ( z /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> ( 0s <_s z <-> 0s <_s ( z /su ( 2s ^su p ) ) ) ) with typecode |-
8	4 7	mpbird	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> 0s <_s z ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> 0s <_s z ) with typecode |-
9		eln0zs	$$⊢z\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(z\in {\mathbb{Z}}_s\wedge 0_s{\le }_{s}z\right)$$
10	1 8 9	sylanbrc	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> z e. NN0_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> z e. NN0_s ) with typecode |-
11		simpr	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to z\in {\mathbb{N}}_{\mathrm{0s}}$$
12		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
13		simplr	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\to p\in {\mathbb{N}}_{\mathrm{0s}}$$
14		nnexpscl	Could not format ( ( 2s e. NN_s /\ p e. NN0_s ) -> ( 2s ^su p ) e. NN_s ) : No typesetting found for |- ( ( 2s e. NN_s /\ p e. NN0_s ) -> ( 2s ^su p ) e. NN_s ) with typecode |-
15	12 13 14	sylancr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) -> ( 2s ^su p ) e. NN_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) -> ( 2s ^su p ) e. NN_s ) with typecode |-
16		eucliddivs	Could not format ( ( z e. NN0_s /\ ( 2s ^su p ) e. NN_s ) -> E. x e. NN0_s E. y e. NN0_s ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y E. x e. NN0_s E. y e. NN0_s ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y
17	11 15 16	syl2anc	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) -> E. x e. NN0_s E. y e. NN0_s ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y E. x e. NN0_s E. y e. NN0_s ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y
18		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
19		simpllr	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to p\in {\mathbb{N}}_{\mathrm{0s}}$$
20		expscl	Could not format ( ( 2s e. No /\ p e. NN0_s ) -> ( 2s ^su p ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ p e. NN0_s ) -> ( 2s ^su p ) e. No ) with typecode |-
21	18 19 20	sylancr	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( 2s ^su p ) e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( 2s ^su p ) e. No ) with typecode |-
22		simprl	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to x\in {\mathbb{N}}_{\mathrm{0s}}$$
23	22	n0snod	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to x\in \mathrm{No}$$
24		simprr	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to y\in {\mathbb{N}}_{\mathrm{0s}}$$
25	24	n0snod	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to y\in \mathrm{No}$$
26	25 19	pw2divscld	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( y /su ( 2s ^su p ) ) e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( y /su ( 2s ^su p ) ) e. No ) with typecode |-
27	21 23 26	addsdid	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = ( ( ( 2s ^su p ) x.s x ) +s ( ( 2s ^su p ) x.s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = ( ( ( 2s ^su p ) x.s x ) +s ( ( 2s ^su p ) x.s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
28	25 19	pw2divscan2d	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s ( y /su ( 2s ^su p ) ) ) = y ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s ( y /su ( 2s ^su p ) ) ) = y ) with typecode |-
29	28	oveq2d	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) +s ( ( 2s ^su p ) x.s ( y /su ( 2s ^su p ) ) ) ) = ( ( ( 2s ^su p ) x.s x ) +s y ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) +s ( ( 2s ^su p ) x.s ( y /su ( 2s ^su p ) ) ) ) = ( ( ( 2s ^su p ) x.s x ) +s y ) ) with typecode |-
30	27 29	eqtrd	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = ( ( ( 2s ^su p ) x.s x ) +s y ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = ( ( ( 2s ^su p ) x.s x ) +s y ) ) with typecode |-
31	30	eqeq2d	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( z = ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) <-> z = ( ( ( 2s ^su p ) x.s x ) +s y ) ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( z = ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) <-> z = ( ( ( 2s ^su p ) x.s x ) +s y ) ) ) with typecode |-
32		eqcom	Could not format ( z = ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) <-> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = z ) : No typesetting found for |- ( z = ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) <-> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = z ) with typecode |-
33	31 32	bitr3di	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) <-> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = z ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) <-> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = z ) ) with typecode |-
34		simplr	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to z\in {\mathbb{N}}_{\mathrm{0s}}$$
35	34	n0snod	$$⊢\left(\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge z\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to z\in \mathrm{No}$$
36	23 26	addscld	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( x +s ( y /su ( 2s ^su p ) ) ) e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( x +s ( y /su ( 2s ^su p ) ) ) e. No ) with typecode |-
37	35 36 19	pw2divsmuld	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) <-> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = z ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) <-> ( ( 2s ^su p ) x.s ( x +s ( y /su ( 2s ^su p ) ) ) ) = z ) ) with typecode |-
38	33 37	bitr4d	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) <-> ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) <-> ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
39	38	anbi1d	Could not format ( ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
40	39	2rexbidva	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) -> ( E. x e. NN0_s E. y e. NN0_s ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( E. x e. NN0_s E. y e. NN0_s ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) /\ y E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
41	17 40	mpbid	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ z e. NN0_s ) -> E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
42	41	adantrl	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
43		simprl	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> A = ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> A = ( z /su ( 2s ^su p ) ) ) with typecode |-
44	43	eqeq1d	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> ( A = ( x +s ( y /su ( 2s ^su p ) ) ) <-> ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> ( A = ( x +s ( y /su ( 2s ^su p ) ) ) <-> ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
45	44	anbi1d	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
46	45	2rexbidv	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> ( E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s ( ( z /su ( 2s ^su p ) ) = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
47	42 46	mpbird	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( A = ( z /su ( 2s ^su p ) ) /\ z e. NN0_s ) ) -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
48	47	expr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ A = ( z /su ( 2s ^su p ) ) ) -> ( z e. NN0_s -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z e. NN0_s -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
49	48	adantrl	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> ( z e. NN0_s -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( z e. NN0_s -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
50	10 49	mpd	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( z e. ZZ_s /\ A = ( z /su ( 2s ^su p ) ) ) ) -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
51	50	rexlimdvaa	Could not format ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) -> ( E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) -> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
52		oveq1	Could not format ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) -> ( z /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) ) : No typesetting found for |- ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) -> ( z /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) ) with typecode |-
53	52	eqeq2d	Could not format ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) -> ( ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) <-> ( x +s ( y /su ( 2s ^su p ) ) ) = ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( z = ( ( ( 2s ^su p ) x.s x ) +s y ) -> ( ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) <-> ( x +s ( y /su ( 2s ^su p ) ) ) = ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) ) ) with typecode |-
54		nnn0s	Could not format ( 2s e. NN_s -> 2s e. NN0_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. NN0_s ) with typecode |-
55	12 54	ax-mp	Could not format 2s e. NN0_s : No typesetting found for |- 2s e. NN0_s with typecode |-
56		simplr	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to p\in {\mathbb{N}}_{\mathrm{0s}}$$
57		n0expscl	Could not format ( ( 2s e. NN0_s /\ p e. NN0_s ) -> ( 2s ^su p ) e. NN0_s ) : No typesetting found for |- ( ( 2s e. NN0_s /\ p e. NN0_s ) -> ( 2s ^su p ) e. NN0_s ) with typecode |-
58	55 56 57	sylancr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( 2s ^su p ) e. NN0_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( 2s ^su p ) e. NN0_s ) with typecode |-
59		simprl	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to x\in {\mathbb{N}}_{\mathrm{0s}}$$
60		n0mulscl	Could not format ( ( ( 2s ^su p ) e. NN0_s /\ x e. NN0_s ) -> ( ( 2s ^su p ) x.s x ) e. NN0_s ) : No typesetting found for |- ( ( ( 2s ^su p ) e. NN0_s /\ x e. NN0_s ) -> ( ( 2s ^su p ) x.s x ) e. NN0_s ) with typecode |-
61	58 59 60	syl2anc	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s x ) e. NN0_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s x ) e. NN0_s ) with typecode |-
62		simprr	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to y\in {\mathbb{N}}_{\mathrm{0s}}$$
63		n0addscl	Could not format ( ( ( ( 2s ^su p ) x.s x ) e. NN0_s /\ y e. NN0_s ) -> ( ( ( 2s ^su p ) x.s x ) +s y ) e. NN0_s ) : No typesetting found for |- ( ( ( ( 2s ^su p ) x.s x ) e. NN0_s /\ y e. NN0_s ) -> ( ( ( 2s ^su p ) x.s x ) +s y ) e. NN0_s ) with typecode |-
64	61 62 63	syl2anc	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) +s y ) e. NN0_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) +s y ) e. NN0_s ) with typecode |-
65	64	n0zsd	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) +s y ) e. ZZ_s ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) +s y ) e. ZZ_s ) with typecode |-
66	59	n0snod	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to x\in \mathrm{No}$$
67	66 56	pw2divscan3d	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) = x ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) = x ) with typecode |-
68	67	eqcomd	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> x = ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> x = ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) ) with typecode |-
69	68	oveq1d	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) +s ( y /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) +s ( y /su ( 2s ^su p ) ) ) ) with typecode |-
70	18 56 20	sylancr	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( 2s ^su p ) e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( 2s ^su p ) e. No ) with typecode |-
71	70 66	mulscld	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s x ) e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( 2s ^su p ) x.s x ) e. No ) with typecode |-
72	62	n0snod	$$⊢\left(\left(\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to y\in \mathrm{No}$$
73	71 72 56	pw2divsdird	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) +s ( y /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su p ) x.s x ) /su ( 2s ^su p ) ) +s ( y /su ( 2s ^su p ) ) ) ) with typecode |-
74	69 73	eqtr4d	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( ( ( ( 2s ^su p ) x.s x ) +s y ) /su ( 2s ^su p ) ) ) with typecode |-
75	53 65 74	rspcedvdw	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> E. z e. ZZ_s ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> E. z e. ZZ_s ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) ) with typecode |-
76		eqeq1	Could not format ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( A = ( z /su ( 2s ^su p ) ) <-> ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( A = ( z /su ( 2s ^su p ) ) <-> ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) ) ) with typecode |-
77	76	rexbidv	Could not format ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) <-> E. z e. ZZ_s ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) <-> E. z e. ZZ_s ( x +s ( y /su ( 2s ^su p ) ) ) = ( z /su ( 2s ^su p ) ) ) ) with typecode |-
78	75 77	syl5ibrcom	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) ) with typecode |-
79	78	adantrd	Could not format ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) /\ ( x e. NN0_s /\ y e. NN0_s ) ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) ) with typecode |-
80	79	rexlimdvva	Could not format ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) -> ( E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) -> ( E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) ) with typecode |-
81	51 80	impbid	Could not format ( ( ( A e. No /\ 0s <_s A ) /\ p e. NN0_s ) -> ( E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) <-> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) <-> E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
82	81	rexbidva	Could not format ( ( A e. No /\ 0s <_s A ) -> ( E. p e. NN0_s E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) <-> E. p e. NN0_s E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( E. p e. NN0_s E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) <-> E. p e. NN0_s E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
83		elzs12	Could not format ( A e. ZZ_s[1/2] <-> E. z e. ZZ_s E. p e. NN0_s A = ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. z e. ZZ_s E. p e. NN0_s A = ( z /su ( 2s ^su p ) ) ) with typecode |-
84		rexcom	Could not format ( E. z e. ZZ_s E. p e. NN0_s A = ( z /su ( 2s ^su p ) ) <-> E. p e. NN0_s E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( E. z e. ZZ_s E. p e. NN0_s A = ( z /su ( 2s ^su p ) ) <-> E. p e. NN0_s E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) with typecode |-
85	83 84	bitri	Could not format ( A e. ZZ_s[1/2] <-> E. p e. NN0_s E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. p e. NN0_s E. z e. ZZ_s A = ( z /su ( 2s ^su p ) ) ) with typecode |-
86		rexcom	Could not format ( E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
87	86	rexbii	Could not format ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. p e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. p e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
88		rexcom	Could not format ( E. x e. NN0_s E. p e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
89	87 88	bitri	Could not format ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s E. x e. NN0_s E. y e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
90	82 85 89	3bitr4g	Could not format ( ( A e. No /\ 0s <_s A ) -> ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y