Metamath Proof Explorer

Theorem sadadd3

Description: Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses sadval.a 
|- ( ph -> A C_ NN0 )
sadval.b 
|- ( ph -> B C_ NN0 )
sadval.c 
|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
sadcp1.n 
|- ( ph -> N e. NN0 )
sadcadd.k 
|- K = `' ( bits |` NN0 )
Assertion sadadd3 
|- ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )

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 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( ph -> 2 e. NN )
8 7 4 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
9 8 nnzd 
 |-  ( ph -> ( 2 ^ N ) e. ZZ )
10 iddvds 
 |-  ( ( 2 ^ N ) e. ZZ -> ( 2 ^ N ) || ( 2 ^ N ) )
11 9 10 syl 
 |-  ( ph -> ( 2 ^ N ) || ( 2 ^ N ) )
12 dvds0 
 |-  ( ( 2 ^ N ) e. ZZ -> ( 2 ^ N ) || 0 )
13 9 12 syl 
 |-  ( ph -> ( 2 ^ N ) || 0 )
14 breq2 
 |-  ( ( 2 ^ N ) = if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) -> ( ( 2 ^ N ) || ( 2 ^ N ) <-> ( 2 ^ N ) || if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
15 breq2 
 |-  ( 0 = if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) -> ( ( 2 ^ N ) || 0 <-> ( 2 ^ N ) || if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) )
16 14 15 ifboth 
 |-  ( ( ( 2 ^ N ) || ( 2 ^ N ) /\ ( 2 ^ N ) || 0 ) -> ( 2 ^ N ) || if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) )
17 11 13 16 syl2anc 
 |-  ( ph -> ( 2 ^ N ) || if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) )
18 inss1 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( A sadd B )
19 1 2 3 sadfval 
 |-  ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
20 ssrab2 
 |-  { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } C_ NN0
21 19 20 eqsstrdi 
 |-  ( ph -> ( A sadd B ) C_ NN0 )
22 18 21 sstrid 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 )
23 fzofi 
 |-  ( 0 ..^ N ) e. Fin
24 23 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
25 inss2 
 |-  ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
26 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
27 24 25 26 sylancl 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin )
28 elfpw 
 |-  ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) C_ NN0 /\ ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. Fin ) )
29 22 27 28 sylanbrc 
 |-  ( ph -> ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
30 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
31 f1ocnv 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
32 f1of 
 |-  ( `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 -> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
33 30 31 32 mp2b 
 |-  `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0
34 5 feq1i 
 |-  ( K : ( ~P NN0 i^i Fin ) --> NN0 <-> `' ( bits |` NN0 ) : ( ~P NN0 i^i Fin ) --> NN0 )
35 33 34 mpbir 
 |-  K : ( ~P NN0 i^i Fin ) --> NN0
36 35 ffvelrni 
 |-  ( ( ( A sadd B ) i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
37 29 36 syl 
 |-  ( ph -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. NN0 )
38 37 nn0cnd 
 |-  ( ph -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. CC )
39 8 nncnd 
 |-  ( ph -> ( 2 ^ N ) e. CC )
40 0cn 
 |-  0 e. CC
41 ifcl 
 |-  ( ( ( 2 ^ N ) e. CC /\ 0 e. CC ) -> if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) e. CC )
42 39 40 41 sylancl 
 |-  ( ph -> if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) e. CC )
43 38 42 pncan2d 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) - ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) = if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) )
44 17 43 breqtrrd 
 |-  ( ph -> ( 2 ^ N ) || ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) - ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) )
45 37 nn0zd 
 |-  ( ph -> ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ZZ )
46 9 adantr 
 |-  ( ( ph /\ (/) e. ( C ` N ) ) -> ( 2 ^ N ) e. ZZ )
47 0zd 
 |-  ( ( ph /\ -. (/) e. ( C ` N ) ) -> 0 e. ZZ )
48 46 47 ifclda 
 |-  ( ph -> if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) e. ZZ )
49 45 48 zaddcld 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) e. ZZ )
50 moddvds 
 |-  ( ( ( 2 ^ N ) e. NN /\ ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) e. ZZ /\ ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) e. ZZ ) -> ( ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) mod ( 2 ^ N ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) <-> ( 2 ^ N ) || ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) - ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) ) )
51 8 49 45 50 syl3anc 
 |-  ( ph -> ( ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) mod ( 2 ^ N ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) <-> ( 2 ^ N ) || ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) - ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) ) ) )
52 44 51 mpbird 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) mod ( 2 ^ N ) ) = ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) )
53 1 2 3 4 5 sadadd2 
 |-  ( 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 ) ) ) ) )
54 53 oveq1d 
 |-  ( ph -> ( ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) + if ( (/) e. ( C ` N ) , ( 2 ^ N ) , 0 ) ) mod ( 2 ^ N ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )
55 52 54 eqtr3d 
 |-  ( ph -> ( ( K ` ( ( A sadd B ) i^i ( 0 ..^ N ) ) ) mod ( 2 ^ N ) ) = ( ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) mod ( 2 ^ N ) ) )