Metamath Proof Explorer

Theorem nn0sumshdiglemA

Description: Lemma for nn0sumshdig (induction step, even multiplier). (Contributed by AV, 3-Jun-2020)

Ref Expression
Assertion nn0sumshdiglemA 
|- ( ( ( a e. NN /\ ( a / 2 ) e. NN ) /\ y e. NN ) -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( ( a / 2 ) e. NN -> ( a / 2 ) e. NN0 )
2 blennn0em1 
 |-  ( ( a e. NN /\ ( a / 2 ) e. NN0 ) -> ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) )
3 1 2 sylan2 
 |-  ( ( a e. NN /\ ( a / 2 ) e. NN ) -> ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) )
4 fveqeq2 
 |-  ( x = ( a / 2 ) -> ( ( #b ` x ) = y <-> ( #b ` ( a / 2 ) ) = y ) )
5 id 
 |-  ( x = ( a / 2 ) -> x = ( a / 2 ) )
6 oveq2 
 |-  ( x = ( a / 2 ) -> ( k ( digit ` 2 ) x ) = ( k ( digit ` 2 ) ( a / 2 ) ) )
7 6 oveq1d 
 |-  ( x = ( a / 2 ) -> ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) = ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) )
8 7 adantr 
 |-  ( ( x = ( a / 2 ) /\ k e. ( 0 ..^ y ) ) -> ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) = ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) )
9 8 sumeq2dv 
 |-  ( x = ( a / 2 ) -> sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) )
10 5 9 eqeq12d 
 |-  ( x = ( a / 2 ) -> ( x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) <-> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) )
11 4 10 imbi12d 
 |-  ( x = ( a / 2 ) -> ( ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) ) )
12 11 rspcva 
 |-  ( ( ( a / 2 ) e. NN0 /\ A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) ) -> ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) )
13 simpr 
 |-  ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) -> ( #b ` a ) = ( y + 1 ) )
14 13 oveq1d 
 |-  ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) -> ( ( #b ` a ) - 1 ) = ( ( y + 1 ) - 1 ) )
15 nncn 
 |-  ( y e. NN -> y e. CC )
16 pncan1 
 |-  ( y e. CC -> ( ( y + 1 ) - 1 ) = y )
17 15 16 syl 
 |-  ( y e. NN -> ( ( y + 1 ) - 1 ) = y )
18 14 17 sylan9eq 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( #b ` a ) - 1 ) = y )
19 18 eqeq2d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) <-> ( #b ` ( a / 2 ) ) = y ) )
20 nnz 
 |-  ( y e. NN -> y e. ZZ )
21 20 adantl 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> y e. ZZ )
22 fzval3 
 |-  ( y e. ZZ -> ( 0 ... y ) = ( 0 ..^ ( y + 1 ) ) )
23 21 22 syl 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 ... y ) = ( 0 ..^ ( y + 1 ) ) )
24 23 eqcomd 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 ..^ ( y + 1 ) ) = ( 0 ... y ) )
25 24 sumeq1d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ... y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
26 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
27 elnn0uz 
 |-  ( y e. NN0 <-> y e. ( ZZ>= ` 0 ) )
28 26 27 sylib 
 |-  ( y e. NN -> y e. ( ZZ>= ` 0 ) )
29 28 adantl 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> y e. ( ZZ>= ` 0 ) )
30 2nn 
 |-  2 e. NN
31 30 a1i 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> 2 e. NN )
32 elfzelz 
 |-  ( k e. ( 0 ... y ) -> k e. ZZ )
33 32 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> k e. ZZ )
34 nnnn0 
 |-  ( a e. NN -> a e. NN0 )
35 nn0rp0 
 |-  ( a e. NN0 -> a e. ( 0 [,) +oo ) )
36 34 35 syl 
 |-  ( a e. NN -> a e. ( 0 [,) +oo ) )
37 36 ad4antlr 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> a e. ( 0 [,) +oo ) )
38 digvalnn0 
 |-  ( ( 2 e. NN /\ k e. ZZ /\ a e. ( 0 [,) +oo ) ) -> ( k ( digit ` 2 ) a ) e. NN0 )
39 31 33 37 38 syl3anc 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> ( k ( digit ` 2 ) a ) e. NN0 )
40 39 nn0cnd 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> ( k ( digit ` 2 ) a ) e. CC )
41 2nn0 
 |-  2 e. NN0
42 41 a1i 
 |-  ( k e. ( 0 ... y ) -> 2 e. NN0 )
43 elfznn0 
 |-  ( k e. ( 0 ... y ) -> k e. NN0 )
44 42 43 nn0expcld 
 |-  ( k e. ( 0 ... y ) -> ( 2 ^ k ) e. NN0 )
45 44 nn0cnd 
 |-  ( k e. ( 0 ... y ) -> ( 2 ^ k ) e. CC )
46 45 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> ( 2 ^ k ) e. CC )
47 40 46 mulcld 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( 0 ... y ) ) -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) e. CC )
48 oveq1 
 |-  ( k = 0 -> ( k ( digit ` 2 ) a ) = ( 0 ( digit ` 2 ) a ) )
49 oveq2 
 |-  ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
50 48 49 oveq12d 
 |-  ( k = 0 -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( 0 ( digit ` 2 ) a ) x. ( 2 ^ 0 ) ) )
51 2cn 
 |-  2 e. CC
52 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
53 51 52 ax-mp 
 |-  ( 2 ^ 0 ) = 1
54 53 oveq2i 
 |-  ( ( 0 ( digit ` 2 ) a ) x. ( 2 ^ 0 ) ) = ( ( 0 ( digit ` 2 ) a ) x. 1 )
55 50 54 eqtrdi 
 |-  ( k = 0 -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( 0 ( digit ` 2 ) a ) x. 1 ) )
56 29 47 55 fsum1p 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ k e. ( 0 ... y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( ( 0 ( digit ` 2 ) a ) x. 1 ) + sum_ k e. ( ( 0 + 1 ) ... y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
57 0dig2nn0e 
 |-  ( ( a e. NN0 /\ ( a / 2 ) e. NN0 ) -> ( 0 ( digit ` 2 ) a ) = 0 )
58 34 1 57 syl2anr 
 |-  ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( 0 ( digit ` 2 ) a ) = 0 )
59 58 oveq1d 
 |-  ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( 0 ( digit ` 2 ) a ) x. 1 ) = ( 0 x. 1 ) )
60 1re 
 |-  1 e. RR
61 mul02lem2 
 |-  ( 1 e. RR -> ( 0 x. 1 ) = 0 )
62 60 61 ax-mp 
 |-  ( 0 x. 1 ) = 0
63 59 62 eqtrdi 
 |-  ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( 0 ( digit ` 2 ) a ) x. 1 ) = 0 )
64 63 adantr 
 |-  ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) -> ( ( 0 ( digit ` 2 ) a ) x. 1 ) = 0 )
65 64 adantr 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( 0 ( digit ` 2 ) a ) x. 1 ) = 0 )
66 1z 
 |-  1 e. ZZ
67 66 a1i 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> 1 e. ZZ )
68 0p1e1 
 |-  ( 0 + 1 ) = 1
69 68 66 eqeltri 
 |-  ( 0 + 1 ) e. ZZ
70 69 a1i 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 + 1 ) e. ZZ )
71 30 a1i 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> 2 e. NN )
72 elfzelz 
 |-  ( k e. ( ( 0 + 1 ) ... y ) -> k e. ZZ )
73 72 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> k e. ZZ )
74 36 ad4antlr 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> a e. ( 0 [,) +oo ) )
75 71 73 74 38 syl3anc 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> ( k ( digit ` 2 ) a ) e. NN0 )
76 75 nn0cnd 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> ( k ( digit ` 2 ) a ) e. CC )
77 2cnd 
 |-  ( k e. ( ( 0 + 1 ) ... y ) -> 2 e. CC )
78 elfznn 
 |-  ( k e. ( 1 ... y ) -> k e. NN )
79 78 nnnn0d 
 |-  ( k e. ( 1 ... y ) -> k e. NN0 )
80 68 oveq1i 
 |-  ( ( 0 + 1 ) ... y ) = ( 1 ... y )
81 79 80 eleq2s 
 |-  ( k e. ( ( 0 + 1 ) ... y ) -> k e. NN0 )
82 77 81 expcld 
 |-  ( k e. ( ( 0 + 1 ) ... y ) -> ( 2 ^ k ) e. CC )
83 82 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> ( 2 ^ k ) e. CC )
84 76 83 mulcld 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ k e. ( ( 0 + 1 ) ... y ) ) -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) e. CC )
85 oveq1 
 |-  ( k = ( i + 1 ) -> ( k ( digit ` 2 ) a ) = ( ( i + 1 ) ( digit ` 2 ) a ) )
86 oveq2 
 |-  ( k = ( i + 1 ) -> ( 2 ^ k ) = ( 2 ^ ( i + 1 ) ) )
87 85 86 oveq12d 
 |-  ( k = ( i + 1 ) -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) )
88 67 70 21 84 87 fsumshftm 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ k e. ( ( 0 + 1 ) ... y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ i e. ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) )
89 65 88 oveq12d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( ( 0 ( digit ` 2 ) a ) x. 1 ) + sum_ k e. ( ( 0 + 1 ) ... y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) = ( 0 + sum_ i e. ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) ) )
90 1 ad4antr 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( a / 2 ) e. NN0 )
91 34 ad4antlr 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> a e. NN0 )
92 elfzonn0 
 |-  ( i e. ( 0 ..^ y ) -> i e. NN0 )
93 92 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> i e. NN0 )
94 dignn0ehalf 
 |-  ( ( ( a / 2 ) e. NN0 /\ a e. NN0 /\ i e. NN0 ) -> ( ( i + 1 ) ( digit ` 2 ) a ) = ( i ( digit ` 2 ) ( a / 2 ) ) )
95 90 91 93 94 syl3anc 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( i + 1 ) ( digit ` 2 ) a ) = ( i ( digit ` 2 ) ( a / 2 ) ) )
96 2cnd 
 |-  ( i e. ( 0 ..^ y ) -> 2 e. CC )
97 96 92 expp1d 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ ( i + 1 ) ) = ( ( 2 ^ i ) x. 2 ) )
98 97 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( 2 ^ ( i + 1 ) ) = ( ( 2 ^ i ) x. 2 ) )
99 95 98 oveq12d 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) = ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( ( 2 ^ i ) x. 2 ) ) )
100 30 a1i 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> 2 e. NN )
101 elfzoelz 
 |-  ( i e. ( 0 ..^ y ) -> i e. ZZ )
102 101 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> i e. ZZ )
103 nn0rp0 
 |-  ( ( a / 2 ) e. NN0 -> ( a / 2 ) e. ( 0 [,) +oo ) )
104 1 103 syl 
 |-  ( ( a / 2 ) e. NN -> ( a / 2 ) e. ( 0 [,) +oo ) )
105 104 ad4antr 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( a / 2 ) e. ( 0 [,) +oo ) )
106 digvalnn0 
 |-  ( ( 2 e. NN /\ i e. ZZ /\ ( a / 2 ) e. ( 0 [,) +oo ) ) -> ( i ( digit ` 2 ) ( a / 2 ) ) e. NN0 )
107 100 102 105 106 syl3anc 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( i ( digit ` 2 ) ( a / 2 ) ) e. NN0 )
108 107 nn0cnd 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( i ( digit ` 2 ) ( a / 2 ) ) e. CC )
109 2re 
 |-  2 e. RR
110 109 a1i 
 |-  ( i e. ( 0 ..^ y ) -> 2 e. RR )
111 110 92 reexpcld 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ i ) e. RR )
112 111 recnd 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ i ) e. CC )
113 112 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( 2 ^ i ) e. CC )
114 2cnd 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> 2 e. CC )
115 mulass 
 |-  ( ( ( i ( digit ` 2 ) ( a / 2 ) ) e. CC /\ ( 2 ^ i ) e. CC /\ 2 e. CC ) -> ( ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) = ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( ( 2 ^ i ) x. 2 ) ) )
116 115 eqcomd 
 |-  ( ( ( i ( digit ` 2 ) ( a / 2 ) ) e. CC /\ ( 2 ^ i ) e. CC /\ 2 e. CC ) -> ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( ( 2 ^ i ) x. 2 ) ) = ( ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
117 108 113 114 116 syl3anc 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( ( 2 ^ i ) x. 2 ) ) = ( ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
118 99 117 eqtrd 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) = ( ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
119 118 sumeq2dv 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) = sum_ i e. ( 0 ..^ y ) ( ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
120 0cn 
 |-  0 e. CC
121 pncan1 
 |-  ( 0 e. CC -> ( ( 0 + 1 ) - 1 ) = 0 )
122 120 121 ax-mp 
 |-  ( ( 0 + 1 ) - 1 ) = 0
123 122 a1i 
 |-  ( y e. NN -> ( ( 0 + 1 ) - 1 ) = 0 )
124 123 oveq1d 
 |-  ( y e. NN -> ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) = ( 0 ... ( y - 1 ) ) )
125 fzoval 
 |-  ( y e. ZZ -> ( 0 ..^ y ) = ( 0 ... ( y - 1 ) ) )
126 125 eqcomd 
 |-  ( y e. ZZ -> ( 0 ... ( y - 1 ) ) = ( 0 ..^ y ) )
127 20 126 syl 
 |-  ( y e. NN -> ( 0 ... ( y - 1 ) ) = ( 0 ..^ y ) )
128 124 127 eqtrd 
 |-  ( y e. NN -> ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) = ( 0 ..^ y ) )
129 128 adantl 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) = ( 0 ..^ y ) )
130 129 sumeq1d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ i e. ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) = sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) )
131 130 oveq2d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 + sum_ i e. ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) ) = ( 0 + sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) ) )
132 fzofi 
 |-  ( 0 ..^ y ) e. Fin
133 132 a1i 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 ..^ y ) e. Fin )
134 101 peano2zd 
 |-  ( i e. ( 0 ..^ y ) -> ( i + 1 ) e. ZZ )
135 134 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( i + 1 ) e. ZZ )
136 36 ad4antlr 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> a e. ( 0 [,) +oo ) )
137 digvalnn0 
 |-  ( ( 2 e. NN /\ ( i + 1 ) e. ZZ /\ a e. ( 0 [,) +oo ) ) -> ( ( i + 1 ) ( digit ` 2 ) a ) e. NN0 )
138 100 135 136 137 syl3anc 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( i + 1 ) ( digit ` 2 ) a ) e. NN0 )
139 138 nn0cnd 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( i + 1 ) ( digit ` 2 ) a ) e. CC )
140 41 a1i 
 |-  ( i e. ( 0 ..^ y ) -> 2 e. NN0 )
141 peano2nn0 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
142 92 141 syl 
 |-  ( i e. ( 0 ..^ y ) -> ( i + 1 ) e. NN0 )
143 140 142 nn0expcld 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ ( i + 1 ) ) e. NN0 )
144 143 nn0cnd 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ ( i + 1 ) ) e. CC )
145 144 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( 2 ^ ( i + 1 ) ) e. CC )
146 139 145 mulcld 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) e. CC )
147 133 146 fsumcl 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) e. CC )
148 147 addid2d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 + sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) ) = sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) )
149 131 148 eqtrd 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 + sum_ i e. ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) ) = sum_ i e. ( 0 ..^ y ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) )
150 2cnd 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> 2 e. CC )
151 140 92 nn0expcld 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ i ) e. NN0 )
152 151 nn0cnd 
 |-  ( i e. ( 0 ..^ y ) -> ( 2 ^ i ) e. CC )
153 152 adantl 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( 2 ^ i ) e. CC )
154 108 153 mulcld 
 |-  ( ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) /\ i e. ( 0 ..^ y ) ) -> ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) e. CC )
155 133 150 154 fsummulc1 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) = sum_ i e. ( 0 ..^ y ) ( ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
156 119 149 155 3eqtr4d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( 0 + sum_ i e. ( ( ( 0 + 1 ) - 1 ) ... ( y - 1 ) ) ( ( ( i + 1 ) ( digit ` 2 ) a ) x. ( 2 ^ ( i + 1 ) ) ) ) = ( sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
157 89 156 eqtrd 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( ( 0 ( digit ` 2 ) a ) x. 1 ) + sum_ k e. ( ( 0 + 1 ) ... y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) = ( sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
158 25 56 157 3eqtrd 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
159 158 adantl 
 |-  ( ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) /\ ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) ) -> sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) )
160 oveq1 
 |-  ( k = i -> ( k ( digit ` 2 ) ( a / 2 ) ) = ( i ( digit ` 2 ) ( a / 2 ) ) )
161 oveq2 
 |-  ( k = i -> ( 2 ^ k ) = ( 2 ^ i ) )
162 160 161 oveq12d 
 |-  ( k = i -> ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) = ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) )
163 162 cbvsumv 
 |-  sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) = sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) )
164 163 a1i 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) = sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) )
165 164 eqeq2d 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) <-> ( a / 2 ) = sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) ) )
166 165 biimpac 
 |-  ( ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) /\ ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) ) -> ( a / 2 ) = sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) )
167 166 eqcomd 
 |-  ( ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) /\ ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) ) -> sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) = ( a / 2 ) )
168 167 oveq1d 
 |-  ( ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) /\ ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) ) -> ( sum_ i e. ( 0 ..^ y ) ( ( i ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ i ) ) x. 2 ) = ( ( a / 2 ) x. 2 ) )
169 nncn 
 |-  ( a e. NN -> a e. CC )
170 2cnd 
 |-  ( a e. NN -> 2 e. CC )
171 2ne0 
 |-  2 =/= 0
172 171 a1i 
 |-  ( a e. NN -> 2 =/= 0 )
173 169 170 172 divcan1d 
 |-  ( a e. NN -> ( ( a / 2 ) x. 2 ) = a )
174 173 ad3antlr 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( a / 2 ) x. 2 ) = a )
175 174 adantl 
 |-  ( ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) /\ ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) ) -> ( ( a / 2 ) x. 2 ) = a )
176 159 168 175 3eqtrrd 
 |-  ( ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) /\ ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
177 176 ex 
 |-  ( ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) -> ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
178 177 imim2i 
 |-  ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> ( ( #b ` ( a / 2 ) ) = y -> ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
179 178 com13 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( #b ` ( a / 2 ) ) = y -> ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
180 19 179 sylbid 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
181 180 com23 
 |-  ( ( ( ( ( a / 2 ) e. NN /\ a e. NN ) /\ ( #b ` a ) = ( y + 1 ) ) /\ y e. NN ) -> ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
182 181 exp31 
 |-  ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( #b ` a ) = ( y + 1 ) -> ( y e. NN -> ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) )
183 182 com25 
 |-  ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) )
184 183 com14 
 |-  ( ( ( #b ` ( a / 2 ) ) = y -> ( a / 2 ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) ( a / 2 ) ) x. ( 2 ^ k ) ) ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) )
185 12 184 syl 
 |-  ( ( ( a / 2 ) e. NN0 /\ A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) )
186 185 ex 
 |-  ( ( a / 2 ) e. NN0 -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) ) )
187 186 com25 
 |-  ( ( a / 2 ) e. NN0 -> ( ( ( a / 2 ) e. NN /\ a e. NN ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) ) )
188 187 expdcom 
 |-  ( ( a / 2 ) e. NN -> ( a e. NN -> ( ( a / 2 ) e. NN0 -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) ) ) )
189 1 188 mpid 
 |-  ( ( a / 2 ) e. NN -> ( a e. NN -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) ) )
190 189 impcom 
 |-  ( ( a e. NN /\ ( a / 2 ) e. NN ) -> ( ( #b ` ( a / 2 ) ) = ( ( #b ` a ) - 1 ) -> ( y e. NN -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) ) )
191 3 190 mpd 
 |-  ( ( a e. NN /\ ( a / 2 ) e. NN ) -> ( y e. NN -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) ) )
192 191 imp 
 |-  ( ( ( a e. NN /\ ( a / 2 ) e. NN ) /\ y e. NN ) -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )