Metamath Proof Explorer

Theorem sadcaddlem

Description: Lemma for sadcadd . (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 )
sadcaddlem.1 
|- ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )
Assertion sadcaddlem 
|- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( 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 sadcaddlem.1 
 |-  ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )
7 cad1 
 |-  ( (/) e. ( C ` N ) -> ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A \/ N e. B ) ) )
8 7 adantl 
 |-  ( ( ph /\ (/) e. ( C ` N ) ) -> ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A \/ N e. B ) ) )
9 2nn 
 |-  2 e. NN
10 9 a1i 
 |-  ( ph -> 2 e. NN )
11 10 4 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
12 11 nnred 
 |-  ( ph -> ( 2 ^ N ) e. RR )
13 12 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( 2 ^ N ) e. RR )
14 inss1 
 |-  ( A i^i ( 0 ..^ N ) ) C_ A
15 14 1 sstrid 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
16 fzofi 
 |-  ( 0 ..^ N ) e. Fin
17 16 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
18 inss2 
 |-  ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
19 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( A i^i ( 0 ..^ N ) ) e. Fin )
20 17 18 19 sylancl 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) e. Fin )
21 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 ) )
22 15 20 21 sylanbrc 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
23 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
24 f1ocnv 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
25 23 24 ax-mp 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
26 f1oeq1 
 |-  ( K = `' ( bits |` NN0 ) -> ( K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 <-> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 ) )
27 5 26 ax-mp 
 |-  ( K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 <-> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
28 25 27 mpbir 
 |-  K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
29 f1of 
 |-  ( K : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> K : ( ~P NN0 i^i Fin ) --> NN0 )
30 28 29 ax-mp 
 |-  K : ( ~P NN0 i^i Fin ) --> NN0
31 30 ffvelrni 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. NN0 )
32 22 31 syl 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. NN0 )
33 inss1 
 |-  ( B i^i ( 0 ..^ N ) ) C_ B
34 33 2 sstrid 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
35 inss2 
 |-  ( B i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
36 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( B i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( B i^i ( 0 ..^ N ) ) e. Fin )
37 17 35 36 sylancl 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) e. Fin )
38 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 ) )
39 34 37 38 sylanbrc 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
40 30 ffvelrni 
 |-  ( ( B i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. NN0 )
41 39 40 syl 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. NN0 )
42 32 41 nn0addcld 
 |-  ( ph -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) e. NN0 )
43 42 nn0red 
 |-  ( ph -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) e. RR )
44 43 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) e. RR )
45 2nn0 
 |-  2 e. NN0
46 45 a1i 
 |-  ( ( ph /\ N e. A ) -> 2 e. NN0 )
47 4 adantr 
 |-  ( ( ph /\ N e. A ) -> N e. NN0 )
48 46 47 nn0expcld 
 |-  ( ( ph /\ N e. A ) -> ( 2 ^ N ) e. NN0 )
49 0nn0 
 |-  0 e. NN0
50 49 a1i 
 |-  ( ( ph /\ -. N e. A ) -> 0 e. NN0 )
51 48 50 ifclda 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
52 45 a1i 
 |-  ( ( ph /\ N e. B ) -> 2 e. NN0 )
53 4 adantr 
 |-  ( ( ph /\ N e. B ) -> N e. NN0 )
54 52 53 nn0expcld 
 |-  ( ( ph /\ N e. B ) -> ( 2 ^ N ) e. NN0 )
55 49 a1i 
 |-  ( ( ph /\ -. N e. B ) -> 0 e. NN0 )
56 54 55 ifclda 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
57 51 56 nn0addcld 
 |-  ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. NN0 )
58 57 nn0red 
 |-  ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. RR )
59 58 ad2antrr 
 |-  ( ( ( 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 )
60 6 biimpa 
 |-  ( ( ph /\ (/) e. ( C ` N ) ) -> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )
61 60 adantr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( N e. A \/ N e. B ) ) -> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )
62 11 nnnn0d 
 |-  ( ph -> ( 2 ^ N ) e. NN0 )
63 ifcl 
 |-  ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
64 62 49 63 sylancl 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. NN0 )
65 64 nn0ge0d 
 |-  ( ph -> 0 <_ if ( N e. B , ( 2 ^ N ) , 0 ) )
66 12 adantr 
 |-  ( ( ph /\ N e. B ) -> ( 2 ^ N ) e. RR )
67 0red 
 |-  ( ( ph /\ -. N e. B ) -> 0 e. RR )
68 66 67 ifclda 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. RR )
69 12 68 addge01d 
 |-  ( ph -> ( 0 <_ if ( N e. B , ( 2 ^ N ) , 0 ) <-> ( 2 ^ N ) <_ ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) ) )
70 65 69 mpbid 
 |-  ( ph -> ( 2 ^ N ) <_ ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
71 70 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. A ) -> ( 2 ^ N ) <_ ( ( 2 ^ N ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
72 iftrue 
 |-  ( N e. A -> if ( N e. A , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
73 72 adantl 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. A ) -> if ( N e. A , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
74 73 oveq1d 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 2 ^ N ) e. NN0 /\ 0 e. NN0 ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
77 62 49 76 sylancl 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. NN0 )
78 77 nn0ge0d 
 |-  ( ph -> 0 <_ if ( N e. A , ( 2 ^ N ) , 0 ) )
79 12 adantr 
 |-  ( ( ph /\ N e. A ) -> ( 2 ^ N ) e. RR )
80 0red 
 |-  ( ( ph /\ -. N e. A ) -> 0 e. RR )
81 79 80 ifclda 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. RR )
82 12 81 addge02d 
 |-  ( ph -> ( 0 <_ if ( N e. A , ( 2 ^ N ) , 0 ) <-> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) ) )
83 78 82 mpbid 
 |-  ( ph -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) )
84 83 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. B ) -> ( 2 ^ N ) <_ ( if ( N e. A , ( 2 ^ N ) , 0 ) + ( 2 ^ N ) ) )
85 iftrue 
 |-  ( N e. B -> if ( N e. B , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
86 85 adantl 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ N e. B ) -> if ( N e. B , ( 2 ^ N ) , 0 ) = ( 2 ^ N ) )
87 86 oveq2d 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 13 13 44 59 61 89 le2addd 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( -. ( N e. A \/ N e. B ) <-> ( -. N e. A /\ -. N e. B ) )
93 iffalse 
 |-  ( -. N e. A -> if ( N e. A , ( 2 ^ N ) , 0 ) = 0 )
94 93 ad2antrl 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. A , ( 2 ^ N ) , 0 ) = 0 )
95 iffalse 
 |-  ( -. N e. B -> if ( N e. B , ( 2 ^ N ) , 0 ) = 0 )
96 95 ad2antll 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. B , ( 2 ^ N ) , 0 ) = 0 )
97 94 96 oveq12d 
 |-  ( ( ( 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 
 |-  ( 0 + 0 ) = 0
99 97 98 eqtrdi 
 |-  ( ( ( 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 
 |-  ( ( ( 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 32 nn0red 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. RR )
102 101 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. RR )
103 41 nn0red 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. RR )
104 103 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. RR )
105 102 104 readdcld 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 5 fveq1i 
 |-  ( K ` ( A i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) )
110 109 fveq2i 
 |-  ( ( bits |` NN0 ) ` ( K ` ( A i^i ( 0 ..^ N ) ) ) ) = ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) )
111 32 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( K ` ( A i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( K ` ( A i^i ( 0 ..^ N ) ) ) ) )
112 f1ocnvfv2 
 |-  ( ( ( 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 ) ) )
113 23 22 112 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( A i^i ( 0 ..^ N ) ) ) ) = ( A i^i ( 0 ..^ N ) ) )
114 110 111 113 3eqtr3a 
 |-  ( ph -> ( bits ` ( K ` ( A i^i ( 0 ..^ N ) ) ) ) = ( A i^i ( 0 ..^ N ) ) )
115 114 18 eqsstrdi 
 |-  ( ph -> ( bits ` ( K ` ( A i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
116 32 nn0zd 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. ZZ )
117 bitsfzo 
 |-  ( ( ( 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 ) ) )
118 116 4 117 syl2anc 
 |-  ( ph -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( K ` ( A i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
119 115 118 mpbird 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
120 elfzolt2 
 |-  ( ( K ` ( A i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
121 119 120 syl 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
122 5 fveq1i 
 |-  ( K ` ( B i^i ( 0 ..^ N ) ) ) = ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) )
123 122 fveq2i 
 |-  ( ( bits |` NN0 ) ` ( K ` ( B i^i ( 0 ..^ N ) ) ) ) = ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) )
124 41 fvresd 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( K ` ( B i^i ( 0 ..^ N ) ) ) ) = ( bits ` ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )
125 f1ocnvfv2 
 |-  ( ( ( 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 ) ) )
126 23 39 125 sylancr 
 |-  ( ph -> ( ( bits |` NN0 ) ` ( `' ( bits |` NN0 ) ` ( B i^i ( 0 ..^ N ) ) ) ) = ( B i^i ( 0 ..^ N ) ) )
127 123 124 126 3eqtr3a 
 |-  ( ph -> ( bits ` ( K ` ( B i^i ( 0 ..^ N ) ) ) ) = ( B i^i ( 0 ..^ N ) ) )
128 127 35 eqsstrdi 
 |-  ( ph -> ( bits ` ( K ` ( B i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) )
129 41 nn0zd 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. ZZ )
130 bitsfzo 
 |-  ( ( ( 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 ) ) )
131 129 4 130 syl2anc 
 |-  ( ph -> ( ( K ` ( B i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` ( K ` ( B i^i ( 0 ..^ N ) ) ) ) C_ ( 0 ..^ N ) ) )
132 128 131 mpbird 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) )
133 elfzolt2 
 |-  ( ( K ` ( B i^i ( 0 ..^ N ) ) ) e. ( 0 ..^ ( 2 ^ N ) ) -> ( K ` ( B i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
134 132 133 syl 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) < ( 2 ^ N ) )
135 101 103 12 12 121 134 lt2addd 
 |-  ( ph -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) )
136 135 ad2antrr 
 |-  ( ( ( 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 ) ) )
137 108 136 eqbrtrd 
 |-  ( ( ( 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 ) ) )
138 81 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. A , ( 2 ^ N ) , 0 ) e. RR )
139 68 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> if ( N e. B , ( 2 ^ N ) , 0 ) e. RR )
140 138 139 readdcld 
 |-  ( ( ( 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 )
141 105 140 readdcld 
 |-  ( ( ( 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 )
142 12 ad2antrr 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( 2 ^ N ) e. RR )
143 142 142 readdcld 
 |-  ( ( ( ph /\ (/) e. ( C ` N ) ) /\ ( -. N e. A /\ -. N e. B ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR )
144 141 143 ltnled 
 |-  ( ( ( 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 ) ) ) ) )
145 137 144 mpbid 
 |-  ( ( ( 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 ) ) ) )
146 145 ex 
 |-  ( ( 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 ) ) ) ) )
147 92 146 syl5bi 
 |-  ( ( 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 91 147 impcon4bid 
 |-  ( ( 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 8 148 bitrd 
 |-  ( ( 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 ) ) ) ) )
150 cad0 
 |-  ( -. (/) e. ( C ` N ) -> ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A /\ N e. B ) ) )
151 150 adantl 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) <-> ( N e. A /\ N e. B ) ) )
152 42 nn0ge0d 
 |-  ( ph -> 0 <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )
153 12 12 readdcld 
 |-  ( ph -> ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR )
154 153 43 addge02d 
 |-  ( 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 ) ) ) ) )
155 152 154 mpbid 
 |-  ( ph -> ( ( 2 ^ N ) + ( 2 ^ N ) ) <_ ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( ( 2 ^ N ) + ( 2 ^ N ) ) ) )
156 155 ad2antrr 
 |-  ( ( ( 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 ) ) ) )
157 72 85 oveqan12d 
 |-  ( ( N e. A /\ N e. B ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
158 157 adantl 
 |-  ( ( ( 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 ) ) )
159 158 oveq2d 
 |-  ( ( ( 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 ) ) ) )
160 156 159 breqtrrd 
 |-  ( ( ( 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 ) ) ) )
161 160 ex 
 |-  ( ( 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 ) ) ) ) )
162 101 adantr 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. RR )
163 103 adantr 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. RR )
164 162 163 readdcld 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) e. RR )
165 12 adantr 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( 2 ^ N ) e. RR )
166 12 43 lenltd 
 |-  ( 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 ) ) )
167 6 166 bitrd 
 |-  ( ph -> ( (/) e. ( C ` N ) <-> -. ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) < ( 2 ^ N ) ) )
168 167 con2bid 
 |-  ( ph -> ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) < ( 2 ^ N ) <-> -. (/) e. ( C ` N ) ) )
169 168 biimpar 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) < ( 2 ^ N ) )
170 164 165 165 169 ltadd1dd 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( 2 ^ N ) ) < ( ( 2 ^ N ) + ( 2 ^ N ) ) )
171 164 165 readdcld 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) + ( 2 ^ N ) ) e. RR )
172 153 adantr 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( 2 ^ N ) + ( 2 ^ N ) ) e. RR )
173 43 58 readdcld 
 |-  ( 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 )
174 173 adantr 
 |-  ( ( 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 )
175 ltletr 
 |-  ( ( ( ( ( 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 ) ) ) ) )
176 171 172 174 175 syl3anc 
 |-  ( ( 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 ) ) ) ) )
177 170 176 mpand 
 |-  ( ( 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 ) ) ) ) )
178 58 adantr 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) e. RR )
179 43 adantr 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) e. RR )
180 165 178 179 ltadd2d 
 |-  ( ( 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 ) ) ) ) )
181 177 180 sylibrd 
 |-  ( ( 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 ) ) ) )
182 12 58 ltnled 
 |-  ( 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 ) ) )
183 64 nn0cnd 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) e. CC )
184 183 addid2d 
 |-  ( ph -> ( 0 + if ( N e. B , ( 2 ^ N ) , 0 ) ) = if ( N e. B , ( 2 ^ N ) , 0 ) )
185 12 leidd 
 |-  ( ph -> ( 2 ^ N ) <_ ( 2 ^ N ) )
186 62 nn0ge0d 
 |-  ( ph -> 0 <_ ( 2 ^ N ) )
187 breq1 
 |-  ( ( 2 ^ N ) = if ( N e. B , ( 2 ^ N ) , 0 ) -> ( ( 2 ^ N ) <_ ( 2 ^ N ) <-> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
188 breq1 
 |-  ( 0 = if ( N e. B , ( 2 ^ N ) , 0 ) -> ( 0 <_ ( 2 ^ N ) <-> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
189 187 188 ifboth 
 |-  ( ( ( 2 ^ N ) <_ ( 2 ^ N ) /\ 0 <_ ( 2 ^ N ) ) -> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
190 185 186 189 syl2anc 
 |-  ( ph -> if ( N e. B , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
191 184 190 eqbrtrd 
 |-  ( ph -> ( 0 + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) )
192 93 oveq1d 
 |-  ( -. 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 ) ) )
193 192 breq1d 
 |-  ( -. 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 ) ) )
194 191 193 syl5ibrcom 
 |-  ( ph -> ( -. N e. A -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) ) )
195 194 con1d 
 |-  ( ph -> ( -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) -> N e. A ) )
196 77 nn0cnd 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) e. CC )
197 196 addid1d 
 |-  ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + 0 ) = if ( N e. A , ( 2 ^ N ) , 0 ) )
198 breq1 
 |-  ( ( 2 ^ N ) = if ( N e. A , ( 2 ^ N ) , 0 ) -> ( ( 2 ^ N ) <_ ( 2 ^ N ) <-> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
199 breq1 
 |-  ( 0 = if ( N e. A , ( 2 ^ N ) , 0 ) -> ( 0 <_ ( 2 ^ N ) <-> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) ) )
200 198 199 ifboth 
 |-  ( ( ( 2 ^ N ) <_ ( 2 ^ N ) /\ 0 <_ ( 2 ^ N ) ) -> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
201 185 186 200 syl2anc 
 |-  ( ph -> if ( N e. A , ( 2 ^ N ) , 0 ) <_ ( 2 ^ N ) )
202 197 201 eqbrtrd 
 |-  ( ph -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + 0 ) <_ ( 2 ^ N ) )
203 95 oveq2d 
 |-  ( -. 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 ) )
204 203 breq1d 
 |-  ( -. 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 ) ) )
205 202 204 syl5ibrcom 
 |-  ( ph -> ( -. N e. B -> ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) ) )
206 205 con1d 
 |-  ( ph -> ( -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) -> N e. B ) )
207 195 206 jcad 
 |-  ( ph -> ( -. ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) <_ ( 2 ^ N ) -> ( N e. A /\ N e. B ) ) )
208 182 207 sylbid 
 |-  ( ph -> ( ( 2 ^ N ) < ( if ( N e. A , ( 2 ^ N ) , 0 ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) -> ( N e. A /\ N e. B ) ) )
209 208 adantr 
 |-  ( ( 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 ) ) )
210 181 209 syld 
 |-  ( ( 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 ) ) )
211 161 210 impbid 
 |-  ( ( 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 ) ) ) ) )
212 151 211 bitrd 
 |-  ( ( 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 ) ) ) ) )
213 149 212 pm2.61dan 
 |-  ( 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 ) ) ) ) )
214 1 2 3 4 sadcp1 
 |-  ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
215 2cnd 
 |-  ( ph -> 2 e. CC )
216 215 4 expp1d 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
217 11 nncnd 
 |-  ( ph -> ( 2 ^ N ) e. CC )
218 217 times2d 
 |-  ( ph -> ( ( 2 ^ N ) x. 2 ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
219 216 218 eqtrd 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) + ( 2 ^ N ) ) )
220 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 ) ) )
221 1 4 220 syl2anc 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )
222 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 ) ) )
223 2 4 222 syl2anc 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( B i^i ( 0 ..^ N ) ) ) + if ( N e. B , ( 2 ^ N ) , 0 ) ) )
224 221 223 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 ) ) ) )
225 32 nn0cnd 
 |-  ( ph -> ( K ` ( A i^i ( 0 ..^ N ) ) ) e. CC )
226 41 nn0cnd 
 |-  ( ph -> ( K ` ( B i^i ( 0 ..^ N ) ) ) e. CC )
227 225 196 226 183 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 ) ) ) )
228 224 227 eqtrd 
 |-  ( 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 ) ) ) )
229 219 228 breq12d 
 |-  ( 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 ) ) ) ) )
230 213 214 229 3bitr4d 
 |-  ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( N + 1 ) ) ) ) ) ) )