Metamath Proof Explorer


Theorem sadeq

Description: Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses sadeq.a φA0
sadeq.b φB0
sadeq.n φN0
Assertion sadeq φAsaddB0..^N=A0..^NsaddB0..^N0..^N

Proof

Step Hyp Ref Expression
1 sadeq.a φA0
2 sadeq.b φB0
3 sadeq.n φN0
4 inass A0..^N0..^N=A0..^N0..^N
5 inidm 0..^N0..^N=0..^N
6 5 ineq2i A0..^N0..^N=A0..^N
7 4 6 eqtri A0..^N0..^N=A0..^N
8 7 fveq2i bits0-1A0..^N0..^N=bits0-1A0..^N
9 inass B0..^N0..^N=B0..^N0..^N
10 5 ineq2i B0..^N0..^N=B0..^N
11 9 10 eqtri B0..^N0..^N=B0..^N
12 11 fveq2i bits0-1B0..^N0..^N=bits0-1B0..^N
13 8 12 oveq12i bits0-1A0..^N0..^N+bits0-1B0..^N0..^N=bits0-1A0..^N+bits0-1B0..^N
14 13 oveq1i bits0-1A0..^N0..^N+bits0-1B0..^N0..^Nmod2N=bits0-1A0..^N+bits0-1B0..^Nmod2N
15 inss1 A0..^NA
16 15 1 sstrid φA0..^N0
17 inss1 B0..^NB
18 17 2 sstrid φB0..^N0
19 eqid seq0c2𝑜,m0ifcaddmA0..^NmB0..^Nc1𝑜n0ifn=0n1=seq0c2𝑜,m0ifcaddmA0..^NmB0..^Nc1𝑜n0ifn=0n1
20 eqid bits0-1=bits0-1
21 16 18 19 3 20 sadadd3 φbits0-1A0..^NsaddB0..^N0..^Nmod2N=bits0-1A0..^N0..^N+bits0-1B0..^N0..^Nmod2N
22 eqid seq0c2𝑜,m0ifcaddmAmBc1𝑜n0ifn=0n1=seq0c2𝑜,m0ifcaddmAmBc1𝑜n0ifn=0n1
23 1 2 22 3 20 sadadd3 φbits0-1AsaddB0..^Nmod2N=bits0-1A0..^N+bits0-1B0..^Nmod2N
24 14 21 23 3eqtr4a φbits0-1A0..^NsaddB0..^N0..^Nmod2N=bits0-1AsaddB0..^Nmod2N
25 inss1 A0..^NsaddB0..^N0..^NA0..^NsaddB0..^N
26 sadcl A0..^N0B0..^N0A0..^NsaddB0..^N0
27 16 18 26 syl2anc φA0..^NsaddB0..^N0
28 25 27 sstrid φA0..^NsaddB0..^N0..^N0
29 fzofi 0..^NFin
30 29 a1i φ0..^NFin
31 inss2 A0..^NsaddB0..^N0..^N0..^N
32 ssfi 0..^NFinA0..^NsaddB0..^N0..^N0..^NA0..^NsaddB0..^N0..^NFin
33 30 31 32 sylancl φA0..^NsaddB0..^N0..^NFin
34 elfpw A0..^NsaddB0..^N0..^N𝒫0FinA0..^NsaddB0..^N0..^N0A0..^NsaddB0..^N0..^NFin
35 28 33 34 sylanbrc φA0..^NsaddB0..^N0..^N𝒫0Fin
36 bitsf1o bits0:01-1 onto𝒫0Fin
37 f1ocnv bits0:01-1 onto𝒫0Finbits0-1:𝒫0Fin1-1 onto0
38 f1of bits0-1:𝒫0Fin1-1 onto0bits0-1:𝒫0Fin0
39 36 37 38 mp2b bits0-1:𝒫0Fin0
40 39 ffvelrni A0..^NsaddB0..^N0..^N𝒫0Finbits0-1A0..^NsaddB0..^N0..^N0
41 35 40 syl φbits0-1A0..^NsaddB0..^N0..^N0
42 41 nn0red φbits0-1A0..^NsaddB0..^N0..^N
43 2rp 2+
44 43 a1i φ2+
45 3 nn0zd φN
46 44 45 rpexpcld φ2N+
47 41 nn0ge0d φ0bits0-1A0..^NsaddB0..^N0..^N
48 41 fvresd φbits0bits0-1A0..^NsaddB0..^N0..^N=bitsbits0-1A0..^NsaddB0..^N0..^N
49 f1ocnvfv2 bits0:01-1 onto𝒫0FinA0..^NsaddB0..^N0..^N𝒫0Finbits0bits0-1A0..^NsaddB0..^N0..^N=A0..^NsaddB0..^N0..^N
50 36 35 49 sylancr φbits0bits0-1A0..^NsaddB0..^N0..^N=A0..^NsaddB0..^N0..^N
51 48 50 eqtr3d φbitsbits0-1A0..^NsaddB0..^N0..^N=A0..^NsaddB0..^N0..^N
52 51 31 eqsstrdi φbitsbits0-1A0..^NsaddB0..^N0..^N0..^N
53 41 nn0zd φbits0-1A0..^NsaddB0..^N0..^N
54 bitsfzo bits0-1A0..^NsaddB0..^N0..^NN0bits0-1A0..^NsaddB0..^N0..^N0..^2Nbitsbits0-1A0..^NsaddB0..^N0..^N0..^N
55 53 3 54 syl2anc φbits0-1A0..^NsaddB0..^N0..^N0..^2Nbitsbits0-1A0..^NsaddB0..^N0..^N0..^N
56 52 55 mpbird φbits0-1A0..^NsaddB0..^N0..^N0..^2N
57 elfzolt2 bits0-1A0..^NsaddB0..^N0..^N0..^2Nbits0-1A0..^NsaddB0..^N0..^N<2N
58 56 57 syl φbits0-1A0..^NsaddB0..^N0..^N<2N
59 modid bits0-1A0..^NsaddB0..^N0..^N2N+0bits0-1A0..^NsaddB0..^N0..^Nbits0-1A0..^NsaddB0..^N0..^N<2Nbits0-1A0..^NsaddB0..^N0..^Nmod2N=bits0-1A0..^NsaddB0..^N0..^N
60 42 46 47 58 59 syl22anc φbits0-1A0..^NsaddB0..^N0..^Nmod2N=bits0-1A0..^NsaddB0..^N0..^N
61 inss1 AsaddB0..^NAsaddB
62 sadcl A0B0AsaddB0
63 1 2 62 syl2anc φAsaddB0
64 61 63 sstrid φAsaddB0..^N0
65 inss2 AsaddB0..^N0..^N
66 ssfi 0..^NFinAsaddB0..^N0..^NAsaddB0..^NFin
67 30 65 66 sylancl φAsaddB0..^NFin
68 elfpw AsaddB0..^N𝒫0FinAsaddB0..^N0AsaddB0..^NFin
69 64 67 68 sylanbrc φAsaddB0..^N𝒫0Fin
70 39 ffvelrni AsaddB0..^N𝒫0Finbits0-1AsaddB0..^N0
71 69 70 syl φbits0-1AsaddB0..^N0
72 71 nn0red φbits0-1AsaddB0..^N
73 71 nn0ge0d φ0bits0-1AsaddB0..^N
74 71 fvresd φbits0bits0-1AsaddB0..^N=bitsbits0-1AsaddB0..^N
75 f1ocnvfv2 bits0:01-1 onto𝒫0FinAsaddB0..^N𝒫0Finbits0bits0-1AsaddB0..^N=AsaddB0..^N
76 36 69 75 sylancr φbits0bits0-1AsaddB0..^N=AsaddB0..^N
77 74 76 eqtr3d φbitsbits0-1AsaddB0..^N=AsaddB0..^N
78 77 65 eqsstrdi φbitsbits0-1AsaddB0..^N0..^N
79 71 nn0zd φbits0-1AsaddB0..^N
80 bitsfzo bits0-1AsaddB0..^NN0bits0-1AsaddB0..^N0..^2Nbitsbits0-1AsaddB0..^N0..^N
81 79 3 80 syl2anc φbits0-1AsaddB0..^N0..^2Nbitsbits0-1AsaddB0..^N0..^N
82 78 81 mpbird φbits0-1AsaddB0..^N0..^2N
83 elfzolt2 bits0-1AsaddB0..^N0..^2Nbits0-1AsaddB0..^N<2N
84 82 83 syl φbits0-1AsaddB0..^N<2N
85 modid bits0-1AsaddB0..^N2N+0bits0-1AsaddB0..^Nbits0-1AsaddB0..^N<2Nbits0-1AsaddB0..^Nmod2N=bits0-1AsaddB0..^N
86 72 46 73 84 85 syl22anc φbits0-1AsaddB0..^Nmod2N=bits0-1AsaddB0..^N
87 24 60 86 3eqtr3rd φbits0-1AsaddB0..^N=bits0-1A0..^NsaddB0..^N0..^N
88 f1of1 bits0-1:𝒫0Fin1-1 onto0bits0-1:𝒫0Fin1-10
89 36 37 88 mp2b bits0-1:𝒫0Fin1-10
90 f1fveq bits0-1:𝒫0Fin1-10AsaddB0..^N𝒫0FinA0..^NsaddB0..^N0..^N𝒫0Finbits0-1AsaddB0..^N=bits0-1A0..^NsaddB0..^N0..^NAsaddB0..^N=A0..^NsaddB0..^N0..^N
91 89 90 mpan AsaddB0..^N𝒫0FinA0..^NsaddB0..^N0..^N𝒫0Finbits0-1AsaddB0..^N=bits0-1A0..^NsaddB0..^N0..^NAsaddB0..^N=A0..^NsaddB0..^N0..^N
92 69 35 91 syl2anc φbits0-1AsaddB0..^N=bits0-1A0..^NsaddB0..^N0..^NAsaddB0..^N=A0..^NsaddB0..^N0..^N
93 87 92 mpbid φAsaddB0..^N=A0..^NsaddB0..^N0..^N