Metamath Proof Explorer

Theorem zs12zodd

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

Ref Expression
Assertion zs12zodd 
|- ( 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 elzs12 
 |-  ( 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 2sno 
 |-  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 divs1 
 |-  ( a e. No -> ( a /su 1s ) = a )
52 50 51 syl 
 |-  ( a e. ZZ_s -> ( a /su 1s ) = a )
53 id 
 |-  ( a e. ZZ_s -> a e. ZZ_s )
54 52 53 eqeltrd 
 |-  ( a e. ZZ_s -> ( a /su 1s ) e. ZZ_s )
55 54 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 ) ) ) )
56 55 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 ) ) )
57 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 ) ) )
58 oveq1 
 |-  ( a = c -> ( a /su ( 2s ^su w ) ) = ( c /su ( 2s ^su w ) ) )
59 58 eleq1d 
 |-  ( a = c -> ( ( a /su ( 2s ^su w ) ) e. ZZ_s <-> ( c /su ( 2s ^su w ) ) e. ZZ_s ) )
60 58 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 ) ) ) )
61 60 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 ) ) ) )
62 59 61 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 ) ) ) ) )
63 62 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 ) ) ) ) )
64 63 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 ) ) ) ) )
65 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 ) ) ) )
66 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 ) ) ) )
67 65 66 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 ) ) )
68 67 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 ) ) ) )
69 64 68 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 ) ) ) ) )
70 69 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 ) ) ) )
71 70 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 ) ) ) )
72 simpl 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> w e. NN0_s )
73 expsp1 
 |-  ( ( 2s e. No /\ w e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) = ( ( 2s ^su w ) x.s 2s ) )
74 3 72 73 sylancr 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) = ( ( 2s ^su w ) x.s 2s ) )
75 74 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 ) )
76 expscl 
 |-  ( ( 2s e. No /\ w e. NN0_s ) -> ( 2s ^su w ) e. No )
77 3 72 76 sylancr 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su w ) e. No )
78 3 a1i 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> 2s e. No )
79 zno 
 |-  ( c e. ZZ_s -> c e. No )
80 79 adantl 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> c e. No )
81 77 78 80 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 ) ) )
82 75 81 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 ) ) )
83 82 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 ) ) ) )
84 peano2n0s 
 |-  ( w e. NN0_s -> ( w +s 1s ) e. NN0_s )
85 84 adantr 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( w +s 1s ) e. NN0_s )
86 80 85 pw2divscan3d 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( ( 2s ^su ( w +s 1s ) ) x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = c )
87 78 80 mulscld 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s x.s c ) e. No )
88 expscl 
 |-  ( ( 2s e. No /\ ( w +s 1s ) e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) e. No )
89 3 85 88 sylancr 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) e. No )
90 2ne0s 
 |-  2s =/= 0s
91 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ ( w +s 1s ) e. NN0_s ) -> ( 2s ^su ( w +s 1s ) ) =/= 0s )
92 3 90 85 91 mp3an12i 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( 2s ^su ( w +s 1s ) ) =/= 0s )
93 pw2recs 
 |-  ( ( w +s 1s ) e. NN0_s -> E. x e. No ( ( 2s ^su ( w +s 1s ) ) x.s x ) = 1s )
94 85 93 syl 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> E. x e. No ( ( 2s ^su ( w +s 1s ) ) x.s x ) = 1s )
95 77 87 89 92 94 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 ) ) ) ) )
96 83 86 95 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 )
97 87 85 pw2divscld 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) e. No )
98 80 97 72 pw2divsmuld 
 |-  ( ( 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 ) )
99 96 98 mpbird 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( c /su ( 2s ^su w ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) )
100 99 eqcomd 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) = ( c /su ( 2s ^su w ) ) )
101 100 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 ) )
102 100 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 ) ) ) )
103 102 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 ) ) ) )
104 101 103 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 ) ) ) ) )
105 104 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 ) ) ) ) )
106 71 105 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 ) ) ) )
107 oveq1 
 |-  ( b = ( 2s x.s c ) -> ( b /su ( 2s ^su ( w +s 1s ) ) ) = ( ( 2s x.s c ) /su ( 2s ^su ( w +s 1s ) ) ) )
108 107 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 ) )
109 107 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 ) ) ) )
110 109 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 ) ) ) )
111 108 110 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 ) ) ) ) )
112 106 111 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 ) ) ) ) )
113 112 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 ) ) ) ) )
114 oveq2 
 |-  ( p = c -> ( 2s x.s p ) = ( 2s x.s c ) )
115 114 oveq1d 
 |-  ( p = c -> ( ( 2s x.s p ) +s 1s ) = ( ( 2s x.s c ) +s 1s ) )
116 115 oveq1d 
 |-  ( p = c -> ( ( ( 2s x.s p ) +s 1s ) /su ( 2s ^su q ) ) = ( ( ( 2s x.s c ) +s 1s ) /su ( 2s ^su q ) ) )
117 116 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 ) ) ) )
118 oveq2 
 |-  ( q = ( w +s 1s ) -> ( 2s ^su q ) = ( 2s ^su ( w +s 1s ) ) )
119 118 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 ) ) ) )
120 119 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 ) ) ) ) )
121 simpr 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> c e. ZZ_s )
122 n0p1nns 
 |-  ( w e. NN0_s -> ( w +s 1s ) e. NN_s )
123 122 adantr 
 |-  ( ( w e. NN0_s /\ c e. ZZ_s ) -> ( w +s 1s ) e. NN_s )
124 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 ) ) ) )
125 117 120 121 123 124 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 ) ) )
126 125 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 ) ) ) )
127 126 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 ) ) ) )
128 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 ) ) ) )
129 128 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 ) )
130 128 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 ) ) ) )
131 130 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 ) ) ) )
132 129 131 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 ) ) ) ) )
133 127 132 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 ) ) ) ) )
134 133 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 ) ) ) ) )
135 113 134 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 ) ) ) ) )
136 57 135 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 ) ) ) ) )
137 136 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 ) ) ) )
138 137 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 ) ) ) ) )
139 12 19 42 49 56 138 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 ) ) ) )
140 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 ) ) ) ) )
141 139 140 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 ) ) ) ) )
142 141 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 ) ) ) )
143 eleq1 
 |-  ( A = ( a /su ( 2s ^su b ) ) -> ( A e. ZZ_s <-> ( a /su ( 2s ^su b ) ) e. ZZ_s ) )
144 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 ) ) ) )
145 144 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 ) ) ) )
146 143 145 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 ) ) ) ) )
147 142 146 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 ) ) ) ) )
148 147 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 ) ) ) )
149 1 148 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 ) ) ) )