Step | Hyp | Ref
| Expression |
1 | | inss1 4189 |
. . . . . . . . 9
β’ ((π΄ sadd π΅) β© (0..^π)) β (π΄ sadd π΅) |
2 | | sadval.a |
. . . . . . . . . . 11
β’ (π β π΄ β
β0) |
3 | | sadval.b |
. . . . . . . . . . 11
β’ (π β π΅ β
β0) |
4 | | sadval.c |
. . . . . . . . . . 11
β’ πΆ = seq0((π β 2o, π β β0 β¦
if(cadd(π β π΄, π β π΅, β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β
1)))) |
5 | 2, 3, 4 | sadfval 16337 |
. . . . . . . . . 10
β’ (π β (π΄ sadd π΅) = {π β β0 β£
hadd(π β π΄, π β π΅, β
β (πΆβπ))}) |
6 | | ssrab2 4038 |
. . . . . . . . . 10
β’ {π β β0
β£ hadd(π β π΄, π β π΅, β
β (πΆβπ))} β
β0 |
7 | 5, 6 | eqsstrdi 3999 |
. . . . . . . . 9
β’ (π β (π΄ sadd π΅) β
β0) |
8 | 1, 7 | sstrid 3956 |
. . . . . . . 8
β’ (π β ((π΄ sadd π΅) β© (0..^π)) β
β0) |
9 | | fzofi 13885 |
. . . . . . . . . 10
β’
(0..^π) β
Fin |
10 | 9 | a1i 11 |
. . . . . . . . 9
β’ (π β (0..^π) β Fin) |
11 | | inss2 4190 |
. . . . . . . . 9
β’ ((π΄ sadd π΅) β© (0..^π)) β (0..^π) |
12 | | ssfi 9120 |
. . . . . . . . 9
β’
(((0..^π) β Fin
β§ ((π΄ sadd π΅) β© (0..^π)) β (0..^π)) β ((π΄ sadd π΅) β© (0..^π)) β Fin) |
13 | 10, 11, 12 | sylancl 587 |
. . . . . . . 8
β’ (π β ((π΄ sadd π΅) β© (0..^π)) β Fin) |
14 | | elfpw 9301 |
. . . . . . . 8
β’ (((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin) β (((π΄ sadd
π΅) β© (0..^π)) β β0
β§ ((π΄ sadd π΅) β© (0..^π)) β Fin)) |
15 | 8, 13, 14 | sylanbrc 584 |
. . . . . . 7
β’ (π β ((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin)) |
16 | | bitsf1o 16330 |
. . . . . . . . . 10
β’ (bits
βΎ β0):β0β1-1-ontoβ(π« β0 β©
Fin) |
17 | | f1ocnv 6797 |
. . . . . . . . . 10
β’ ((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1-ontoββ0) |
18 | | f1of 6785 |
. . . . . . . . . 10
β’ (β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1-ontoββ0 β β‘(bits βΎ
β0):(π« β0 β©
Fin)βΆβ0) |
19 | 16, 17, 18 | mp2b 10 |
. . . . . . . . 9
β’ β‘(bits βΎ
β0):(π« β0 β©
Fin)βΆβ0 |
20 | | sadcadd.k |
. . . . . . . . . 10
β’ πΎ = β‘(bits βΎ
β0) |
21 | 20 | feq1i 6660 |
. . . . . . . . 9
β’ (πΎ:(π« β0
β© Fin)βΆβ0 β β‘(bits βΎ
β0):(π« β0 β©
Fin)βΆβ0) |
22 | 19, 21 | mpbir 230 |
. . . . . . . 8
β’ πΎ:(π« β0
β© Fin)βΆβ0 |
23 | 22 | ffvelcdmi 7035 |
. . . . . . 7
β’ (((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin) β (πΎβ((π΄ sadd π΅) β© (0..^π))) β
β0) |
24 | 15, 23 | syl 17 |
. . . . . 6
β’ (π β (πΎβ((π΄ sadd π΅) β© (0..^π))) β
β0) |
25 | 24 | nn0cnd 12480 |
. . . . 5
β’ (π β (πΎβ((π΄ sadd π΅) β© (0..^π))) β β) |
26 | | 2nn0 12435 |
. . . . . . . . . 10
β’ 2 β
β0 |
27 | 26 | a1i 11 |
. . . . . . . . 9
β’ (π β 2 β
β0) |
28 | | sadcp1.n |
. . . . . . . . 9
β’ (π β π β
β0) |
29 | 27, 28 | nn0expcld 14155 |
. . . . . . . 8
β’ (π β (2βπ) β
β0) |
30 | | 0nn0 12433 |
. . . . . . . 8
β’ 0 β
β0 |
31 | | ifcl 4532 |
. . . . . . . 8
β’
(((2βπ) β
β0 β§ 0 β β0) β if(π β (π΄ sadd π΅), (2βπ), 0) β
β0) |
32 | 29, 30, 31 | sylancl 587 |
. . . . . . 7
β’ (π β if(π β (π΄ sadd π΅), (2βπ), 0) β
β0) |
33 | 32 | nn0cnd 12480 |
. . . . . 6
β’ (π β if(π β (π΄ sadd π΅), (2βπ), 0) β β) |
34 | | 1nn0 12434 |
. . . . . . . . . . 11
β’ 1 β
β0 |
35 | 34 | a1i 11 |
. . . . . . . . . 10
β’ (π β 1 β
β0) |
36 | 28, 35 | nn0addcld 12482 |
. . . . . . . . 9
β’ (π β (π + 1) β
β0) |
37 | 27, 36 | nn0expcld 14155 |
. . . . . . . 8
β’ (π β (2β(π + 1)) β
β0) |
38 | | ifcl 4532 |
. . . . . . . 8
β’
(((2β(π + 1))
β β0 β§ 0 β β0) β
if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0) β
β0) |
39 | 37, 30, 38 | sylancl 587 |
. . . . . . 7
β’ (π β if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0) β
β0) |
40 | 39 | nn0cnd 12480 |
. . . . . 6
β’ (π β if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0) β β) |
41 | 33, 40 | addcld 11179 |
. . . . 5
β’ (π β (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) β β) |
42 | 25, 41 | addcld 11179 |
. . . 4
β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) β
β) |
43 | | inss1 4189 |
. . . . . . . . . 10
β’ (π΄ β© (0..^π)) β π΄ |
44 | 43, 2 | sstrid 3956 |
. . . . . . . . 9
β’ (π β (π΄ β© (0..^π)) β
β0) |
45 | | inss2 4190 |
. . . . . . . . . 10
β’ (π΄ β© (0..^π)) β (0..^π) |
46 | | ssfi 9120 |
. . . . . . . . . 10
β’
(((0..^π) β Fin
β§ (π΄ β© (0..^π)) β (0..^π)) β (π΄ β© (0..^π)) β Fin) |
47 | 10, 45, 46 | sylancl 587 |
. . . . . . . . 9
β’ (π β (π΄ β© (0..^π)) β Fin) |
48 | | elfpw 9301 |
. . . . . . . . 9
β’ ((π΄ β© (0..^π)) β (π« β0
β© Fin) β ((π΄ β©
(0..^π)) β
β0 β§ (π΄ β© (0..^π)) β Fin)) |
49 | 44, 47, 48 | sylanbrc 584 |
. . . . . . . 8
β’ (π β (π΄ β© (0..^π)) β (π« β0
β© Fin)) |
50 | 22 | ffvelcdmi 7035 |
. . . . . . . 8
β’ ((π΄ β© (0..^π)) β (π« β0
β© Fin) β (πΎβ(π΄ β© (0..^π))) β
β0) |
51 | 49, 50 | syl 17 |
. . . . . . 7
β’ (π β (πΎβ(π΄ β© (0..^π))) β
β0) |
52 | 51 | nn0cnd 12480 |
. . . . . 6
β’ (π β (πΎβ(π΄ β© (0..^π))) β β) |
53 | | inss1 4189 |
. . . . . . . . . 10
β’ (π΅ β© (0..^π)) β π΅ |
54 | 53, 3 | sstrid 3956 |
. . . . . . . . 9
β’ (π β (π΅ β© (0..^π)) β
β0) |
55 | | inss2 4190 |
. . . . . . . . . 10
β’ (π΅ β© (0..^π)) β (0..^π) |
56 | | ssfi 9120 |
. . . . . . . . . 10
β’
(((0..^π) β Fin
β§ (π΅ β© (0..^π)) β (0..^π)) β (π΅ β© (0..^π)) β Fin) |
57 | 10, 55, 56 | sylancl 587 |
. . . . . . . . 9
β’ (π β (π΅ β© (0..^π)) β Fin) |
58 | | elfpw 9301 |
. . . . . . . . 9
β’ ((π΅ β© (0..^π)) β (π« β0
β© Fin) β ((π΅ β©
(0..^π)) β
β0 β§ (π΅ β© (0..^π)) β Fin)) |
59 | 54, 57, 58 | sylanbrc 584 |
. . . . . . . 8
β’ (π β (π΅ β© (0..^π)) β (π« β0
β© Fin)) |
60 | 22 | ffvelcdmi 7035 |
. . . . . . . 8
β’ ((π΅ β© (0..^π)) β (π« β0
β© Fin) β (πΎβ(π΅ β© (0..^π))) β
β0) |
61 | 59, 60 | syl 17 |
. . . . . . 7
β’ (π β (πΎβ(π΅ β© (0..^π))) β
β0) |
62 | 61 | nn0cnd 12480 |
. . . . . 6
β’ (π β (πΎβ(π΅ β© (0..^π))) β β) |
63 | 52, 62 | addcld 11179 |
. . . . 5
β’ (π β ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) β β) |
64 | | ifcl 4532 |
. . . . . . . 8
β’
(((2βπ) β
β0 β§ 0 β β0) β if(π β π΄, (2βπ), 0) β
β0) |
65 | 29, 30, 64 | sylancl 587 |
. . . . . . 7
β’ (π β if(π β π΄, (2βπ), 0) β
β0) |
66 | 65 | nn0cnd 12480 |
. . . . . 6
β’ (π β if(π β π΄, (2βπ), 0) β β) |
67 | | ifcl 4532 |
. . . . . . . 8
β’
(((2βπ) β
β0 β§ 0 β β0) β if(π β π΅, (2βπ), 0) β
β0) |
68 | 29, 30, 67 | sylancl 587 |
. . . . . . 7
β’ (π β if(π β π΅, (2βπ), 0) β
β0) |
69 | 68 | nn0cnd 12480 |
. . . . . 6
β’ (π β if(π β π΅, (2βπ), 0) β β) |
70 | 66, 69 | addcld 11179 |
. . . . 5
β’ (π β (if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)) β β) |
71 | 63, 70 | addcld 11179 |
. . . 4
β’ (π β (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + (if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0))) β β) |
72 | 29 | nn0cnd 12480 |
. . . . . 6
β’ (π β (2βπ) β β) |
73 | 72 | adantr 482 |
. . . . 5
β’ ((π β§ β
β (πΆβπ)) β (2βπ) β β) |
74 | | 0cnd 11153 |
. . . . 5
β’ ((π β§ Β¬ β
β (πΆβπ)) β 0 β β) |
75 | 73, 74 | ifclda 4522 |
. . . 4
β’ (π β if(β
β (πΆβπ), (2βπ), 0) β β) |
76 | | sadadd2lem.1 |
. . . . . 6
β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |
77 | 2, 3, 4, 28 | sadval 16341 |
. . . . . . . . 9
β’ (π β (π β (π΄ sadd π΅) β hadd(π β π΄, π β π΅, β
β (πΆβπ)))) |
78 | 77 | ifbid 4510 |
. . . . . . . 8
β’ (π β if(π β (π΄ sadd π΅), (2βπ), 0) = if(hadd(π β π΄, π β π΅, β
β (πΆβπ)), (2βπ), 0)) |
79 | 2, 3, 4, 28 | sadcp1 16340 |
. . . . . . . . 9
β’ (π β (β
β (πΆβ(π + 1)) β cadd(π β π΄, π β π΅, β
β (πΆβπ)))) |
80 | 27 | nn0cnd 12480 |
. . . . . . . . . . 11
β’ (π β 2 β
β) |
81 | 80, 28 | expp1d 14058 |
. . . . . . . . . 10
β’ (π β (2β(π + 1)) = ((2βπ) Β· 2)) |
82 | 72, 80 | mulcomd 11181 |
. . . . . . . . . 10
β’ (π β ((2βπ) Β· 2) = (2 Β· (2βπ))) |
83 | 81, 82 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (2β(π + 1)) = (2 Β· (2βπ))) |
84 | 79, 83 | ifbieq1d 4511 |
. . . . . . . 8
β’ (π β if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0) = if(cadd(π β π΄, π β π΅, β
β (πΆβπ)), (2 Β· (2βπ)), 0)) |
85 | 78, 84 | oveq12d 7376 |
. . . . . . 7
β’ (π β (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = (if(hadd(π β π΄, π β π΅, β
β (πΆβπ)), (2βπ), 0) + if(cadd(π β π΄, π β π΅, β
β (πΆβπ)), (2 Β· (2βπ)), 0))) |
86 | | sadadd2lem2 16335 |
. . . . . . . 8
β’
((2βπ) β
β β (if(hadd(π
β π΄, π β π΅, β
β (πΆβπ)), (2βπ), 0) + if(cadd(π β π΄, π β π΅, β
β (πΆβπ)), (2 Β· (2βπ)), 0)) = ((if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)) + if(β
β (πΆβπ), (2βπ), 0))) |
87 | 72, 86 | syl 17 |
. . . . . . 7
β’ (π β (if(hadd(π β π΄, π β π΅, β
β (πΆβπ)), (2βπ), 0) + if(cadd(π β π΄, π β π΅, β
β (πΆβπ)), (2 Β· (2βπ)), 0)) = ((if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)) + if(β
β (πΆβπ), (2βπ), 0))) |
88 | 85, 87 | eqtrd 2773 |
. . . . . 6
β’ (π β (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)) + if(β
β (πΆβπ), (2βπ), 0))) |
89 | 76, 88 | oveq12d 7376 |
. . . . 5
β’ (π β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) = (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + ((if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)) + if(β
β (πΆβπ), (2βπ), 0)))) |
90 | 25, 41, 75 | add32d 11387 |
. . . . 5
β’ (π β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) + if(β
β (πΆβπ), (2βπ), 0)) = (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)))) |
91 | 63, 70, 75 | addassd 11182 |
. . . . 5
β’ (π β ((((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + (if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0))) + if(β
β (πΆβπ), (2βπ), 0)) = (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + ((if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)) + if(β
β (πΆβπ), (2βπ), 0)))) |
92 | 89, 90, 91 | 3eqtr4d 2783 |
. . . 4
β’ (π β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) + if(β
β (πΆβπ), (2βπ), 0)) = ((((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + (if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0))) + if(β
β (πΆβπ), (2βπ), 0))) |
93 | 42, 71, 75, 92 | addcan2ad 11366 |
. . 3
β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) = (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + (if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)))) |
94 | 25, 33, 40 | addassd 11182 |
. . 3
β’ (π β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(π β (π΄ sadd π΅), (2βπ), 0)) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ((π΄ sadd π΅) β© (0..^π))) + (if(π β (π΄ sadd π΅), (2βπ), 0) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)))) |
95 | 52, 66, 62, 69 | add4d 11388 |
. . 3
β’ (π β (((πΎβ(π΄ β© (0..^π))) + if(π β π΄, (2βπ), 0)) + ((πΎβ(π΅ β© (0..^π))) + if(π β π΅, (2βπ), 0))) = (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) + (if(π β π΄, (2βπ), 0) + if(π β π΅, (2βπ), 0)))) |
96 | 93, 94, 95 | 3eqtr4d 2783 |
. 2
β’ (π β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(π β (π΄ sadd π΅), (2βπ), 0)) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = (((πΎβ(π΄ β© (0..^π))) + if(π β π΄, (2βπ), 0)) + ((πΎβ(π΅ β© (0..^π))) + if(π β π΅, (2βπ), 0)))) |
97 | 20 | bitsinvp1 16334 |
. . . 4
β’ (((π΄ sadd π΅) β β0 β§ π β β0)
β (πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) = ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(π β (π΄ sadd π΅), (2βπ), 0))) |
98 | 7, 28, 97 | syl2anc 585 |
. . 3
β’ (π β (πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) = ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(π β (π΄ sadd π΅), (2βπ), 0))) |
99 | 98 | oveq1d 7373 |
. 2
β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(π β (π΄ sadd π΅), (2βπ), 0)) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) |
100 | 20 | bitsinvp1 16334 |
. . . 4
β’ ((π΄ β β0
β§ π β
β0) β (πΎβ(π΄ β© (0..^(π + 1)))) = ((πΎβ(π΄ β© (0..^π))) + if(π β π΄, (2βπ), 0))) |
101 | 2, 28, 100 | syl2anc 585 |
. . 3
β’ (π β (πΎβ(π΄ β© (0..^(π + 1)))) = ((πΎβ(π΄ β© (0..^π))) + if(π β π΄, (2βπ), 0))) |
102 | 20 | bitsinvp1 16334 |
. . . 4
β’ ((π΅ β β0
β§ π β
β0) β (πΎβ(π΅ β© (0..^(π + 1)))) = ((πΎβ(π΅ β© (0..^π))) + if(π β π΅, (2βπ), 0))) |
103 | 3, 28, 102 | syl2anc 585 |
. . 3
β’ (π β (πΎβ(π΅ β© (0..^(π + 1)))) = ((πΎβ(π΅ β© (0..^π))) + if(π β π΅, (2βπ), 0))) |
104 | 101, 103 | oveq12d 7376 |
. 2
β’ (π β ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))) = (((πΎβ(π΄ β© (0..^π))) + if(π β π΄, (2βπ), 0)) + ((πΎβ(π΅ β© (0..^π))) + if(π β π΅, (2βπ), 0)))) |
105 | 96, 99, 104 | 3eqtr4d 2783 |
1
β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))) |