Metamath Proof Explorer

Theorem zs12ge0

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

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