Metamath Proof Explorer

Theorem sadadd2lem

Description: Lemma for sadadd2 . (Contributed by Mario Carneiro, 9-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 )
sadadd2lem.1 
|- ( 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 ) ) ) ) )
Assertion sadadd2lem 
|- ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( N + 1 ) ) ) ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) ) )

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 sadadd2lem.1 
 |-  ( 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 ) ) ) ) )
7 inss1 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( A sadd B )
8 1 2 3 sadfval 
 |-  ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
9 ssrab2 
 |-  { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } C_ NN0
10 8 9 eqsstrdi 
 |-  ( ph -> ( A sadd B ) C_ NN0 )
11 7 10 sstrid 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 )
12 fzofi 
 |-  ( 0 ..^ N ) e. Fin
13 12 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
14 inss2 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
15 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
16 13 14 15 sylancl 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
17 elfpw 
 |-  ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin ) )
18 11 16 17 sylanbrc 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
19 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
20 f1ocnv 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
21 f1of 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
22 19 20 21 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0
23 5 feq1i 
 |-  ( K : ( ~P NN0 i^i Fin ) --> NN0 <-> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
24 22 23 mpbir 
 |-  K : ( ~P NN0 i^i Fin ) --> NN0
25 24 ffvelcdmi 
 |-  ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
26 18 25 syl 
 |-  ( ph -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
27 26 nn0cnd 
 |-  ( ph -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. CC )
28 2nn0 
 |-  2 e. NN0
29 28 a1i 
 |-  ( ph -> 2 e. NN0 )
30 29 4 nn0expcld 
 |-  ( ph -> ( 2 ^ N ) e. NN0 )
31 0nn0 
 |-  0 e. NN0
32 ifcl 
 |-  ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. NN0 )
33 30 31 32 sylancl 
 |-  ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. NN0 )
34 33 nn0cnd 
 |-  ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. CC )
35 1nn0 
 |-  1 e. NN0
36 35 a1i 
 |-  ( ph -> 1 e. NN0 )
37 4 36 nn0addcld 
 |-  ( ph -> ( N + 1 ) e. NN0 )
38 29 37 nn0expcld 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) e. NN0 )
39 ifcl 
 |-  ( ( ( 2 ^ ( N + 1 ) ) e. NN0 /\ 0 e. NN0 ) -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. NN0 )
40 38 31 39 sylancl 
 |-  ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. NN0 )
41 40 nn0cnd 
 |-  ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. CC )
42 34 41 addcld 
 |-  ( ph -> ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) e. CC )
43 27 42 addcld 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) e. CC )
44 inss1 
 |-  ( A i^i ( 0 ..^ N ) ) C_ A
45 44 1 sstrid 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
46 inss2 
 |-  ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
47 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( A i^i ( 0 ..^ N ) ) e. Fin )
48 13 46 47 sylancl 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) e. Fin )
49 elfpw 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( A i^i ( 0 ..^ N ) ) C_ NN0 /\ ( A i^i ( 0 ..^ N ) ) e. Fin ) )
50 45 48 49 sylanbrc 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
51 24 ffvelcdmi 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. NN0 )
52 50 51 syl 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. NN0 )
53 52 nn0cnd 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. CC )
54 inss1 
 |-  ( B i^i ( 0 ..^ N ) ) C_ B
55 54 2 sstrid 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
56 inss2 
 |-  ( B i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
57 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( B i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( B i^i ( 0 ..^ N ) ) e. Fin )
58 13 56 57 sylancl 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) e. Fin )
59 elfpw 
 |-  ( ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( B i^i ( 0 ..^ N ) ) C_ NN0 /\ ( B i^i ( 0 ..^ N ) ) e. Fin ) )
60 55 58 59 sylanbrc 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
61 24 ffvelcdmi 
 |-  ( ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. NN0 )
62 60 61 syl 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. NN0 )
63 62 nn0cnd 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. CC )
64 53 63 addcld 
 |-  ( ph -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) e. CC )
65 ifcl 
 |-  ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
66 30 31 65 sylancl 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
67 66 nn0cnd 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. CC )
68 ifcl 
 |-  ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
69 30 31 68 sylancl 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
70 69 nn0cnd 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. CC )
71 67 70 addcld 
 |-  ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. CC )
72 64 71 addcld 
 |-  ( ph -> ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) e. CC )
73 30 nn0cnd 
 |-  ( ph -> ( 2 ^ N ) e. CC )
74 73 adantr 
 |-  ( ( ph /\ (/) e. ( C ` N ) ) -> ( 2 ^ N ) e. CC )
75 0cnd 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> 0 e. CC )
76 74 75 ifclda 
 |-  ( ph -> if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) e. CC )
77 1 2 3 4 sadval 
 |-  ( ph -> ( N e. ( A sadd B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
78 77 ifbid 
 |-  ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) = if ( hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 ^ N ) , 0 ) )
79 1 2 3 4 sadcp1 
 |-  ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
80 29 nn0cnd 
 |-  ( ph -> 2 e. CC )
81 80 4 expp1d 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
82 73 80 mulcomd 
 |-  ( ph -> ( ( 2 ^ N ) x. 2 ) = ( 2 x. ( 2 ^ N ) ) )
83 81 82 eqtrd 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) = ( 2 x. ( 2 ^ N ) ) )
84 79 83 ifbieq1d 
 |-  ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) = if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 x. ( 2 ^ N ) ) , 0 ) )
85 78 84 oveq12d 
 |-  ( ph -> ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( if ( hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 ^ N ) , 0 ) + if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 x. ( 2 ^ N ) ) , 0 ) ) )
86 sadadd2lem2 
 |-  ( ( 2 ^ N ) e. CC -> ( if ( hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 ^ N ) , 0 ) + if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 x. ( 2 ^ N ) ) , 0 ) ) = ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
87 73 86 syl 
 |-  ( ph -> ( if ( hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 ^ N ) , 0 ) + if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 x. ( 2 ^ N ) ) , 0 ) ) = ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
88 85 87 eqtrd 
 |-  ( ph -> ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
89 6 88 oveq12d 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) ) )
90 27 42 76 add32d 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) )
91 64 71 76 addassd 
 |-  ( ph -> ( ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) ) )
92 89 90 91 3eqtr4d 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) = ( ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
93 43 72 76 92 addcan2ad 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
94 27 34 41 addassd 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) ) )
95 53 67 63 70 add4d 
 |-  ( ph -> ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) + ( ( K ` ( B i^i ( 0 ..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
96 93 94 95 3eqtr4d 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) + ( ( K ` ( B i^i ( 0 ..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
97 5 bitsinvp1 
 |-  ( ( ( A sadd B ) C_ NN0 /\ N e. NN0 ) -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) ) )
98 10 4 97 syl2anc 
 |-  ( ph -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) ) )
99 98 oveq1d 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( N + 1 ) ) ) ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) )
100 5 bitsinvp1 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )
101 1 4 100 syl2anc 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )
102 5 bitsinvp1 
 |-  ( ( B C_ NN0 /\ N e. NN0 ) -> ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( B i^i ( 0 ..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
103 2 4 102 syl2anc 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( B i^i ( 0 ..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
104 101 103 oveq12d 
 |-  ( ph -> ( ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) + ( ( K ` ( B i^i ( 0 ..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
105 96 99 104 3eqtr4d 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ ( N + 1 ) ) ) ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) = ( ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) ) )