Theorem sadadd2lem 12934

Description: Lemma for sadadd2 12935. (Contributed by Mario Carneiro, 9-Sep-2016.)

Hypotheses

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

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

Distinct variable groups:   m, c, n   A, c, m   B, c, m   n, N

Allowed substitution hints:   ph( m, n, c)   A( n)   B( n)   C( m, n, c)   K( m, n, c)   N( m, c)

Proof of Theorem sadadd2lem

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3529	. . . . . . . . 9 |- ( ( A sadd B ) i^i ( 0..^ N ) ) C_ ( A sadd B )
2		sadval.a	. . . . . . . . . . 11 |- ( ph -> A C_ NN0 )
3		sadval.b	. . . . . . . . . . 11 |- ( ph -> B C_ NN0 )
4		sadval.c	. . . . . . . . . . 11 |- 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 ) ) ) )
5	2, 3, 4	sadfval 12927	. . . . . . . . . 10 |- ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
6		ssrab2 3396	. . . . . . . . . 10 |- { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } C_ NN0
7	5, 6	syl6eqss 3366	. . . . . . . . 9 |- ( ph -> ( A sadd B ) C_ NN0 )
8	1, 7	syl5ss 3327	. . . . . . . 8 |- ( ph -> ( ( A sadd B ) i^i ( 0..^ N ) ) C_ NN0 )
9		fzofi 11276	. . . . . . . . . 10 |- ( 0..^ N ) e. Fin
10	9	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ N ) e. Fin )
11		inss2 3530	. . . . . . . . 9 |- ( ( A sadd B ) i^i ( 0..^ N ) ) C_ ( 0..^ N )
12		ssfi 7296	. . . . . . . . 9 |- ( ( ( 0..^ N ) e. Fin /\ ( ( A sadd B ) i^i ( 0..^ N ) ) C_ ( 0..^ N ) ) -> ( ( A sadd B ) i^i ( 0..^ N ) ) e. Fin )
13	10, 11, 12	sylancl 644	. . . . . . . 8 |- ( ph -> ( ( A sadd B ) i^i ( 0..^ N ) ) e. Fin )
14		elfpw 7374	. . . . . . . 8 |- ( ( ( 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 ) )
15	8, 13, 14	sylanbrc 646	. . . . . . 7 |- ( ph -> ( ( A sadd B ) i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
16		bitsf1o 12920	. . . . . . . . . 10 |- (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
17		f1ocnv 5654	. . . . . . . . . 10 |- ( (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
18		f1of 5641	. . . . . . . . . 10 |- ( `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
19	16, 17, 18	mp2b 10	. . . . . . . . 9 |- `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0
20		sadcadd.k	. . . . . . . . . 10 |- K = `' (bits |` NN0 )
21	20	feq1i 5552	. . . . . . . . 9 |- ( K : ( ~P NN0 i^i Fin ) --> NN0 <-> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
22	19, 21	mpbir 201	. . . . . . . 8 |- K : ( ~P NN0 i^i Fin ) --> NN0
23	22	ffvelrni 5836	. . . . . . 7 |- ( ( ( A sadd B ) i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( ( A sadd B ) i^i ( 0..^ N ) ) ) e. NN0 )
24	15, 23	syl 16	. . . . . 6 |- ( ph -> ( K ` ( ( A sadd B ) i^i ( 0..^ N ) ) ) e. NN0 )
25	24	nn0cnd 10240	. . . . 5 |- ( ph -> ( K ` ( ( A sadd B ) i^i ( 0..^ N ) ) ) e. CC )
26		2nn0 10202	. . . . . . . . . 10 |- 2 e. NN0
27	26	a1i 11	. . . . . . . . 9 |- ( ph -> 2 e. NN0 )
28		sadcp1.n	. . . . . . . . 9 |- ( ph -> N e. NN0 )
29	27, 28	nn0expcld 11508	. . . . . . . 8 |- ( ph -> ( 2 ^ N ) e. NN0 )
30		0nn0 10200	. . . . . . . 8 |- 0 e. NN0
31		ifcl 3743	. . . . . . . 8 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. NN0 )
32	29, 30, 31	sylancl 644	. . . . . . 7 |- ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. NN0 )
33	32	nn0cnd 10240	. . . . . 6 |- ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. CC )
34		1nn0 10201	. . . . . . . . . . 11 |- 1 e. NN0
35	34	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. NN0 )
36	28, 35	nn0addcld 10242	. . . . . . . . 9 |- ( ph -> ( N + 1 ) e. NN0 )
37	27, 36	nn0expcld 11508	. . . . . . . 8 |- ( ph -> ( 2 ^ ( N + 1 ) ) e. NN0 )
38		ifcl 3743	. . . . . . . 8 |- ( ( ( 2 ^ ( N + 1 ) ) e. NN0 /\ 0 e. NN0 ) -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. NN0 )
39	37, 30, 38	sylancl 644	. . . . . . 7 |- ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. NN0 )
40	39	nn0cnd 10240	. . . . . 6 |- ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. CC )
41	33, 40	addcld 9071	. . . . 5 |- ( ph -> ( if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) + if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) ) e. CC )
42	25, 41	addcld 9071	. . . 4 |- ( 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 )
43		inss1 3529	. . . . . . . . . 10 |- ( A i^i ( 0..^ N ) ) C_ A
44	43, 2	syl5ss 3327	. . . . . . . . 9 |- ( ph -> ( A i^i ( 0..^ N ) ) C_ NN0 )
45		inss2 3530	. . . . . . . . . 10 |- ( A i^i ( 0..^ N ) ) C_ ( 0..^ N )
46		ssfi 7296	. . . . . . . . . 10 |- ( ( ( 0..^ N ) e. Fin /\ ( A i^i ( 0..^ N ) ) C_ ( 0..^ N ) ) -> ( A i^i ( 0..^ N ) ) e. Fin )
47	10, 45, 46	sylancl 644	. . . . . . . . 9 |- ( ph -> ( A i^i ( 0..^ N ) ) e. Fin )
48		elfpw 7374	. . . . . . . . 9 |- ( ( 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 ) )
49	44, 47, 48	sylanbrc 646	. . . . . . . 8 |- ( ph -> ( A i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
50	22	ffvelrni 5836	. . . . . . . 8 |- ( ( A i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( A i^i ( 0..^ N ) ) ) e. NN0 )
51	49, 50	syl 16	. . . . . . 7 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. NN0 )
52	51	nn0cnd 10240	. . . . . 6 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. CC )
53		inss1 3529	. . . . . . . . . 10 |- ( B i^i ( 0..^ N ) ) C_ B
54	53, 3	syl5ss 3327	. . . . . . . . 9 |- ( ph -> ( B i^i ( 0..^ N ) ) C_ NN0 )
55		inss2 3530	. . . . . . . . . 10 |- ( B i^i ( 0..^ N ) ) C_ ( 0..^ N )
56		ssfi 7296	. . . . . . . . . 10 |- ( ( ( 0..^ N ) e. Fin /\ ( B i^i ( 0..^ N ) ) C_ ( 0..^ N ) ) -> ( B i^i ( 0..^ N ) ) e. Fin )
57	10, 55, 56	sylancl 644	. . . . . . . . 9 |- ( ph -> ( B i^i ( 0..^ N ) ) e. Fin )
58		elfpw 7374	. . . . . . . . 9 |- ( ( 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 ) )
59	54, 57, 58	sylanbrc 646	. . . . . . . 8 |- ( ph -> ( B i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
60	22	ffvelrni 5836	. . . . . . . 8 |- ( ( B i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( B i^i ( 0..^ N ) ) ) e. NN0 )
61	59, 60	syl 16	. . . . . . 7 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. NN0 )
62	61	nn0cnd 10240	. . . . . 6 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. CC )
63	52, 62	addcld 9071	. . . . 5 |- ( ph -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. CC )
64		ifcl 3743	. . . . . . . 8 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
65	29, 30, 64	sylancl 644	. . . . . . 7 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
66	65	nn0cnd 10240	. . . . . 6 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. CC )
67		ifcl 3743	. . . . . . . 8 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
68	29, 30, 67	sylancl 644	. . . . . . 7 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
69	68	nn0cnd 10240	. . . . . 6 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. CC )
70	66, 69	addcld 9071	. . . . 5 |- ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. CC )
71	63, 70	addcld 9071	. . . 4 |- ( 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 )
72	29	nn0cnd 10240	. . . . . 6 |- ( ph -> ( 2 ^ N ) e. CC )
73	72	adantr 452	. . . . 5 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( 2 ^ N ) e. CC )
74		0cn 9048	. . . . . 6 |- 0 e. CC
75	74	a1i 11	. . . . 5 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> 0 e. CC )
76	73, 75	ifclda 3734	. . . 4 |- ( ph -> if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) e. CC )
77		sadadd2lem.1	. . . . . 6 |- ( 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 ) ) ) ) )
78	2, 3, 4, 28	sadval 12931	. . . . . . . . 9 |- ( ph -> ( N e. ( A sadd B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
79	78	ifbid 3725	. . . . . . . 8 |- ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) = if (hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , ( 2 ^ N ) , 0 ) )
80	2, 3, 4, 28	sadcp1 12930	. . . . . . . . 9 |- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
81	27	nn0cnd 10240	. . . . . . . . . . 11 |- ( ph -> 2 e. CC )
82	81, 28	expp1d 11487	. . . . . . . . . 10 |- ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
83	72, 81	mulcomd 9073	. . . . . . . . . 10 |- ( ph -> ( ( 2 ^ N ) x. 2 ) = ( 2 x. ( 2 ^ N ) ) )
84	82, 83	eqtrd 2444	. . . . . . . . 9 |- ( ph -> ( 2 ^ ( N + 1 ) ) = ( 2 x. ( 2 ^ N ) ) )
85		eqidd 2413	. . . . . . . . 9 |- ( ph -> 0 = 0 )
86	80, 84, 85	ifbieq12d 3729	. . . . . . . 8 |- ( 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 ) )
87	79, 86	oveq12d 6066	. . . . . . 7 |- ( 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 ) ) )
88		sadadd2lem2 12925	. . . . . . . 8 |- ( ( 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 ) ) )
89	72, 88	syl 16	. . . . . . 7 |- ( 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 ) ) )
90	87, 89	eqtrd 2444	. . . . . 6 |- ( 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 ) ) )
91	77, 90	oveq12d 6066	. . . . 5 |- ( 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 ) ) ) )
92	25, 41, 76	add32d 9252	. . . . 5 |- ( 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 ) ) ) )
93	63, 70, 76	addassd 9074	. . . . 5 |- ( 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 ) ) ) )
94	91, 92, 93	3eqtr4d 2454	. . . 4 |- ( 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 ) ) )
95	42, 71, 76, 94	addcan2ad 9236	. . 3 |- ( 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 ) ) ) )
96	25, 33, 40	addassd 9074	. . 3 |- ( 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 ) ) ) )
97	52, 66, 62, 69	add4d 9253	. . 3 |- ( 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 ) ) ) )
98	95, 96, 97	3eqtr4d 2454	. 2 |- ( 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 ) ) ) )
99	20	bitsinvp1 12924	. . . 4 |- ( ( ( 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 ) ) )
100	7, 28, 99	syl2anc 643	. . 3 |- ( 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 ) ) )
101	100	oveq1d 6063	. 2 |- ( 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 ) ) )
102	20	bitsinvp1 12924	. . . 4 |- ( ( 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 ) ) )
103	2, 28, 102	syl2anc 643	. . 3 |- ( ph -> ( K ` ( A i^i ( 0..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )
104	20	bitsinvp1 12924	. . . 4 |- ( ( 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 ) ) )
105	3, 28, 104	syl2anc 643	. . 3 |- ( ph -> ( K ` ( B i^i ( 0..^ ( N + 1 ) ) ) ) = ( ( K ` ( B i^i ( 0..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
106	103, 105	oveq12d 6066	. 2 |- ( 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 ) ) ) )
107	98, 101, 106	3eqtr4d 2454	1 |- ( 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 ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 359  haddwhad 1384  caddwcad 1385   = wceq 1649   e. wcel 1721   {crab 2678   i^i cin 3287   C_ wss 3288   (/)c0 3596   ifcif 3707   ~Pcpw 3767   e. cmpt 4234   `'ccnv 4844   |` cres 4847   -->wf 5417   -1-1-onto->wf1o 5420   ` cfv 5421  (class class class)co 6048   e. cmpt2 6050   1oc1o 6684   2oc2o 6685   Fincfn 7076   CCcc 8952   0cc0 8954   1c1 8955   + caddc 8957   x. cmul 8959   - cmin 9255   2c2 10013   NN0cn0 10185  ..^cfzo 11098   seq cseq 11286   ^cexp 11345  bitscbits 12894   sadd csad 12895

This theorem is referenced by:  sadadd2  12935

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-inf2 7560  ax-cnex 9010  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031  ax-pre-sup 9032

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-xor 1311  df-tru 1325  df-had 1386  df-cad 1387  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-disj 4151  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-1st 6316  df-2nd 6317  df-riota 6516  df-recs 6600  df-rdg 6635  df-1o 6691  df-2o 6692  df-oadd 6695  df-er 6872  df-map 6987  df-pm 6988  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-sup 7412  df-oi 7443  df-card 7790  df-cda 8012  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-div 9642  df-nn 9965  df-2 10022  df-3 10023  df-n0 10186  df-z 10247  df-uz 10453  df-rp 10577  df-fz 11008  df-fzo 11099  df-fl 11165  df-mod 11214  df-seq 11287  df-exp 11346  df-hash 11582  df-cj 11867  df-re 11868  df-im 11869  df-sqr 12003  df-abs 12004  df-clim 12245  df-sum 12443  df-dvds 12816  df-bits 12897  df-sad 12926