Metamath Proof Explorer

Theorem nn0sumshdiglem2

Description: Lemma 2 for nn0sumshdig . (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion nn0sumshdiglem2 
|- ( L e. NN -> A. a e. NN0 ( ( #b ` a ) = L -> a = sum_ k e. ( 0 ..^ L ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( x = 1 -> ( ( #b ` a ) = x <-> ( #b ` a ) = 1 ) )
2 oveq2 
 |-  ( x = 1 -> ( 0 ..^ x ) = ( 0 ..^ 1 ) )
3 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
4 2 3 eqtrdi 
 |-  ( x = 1 -> ( 0 ..^ x ) = { 0 } )
5 4 sumeq1d 
 |-  ( x = 1 -> sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
6 5 eqeq2d 
 |-  ( x = 1 -> ( a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> a = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
7 1 6 imbi12d 
 |-  ( x = 1 -> ( ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` a ) = 1 -> a = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
8 7 ralbidv 
 |-  ( x = 1 -> ( A. a e. NN0 ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> A. a e. NN0 ( ( #b ` a ) = 1 -> a = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
9 eqeq2 
 |-  ( x = y -> ( ( #b ` a ) = x <-> ( #b ` a ) = y ) )
10 oveq2 
 |-  ( x = y -> ( 0 ..^ x ) = ( 0 ..^ y ) )
11 10 sumeq1d 
 |-  ( x = y -> sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
12 11 eqeq2d 
 |-  ( x = y -> ( a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
13 9 12 imbi12d 
 |-  ( x = y -> ( ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` a ) = y -> a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
14 13 ralbidv 
 |-  ( x = y -> ( A. a e. NN0 ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> A. a e. NN0 ( ( #b ` a ) = y -> a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
15 eqeq2 
 |-  ( x = ( y + 1 ) -> ( ( #b ` a ) = x <-> ( #b ` a ) = ( y + 1 ) ) )
16 oveq2 
 |-  ( x = ( y + 1 ) -> ( 0 ..^ x ) = ( 0 ..^ ( y + 1 ) ) )
17 16 sumeq1d 
 |-  ( x = ( y + 1 ) -> sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
18 17 eqeq2d 
 |-  ( x = ( y + 1 ) -> ( a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
19 15 18 imbi12d 
 |-  ( x = ( y + 1 ) -> ( ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
20 19 ralbidv 
 |-  ( x = ( y + 1 ) -> ( A. a e. NN0 ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> A. a e. NN0 ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
21 eqeq2 
 |-  ( x = L -> ( ( #b ` a ) = x <-> ( #b ` a ) = L ) )
22 oveq2 
 |-  ( x = L -> ( 0 ..^ x ) = ( 0 ..^ L ) )
23 22 sumeq1d 
 |-  ( x = L -> sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ L ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
24 23 eqeq2d 
 |-  ( x = L -> ( a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> a = sum_ k e. ( 0 ..^ L ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
25 21 24 imbi12d 
 |-  ( x = L -> ( ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` a ) = L -> a = sum_ k e. ( 0 ..^ L ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
26 25 ralbidv 
 |-  ( x = L -> ( A. a e. NN0 ( ( #b ` a ) = x -> a = sum_ k e. ( 0 ..^ x ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> A. a e. NN0 ( ( #b ` a ) = L -> a = sum_ k e. ( 0 ..^ L ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
27 0cnd 
 |-  ( a e. NN0 -> 0 e. CC )
28 2nn 
 |-  2 e. NN
29 28 a1i 
 |-  ( a e. NN0 -> 2 e. NN )
30 0zd 
 |-  ( a e. NN0 -> 0 e. ZZ )
31 nn0rp0 
 |-  ( a e. NN0 -> a e. ( 0 [,) +oo ) )
32 digvalnn0 
 |-  ( ( 2 e. NN /\ 0 e. ZZ /\ a e. ( 0 [,) +oo ) ) -> ( 0 ( digit ` 2 ) a ) e. NN0 )
33 29 30 31 32 syl3anc 
 |-  ( a e. NN0 -> ( 0 ( digit ` 2 ) a ) e. NN0 )
34 33 nn0cnd 
 |-  ( a e. NN0 -> ( 0 ( digit ` 2 ) a ) e. CC )
35 1cnd 
 |-  ( a e. NN0 -> 1 e. CC )
36 34 35 mulcld 
 |-  ( a e. NN0 -> ( ( 0 ( digit ` 2 ) a ) x. 1 ) e. CC )
37 27 36 jca 
 |-  ( a e. NN0 -> ( 0 e. CC /\ ( ( 0 ( digit ` 2 ) a ) x. 1 ) e. CC ) )
38 37 adantr 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> ( 0 e. CC /\ ( ( 0 ( digit ` 2 ) a ) x. 1 ) e. CC ) )
39 oveq1 
 |-  ( k = 0 -> ( k ( digit ` 2 ) a ) = ( 0 ( digit ` 2 ) a ) )
40 oveq2 
 |-  ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
41 2cn 
 |-  2 e. CC
42 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
43 41 42 ax-mp 
 |-  ( 2 ^ 0 ) = 1
44 40 43 eqtrdi 
 |-  ( k = 0 -> ( 2 ^ k ) = 1 )
45 39 44 oveq12d 
 |-  ( k = 0 -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( 0 ( digit ` 2 ) a ) x. 1 ) )
46 45 sumsn 
 |-  ( ( 0 e. CC /\ ( ( 0 ( digit ` 2 ) a ) x. 1 ) e. CC ) -> sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( 0 ( digit ` 2 ) a ) x. 1 ) )
47 38 46 syl 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( 0 ( digit ` 2 ) a ) x. 1 ) )
48 34 adantr 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> ( 0 ( digit ` 2 ) a ) e. CC )
49 48 mulid1d 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> ( ( 0 ( digit ` 2 ) a ) x. 1 ) = ( 0 ( digit ` 2 ) a ) )
50 blen1b 
 |-  ( a e. NN0 -> ( ( #b ` a ) = 1 <-> ( a = 0 \/ a = 1 ) ) )
51 50 biimpa 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> ( a = 0 \/ a = 1 ) )
52 vex 
 |-  a e. _V
53 52 elpr 
 |-  ( a e. { 0 , 1 } <-> ( a = 0 \/ a = 1 ) )
54 51 53 sylibr 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> a e. { 0 , 1 } )
55 0dig2pr01 
 |-  ( a e. { 0 , 1 } -> ( 0 ( digit ` 2 ) a ) = a )
56 54 55 syl 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> ( 0 ( digit ` 2 ) a ) = a )
57 47 49 56 3eqtrrd 
 |-  ( ( a e. NN0 /\ ( #b ` a ) = 1 ) -> a = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
58 57 ex 
 |-  ( a e. NN0 -> ( ( #b ` a ) = 1 -> a = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
59 58 rgen 
 |-  A. a e. NN0 ( ( #b ` a ) = 1 -> a = sum_ k e. { 0 } ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) )
60 nn0sumshdiglem1 
 |-  ( y e. NN -> ( A. a e. NN0 ( ( #b ` a ) = y -> a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) -> A. a e. NN0 ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
61 8 14 20 26 59 60 nnind 
 |-  ( L e. NN -> A. a e. NN0 ( ( #b ` a ) = L -> a = sum_ k e. ( 0 ..^ L ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )