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 2sno 
 |-  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 zscut 
 |-  ( A e. ZZ_s -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
42 zno 
 |-  ( A e. ZZ_s -> A e. No )
43 divs1 
 |-  ( A e. No -> ( A /su 1s ) = A )
44 42 43 syl 
 |-  ( A e. ZZ_s -> ( A /su 1s ) = A )
45 1sno 
 |-  1s e. No
46 45 a1i 
 |-  ( A e. ZZ_s -> 1s e. No )
47 42 46 subscld 
 |-  ( A e. ZZ_s -> ( A -s 1s ) e. No )
48 divs1 
 |-  ( ( A -s 1s ) e. No -> ( ( A -s 1s ) /su 1s ) = ( A -s 1s ) )
49 47 48 syl 
 |-  ( A e. ZZ_s -> ( ( A -s 1s ) /su 1s ) = ( A -s 1s ) )
50 49 sneqd 
 |-  ( A e. ZZ_s -> { ( ( A -s 1s ) /su 1s ) } = { ( A -s 1s ) } )
51 42 46 addscld 
 |-  ( A e. ZZ_s -> ( A +s 1s ) e. No )
52 divs1 
 |-  ( ( A +s 1s ) e. No -> ( ( A +s 1s ) /su 1s ) = ( A +s 1s ) )
53 51 52 syl 
 |-  ( A e. ZZ_s -> ( ( A +s 1s ) /su 1s ) = ( A +s 1s ) )
54 53 sneqd 
 |-  ( A e. ZZ_s -> { ( ( A +s 1s ) /su 1s ) } = { ( A +s 1s ) } )
55 50 54 oveq12d 
 |-  ( A e. ZZ_s -> ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
56 41 44 55 3eqtr4d 
 |-  ( A e. ZZ_s -> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) )
57 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 )
58 57 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 )
59 45 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 )
60 58 59 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 )
61 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 )
62 peano2n0s 
 |-  ( n e. NN0_s -> ( n +s 1s ) e. NN0_s )
63 61 62 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 )
64 60 63 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 )
65 58 59 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 )
66 65 63 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 )
67 58 sltm1d 
 |-  ( ( 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 )
68 58 sltp1d 
 |-  ( ( 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
69 60 58 65 67 68 slttrd 
 |-  ( ( 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 )
70 60 65 63 pw2sltdiv1d 
 |-  ( ( 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 ) ) )
71 69 70 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 ) ) )
72 64 66 71 ssltsn 
 |-  ( ( 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 ) ) ) } <
73 72 scutcld 
 |-  ( ( 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 )
74 64 73 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 )
75 66 73 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 )
76 64 66 73 sltadd1d 
 |-  ( ( 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 ) ) ) } ) )
77 71 76 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 ) ) ) } ) )
78 74 75 77 ssltsn 
 |-  ( ( 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 ) ) ) } ) ) } <
79 60 61 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 )
80 65 61 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 )
81 60 65 61 pw2sltdiv1d 
 |-  ( ( 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 ) )
82 69 81 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 ) )
83 79 80 82 ssltsn 
 |-  ( ( 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 ) ) } <
84 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 ) ) ) } ) ) } ) )
85 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 ) ) } ) )
86 58 61 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 )
87 scutcut 
 |-  ( { ( ( 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 ) ) ) } <
88 72 87 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 ) ) ) } <
89 88 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 ) ) ) } ) } <
90 ovex 
 |-  ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. _V
91 90 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 ) ) ) } ) }
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 ) ) ) } |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 ) ) ) } ) } )
93 ovex 
 |-  ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V
94 93 snid 
 |-  ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) }
95 94 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 ) ) ) } )
96 89 92 95 ssltsepcd 
 |-  ( ( 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 ) ) ) } )
97 73 66 64 sltadd2d 
 |-  ( ( 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 ) ) ) } ) )
98 96 97 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 ) ) ) } ) )
99 58 58 59 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 ) ) )
100 99 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 ) )
101 58 58 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 )
102 pncans 
 |-  ( ( ( A +s A ) e. No /\ 1s e. No ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( A +s A ) )
103 101 45 102 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 ) )
104 no2times 
 |-  ( A e. No -> ( 2s x.s A ) = ( A +s A ) )
105 58 104 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 ) )
106 103 105 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 ) )
107 58 65 59 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 ) ) )
108 100 106 107 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 ) )
109 108 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 ) ) ) )
110 60 65 63 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 ) ) ) ) )
111 1n0s 
 |-  1s e. NN0_s
112 111 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 )
113 58 61 112 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 ) ) ) )
114 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
115 2 114 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
116 115 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s A ) = ( 2s x.s A )
117 116 oveq1i 
 |-  ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) )
118 113 117 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 ) ) )
119 109 110 118 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 ) ) )
120 98 119 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 ) ) ) } ) )
121 74 86 120 ssltsn 
 |-  ( ( 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 ) ) ) } ) ) } <
122 66 64 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 ) ) ) ) )
123 122 119 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 ) ) )
124 88 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 ) ) ) } <
125 ovex 
 |-  ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V
126 125 snid 
 |-  ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) }
127 126 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 ) ) ) } )
128 124 127 92 ssltsepcd 
 |-  ( ( 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 ) ) )
129 64 73 66 sltadd2d 
 |-  ( ( 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 ) ) ) )
130 128 129 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 ) ) ) )
131 123 130 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 ) )
132 86 75 131 ssltsn 
 |-  ( ( 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 ) ) } <
133 60 61 112 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 ) ) ) )
134 115 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( 2s x.s ( A -s 1s ) )
135 no2times 
 |-  ( ( A -s 1s ) e. No -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) )
136 60 135 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 ) ) )
137 134 136 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 ) ) )
138 137 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 ) ) ) )
139 60 60 63 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 ) ) ) ) )
140 133 138 139 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 ) ) )
141 64 73 64 sltadd2d 
 |-  ( ( 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 ) ) ) )
142 128 141 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 ) ) ) )
143 140 142 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 ) )
144 sltasym 
 |-  ( ( ( ( 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 ) ) ) } ) )
145 79 74 144 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 ) ) ) } ) )
146 143 145 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 ) ) ) } ) )
147 74 79 ssltsnb 
 |-  ( ( 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 ) ) ) } ) )
148 146 147 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 ) ) ) } ) ) } <
149 148 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 ) ) ) } ) ) } <
150 ovex 
 |-  ( ( A -s 1s ) /su ( 2s ^su n ) ) e. _V
151 sneq 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } )
152 151 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 ) ) ) } ) ) } <
153 151 breq1d 
 |-  ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( { xO } < { ( ( A -s 1s ) /su ( 2s ^su n ) ) } <
154 152 153 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 ) ) ) } ) ) } <
155 154 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 ) ) ) } ) ) } <
156 150 155 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 ) ) ) } ) ) } <
157 149 156 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 ) ) ) } ) ) } <
158 73 66 66 sltadd2d 
 |-  ( ( 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 ) ) ) } ) )
159 96 158 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 ) ) ) } ) )
160 65 61 112 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 ) ) ) )
161 115 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( 2s x.s ( A +s 1s ) )
162 no2times 
 |-  ( ( A +s 1s ) e. No -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) )
163 65 162 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 ) ) )
164 161 163 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 ) ) )
165 164 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 ) ) ) )
166 65 65 63 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 ) ) ) ) )
167 160 165 166 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 ) ) )
168 159 167 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 ) ) ) } ) )
169 sltasym 
 |-  ( ( ( ( ( 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 ) )
170 75 80 169 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 ) )
171 168 170 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 ) )
172 80 75 ssltsnb 
 |-  ( ( 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 ) )
173 171 172 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 ) ) } <
174 173 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 ) ) ) } ) ) } <
175 ovex 
 |-  ( ( A +s 1s ) /su ( 2s ^su n ) ) e. _V
176 sneq 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } )
177 176 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 ) ) ) } ) ) } <
178 176 breq1d 
 |-  ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( { xO } < { ( ( A +s 1s ) /su ( 2s ^su n ) ) } <
179 177 178 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 ) ) ) } ) ) } <
180 179 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 ) ) ) } ) ) } <
181 175 180 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 ) ) ) } ) ) } <
182 174 181 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 ) ) ) } ) ) } <
183 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 ) ) ) } ) ) } <
184 157 182 183 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 ) ) ) } ) ) } <
185 78 83 84 85 121 132 184 eqscut3 
 |-  ( ( 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 ) ) )
186 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 ) ) ) } ) ) )
187 73 186 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 ) ) ) } ) ) )
188 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 ) ) ) } ) )
189 72 72 188 188 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 ) } ) ) )
190 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 ) ) ) } ) ) )
191 190 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 ) ) ) } ) ) ) )
192 125 191 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 ) ) ) } ) ) )
193 192 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 ) ) ) } ) ) }
194 193 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 ) ) ) } ) ) } )
195 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 ) ) ) ) )
196 195 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 ) ) ) ) ) )
197 125 196 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 ) ) ) ) )
198 73 64 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 ) ) ) } ) ) )
199 198 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 ) ) ) } ) ) ) )
200 197 199 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 ) ) ) } ) ) ) )
201 200 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 ) ) ) } ) ) } )
202 194 201 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 ) ) ) } ) ) } ) )
203 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 ) ) ) } ) ) }
204 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 ) ) ) } ) ) }
205 203 204 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 ) ) ) } ) ) }
206 202 205 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 ) ) ) } ) ) } )
207 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 ) ) ) } ) ) )
208 207 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 ) ) ) } ) ) ) )
209 93 208 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 ) ) ) } ) ) )
210 209 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 ) ) ) } ) ) }
211 210 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 ) ) ) } ) ) } )
212 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 ) ) ) ) )
213 212 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 ) ) ) ) ) )
214 93 213 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 ) ) ) ) )
215 73 66 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 ) ) ) } ) ) )
216 215 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 ) ) ) } ) ) ) )
217 214 216 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 ) ) ) } ) ) ) )
218 217 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 ) ) ) } ) ) } )
219 211 218 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 ) ) ) } ) ) } ) )
220 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 ) ) ) } ) ) }
221 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 ) ) ) } ) ) }
222 220 221 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 ) ) ) } ) ) }
223 219 222 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 ) ) ) } ) ) } )
224 206 223 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 ) ) ) } ) ) } ) )
225 187 189 224 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 ) ) ) } ) ) } ) )
226 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 )
227 226 58 63 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 ) ) ) ) )
228 117 227 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 ) ) ) )
229 228 113 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 ) ) )
230 185 225 229 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 ) ) ) } ) ) )
231 58 63 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 )
232 2ne0s 
 |-  2s =/= 0s
233 232 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 )
234 231 73 226 233 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 ) ) ) } ) ) )
235 230 234 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 ) ) ) } ) )
236 235 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 ) ) ) } ) ) ) )
237 236 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 ) ) ) } ) ) ) )
238 13 22 31 40 56 237 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 ) ) } ) ) )
239 238 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 ) ) } ) )