Theorem sadcaddlem 12924

Description: Lemma for sadcadd 12925. (Contributed by Mario Carneiro, 8-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 )
sadcaddlem.1	|- ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) ) )

Assertion

Ref	Expression
sadcaddlem	|- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( 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 sadcaddlem

Step	Hyp	Ref	Expression
1		cad1 1404	. . . . 5 |- ( (/) e. ( C ` N ) -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A \/ N e. B ) ) )
2	1	adantl 453	. . . 4 |- ( ( ph /\ (/) e. ( C ` N ) ) -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A \/ N e. B ) ) )
3		2nn 10089	. . . . . . . . . . 11 |- 2 e. NN
4	3	a1i 11	. . . . . . . . . 10 |- ( ph -> 2 e. NN )
5		sadcp1.n	. . . . . . . . . 10 |- ( ph -> N e. NN0 )
6	4, 5	nnexpcld 11499	. . . . . . . . 9 |- ( ph -> ( 2 ^ N ) e. NN )
7	6	nnred 9971	. . . . . . . 8 |- ( ph -> ( 2 ^ N ) e. RR )
8	7	ad2antrr 707	. . . . . . 7 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( 2 ^ N ) e. RR )
9		inss1 3521	. . . . . . . . . . . . 13 |- ( A i^i ( 0..^ N ) ) C_ A
10		sadval.a	. . . . . . . . . . . . 13 |- ( ph -> A C_ NN0 )
11	9, 10	syl5ss 3319	. . . . . . . . . . . 12 |- ( ph -> ( A i^i ( 0..^ N ) ) C_ NN0 )
12		fzofi 11268	. . . . . . . . . . . . . 14 |- ( 0..^ N ) e. Fin
13	12	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( 0..^ N ) e. Fin )
14		inss2 3522	. . . . . . . . . . . . 13 |- ( A i^i ( 0..^ N ) ) C_ ( 0..^ N )
15		ssfi 7288	. . . . . . . . . . . . 13 |- ( ( ( 0..^ N ) e. Fin /\ ( A i^i ( 0..^ N ) ) C_ ( 0..^ N ) ) -> ( A i^i ( 0..^ N ) ) e. Fin )
16	13, 14, 15	sylancl 644	. . . . . . . . . . . 12 |- ( ph -> ( A i^i ( 0..^ N ) ) e. Fin )
17		elfpw 7366	. . . . . . . . . . . 12 |- ( ( 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 ) )
18	11, 16, 17	sylanbrc 646	. . . . . . . . . . 11 |- ( ph -> ( A i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
19		bitsf1o 12912	. . . . . . . . . . . . . . 15 |- (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
20		f1ocnv 5646	. . . . . . . . . . . . . . 15 |- ( (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
21	19, 20	ax-mp 8	. . . . . . . . . . . . . 14 |- `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
22		sadcadd.k	. . . . . . . . . . . . . . 15 |- K = `' (bits |` NN0 )
23		f1oeq1 5624	. . . . . . . . . . . . . . 15 |- ( K = `' (bits |` NN0 ) -> ( K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 <-> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 ) )
24	22, 23	ax-mp 8	. . . . . . . . . . . . . 14 |- ( K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 <-> `' (bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
25	21, 24	mpbir 201	. . . . . . . . . . . . 13 |- K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
26		f1of 5633	. . . . . . . . . . . . 13 |- ( K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> K : ( ~P NN0 i^i Fin ) --> NN0 )
27	25, 26	ax-mp 8	. . . . . . . . . . . 12 |- K : ( ~P NN0 i^i Fin ) --> NN0
28	27	ffvelrni 5828	. . . . . . . . . . 11 |- ( ( A i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( A i^i ( 0..^ N ) ) ) e. NN0 )
29	18, 28	syl 16	. . . . . . . . . 10 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. NN0 )
30		inss1 3521	. . . . . . . . . . . . 13 |- ( B i^i ( 0..^ N ) ) C_ B
31		sadval.b	. . . . . . . . . . . . 13 |- ( ph -> B C_ NN0 )
32	30, 31	syl5ss 3319	. . . . . . . . . . . 12 |- ( ph -> ( B i^i ( 0..^ N ) ) C_ NN0 )
33		inss2 3522	. . . . . . . . . . . . 13 |- ( B i^i ( 0..^ N ) ) C_ ( 0..^ N )
34		ssfi 7288	. . . . . . . . . . . . 13 |- ( ( ( 0..^ N ) e. Fin /\ ( B i^i ( 0..^ N ) ) C_ ( 0..^ N ) ) -> ( B i^i ( 0..^ N ) ) e. Fin )
35	13, 33, 34	sylancl 644	. . . . . . . . . . . 12 |- ( ph -> ( B i^i ( 0..^ N ) ) e. Fin )
36		elfpw 7366	. . . . . . . . . . . 12 |- ( ( 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 ) )
37	32, 35, 36	sylanbrc 646	. . . . . . . . . . 11 |- ( ph -> ( B i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) )
38	27	ffvelrni 5828	. . . . . . . . . . 11 |- ( ( B i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( B i^i ( 0..^ N ) ) ) e. NN0 )
39	37, 38	syl 16	. . . . . . . . . 10 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. NN0 )
40	29, 39	nn0addcld 10234	. . . . . . . . 9 |- ( ph -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. NN0 )
41	40	nn0red 10231	. . . . . . . 8 |- ( ph -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. RR )
42	41	ad2antrr 707	. . . . . . 7 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. RR )
43		2nn0 10194	. . . . . . . . . . . . 13 |- 2 e. NN0
44	43	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ N e. A ) -> 2 e. NN0 )
45	5	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ N e. A ) -> N e. NN0 )
46	44, 45	nn0expcld 11500	. . . . . . . . . . 11 |- ( ( ph /\ N e. A ) -> ( 2 ^ N ) e. NN0 )
47		0nn0 10192	. . . . . . . . . . . 12 |- 0 e. NN0
48	47	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ -. N e. A ) -> 0 e. NN0 )
49	46, 48	ifclda 3726	. . . . . . . . . 10 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
50	43	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ N e. B ) -> 2 e. NN0 )
51	5	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ N e. B ) -> N e. NN0 )
52	50, 51	nn0expcld 11500	. . . . . . . . . . 11 |- ( ( ph /\ N e. B ) -> ( 2 ^ N ) e. NN0 )
53	47	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ -. N e. B ) -> 0 e. NN0 )
54	52, 53	ifclda 3726	. . . . . . . . . 10 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
55	49, 54	nn0addcld 10234	. . . . . . . . 9 |- ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. NN0 )
56	55	nn0red 10231	. . . . . . . 8 |- ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. RR )
57	56	ad2antrr 707	. . . . . . 7 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. RR )
58		sadcaddlem.1	. . . . . . . . 9 |- ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) ) )
59	58	biimpa 471	. . . . . . . 8 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) )
60	59	adantr 452	. . . . . . 7 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) )
61	6	nnnn0d 10230	. . . . . . . . . . . . 13 |- ( ph -> ( 2 ^ N ) e. NN0 )
62		ifcl 3735	. . . . . . . . . . . . 13 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
63	61, 47, 62	sylancl 644	. . . . . . . . . . . 12 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
64	63	nn0ge0d 10233	. . . . . . . . . . 11 |- ( ph -> 0 <_ if ( N e. B , ( 2 ^ N ) , 0 ) )
65	7	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ N e. B ) -> ( 2 ^ N ) e. RR )
66		0re 9047	. . . . . . . . . . . . . 14 |- 0 e. RR
67	66	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ -. N e. B ) -> 0 e. RR )
68	65, 67	ifclda 3726	. . . . . . . . . . . 12 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. RR )
69	7, 68	addge01d 9570	. . . . . . . . . . 11 |- ( ph -> ( 0 <_ if ( N e. B , ( 2 ^ N ) , 0 ) <-> ( 2 ^ N ) <_ ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
70	64, 69	mpbid 202	. . . . . . . . . 10 |- ( ph -> ( 2 ^ N ) <_ ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
71	70	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. A ) -> ( 2 ^ N ) <_ ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
72		iftrue 3705	. . . . . . . . . . 11 |- ( N e. A -> if ( N e. A , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
73	72	adantl 453	. . . . . . . . . 10 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. A ) -> if ( N e. A , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
74	73	oveq1d 6055	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. A ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
75	71, 74	breqtrrd 4198	. . . . . . . 8 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. A ) -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
76		ifcl 3735	. . . . . . . . . . . . 13 |- ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
77	61, 47, 76	sylancl 644	. . . . . . . . . . . 12 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
78	77	nn0ge0d 10233	. . . . . . . . . . 11 |- ( ph -> 0 <_ if ( N e. A , ( 2 ^ N ) , 0 ) )
79	7	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ N e. A ) -> ( 2 ^ N ) e. RR )
80	66	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ -. N e. A ) -> 0 e. RR )
81	79, 80	ifclda 3726	. . . . . . . . . . . 12 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. RR )
82	7, 81	addge02d 9571	. . . . . . . . . . 11 |- ( ph -> ( 0 <_ if ( N e. A , ( 2 ^ N ) , 0 ) <-> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) ) )
83	78, 82	mpbid 202	. . . . . . . . . 10 |- ( ph -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) )
84	83	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. B ) -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) )
85		iftrue 3705	. . . . . . . . . . 11 |- ( N e. B -> if ( N e. B , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
86	85	adantl 453	. . . . . . . . . 10 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. B ) -> if ( N e. B , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
87	86	oveq2d 6056	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. B ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) )
88	84, 87	breqtrrd 4198	. . . . . . . 8 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. B ) -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
89	75, 88	jaodan 761	. . . . . . 7 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
90	8, 8, 42, 57, 60, 89	le2addd 9600	. . . . . 6 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) )
91	90	ex 424	. . . . 5 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( ( N e. A \/ N e. B ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
92		ioran 477	. . . . . 6 |- ( -. ( N e. A \/ N e. B ) <-> ( -. N e. A /\ -. N e. B ) )
93		iffalse 3706	. . . . . . . . . . . . . 14 |- ( -. N e. A -> if ( N e. A , ( 2 ^ N ) , 0 ) = 0 )
94	93	ad2antrl 709	. . . . . . . . . . . . 13 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. A , ( 2 ^ N ) , 0 ) = 0 )
95		iffalse 3706	. . . . . . . . . . . . . 14 |- ( -. N e. B -> if ( N e. B , ( 2 ^ N ) , 0 ) = 0 )
96	95	ad2antll 710	. . . . . . . . . . . . 13 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. B , ( 2 ^ N ) , 0 ) = 0 )
97	94, 96	oveq12d 6058	. . . . . . . . . . . 12 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( 0 + 0 ) )
98		00id 9197	. . . . . . . . . . . 12 |- ( 0 + 0 ) = 0
99	97, 98	syl6eq 2452	. . . . . . . . . . 11 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = 0 )
100	99	oveq2d 6056	. . . . . . . . . 10 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( ( 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 ) ) ) = ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + 0 ) )
101	29	nn0red 10231	. . . . . . . . . . . . . 14 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. RR )
102	101	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( K ` ( A i^i ( 0..^ N ) ) ) e. RR )
103	39	nn0red 10231	. . . . . . . . . . . . . 14 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. RR )
104	103	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( K ` ( B i^i ( 0..^ N ) ) ) e. RR )
105	102, 104	readdcld 9071	. . . . . . . . . . . 12 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. RR )
106	105	recnd 9070	. . . . . . . . . . 11 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. CC )
107	106	addid1d 9222	. . . . . . . . . 10 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + 0 ) = ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) )
108	100, 107	eqtrd 2436	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( ( 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 ) ) ) = ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) )
109	22	fveq1i 5688	. . . . . . . . . . . . . . . 16 |- ( K ` ( A i^i ( 0..^ N ) ) ) = ( `' (bits |` NN0 ) ` ( A i^i ( 0..^ N ) ) )
110	109	fveq2i 5690	. . . . . . . . . . . . . . 15 |- ( (bits |` NN0 ) ` ( K ` ( A i^i ( 0..^ N ) ) ) ) = ( (bits |` NN0 ) ` ( `' (bits |` NN0 ) ` ( A i^i ( 0..^ N ) ) ) )
111		fvres 5704	. . . . . . . . . . . . . . . 16 |- ( ( K ` ( A i^i ( 0..^ N ) ) ) e. NN0 -> ( (bits |` NN0 ) ` ( K ` ( A i^i ( 0..^ N ) ) ) ) = (bits ` ( K ` ( A i^i ( 0..^ N ) ) ) ) )
112	29, 111	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( (bits |` NN0 ) ` ( K ` ( A i^i ( 0..^ N ) ) ) ) = (bits ` ( K ` ( A i^i ( 0..^ N ) ) ) ) )
113		f1ocnvfv2 5974	. . . . . . . . . . . . . . . 16 |- ( ( (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( A i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( (bits |` NN0 ) ` ( `' (bits |` NN0 ) ` ( A i^i ( 0..^ N ) ) ) ) = ( A i^i ( 0..^ N ) ) )
114	19, 18, 113	sylancr 645	. . . . . . . . . . . . . . 15 |- ( ph -> ( (bits |` NN0 ) ` ( `' (bits |` NN0 ) ` ( A i^i ( 0..^ N ) ) ) ) = ( A i^i ( 0..^ N ) ) )
115	110, 112, 114	3eqtr3a 2460	. . . . . . . . . . . . . 14 |- ( ph -> (bits ` ( K ` ( A i^i ( 0..^ N ) ) ) ) = ( A i^i ( 0..^ N ) ) )
116	115, 14	syl6eqss 3358	. . . . . . . . . . . . 13 |- ( ph -> (bits ` ( K ` ( A i^i ( 0..^ N ) ) ) ) C_ ( 0..^ N ) )
117	29	nn0zd 10329	. . . . . . . . . . . . . 14 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. ZZ )
118		bitsfzo 12902	. . . . . . . . . . . . . 14 |- ( ( ( K ` ( A i^i ( 0..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) <-> (bits ` ( K ` ( A i^i ( 0..^ N ) ) ) ) C_ ( 0..^ N ) ) )
119	117, 5, 118	syl2anc 643	. . . . . . . . . . . . 13 |- ( ph -> ( ( K ` ( A i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) <-> (bits ` ( K ` ( A i^i ( 0..^ N ) ) ) ) C_ ( 0..^ N ) ) )
120	116, 119	mpbird 224	. . . . . . . . . . . 12 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) )
121		elfzolt2 11103	. . . . . . . . . . . 12 |- ( ( K ` ( A i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) -> ( K ` ( A i^i ( 0..^ N ) ) ) < ( 2 ^ N ) )
122	120, 121	syl 16	. . . . . . . . . . 11 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) < ( 2 ^ N ) )
123	22	fveq1i 5688	. . . . . . . . . . . . . . . 16 |- ( K ` ( B i^i ( 0..^ N ) ) ) = ( `' (bits |` NN0 ) ` ( B i^i ( 0..^ N ) ) )
124	123	fveq2i 5690	. . . . . . . . . . . . . . 15 |- ( (bits |` NN0 ) ` ( K ` ( B i^i ( 0..^ N ) ) ) ) = ( (bits |` NN0 ) ` ( `' (bits |` NN0 ) ` ( B i^i ( 0..^ N ) ) ) )
125		fvres 5704	. . . . . . . . . . . . . . . 16 |- ( ( K ` ( B i^i ( 0..^ N ) ) ) e. NN0 -> ( (bits |` NN0 ) ` ( K ` ( B i^i ( 0..^ N ) ) ) ) = (bits ` ( K ` ( B i^i ( 0..^ N ) ) ) ) )
126	39, 125	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( (bits |` NN0 ) ` ( K ` ( B i^i ( 0..^ N ) ) ) ) = (bits ` ( K ` ( B i^i ( 0..^ N ) ) ) ) )
127		f1ocnvfv2 5974	. . . . . . . . . . . . . . . 16 |- ( ( (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ ( B i^i ( 0..^ N ) ) e. ( ~P NN0 i^i Fin ) ) -> ( (bits |` NN0 ) ` ( `' (bits |` NN0 ) ` ( B i^i ( 0..^ N ) ) ) ) = ( B i^i ( 0..^ N ) ) )
128	19, 37, 127	sylancr 645	. . . . . . . . . . . . . . 15 |- ( ph -> ( (bits |` NN0 ) ` ( `' (bits |` NN0 ) ` ( B i^i ( 0..^ N ) ) ) ) = ( B i^i ( 0..^ N ) ) )
129	124, 126, 128	3eqtr3a 2460	. . . . . . . . . . . . . 14 |- ( ph -> (bits ` ( K ` ( B i^i ( 0..^ N ) ) ) ) = ( B i^i ( 0..^ N ) ) )
130	129, 33	syl6eqss 3358	. . . . . . . . . . . . 13 |- ( ph -> (bits ` ( K ` ( B i^i ( 0..^ N ) ) ) ) C_ ( 0..^ N ) )
131	39	nn0zd 10329	. . . . . . . . . . . . . 14 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. ZZ )
132		bitsfzo 12902	. . . . . . . . . . . . . 14 |- ( ( ( K ` ( B i^i ( 0..^ N ) ) ) e. ZZ /\ N e. NN0 ) -> ( ( K ` ( B i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) <-> (bits ` ( K ` ( B i^i ( 0..^ N ) ) ) ) C_ ( 0..^ N ) ) )
133	131, 5, 132	syl2anc 643	. . . . . . . . . . . . 13 |- ( ph -> ( ( K ` ( B i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) <-> (bits ` ( K ` ( B i^i ( 0..^ N ) ) ) ) C_ ( 0..^ N ) ) )
134	130, 133	mpbird 224	. . . . . . . . . . . 12 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) )
135		elfzolt2 11103	. . . . . . . . . . . 12 |- ( ( K ` ( B i^i ( 0..^ N ) ) ) e. ( 0..^ ( 2 ^ N ) ) -> ( K ` ( B i^i ( 0..^ N ) ) ) < ( 2 ^ N ) )
136	134, 135	syl 16	. . . . . . . . . . 11 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) < ( 2 ^ N ) )
137	101, 103, 7, 7, 122, 136	lt2addd 9604	. . . . . . . . . 10 |- ( ph -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) )
138	137	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) )
139	108, 138	eqbrtrd 4192	. . . . . . . 8 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( ( 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 ) ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) )
140	81	ad2antrr 707	. . . . . . . . . . 11 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. RR )
141	68	ad2antrr 707	. . . . . . . . . . 11 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. RR )
142	140, 141	readdcld 9071	. . . . . . . . . 10 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. RR )
143	105, 142	readdcld 9071	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( ( 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. RR )
144	7	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( 2 ^ N ) e. RR )
145	144, 144	readdcld 9071	. . . . . . . . 9 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR )
146	143, 145	ltnled 9176	. . . . . . . 8 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( ( ( 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 ) ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) <-> -. ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
147	139, 146	mpbid 202	. . . . . . 7 |- ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> -. ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) )
148	147	ex 424	. . . . . 6 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( ( -. N e. A /\ -. N e. B ) -> -. ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
149	92, 148	syl5bi 209	. . . . 5 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( -. ( N e. A \/ N e. B ) -> -. ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
150	91, 149	impcon4bid 197	. . . 4 |- ( ( ph /\ (/) e. ( C ` N ) ) -> ( ( N e. A \/ N e. B ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
151	2, 150	bitrd 245	. . 3 |- ( ( ph /\ (/) e. ( C ` N ) ) -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
152		cad0 1406	. . . . 5 |- ( -. (/) e. ( C ` N ) -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A /\ N e. B ) ) )
153	152	adantl 453	. . . 4 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A /\ N e. B ) ) )
154	40	nn0ge0d 10233	. . . . . . . . 9 |- ( ph -> 0 <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) )
155	7, 7	readdcld 9071	. . . . . . . . . 10 |- ( ph -> ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR )
156	155, 41	addge02d 9571	. . . . . . . . 9 |- ( ph -> ( 0 <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( ( 2 ^ N ) + ( 2 ^ N ) ) ) ) )
157	154, 156	mpbid 202	. . . . . . . 8 |- ( ph -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( ( 2 ^ N ) + ( 2 ^ N ) ) ) )
158	157	ad2antrr 707	. . . . . . 7 |- ( ( ( ph /\ -. (/) e. ( C ` N ) ) /\ ( N e. A /\ N e. B ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( ( 2 ^ N ) + ( 2 ^ N ) ) ) )
159	72, 85	oveqan12d 6059	. . . . . . . . 9 |- ( ( N e. A /\ N e. B ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
160	159	adantl 453	. . . . . . . 8 |- ( ( ( ph /\ -. (/) e. ( C ` N ) ) /\ ( N e. A /\ N e. B ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
161	160	oveq2d 6056	. . . . . . 7 |- ( ( ( ph /\ -. (/) e. ( C ` N ) ) /\ ( N e. A /\ N e. B ) ) -> ( ( ( 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 ) ) ) = ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( ( 2 ^ N ) + ( 2 ^ N ) ) ) )
162	158, 161	breqtrrd 4198	. . . . . 6 |- ( ( ( ph /\ -. (/) e. ( C ` N ) ) /\ ( N e. A /\ N e. B ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) )
163	162	ex 424	. . . . 5 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( N e. A /\ N e. B ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
164	101	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( K ` ( A i^i ( 0..^ N ) ) ) e. RR )
165	103	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( K ` ( B i^i ( 0..^ N ) ) ) e. RR )
166	164, 165	readdcld 9071	. . . . . . . . 9 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. RR )
167	7	adantr 452	. . . . . . . . 9 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( 2 ^ N ) e. RR )
168	7, 41	lenltd 9175	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) <-> -. ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) < ( 2 ^ N ) ) )
169	58, 168	bitrd 245	. . . . . . . . . . 11 |- ( ph -> ( (/) e. ( C ` N ) <-> -. ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) < ( 2 ^ N ) ) )
170	169	con2bid 320	. . . . . . . . . 10 |- ( ph -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) < ( 2 ^ N ) <-> -. (/) e. ( C ` N ) ) )
171	170	biimpar 472	. . . . . . . . 9 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) < ( 2 ^ N ) )
172	166, 167, 167, 171	ltadd1dd 9593	. . . . . . . 8 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) )
173	166, 167	readdcld 9071	. . . . . . . . 9 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) e. RR )
174	155	adantr 452	. . . . . . . . 9 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR )
175	41, 56	readdcld 9071	. . . . . . . . . 10 |- ( 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. RR )
176	175	adantr 452	. . . . . . . . 9 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( 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. RR )
177		ltletr 9122	. . . . . . . . 9 |- ( ( ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) e. RR /\ ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR /\ ( ( ( 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. RR ) -> ( ( ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) /\ ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( ( 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 ) ) ) ) )
178	173, 174, 176, 177	syl3anc 1184	. . . . . . . 8 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) /\ ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( ( 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 ) ) ) ) )
179	172, 178	mpand 657	. . . . . . 7 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) -> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( ( 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 ) ) ) ) )
180	56	adantr 452	. . . . . . . 8 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. RR )
181	41	adantr 452	. . . . . . . 8 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) e. RR )
182	167, 180, 181	ltadd2d 9182	. . . . . . 7 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( 2 ^ N ) < ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <-> ( ( ( K ` ( A i^i ( 0..^ N ) ) ) + ( K ` ( B i^i ( 0..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( ( 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 ) ) ) ) )
183	179, 182	sylibrd 226	. . . . . 6 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) -> ( 2 ^ N ) < ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
184	7, 56	ltnled 9176	. . . . . . . 8 |- ( ph -> ( ( 2 ^ N ) < ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <-> -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) ) )
185	63	nn0cnd 10232	. . . . . . . . . . . . 13 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. CC )
186	185	addid2d 9223	. . . . . . . . . . . 12 |- ( ph -> ( 0 + if ( N e. B , ( 2 ^ N ) , 0 ) ) = if ( N e. B , ( 2 ^ N ) , 0 ) )
187	7	leidd 9549	. . . . . . . . . . . . 13 |- ( ph -> ( 2 ^ N ) <_ ( 2 ^ N ) )
188	61	nn0ge0d 10233	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ ( 2 ^ N ) )
189		breq1 4175	. . . . . . . . . . . . . 14 |- ( ( 2 ^ N ) = if ( N e. B , ( 2 ^ N ) , 0 ) -> ( ( 2 ^ N ) <_ ( 2 ^ N ) <-> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
190		breq1 4175	. . . . . . . . . . . . . 14 |- ( 0 = if ( N e. B , ( 2 ^ N ) , 0 ) -> ( 0 <_ ( 2 ^ N ) <-> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
191	189, 190	ifboth 3730	. . . . . . . . . . . . 13 |- ( ( ( 2 ^ N ) <_ ( 2 ^ N ) /\ 0 <_ ( 2 ^ N ) ) -> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
192	187, 188, 191	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
193	186, 192	eqbrtrd 4192	. . . . . . . . . . 11 |- ( ph -> ( 0 + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) )
194	93	oveq1d 6055	. . . . . . . . . . . 12 |- ( -. N e. A -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( 0 + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
195	194	breq1d 4182	. . . . . . . . . . 11 |- ( -. N e. A -> ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) <-> ( 0 + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) ) )
196	193, 195	syl5ibrcom 214	. . . . . . . . . 10 |- ( ph -> ( -. N e. A -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) ) )
197	196	con1d 118	. . . . . . . . 9 |- ( ph -> ( -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) -> N e. A ) )
198	77	nn0cnd 10232	. . . . . . . . . . . . 13 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. CC )
199	198	addid1d 9222	. . . . . . . . . . . 12 |- ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + 0 ) = if ( N e. A , ( 2 ^ N ) , 0 ) )
200		breq1 4175	. . . . . . . . . . . . . 14 |- ( ( 2 ^ N ) = if ( N e. A , ( 2 ^ N ) , 0 ) -> ( ( 2 ^ N ) <_ ( 2 ^ N ) <-> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
201		breq1 4175	. . . . . . . . . . . . . 14 |- ( 0 = if ( N e. A , ( 2 ^ N ) , 0 ) -> ( 0 <_ ( 2 ^ N ) <-> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
202	200, 201	ifboth 3730	. . . . . . . . . . . . 13 |- ( ( ( 2 ^ N ) <_ ( 2 ^ N ) /\ 0 <_ ( 2 ^ N ) ) -> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
203	187, 188, 202	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
204	199, 203	eqbrtrd 4192	. . . . . . . . . . 11 |- ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + 0 ) <_ ( 2 ^ N ) )
205	95	oveq2d 6056	. . . . . . . . . . . 12 |- ( -. N e. B -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( if ( N e. A , ( 2 ^ N ) , 0 ) + 0 ) )
206	205	breq1d 4182	. . . . . . . . . . 11 |- ( -. N e. B -> ( ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) <-> ( if ( N e. A , ( 2 ^ N ) , 0 ) + 0 ) <_ ( 2 ^ N ) ) )
207	204, 206	syl5ibrcom 214	. . . . . . . . . 10 |- ( ph -> ( -. N e. B -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) ) )
208	207	con1d 118	. . . . . . . . 9 |- ( ph -> ( -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) -> N e. B ) )
209	197, 208	jcad 520	. . . . . . . 8 |- ( ph -> ( -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) -> ( N e. A /\ N e. B ) ) )
210	184, 209	sylbid 207	. . . . . . 7 |- ( ph -> ( ( 2 ^ N ) < ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) -> ( N e. A /\ N e. B ) ) )
211	210	adantr 452	. . . . . 6 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( 2 ^ N ) < ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) -> ( N e. A /\ N e. B ) ) )
212	183, 211	syld 42	. . . . 5 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) -> ( N e. A /\ N e. B ) ) )
213	163, 212	impbid 184	. . . 4 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( N e. A /\ N e. B ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
214	153, 213	bitrd 245	. . 3 |- ( ( ph /\ -. (/) e. ( C ` N ) ) -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
215	151, 214	pm2.61dan 767	. 2 |- ( ph -> (cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
216		sadval.c	. . 3 |- 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 ) ) ) )
217	10, 31, 216, 5	sadcp1 12922	. 2 |- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
218	4	nncnd 9972	. . . . 5 |- ( ph -> 2 e. CC )
219	218, 5	expp1d 11479	. . . 4 |- ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
220	6	nncnd 9972	. . . . 5 |- ( ph -> ( 2 ^ N ) e. CC )
221	220	times2d 10167	. . . 4 |- ( ph -> ( ( 2 ^ N ) x. 2 ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
222	219, 221	eqtrd 2436	. . 3 |- ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
223	22	bitsinvp1 12916	. . . . . 6 |- ( ( 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 ) ) )
224	10, 5, 223	syl2anc 643	. . . . 5 |- ( ph -> ( K ` ( A i^i ( 0..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )
225	22	bitsinvp1 12916	. . . . . 6 |- ( ( 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 ) ) )
226	31, 5, 225	syl2anc 643	. . . . 5 |- ( ph -> ( K ` ( B i^i ( 0..^ ( N + 1 ) ) ) ) = ( ( K ` ( B i^i ( 0..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
227	224, 226	oveq12d 6058	. . . 4 |- ( 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 ) ) ) )
228	29	nn0cnd 10232	. . . . 5 |- ( ph -> ( K ` ( A i^i ( 0..^ N ) ) ) e. CC )
229	39	nn0cnd 10232	. . . . 5 |- ( ph -> ( K ` ( B i^i ( 0..^ N ) ) ) e. CC )
230	228, 198, 229, 185	add4d 9245	. . . 4 |- ( 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 ) ) ) )
231	227, 230	eqtrd 2436	. . 3 |- ( ph -> ( ( K ` ( A i^i ( 0..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0..^ ( N + 1 ) ) ) ) ) = ( ( ( 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 ) ) ) )
232	222, 231	breq12d 4185	. 2 |- ( ph -> ( ( 2 ^ ( N + 1 ) ) <_ ( ( K ` ( A i^i ( 0..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0..^ ( N + 1 ) ) ) ) ) <-> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( 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 ) ) ) ) )
233	215, 217, 232	3bitr4d 277	1 |- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( K ` ( A i^i ( 0..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0..^ ( N + 1 ) ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359  caddwcad 1385   = wceq 1649   e. wcel 1721   i^i cin 3279   C_ wss 3280   (/)c0 3588   ifcif 3699   ~Pcpw 3759   class class class wbr 4172   e. cmpt 4226   `'ccnv 4836   |` cres 4839   -->wf 5409   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   e. cmpt2 6042   1oc1o 6676   2oc2o 6677   Fincfn 7068   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238  ..^cfzo 11090   seq cseq 11278   ^cexp 11337  bitscbits 12886

This theorem is referenced by:  sadcadd  12925

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 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

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-cad 1387  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-disj 4143  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-dvds 12808  df-bits 12889