Metamath Proof Explorer

Theorem pw2cut

Description: Extend halfcut to arbitrary powers of two. Part of theorem 4.2 of Gonshor p. 28. (Contributed by Scott Fenton, 18-Aug-2025)

Ref Expression
Hypotheses pw2cut.1 
|- ( ph -> A e. No )
pw2cut.2 
|- ( ph -> B e. No )
pw2cut.3 
|- ( ph -> N e. NN0_s )
pw2cut.4 
|- ( ph -> A
pw2cut.5 
|- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) )
Assertion pw2cut 
|- ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2cut.1 
 |-  ( ph -> A e. No )
2 pw2cut.2 
 |-  ( ph -> B e. No )
3 pw2cut.3 
 |-  ( ph -> N e. NN0_s )
4 pw2cut.4 
 |-  ( ph -> A
5 pw2cut.5 
 |-  ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) )
6 oveq2 
 |-  ( x = 0s -> ( 2s ^su x ) = ( 2s ^su 0s ) )
7 2sno 
 |-  2s e. No
8 exps0 
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
9 7 8 ax-mp 
 |-  ( 2s ^su 0s ) = 1s
10 6 9 eqtrdi 
 |-  ( x = 0s -> ( 2s ^su x ) = 1s )
11 10 oveq2d 
 |-  ( x = 0s -> ( A /su ( 2s ^su x ) ) = ( A /su 1s ) )
12 11 sneqd 
 |-  ( x = 0s -> { ( A /su ( 2s ^su x ) ) } = { ( A /su 1s ) } )
13 10 oveq2d 
 |-  ( x = 0s -> ( B /su ( 2s ^su x ) ) = ( B /su 1s ) )
14 13 sneqd 
 |-  ( x = 0s -> { ( B /su ( 2s ^su x ) ) } = { ( B /su 1s ) } )
15 12 14 oveq12d 
 |-  ( x = 0s -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) )
16 oveq1 
 |-  ( x = 0s -> ( x +s 1s ) = ( 0s +s 1s ) )
17 1sno 
 |-  1s e. No
18 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
19 17 18 ax-mp 
 |-  ( 0s +s 1s ) = 1s
20 16 19 eqtrdi 
 |-  ( x = 0s -> ( x +s 1s ) = 1s )
21 20 oveq2d 
 |-  ( x = 0s -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su 1s ) )
22 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
23 7 22 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
24 21 23 eqtrdi 
 |-  ( x = 0s -> ( 2s ^su ( x +s 1s ) ) = 2s )
25 24 oveq2d 
 |-  ( x = 0s -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su 2s ) )
26 15 25 eqeq12d 
 |-  ( x = 0s -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) )
27 26 imbi2d 
 |-  ( x = 0s -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) ) ) )
28 oveq2 
 |-  ( x = y -> ( 2s ^su x ) = ( 2s ^su y ) )
29 28 oveq2d 
 |-  ( x = y -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su y ) ) )
30 29 sneqd 
 |-  ( x = y -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su y ) ) } )
31 28 oveq2d 
 |-  ( x = y -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su y ) ) )
32 31 sneqd 
 |-  ( x = y -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su y ) ) } )
33 30 32 oveq12d 
 |-  ( x = y -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) )
34 oveq1 
 |-  ( x = y -> ( x +s 1s ) = ( y +s 1s ) )
35 34 oveq2d 
 |-  ( x = y -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( y +s 1s ) ) )
36 35 oveq2d 
 |-  ( x = y -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) )
37 33 36 eqeq12d 
 |-  ( x = y -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) )
38 37 imbi2d 
 |-  ( x = y -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) ) )
39 oveq2 
 |-  ( x = ( y +s 1s ) -> ( 2s ^su x ) = ( 2s ^su ( y +s 1s ) ) )
40 39 oveq2d 
 |-  ( x = ( y +s 1s ) -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su ( y +s 1s ) ) ) )
41 40 sneqd 
 |-  ( x = ( y +s 1s ) -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su ( y +s 1s ) ) ) } )
42 39 oveq2d 
 |-  ( x = ( y +s 1s ) -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su ( y +s 1s ) ) ) )
43 42 sneqd 
 |-  ( x = ( y +s 1s ) -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su ( y +s 1s ) ) ) } )
44 41 43 oveq12d 
 |-  ( x = ( y +s 1s ) -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) )
45 oveq1 
 |-  ( x = ( y +s 1s ) -> ( x +s 1s ) = ( ( y +s 1s ) +s 1s ) )
46 45 oveq2d 
 |-  ( x = ( y +s 1s ) -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( ( y +s 1s ) +s 1s ) ) )
47 46 oveq2d 
 |-  ( x = ( y +s 1s ) -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) )
48 44 47 eqeq12d 
 |-  ( x = ( y +s 1s ) -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) )
49 48 imbi2d 
 |-  ( x = ( y +s 1s ) -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) )
50 oveq2 
 |-  ( x = N -> ( 2s ^su x ) = ( 2s ^su N ) )
51 50 oveq2d 
 |-  ( x = N -> ( A /su ( 2s ^su x ) ) = ( A /su ( 2s ^su N ) ) )
52 51 sneqd 
 |-  ( x = N -> { ( A /su ( 2s ^su x ) ) } = { ( A /su ( 2s ^su N ) ) } )
53 50 oveq2d 
 |-  ( x = N -> ( B /su ( 2s ^su x ) ) = ( B /su ( 2s ^su N ) ) )
54 53 sneqd 
 |-  ( x = N -> { ( B /su ( 2s ^su x ) ) } = { ( B /su ( 2s ^su N ) ) } )
55 52 54 oveq12d 
 |-  ( x = N -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) )
56 oveq1 
 |-  ( x = N -> ( x +s 1s ) = ( N +s 1s ) )
57 56 oveq2d 
 |-  ( x = N -> ( 2s ^su ( x +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) )
58 57 oveq2d 
 |-  ( x = N -> ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) )
59 55 58 eqeq12d 
 |-  ( x = N -> ( ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) <-> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) )
60 59 imbi2d 
 |-  ( x = N -> ( ( ph -> ( { ( A /su ( 2s ^su x ) ) } |s { ( B /su ( 2s ^su x ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( x +s 1s ) ) ) ) <-> ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) ) )
61 divs1 
 |-  ( A e. No -> ( A /su 1s ) = A )
62 1 61 syl 
 |-  ( ph -> ( A /su 1s ) = A )
63 62 sneqd 
 |-  ( ph -> { ( A /su 1s ) } = { A } )
64 divs1 
 |-  ( B e. No -> ( B /su 1s ) = B )
65 2 64 syl 
 |-  ( ph -> ( B /su 1s ) = B )
66 65 sneqd 
 |-  ( ph -> { ( B /su 1s ) } = { B } )
67 63 66 oveq12d 
 |-  ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( { A } |s { B } ) )
68 eqid 
 |-  ( { A } |s { B } ) = ( { A } |s { B } )
69 1 2 4 5 68 halfcut 
 |-  ( ph -> ( { A } |s { B } ) = ( ( A +s B ) /su 2s ) )
70 67 69 eqtrd 
 |-  ( ph -> ( { ( A /su 1s ) } |s { ( B /su 1s ) } ) = ( ( A +s B ) /su 2s ) )
71 1 adantl 
 |-  ( ( y e. NN0_s /\ ph ) -> A e. No )
72 peano2n0s 
 |-  ( y e. NN0_s -> ( y +s 1s ) e. NN0_s )
73 expscl 
 |-  ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) e. No )
74 7 72 73 sylancr 
 |-  ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) e. No )
75 74 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) e. No )
76 2ne0s 
 |-  2s =/= 0s
77 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) =/= 0s )
78 7 76 77 mp3an12 
 |-  ( ( y +s 1s ) e. NN0_s -> ( 2s ^su ( y +s 1s ) ) =/= 0s )
79 72 78 syl 
 |-  ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) =/= 0s )
80 79 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) =/= 0s )
81 71 75 80 divscld 
 |-  ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) e. No )
82 81 3adant3 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) e. No )
83 2 adantl 
 |-  ( ( y e. NN0_s /\ ph ) -> B e. No )
84 83 75 80 divscld 
 |-  ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) e. No )
85 84 3adant3 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) e. No )
86 71 75 80 divscan1d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) ) = A )
87 4 adantl 
 |-  ( ( y e. NN0_s /\ ph ) -> A
88 86 87 eqbrtrd 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) )
89 2nns 
 |-  2s e. NN_s
90 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
91 89 90 ax-mp 
 |-  0s
92 expsgt0 
 |-  ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s /\ 0s  0s
93 7 91 92 mp3an13 
 |-  ( ( y +s 1s ) e. NN0_s -> 0s
94 72 93 syl 
 |-  ( y e. NN0_s -> 0s
95 94 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> 0s
96 81 83 75 95 sltmuldivd 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) x.s ( 2s ^su ( y +s 1s ) ) )  ( A /su ( 2s ^su ( y +s 1s ) ) )
97 88 96 mpbid 
 |-  ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) )
98 97 3adant3 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( A /su ( 2s ^su ( y +s 1s ) ) )
99 expsp1 
 |-  ( ( 2s e. No /\ y e. NN0_s ) -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) )
100 7 99 mpan 
 |-  ( y e. NN0_s -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) )
101 100 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( y +s 1s ) ) = ( ( 2s ^su y ) x.s 2s ) )
102 101 oveq2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) = ( A /su ( ( 2s ^su y ) x.s 2s ) ) )
103 expscl 
 |-  ( ( 2s e. No /\ y e. NN0_s ) -> ( 2s ^su y ) e. No )
104 7 103 mpan 
 |-  ( y e. NN0_s -> ( 2s ^su y ) e. No )
105 104 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s ^su y ) e. No )
106 7 a1i 
 |-  ( ( y e. NN0_s /\ ph ) -> 2s e. No )
107 expsne0 
 |-  ( ( 2s e. No /\ 2s =/= 0s /\ y e. NN0_s ) -> ( 2s ^su y ) =/= 0s )
108 7 76 107 mp3an12 
 |-  ( y e. NN0_s -> ( 2s ^su y ) =/= 0s )
109 108 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s ^su y ) =/= 0s )
110 76 a1i 
 |-  ( ( y e. NN0_s /\ ph ) -> 2s =/= 0s )
111 71 105 106 109 110 divdivs1d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( A /su ( 2s ^su y ) ) /su 2s ) = ( A /su ( ( 2s ^su y ) x.s 2s ) ) )
112 102 111 eqtr4d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su ( y +s 1s ) ) ) = ( ( A /su ( 2s ^su y ) ) /su 2s ) )
113 112 oveq2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) = ( 2s x.s ( ( A /su ( 2s ^su y ) ) /su 2s ) ) )
114 71 105 109 divscld 
 |-  ( ( y e. NN0_s /\ ph ) -> ( A /su ( 2s ^su y ) ) e. No )
115 114 106 110 divscan2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( ( A /su ( 2s ^su y ) ) /su 2s ) ) = ( A /su ( 2s ^su y ) ) )
116 113 115 eqtrd 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) = ( A /su ( 2s ^su y ) ) )
117 116 sneqd 
 |-  ( ( y e. NN0_s /\ ph ) -> { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } = { ( A /su ( 2s ^su y ) ) } )
118 101 oveq2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) = ( B /su ( ( 2s ^su y ) x.s 2s ) ) )
119 83 105 106 109 110 divdivs1d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( B /su ( 2s ^su y ) ) /su 2s ) = ( B /su ( ( 2s ^su y ) x.s 2s ) ) )
120 118 119 eqtr4d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su ( y +s 1s ) ) ) = ( ( B /su ( 2s ^su y ) ) /su 2s ) )
121 120 oveq2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) = ( 2s x.s ( ( B /su ( 2s ^su y ) ) /su 2s ) ) )
122 83 105 109 divscld 
 |-  ( ( y e. NN0_s /\ ph ) -> ( B /su ( 2s ^su y ) ) e. No )
123 122 106 110 divscan2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( ( B /su ( 2s ^su y ) ) /su 2s ) ) = ( B /su ( 2s ^su y ) ) )
124 121 123 eqtrd 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) = ( B /su ( 2s ^su y ) ) )
125 124 sneqd 
 |-  ( ( y e. NN0_s /\ ph ) -> { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } = { ( B /su ( 2s ^su y ) ) } )
126 117 125 oveq12d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) )
127 126 eqcomd 
 |-  ( ( y e. NN0_s /\ ph ) -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) )
128 71 83 75 80 divsdird 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) )
129 127 128 eqeq12d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) <-> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) ) )
130 129 biimp3a 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( 2s x.s ( A /su ( 2s ^su ( y +s 1s ) ) ) ) } |s { ( 2s x.s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) } ) = ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) )
131 eqid 
 |-  ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } )
132 82 85 98 130 131 halfcut 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) )
133 128 oveq1d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) )
134 133 3adant3 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( ( A /su ( 2s ^su ( y +s 1s ) ) ) +s ( B /su ( 2s ^su ( y +s 1s ) ) ) ) /su 2s ) )
135 132 134 eqtr4d 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) )
136 expsp1 
 |-  ( ( 2s e. No /\ ( y +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) )
137 7 72 136 sylancr 
 |-  ( y e. NN0_s -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) )
138 137 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> ( 2s ^su ( ( y +s 1s ) +s 1s ) ) = ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) )
139 138 oveq2d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( A +s B ) /su ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) )
140 71 83 addscld 
 |-  ( ( y e. NN0_s /\ ph ) -> ( A +s B ) e. No )
141 140 75 106 80 110 divdivs1d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) = ( ( A +s B ) /su ( ( 2s ^su ( y +s 1s ) ) x.s 2s ) ) )
142 139 141 eqtr4d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) )
143 142 3adant3 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) = ( ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) /su 2s ) )
144 135 143 eqtr4d 
 |-  ( ( y e. NN0_s /\ ph /\ ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) )
145 144 3exp 
 |-  ( y e. NN0_s -> ( ph -> ( ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) )
146 145 a2d 
 |-  ( y e. NN0_s -> ( ( ph -> ( { ( A /su ( 2s ^su y ) ) } |s { ( B /su ( 2s ^su y ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( y +s 1s ) ) ) ) -> ( ph -> ( { ( A /su ( 2s ^su ( y +s 1s ) ) ) } |s { ( B /su ( 2s ^su ( y +s 1s ) ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( ( y +s 1s ) +s 1s ) ) ) ) ) )
147 27 38 49 60 70 146 n0sind 
 |-  ( N e. NN0_s -> ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) ) )
148 3 147 mpcom 
 |-  ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( B /su ( 2s ^su N ) ) } ) = ( ( A +s B ) /su ( 2s ^su ( N +s 1s ) ) ) )