Theorem sadadd2lem 12976

Description: Lemma for sadadd2 12977. (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 3563	. . . . . . . . 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 12969	. . . . . . . . . 10 |- ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
6		ssrab2 3430	. . . . . . . . . 10 |- { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } C_ NN0
7	5, 6	syl6eqss 3400	. . . . . . . . 9 |- ( ph -> ( A sadd B ) C_ NN0 )
8	1, 7	syl5ss 3361	. . . . . . . 8 |- ( ph -> ( ( A sadd B ) i^i ( 0..^ N ) ) C_ NN0 )
9		fzofi 11318	. . . . . . . . . 10 |- ( 0..^ N ) e. Fin
10	9	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ N ) e. Fin )
11		inss2 3564	. . . . . . . . 9 |- ( ( A sadd B ) i^i ( 0..^ N ) ) C_ ( 0..^ N )
12		ssfi 7332	. . . . . . . . 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 645	. . . . . . . 8 |- ( ph -> ( ( A sadd B ) i^i ( 0..^ N ) ) e. Fin )
14		elfpw 7411	. . . . . . . 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 647	. . . . . . 7 |- ( ph -> ( ( A sadd B ) i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
16		bitsf1o 12962	. . . . . . . . . 10 |- (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
17		f1ocnv 5690	. . . . . . . . . 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 5677	. . . . . . . . . 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 5588	. . . . . . . . 9 |- ( K : ( ~P NN0 i^i Fin ) --> NN0 <-> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
22	19, 21	mpbir 202	. . . . . . . 8 |- K : ( ~P NN0 i^i Fin ) --> NN0
23	22	ffvelrni 5872	. . . . . . 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 10281	. . . . 5 |- ( ph -> ( K ` ( ( A sadd B ) i^i ( 0..^ N ) ) ) e. CC )
26		2nn0 10243	. . . . . . . . . 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 11550	. . . . . . . 8 |- ( ph -> ( 2 ^ N ) e. NN0 )
30		0nn0 10241	. . . . . . . 8 |- 0 e. NN0
31		ifcl 3777	. . . . . . . 8 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. NN0 )
32	29, 30, 31	sylancl 645	. . . . . . 7 |- ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. NN0 )
33	32	nn0cnd 10281	. . . . . 6 |- ( ph -> if ( N e. ( A sadd B ) , ( 2 ^ N ) , 0 ) e. CC )
34		1nn0 10242	. . . . . . . . . . 11 |- 1 e. NN0
35	34	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. NN0 )
36	28, 35	nn0addcld 10283	. . . . . . . . 9 |- ( ph -> ( N + 1 ) e. NN0 )
37	27, 36	nn0expcld 11550	. . . . . . . 8 |- ( ph -> ( 2 ^ ( N + 1 ) ) e. NN0 )
38		ifcl 3777	. . . . . . . 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 645	. . . . . . 7 |- ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. NN0 )
40	39	nn0cnd 10281	. . . . . 6 |- ( ph -> if ( (/) e. ( C ` ( N + 1 ) ) , ( 2 ^ ( N + 1 ) ) , 0 ) e. CC )
41	33, 40	addcld 9112	. . . . 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 9112	. . . 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 3563	. . . . . . . . . 10 |- ( A i^i ( 0..^ N ) ) C_ A
44	43, 2	syl5ss 3361	. . . . . . . . 9 |- ( ph -> ( A i^i ( 0..^ N ) ) C_ NN0 )
45		inss2 3564	. . . . . . . . . 10 |- ( A i^i ( 0..^ N ) ) C_ ( 0..^ N )
46		ssfi 7332	. . . . . . . . . 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 645	. . . . . . . . 9 |- ( ph -> ( A i^i ( 0..^ N ) ) e. Fin )
48		elfpw 7411	. . . . . . . . 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 647	. . . . . . . 8 |- ( ph -> ( A i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
50	22	ffvelrni 5872	. . . . . . . 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 10281	. . . . . 6 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. CC )
53		inss1 3563	. . . . . . . . . 10 |- ( B i^i ( 0..^ N ) ) C_ B
54	53, 3	syl5ss 3361	. . . . . . . . 9 |- ( ph -> ( B i^i ( 0..^ N ) ) C_ NN0 )
55		inss2 3564	. . . . . . . . . 10 |- ( B i^i ( 0..^ N ) ) C_ ( 0..^ N )
56		ssfi 7332	. . . . . . . . . 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 645	. . . . . . . . 9 |- ( ph -> ( B i^i ( 0..^ N ) ) e. Fin )
58		elfpw 7411	. . . . . . . . 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 647	. . . . . . . 8 |- ( ph -> ( B i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
60	22	ffvelrni 5872	. . . . . . . 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 10281	. . . . . 6 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. CC )
63	52, 62	addcld 9112	. . . . 5 |- ( ph -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. CC )
64		ifcl 3777	. . . . . . . 8 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
65	29, 30, 64	sylancl 645	. . . . . . 7 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
66	65	nn0cnd 10281	. . . . . 6 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. CC )
67		ifcl 3777	. . . . . . . 8 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
68	29, 30, 67	sylancl 645	. . . . . . 7 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
69	68	nn0cnd 10281	. . . . . 6 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. CC )
70	66, 69	addcld 9112	. . . . 5 |- ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. CC )
71	63, 70	addcld 9112	. . . 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 10281	. . . . . 6 |- ( ph -> ( 2 ^ N ) e. CC )
73	72	adantr 453	. . . . 5 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( 2 ^ N ) e. CC )
74		0cn 9089	. . . . . 6 |- 0 e. CC
75	74	a1i 11	. . . . 5 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> 0 e. CC )
76	73, 75	ifclda 3768	. . . 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 12973	. . . . . . . . 9 |- ( ph -> ( N e. ( A sadd B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
79	78	ifbid 3759	. . . . . . . 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 12972	. . . . . . . . 9 |- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
81	27	nn0cnd 10281	. . . . . . . . . . 11 |- ( ph -> 2 e. CC )
82	81, 28	expp1d 11529	. . . . . . . . . 10 |- ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
83	72, 81	mulcomd 9114	. . . . . . . . . 10 |- ( ph -> ( ( 2 ^ N ) x. 2 ) = ( 2 x. ( 2 ^ N ) ) )
84	82, 83	eqtrd 2470	. . . . . . . . 9 |- ( ph -> ( 2 ^ ( N + 1 ) ) = ( 2 x. ( 2 ^ N ) ) )
85		eqidd 2439	. . . . . . . . 9 |- ( ph -> 0 = 0 )
86	80, 84, 85	ifbieq12d 3763	. . . . . . . 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 6102	. . . . . . 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 12967	. . . . . . . 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 2470	. . . . . 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 6102	. . . . 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 9293	. . . . 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 9115	. . . . 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 2480	. . . 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 9277	. . 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 9115	. . 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 9294	. . 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 2480	. 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 12966	. . . 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 644	. . 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 6099	. 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 12966	. . . 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 644	. . 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 12966	. . . 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 644	. . 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 6102	. 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 2480	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 360  haddwhad 1388  caddwcad 1389   = wceq 1653   e. wcel 1726   {crab 2711   i^i cin 3321   C_ wss 3322   (/)c0 3630   ifcif 3741   ~Pcpw 3801   e. cmpt 4269   `'ccnv 4880   |` cres 4883   -->wf 5453   -1-1-onto->wf1o 5456   ` cfv 5457  (class class class)co 6084   e. cmpt2 6086   1oc1o 6720   2oc2o 6721   Fincfn 7112   CCcc 8993   0cc0 8995   1c1 8996   + caddc 8998   x. cmul 9000   - cmin 9296   2c2 10054   NN0cn0 10226  ..^cfzo 11140   seq cseq 11328   ^cexp 11387  bitscbits 12936   sadd csad 12937

This theorem is referenced by:  sadadd2  12977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-xor 1315  df-tru 1329  df-had 1390  df-cad 1391  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-disj 4186  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-pm 7024  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-sup 7449  df-oi 7482  df-card 7831  df-cda 8053  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-div 9683  df-nn 10006  df-2 10063  df-3 10064  df-n0 10227  df-z 10288  df-uz 10494  df-rp 10618  df-fz 11049  df-fzo 11141  df-fl 11207  df-mod 11256  df-seq 11329  df-exp 11388  df-hash 11624  df-cj 11909  df-re 11910  df-im 11911  df-sqr 12045  df-abs 12046  df-clim 12287  df-sum 12485  df-dvds 12858  df-bits 12939  df-sad 12968