Metamath Proof Explorer

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 
|- ( 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 ) ) ) )

Proof

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