Metamath Proof Explorer

Theorem nn0sumshdiglem1

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

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( a = x -> ( ( #b ` a ) = y <-> ( #b ` x ) = y ) )
2 id 
 |-  ( a = x -> a = x )
3 oveq2 
 |-  ( a = x -> ( k ( digit ` 2 ) a ) = ( k ( digit ` 2 ) x ) )
4 3 oveq1d 
 |-  ( a = x -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) )
5 4 sumeq2sdv 
 |-  ( a = x -> sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) )
6 2 5 eqeq12d 
 |-  ( a = x -> ( a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) )
7 1 6 imbi12d 
 |-  ( a = x -> ( ( ( #b ` a ) = y -> a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) ) )
8 7 cbvralvw 
 |-  ( A. a e. NN0 ( ( #b ` a ) = y -> a = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) )
9 elnn0 
 |-  ( a e. NN0 <-> ( a e. NN \/ a = 0 ) )
10 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 ) ) ) ) )
11 10 expimpd 
 |-  ( ( 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 ) ) ) ) )
12 nn0sumshdiglemB 
 |-  ( ( ( a e. NN /\ ( ( a - 1 ) / 2 ) e. NN0 ) /\ 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 ) ) ) ) )
13 12 expimpd 
 |-  ( ( a e. NN /\ ( ( a - 1 ) / 2 ) e. NN0 ) -> ( ( 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 ) ) ) ) )
14 nneom 
 |-  ( a e. NN -> ( ( a / 2 ) e. NN \/ ( ( a - 1 ) / 2 ) e. NN0 ) )
15 11 13 14 mpjaodan 
 |-  ( a 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 ) ) ) ) )
16 eqcom 
 |-  ( 1 = ( y + 1 ) <-> ( y + 1 ) = 1 )
17 16 a1i 
 |-  ( y e. NN -> ( 1 = ( y + 1 ) <-> ( y + 1 ) = 1 ) )
18 nncn 
 |-  ( y e. NN -> y e. CC )
19 1cnd 
 |-  ( y e. NN -> 1 e. CC )
20 18 19 19 addlsub 
 |-  ( y e. NN -> ( ( y + 1 ) = 1 <-> y = ( 1 - 1 ) ) )
21 1m1e0 
 |-  ( 1 - 1 ) = 0
22 21 a1i 
 |-  ( y e. NN -> ( 1 - 1 ) = 0 )
23 22 eqeq2d 
 |-  ( y e. NN -> ( y = ( 1 - 1 ) <-> y = 0 ) )
24 17 20 23 3bitrd 
 |-  ( y e. NN -> ( 1 = ( y + 1 ) <-> y = 0 ) )
25 oveq1 
 |-  ( y = 0 -> ( y + 1 ) = ( 0 + 1 ) )
26 25 oveq2d 
 |-  ( y = 0 -> ( 0 ..^ ( y + 1 ) ) = ( 0 ..^ ( 0 + 1 ) ) )
27 0p1e1 
 |-  ( 0 + 1 ) = 1
28 27 oveq2i 
 |-  ( 0 ..^ ( 0 + 1 ) ) = ( 0 ..^ 1 )
29 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
30 28 29 eqtri 
 |-  ( 0 ..^ ( 0 + 1 ) ) = { 0 }
31 26 30 eqtrdi 
 |-  ( y = 0 -> ( 0 ..^ ( y + 1 ) ) = { 0 } )
32 31 sumeq1d 
 |-  ( y = 0 -> sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) = sum_ k e. { 0 } ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) )
33 0cn 
 |-  0 e. CC
34 oveq1 
 |-  ( k = 0 -> ( k ( digit ` 2 ) 0 ) = ( 0 ( digit ` 2 ) 0 ) )
35 2nn 
 |-  2 e. NN
36 0z 
 |-  0 e. ZZ
37 dig0 
 |-  ( ( 2 e. NN /\ 0 e. ZZ ) -> ( 0 ( digit ` 2 ) 0 ) = 0 )
38 35 36 37 mp2an 
 |-  ( 0 ( digit ` 2 ) 0 ) = 0
39 34 38 eqtrdi 
 |-  ( k = 0 -> ( k ( digit ` 2 ) 0 ) = 0 )
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 ) 0 ) x. ( 2 ^ k ) ) = ( 0 x. 1 ) )
46 1re 
 |-  1 e. RR
47 mul02lem2 
 |-  ( 1 e. RR -> ( 0 x. 1 ) = 0 )
48 46 47 ax-mp 
 |-  ( 0 x. 1 ) = 0
49 45 48 eqtrdi 
 |-  ( k = 0 -> ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) = 0 )
50 49 sumsn 
 |-  ( ( 0 e. CC /\ 0 e. CC ) -> sum_ k e. { 0 } ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) = 0 )
51 33 33 50 mp2an 
 |-  sum_ k e. { 0 } ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) = 0
52 32 51 eqtr2di 
 |-  ( y = 0 -> 0 = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) )
53 24 52 syl6bi 
 |-  ( y e. NN -> ( 1 = ( y + 1 ) -> 0 = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) ) )
54 53 adantl 
 |-  ( ( a = 0 /\ y e. NN ) -> ( 1 = ( y + 1 ) -> 0 = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) ) )
55 fveq2 
 |-  ( a = 0 -> ( #b ` a ) = ( #b ` 0 ) )
56 blen0 
 |-  ( #b ` 0 ) = 1
57 55 56 eqtrdi 
 |-  ( a = 0 -> ( #b ` a ) = 1 )
58 57 eqeq1d 
 |-  ( a = 0 -> ( ( #b ` a ) = ( y + 1 ) <-> 1 = ( y + 1 ) ) )
59 id 
 |-  ( a = 0 -> a = 0 )
60 oveq2 
 |-  ( a = 0 -> ( k ( digit ` 2 ) a ) = ( k ( digit ` 2 ) 0 ) )
61 60 oveq1d 
 |-  ( a = 0 -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) )
62 61 sumeq2sdv 
 |-  ( a = 0 -> sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) )
63 59 62 eqeq12d 
 |-  ( a = 0 -> ( a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> 0 = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) ) )
64 58 63 imbi12d 
 |-  ( a = 0 -> ( ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( 1 = ( y + 1 ) -> 0 = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) ) ) )
65 64 adantr 
 |-  ( ( a = 0 /\ y e. NN ) -> ( ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( 1 = ( y + 1 ) -> 0 = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) 0 ) x. ( 2 ^ k ) ) ) ) )
66 54 65 mpbird 
 |-  ( ( a = 0 /\ y e. NN ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
67 66 a1d 
 |-  ( ( a = 0 /\ 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 ) ) ) ) )
68 67 expimpd 
 |-  ( a = 0 -> ( ( 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 ) ) ) ) )
69 15 68 jaoi 
 |-  ( ( a e. NN \/ a = 0 ) -> ( ( 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 ) ) ) ) )
70 9 69 sylbi 
 |-  ( a e. NN0 -> ( ( 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 ) ) ) ) )
71 70 com12 
 |-  ( ( y e. NN /\ A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) ) -> ( a e. NN0 -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
72 71 ralrimiv 
 |-  ( ( y e. NN /\ A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) 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 ) ) ) )
73 72 ex 
 |-  ( y e. NN -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) 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 ) ) ) ) )
74 8 73 syl5bi 
 |-  ( 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 ) ) ) ) )