Metamath Proof Explorer

Theorem pw2cut2

Description: Cut expression for powers of two. Theorem 12 of Conway p. 12-13. (Contributed by Scott Fenton, 18-Jan-2026)

Ref Expression
Assertion pw2cut2 
|- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) )
2 2no 
 |-  2s e. No
3 exps0 
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
4 2 3 ax-mp 
 |-  ( 2s ^su 0s ) = 1s
5 1 4 eqtrdi 
 |-  ( m = 0s -> ( 2s ^su m ) = 1s )
6 5 oveq2d 
 |-  ( m = 0s -> ( A /su ( 2s ^su m ) ) = ( A /su 1s ) )
7 5 oveq2d 
 |-  ( m = 0s -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su 1s ) )
8 7 sneqd 
 |-  ( m = 0s -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su 1s ) } )
9 5 oveq2d 
 |-  ( m = 0s -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su 1s ) )
10 9 sneqd 
 |-  ( m = 0s -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su 1s ) } )
11 8 10 oveq12d 
 |-  ( m = 0s -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) )
12 6 11 eqeq12d 
 |-  ( m = 0s -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) )
13 12 imbi2d 
 |-  ( m = 0s -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) ) )
14 oveq2 
 |-  ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) )
15 14 oveq2d 
 |-  ( m = n -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su n ) ) )
16 14 oveq2d 
 |-  ( m = n -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su n ) ) )
17 16 sneqd 
 |-  ( m = n -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } )
18 14 oveq2d 
 |-  ( m = n -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su n ) ) )
19 18 sneqd 
 |-  ( m = n -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } )
20 17 19 oveq12d 
 |-  ( m = n -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) )
21 15 20 eqeq12d 
 |-  ( m = n -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) )
22 21 imbi2d 
 |-  ( m = n -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) ) )
23 oveq2 
 |-  ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) )
24 23 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su ( n +s 1s ) ) ) )
25 23 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
26 25 sneqd 
 |-  ( m = ( n +s 1s ) -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )
27 23 oveq2d 
 |-  ( m = ( n +s 1s ) -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
28 27 sneqd 
 |-  ( m = ( n +s 1s ) -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )
29 26 28 oveq12d 
 |-  ( m = ( n +s 1s ) -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
30 24 29 eqeq12d 
 |-  ( m = ( n +s 1s ) -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
31 30 imbi2d 
 |-  ( m = ( n +s 1s ) -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
32 oveq2 
 |-  ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) )
33 32 oveq2d 
 |-  ( m = N -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su N ) ) )
34 32 oveq2d 
 |-  ( m = N -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su N ) ) )
35 34 sneqd 
 |-  ( m = N -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su N ) ) } )
36 32 oveq2d 
 |-  ( m = N -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su N ) ) )
37 36 sneqd 
 |-  ( m = N -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su N ) ) } )
38 35 37 oveq12d 
 |-  ( m = N -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) )
39 33 38 eqeq12d 
 |-  ( m = N -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) )
40 39 imbi2d 
 |-  ( m = N -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) )
41 zcuts 
 |-  ( A e. ZZ_s -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
42 zno 
 |-  ( A e. ZZ_s -> A e. No )
43 42 divs1d 
 |-  ( A e. ZZ_s -> ( A /su 1s ) = A )
44 1no 
 |-  1s e. No
45 44 a1i 
 |-  ( A e. ZZ_s -> 1s e. No )
46 42 45 subscld 
 |-  ( A e. ZZ_s -> ( A -s 1s ) e. No )
47 46 divs1d 
 |-  ( A e. ZZ_s -> ( ( A -s 1s ) /su 1s ) = ( A -s 1s ) )
48 47 sneqd 
 |-  ( A e. ZZ_s -> { ( ( A -s 1s ) /su 1s ) } = { ( A -s 1s ) } )
49 42 45 addscld 
 |-  ( A e. ZZ_s -> ( A +s 1s ) e. No )
50 49 divs1d 
 |-  ( A e. ZZ_s -> ( ( A +s 1s ) /su 1s ) = ( A +s 1s ) )
51 50 sneqd 
 |-  ( A e. ZZ_s -> { ( ( A +s 1s ) /su 1s ) } = { ( A +s 1s ) } )
52 48 51 oveq12d 
 |-  ( A e. ZZ_s -> ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
53 41 43 52 3eqtr4d 
 |-  ( A e. ZZ_s -> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) )
54 simp2 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A e. ZZ_s )
55 54 znod 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A e. No )
56 44 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 1s e. No )
57 55 56 subscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s ) e. No )
58 simp1 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> n e. NN0_s )
59 peano2n0s 
 |-  ( n e. NN0_s -> ( n +s 1s ) e. NN0_s )
60 58 59 syl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( n +s 1s ) e. NN0_s )
61 57 60 pw2divscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No )
62 55 56 addscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A +s 1s ) e. No )
63 62 60 pw2divscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No )
64 55 ltsm1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s )
65 55 ltsp1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A
66 57 55 62 64 65 ltstrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s )
67 57 62 60 pw2ltsdiv1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s )  ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )
68 66 67 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )
69 61 63 68 sltssn 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
70 69 cutscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No )
71 61 70 addscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No )
72 63 70 addscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No )
73 61 63 70 ltadds1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )  ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
74 68 73 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
75 71 72 74 sltssn 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
76 57 58 pw2divscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) e. No )
77 62 58 pw2divscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su n ) ) e. No )
78 57 62 58 pw2ltsdiv1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s )  ( ( A -s 1s ) /su ( 2s ^su n ) )
79 66 78 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) )
80 76 77 79 sltssn 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( A -s 1s ) /su ( 2s ^su n ) ) } <
81 eqidd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) )
82 simp3 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) )
83 55 58 pw2divscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) e. No )
84 cutcuts 
 |-  ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } < ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No /\ { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
85 69 84 syl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No /\ { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
86 85 simp3d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } <
87 ovex 
 |-  ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. _V
88 87 snid 
 |-  ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) }
89 88 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } )
90 ovex 
 |-  ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V
91 90 snid 
 |-  ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) }
92 91 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )
93 86 89 92 sltssepcd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )
94 70 63 61 ltadds2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )  ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
95 93 94 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
96 55 55 56 addsassd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s A ) +s 1s ) = ( A +s ( A +s 1s ) ) )
97 96 oveq1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( ( A +s ( A +s 1s ) ) -s 1s ) )
98 55 55 addscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A +s A ) e. No )
99 pncans 
 |-  ( ( ( A +s A ) e. No /\ 1s e. No ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( A +s A ) )
100 98 44 99 sylancl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( A +s A ) )
101 no2times 
 |-  ( A e. No -> ( 2s x.s A ) = ( A +s A ) )
102 55 101 syl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s A ) = ( A +s A ) )
103 100 102 eqtr4d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) )
104 55 62 56 addsubsd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s ( A +s 1s ) ) -s 1s ) = ( ( A -s 1s ) +s ( A +s 1s ) ) )
105 97 103 104 3eqtr3rd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) +s ( A +s 1s ) ) = ( 2s x.s A ) )
106 105 oveq1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) )
107 57 62 60 pw2divsdird 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
108 1n0s 
 |-  1s e. NN0_s
109 108 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 1s e. NN0_s )
110 55 58 109 pw2divscan4d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) )
111 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
112 2 111 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
113 112 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s A ) = ( 2s x.s A )
114 113 oveq1i 
 |-  ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) )
115 110 114 eqtr2di 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( A /su ( 2s ^su n ) ) )
116 106 107 115 3eqtr3d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) )
117 95 116 breqtrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
118 71 83 117 sltssn 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
119 63 61 addscomd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
120 119 116 eqtrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) )
121 85 simp2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
122 ovex 
 |-  ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V
123 122 snid 
 |-  ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) }
124 123 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )
125 121 124 89 sltssepcd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )
126 61 70 63 ltadds2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )  ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
127 125 126 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
128 120 127 eqbrtrrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) )
129 83 72 128 sltssn 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( A /su ( 2s ^su n ) ) } <
130 57 58 109 pw2divscan4d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
131 112 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( 2s x.s ( A -s 1s ) )
132 no2times 
 |-  ( ( A -s 1s ) e. No -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) )
133 57 132 syl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) )
134 131 133 eqtrid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) )
135 134 oveq1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) +s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
136 57 57 60 pw2divsdird 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
137 130 135 136 3eqtrrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( A -s 1s ) /su ( 2s ^su n ) ) )
138 61 70 61 ltadds2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )  ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
139 125 138 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
140 137 139 eqbrtrrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) )
141 ltsasym 
 |-  ( ( ( ( A -s 1s ) /su ( 2s ^su n ) ) e. No /\ ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No ) -> ( ( ( A -s 1s ) /su ( 2s ^su n ) )  -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
142 76 71 141 syl2anc 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su n ) )  -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
143 140 142 mpd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
144 71 76 sltssnb 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
145 143 144 mtbird 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
146 145 intnanrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
147 ovex 
 |-  ( ( A -s 1s ) /su ( 2s ^su n ) ) e. _V
148 sneq 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } )
149 148 breq2d 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
150 148 breq1d 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( { xO } < { ( ( A -s 1s ) /su ( 2s ^su n ) ) } <
151 149 150 anbi12d 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
152 151 notbid 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
153 147 152 ralsn 
 |-  ( A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
154 146 153 sylibr 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
155 70 63 63 ltadds2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )  ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
156 93 155 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
157 62 58 109 pw2divscan4d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
158 112 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( 2s x.s ( A +s 1s ) )
159 no2times 
 |-  ( ( A +s 1s ) e. No -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) )
160 62 159 syl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) )
161 158 160 eqtrid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) )
162 161 oveq1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A +s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) )
163 62 62 60 pw2divsdird 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
164 157 162 163 3eqtrrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( A +s 1s ) /su ( 2s ^su n ) ) )
165 156 164 breqtrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
166 ltsasym 
 |-  ( ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No /\ ( ( A +s 1s ) /su ( 2s ^su n ) ) e. No ) -> ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )  -. ( ( A +s 1s ) /su ( 2s ^su n ) )
167 72 77 166 syl2anc 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )  -. ( ( A +s 1s ) /su ( 2s ^su n ) )
168 165 167 mpd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( ( A +s 1s ) /su ( 2s ^su n ) )
169 77 72 sltssnb 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A +s 1s ) /su ( 2s ^su n ) ) } < ( ( A +s 1s ) /su ( 2s ^su n ) )
170 168 169 mtbird 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } <
171 170 intnand 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
172 ovex 
 |-  ( ( A +s 1s ) /su ( 2s ^su n ) ) e. _V
173 sneq 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } )
174 173 breq2d 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
175 173 breq1d 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( { xO } < { ( ( A +s 1s ) /su ( 2s ^su n ) ) } <
176 174 175 anbi12d 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
177 176 notbid 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
178 172 177 ralsn 
 |-  ( A. xO e. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
179 171 178 sylibr 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A. xO e. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
180 ralunb 
 |-  ( A. xO e. ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } u. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
181 154 179 180 sylanbrc 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A. xO e. ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } u. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
182 75 80 81 82 118 129 181 eqcuts3 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = ( A /su ( 2s ^su n ) ) )
183 no2times 
 |-  ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
184 70 183 syl 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
185 eqidd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
186 69 69 185 185 addsunif 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) |s ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) ) )
187 oveq1 
 |-  ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
188 187 eqeq2d 
 |-  ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
189 122 188 rexsn 
 |-  ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
190 189 abbii 
 |-  { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
191 190 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } )
192 oveq2 
 |-  ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
193 192 eqeq2d 
 |-  ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) )
194 122 193 rexsn 
 |-  ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
195 70 61 addscomd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
196 195 eqeq2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
197 194 196 bitrid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
198 197 abbidv 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } )
199 191 198 uneq12d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) )
200 unidm 
 |-  ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
201 df-sn 
 |-  { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
202 200 201 eqtr4i 
 |-  ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
203 199 202 eqtrdi 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } )
204 oveq1 
 |-  ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
205 204 eqeq2d 
 |-  ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
206 90 205 rexsn 
 |-  ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
207 206 abbii 
 |-  { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
208 207 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } )
209 oveq2 
 |-  ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
210 209 eqeq2d 
 |-  ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) )
211 90 210 rexsn 
 |-  ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) )
212 70 63 addscomd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
213 212 eqeq2d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
214 211 213 bitrid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
215 214 abbidv 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } )
216 208 215 uneq12d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) )
217 unidm 
 |-  ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
218 df-sn 
 |-  { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
219 217 218 eqtr4i 
 |-  ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) }
220 216 219 eqtrdi 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } )
221 203 220 oveq12d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) |s ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) )
222 184 186 221 3eqtrd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) )
223 2 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 2s e. No )
224 223 55 60 pw2divsassd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) )
225 114 224 eqtr2id 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) )
226 225 110 eqtr4d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) )
227 182 222 226 3eqtr4rd 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
228 55 60 pw2divscld 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) e. No )
229 2ne0s 
 |-  2s =/= 0s
230 229 a1i 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 2s =/= 0s )
231 228 70 223 230 mulscan1d 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) )
232 227 231 mpbid 
 |-  ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
233 232 3exp 
 |-  ( n e. NN0_s -> ( A e. ZZ_s -> ( ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
234 233 a2d 
 |-  ( n e. NN0_s -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A e. ZZ_s -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) )
235 13 22 31 40 53 234 n0sind 
 |-  ( N e. NN0_s -> ( A e. ZZ_s -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) )
236 235 impcom 
 |-  ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) )