Metamath Proof Explorer

Theorem sadadd2

Description: Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Hypotheses sadval.a 
|- ( ph -> A C_ NN0 )
sadval.b 
|- ( ph -> B C_ NN0 )
sadval.c 
|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
sadcp1.n 
|- ( ph -> N e. NN0 )
sadcadd.k 
|- K = `' ( bits |` NN0 )
Assertion sadadd2 
|- ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sadval.a 
 |-  ( ph -> A C_ NN0 )
2 sadval.b 
 |-  ( ph -> B C_ NN0 )
3 sadval.c 
 |-  C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 sadcp1.n 
 |-  ( ph -> N e. NN0 )
5 sadcadd.k 
 |-  K = `' ( bits |` NN0 )
6 oveq2 
 |-  ( x = 0 -> ( 0 ..^ x ) = ( 0 ..^ 0 ) )
7 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
8 6 7 eqtrdi 
 |-  ( x = 0 -> ( 0 ..^ x ) = (/) )
9 8 ineq2d 
 |-  ( x = 0 -> ( ( A sadd B ) i^i ( 0 ..^ x ) ) = ( ( A sadd B ) i^i (/) ) )
10 in0 
 |-  ( ( A sadd B ) i^i (/) ) = (/)
11 9 10 eqtrdi 
 |-  ( x = 0 -> ( ( A sadd B ) i^i ( 0 ..^ x ) ) = (/) )
12 11 fveq2d 
 |-  ( x = 0 -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) = ( K ` (/) ) )
13 0nn0 
 |-  0 e. NN0
14 fvres 
 |-  ( 0 e. NN0 -> ( ( bits |` NN0 ) ` 0 ) = ( bits ` 0 ) )
15 13 14 ax-mp 
 |-  ( ( bits |` NN0 ) ` 0 ) = ( bits ` 0 )
16 0bits 
 |-  ( bits ` 0 ) = (/)
17 15 16 eqtr2i 
 |-  (/) = ( ( bits |` NN0 ) ` 0 )
18 5 17 fveq12i 
 |-  ( K ` (/) ) = ( `' ( bits |` NN0 ) ` ( ( bits |` NN0 ) ` 0 ) )
19 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
20 f1ocnvfv1 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ 0 e. NN0 ) -> ( `' ( bits |` NN0 ) ` ( ( bits |` NN0 ) ` 0 ) ) = 0 )
21 19 13 20 mp2an 
 |-  ( `' ( bits |` NN0 ) ` ( ( bits |` NN0 ) ` 0 ) ) = 0
22 18 21 eqtri 
 |-  ( K ` (/) ) = 0
23 12 22 eqtrdi 
 |-  ( x = 0 -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) = 0 )
24 fveq2 
 |-  ( x = 0 -> ( C ` x ) = ( C ` 0 ) )
25 24 eleq2d 
 |-  ( x = 0 -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` 0 ) ) )
26 oveq2 
 |-  ( x = 0 -> ( 2 ^ x ) = ( 2 ^ 0 ) )
27 25 26 ifbieq1d 
 |-  ( x = 0 -> if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) = if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) )
28 23 27 oveq12d 
 |-  ( x = 0 -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( 0 + if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) ) )
29 8 ineq2d 
 |-  ( x = 0 -> ( A i^i ( 0 ..^ x ) ) = ( A i^i (/) ) )
30 in0 
 |-  ( A i^i (/) ) = (/)
31 29 30 eqtrdi 
 |-  ( x = 0 -> ( A i^i ( 0 ..^ x ) ) = (/) )
32 31 fveq2d 
 |-  ( x = 0 -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` (/) ) )
33 32 22 eqtrdi 
 |-  ( x = 0 -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = 0 )
34 8 ineq2d 
 |-  ( x = 0 -> ( B i^i ( 0 ..^ x ) ) = ( B i^i (/) ) )
35 in0 
 |-  ( B i^i (/) ) = (/)
36 34 35 eqtrdi 
 |-  ( x = 0 -> ( B i^i ( 0 ..^ x ) ) = (/) )
37 36 fveq2d 
 |-  ( x = 0 -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` (/) ) )
38 37 22 eqtrdi 
 |-  ( x = 0 -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = 0 )
39 33 38 oveq12d 
 |-  ( x = 0 -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( 0 + 0 ) )
40 00id 
 |-  ( 0 + 0 ) = 0
41 39 40 eqtrdi 
 |-  ( x = 0 -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = 0 )
42 28 41 eqeq12d 
 |-  ( x = 0 -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( 0 + if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) ) = 0 ) )
43 42 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( ph -> ( 0 + if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) ) = 0 ) ) )
44 oveq2 
 |-  ( x = k -> ( 0 ..^ x ) = ( 0 ..^ k ) )
45 44 ineq2d 
 |-  ( x = k -> ( ( A sadd B ) i^i ( 0 ..^ x ) ) = ( ( A sadd B ) i^i ( 0 ..^ k ) ) )
46 45 fveq2d 
 |-  ( x = k -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) = ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) )
47 fveq2 
 |-  ( x = k -> ( C ` x ) = ( C ` k ) )
48 47 eleq2d 
 |-  ( x = k -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` k ) ) )
49 oveq2 
 |-  ( x = k -> ( 2 ^ x ) = ( 2 ^ k ) )
50 48 49 ifbieq1d 
 |-  ( x = k -> if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) = if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) )
51 46 50 oveq12d 
 |-  ( x = k -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) )
52 44 ineq2d 
 |-  ( x = k -> ( A i^i ( 0 ..^ x ) ) = ( A i^i ( 0 ..^ k ) ) )
53 52 fveq2d 
 |-  ( x = k -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` ( A i^i ( 0 ..^ k ) ) ) )
54 44 ineq2d 
 |-  ( x = k -> ( B i^i ( 0 ..^ x ) ) = ( B i^i ( 0 ..^ k ) ) )
55 54 fveq2d 
 |-  ( x = k -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` ( B i^i ( 0 ..^ k ) ) ) )
56 53 55 oveq12d 
 |-  ( x = k -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) )
57 51 56 eqeq12d 
 |-  ( x = k -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) )
58 57 imbi2d 
 |-  ( x = k -> ( ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) )
59 oveq2 
 |-  ( x = ( k + 1 ) -> ( 0 ..^ x ) = ( 0 ..^ ( k + 1 ) ) )
60 59 ineq2d 
 |-  ( x = ( k + 1 ) -> ( ( A sadd B ) i^i ( 0 ..^ x ) ) = ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) )
61 60 fveq2d 
 |-  ( x = ( k + 1 ) -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) = ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) )
62 fveq2 
 |-  ( x = ( k + 1 ) -> ( C ` x ) = ( C ` ( k + 1 ) ) )
63 62 eleq2d 
 |-  ( x = ( k + 1 ) -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` ( k + 1 ) ) ) )
64 oveq2 
 |-  ( x = ( k + 1 ) -> ( 2 ^ x ) = ( 2 ^ ( k + 1 ) ) )
65 63 64 ifbieq1d 
 |-  ( x = ( k + 1 ) -> if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) = if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) )
66 61 65 oveq12d 
 |-  ( x = ( k + 1 ) -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) )
67 59 ineq2d 
 |-  ( x = ( k + 1 ) -> ( A i^i ( 0 ..^ x ) ) = ( A i^i ( 0 ..^ ( k + 1 ) ) ) )
68 67 fveq2d 
 |-  ( x = ( k + 1 ) -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) )
69 59 ineq2d 
 |-  ( x = ( k + 1 ) -> ( B i^i ( 0 ..^ x ) ) = ( B i^i ( 0 ..^ ( k + 1 ) ) ) )
70 69 fveq2d 
 |-  ( x = ( k + 1 ) -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) )
71 68 70 oveq12d 
 |-  ( x = ( k + 1 ) -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) )
72 66 71 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) )
73 72 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) )
74 oveq2 
 |-  ( x = N -> ( 0 ..^ x ) = ( 0 ..^ N ) )
75 74 ineq2d 
 |-  ( x = N -> ( ( A sadd B ) i^i ( 0 ..^ x ) ) = ( ( A sadd B ) i^i ( 0 ..^ N ) ) )
76 75 fveq2d 
 |-  ( x = N -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) = ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) )
77 fveq2 
 |-  ( x = N -> ( C ` x ) = ( C ` N ) )
78 77 eleq2d 
 |-  ( x = N -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` N ) ) )
79 oveq2 
 |-  ( x = N -> ( 2 ^ x ) = ( 2 ^ N ) )
80 78 79 ifbieq1d 
 |-  ( x = N -> if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) = if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) )
81 76 80 oveq12d 
 |-  ( x = N -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
82 74 ineq2d 
 |-  ( x = N -> ( A i^i ( 0 ..^ x ) ) = ( A i^i ( 0 ..^ N ) ) )
83 82 fveq2d 
 |-  ( x = N -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` ( A i^i ( 0 ..^ N ) ) ) )
84 74 ineq2d 
 |-  ( x = N -> ( B i^i ( 0 ..^ x ) ) = ( B i^i ( 0 ..^ N ) ) )
85 84 fveq2d 
 |-  ( x = N -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` ( B i^i ( 0 ..^ N ) ) ) )
86 83 85 oveq12d 
 |-  ( x = N -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )
87 81 86 eqeq12d 
 |-  ( x = N -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )
88 87 imbi2d 
 |-  ( x = N -> ( ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ x ) ) ) + if ( (/) e. ( C ` x ) , ( 2 ^ x ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) ) )
89 1 2 3 sadc0 
 |-  ( ph -> -. (/) e. ( C ` 0 ) )
90 89 iffalsed 
 |-  ( ph -> if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) = 0 )
91 90 oveq2d 
 |-  ( ph -> ( 0 + if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) ) = ( 0 + 0 ) )
92 91 40 eqtrdi 
 |-  ( ph -> ( 0 + if ( (/) e. ( C ` 0 ) , ( 2 ^ 0 ) , 0 ) ) = 0 )
93 1 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> A C_ NN0 )
94 2 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> B C_ NN0 )
95 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> k e. NN0 )
96 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) )
97 93 94 3 95 5 96 sadadd2lem 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) )
98 97 ex 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) )
99 98 expcom 
 |-  ( k e. NN0 -> ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) )
100 99 a2d 
 |-  ( k e. NN0 -> ( ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ k ) ) ) + if ( (/) e. ( C ` k ) , ( 2 ^ k ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( k + 1 ) ) ) ) + if ( (/) e. ( C ` ( k + 1 ) ) , ( 2 ^ ( k + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) )
101 43 58 73 88 92 100 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )
102 4 101 mpcom 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )