Step | Hyp | Ref
| Expression |
1 | | inass 4220 |
. . . . . . . 8
β’ ((π΄ β© (0..^π)) β© (0..^π)) = (π΄ β© ((0..^π) β© (0..^π))) |
2 | | inidm 4219 |
. . . . . . . . 9
β’
((0..^π) β©
(0..^π)) = (0..^π) |
3 | 2 | ineq2i 4210 |
. . . . . . . 8
β’ (π΄ β© ((0..^π) β© (0..^π))) = (π΄ β© (0..^π)) |
4 | 1, 3 | eqtri 2761 |
. . . . . . 7
β’ ((π΄ β© (0..^π)) β© (0..^π)) = (π΄ β© (0..^π)) |
5 | 4 | fveq2i 6895 |
. . . . . 6
β’ (β‘(bits βΎ
β0)β((π΄ β© (0..^π)) β© (0..^π))) = (β‘(bits βΎ
β0)β(π΄ β© (0..^π))) |
6 | | inass 4220 |
. . . . . . . 8
β’ ((π΅ β© (0..^π)) β© (0..^π)) = (π΅ β© ((0..^π) β© (0..^π))) |
7 | 2 | ineq2i 4210 |
. . . . . . . 8
β’ (π΅ β© ((0..^π) β© (0..^π))) = (π΅ β© (0..^π)) |
8 | 6, 7 | eqtri 2761 |
. . . . . . 7
β’ ((π΅ β© (0..^π)) β© (0..^π)) = (π΅ β© (0..^π)) |
9 | 8 | fveq2i 6895 |
. . . . . 6
β’ (β‘(bits βΎ
β0)β((π΅ β© (0..^π)) β© (0..^π))) = (β‘(bits βΎ
β0)β(π΅ β© (0..^π))) |
10 | 5, 9 | oveq12i 7421 |
. . . . 5
β’ ((β‘(bits βΎ
β0)β((π΄ β© (0..^π)) β© (0..^π))) + (β‘(bits βΎ
β0)β((π΅ β© (0..^π)) β© (0..^π)))) = ((β‘(bits βΎ
β0)β(π΄ β© (0..^π))) + (β‘(bits βΎ
β0)β(π΅ β© (0..^π)))) |
11 | 10 | oveq1i 7419 |
. . . 4
β’ (((β‘(bits βΎ
β0)β((π΄ β© (0..^π)) β© (0..^π))) + (β‘(bits βΎ
β0)β((π΅ β© (0..^π)) β© (0..^π)))) mod (2βπ)) = (((β‘(bits βΎ
β0)β(π΄ β© (0..^π))) + (β‘(bits βΎ
β0)β(π΅ β© (0..^π)))) mod (2βπ)) |
12 | | inss1 4229 |
. . . . . 6
β’ (π΄ β© (0..^π)) β π΄ |
13 | | sadeq.a |
. . . . . 6
β’ (π β π΄ β
β0) |
14 | 12, 13 | sstrid 3994 |
. . . . 5
β’ (π β (π΄ β© (0..^π)) β
β0) |
15 | | inss1 4229 |
. . . . . 6
β’ (π΅ β© (0..^π)) β π΅ |
16 | | sadeq.b |
. . . . . 6
β’ (π β π΅ β
β0) |
17 | 15, 16 | sstrid 3994 |
. . . . 5
β’ (π β (π΅ β© (0..^π)) β
β0) |
18 | | eqid 2733 |
. . . . 5
β’
seq0((π β
2o, π β
β0 β¦ if(cadd(π β (π΄ β© (0..^π)), π β (π΅ β© (0..^π)), β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β 1)))) =
seq0((π β
2o, π β
β0 β¦ if(cadd(π β (π΄ β© (0..^π)), π β (π΅ β© (0..^π)), β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β
1)))) |
19 | | sadeq.n |
. . . . 5
β’ (π β π β
β0) |
20 | | eqid 2733 |
. . . . 5
β’ β‘(bits βΎ β0) = β‘(bits βΎ
β0) |
21 | 14, 17, 18, 19, 20 | sadadd3 16402 |
. . . 4
β’ (π β ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) mod (2βπ)) = (((β‘(bits βΎ
β0)β((π΄ β© (0..^π)) β© (0..^π))) + (β‘(bits βΎ
β0)β((π΅ β© (0..^π)) β© (0..^π)))) mod (2βπ))) |
22 | | eqid 2733 |
. . . . 5
β’
seq0((π β
2o, π β
β0 β¦ if(cadd(π β π΄, π β π΅, β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β 1)))) =
seq0((π β
2o, π β
β0 β¦ if(cadd(π β π΄, π β π΅, β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β
1)))) |
23 | 13, 16, 22, 19, 20 | sadadd3 16402 |
. . . 4
β’ (π β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) mod (2βπ)) = (((β‘(bits βΎ
β0)β(π΄ β© (0..^π))) + (β‘(bits βΎ
β0)β(π΅ β© (0..^π)))) mod (2βπ))) |
24 | 11, 21, 23 | 3eqtr4a 2799 |
. . 3
β’ (π β ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) mod (2βπ)) = ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) mod (2βπ))) |
25 | | inss1 4229 |
. . . . . . . 8
β’ (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β ((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) |
26 | | sadcl 16403 |
. . . . . . . . 9
β’ (((π΄ β© (0..^π)) β β0 β§ (π΅ β© (0..^π)) β β0) β
((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β
β0) |
27 | 14, 17, 26 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β
β0) |
28 | 25, 27 | sstrid 3994 |
. . . . . . 7
β’ (π β (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β
β0) |
29 | | fzofi 13939 |
. . . . . . . . 9
β’
(0..^π) β
Fin |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ (π β (0..^π) β Fin) |
31 | | inss2 4230 |
. . . . . . . 8
β’ (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (0..^π) |
32 | | ssfi 9173 |
. . . . . . . 8
β’
(((0..^π) β Fin
β§ (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (0..^π)) β (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β Fin) |
33 | 30, 31, 32 | sylancl 587 |
. . . . . . 7
β’ (π β (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β Fin) |
34 | | elfpw 9354 |
. . . . . . 7
β’ ((((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (π« β0
β© Fin) β ((((π΄
β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β β0 β§
(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β Fin)) |
35 | 28, 33, 34 | sylanbrc 584 |
. . . . . 6
β’ (π β (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (π« β0
β© Fin)) |
36 | | bitsf1o 16386 |
. . . . . . . 8
β’ (bits
βΎ β0):β0β1-1-ontoβ(π« β0 β©
Fin) |
37 | | f1ocnv 6846 |
. . . . . . . 8
β’ ((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1-ontoββ0) |
38 | | f1of 6834 |
. . . . . . . 8
β’ (β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1-ontoββ0 β β‘(bits βΎ
β0):(π« β0 β©
Fin)βΆβ0) |
39 | 36, 37, 38 | mp2b 10 |
. . . . . . 7
β’ β‘(bits βΎ
β0):(π« β0 β©
Fin)βΆβ0 |
40 | 39 | ffvelcdmi 7086 |
. . . . . 6
β’ ((((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (π« β0
β© Fin) β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β
β0) |
41 | 35, 40 | syl 17 |
. . . . 5
β’ (π β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β
β0) |
42 | 41 | nn0red 12533 |
. . . 4
β’ (π β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β β) |
43 | | 2rp 12979 |
. . . . . 6
β’ 2 β
β+ |
44 | 43 | a1i 11 |
. . . . 5
β’ (π β 2 β
β+) |
45 | 19 | nn0zd 12584 |
. . . . 5
β’ (π β π β β€) |
46 | 44, 45 | rpexpcld 14210 |
. . . 4
β’ (π β (2βπ) β
β+) |
47 | 41 | nn0ge0d 12535 |
. . . 4
β’ (π β 0 β€ (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
48 | 41 | fvresd 6912 |
. . . . . . . 8
β’ (π β ((bits βΎ
β0)β(β‘(bits
βΎ β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) = (bitsβ(β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))))) |
49 | | f1ocnvfv2 7275 |
. . . . . . . . 9
β’ (((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β§ (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (π« β0
β© Fin)) β ((bits βΎ β0)β(β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) |
50 | 36, 35, 49 | sylancr 588 |
. . . . . . . 8
β’ (π β ((bits βΎ
β0)β(β‘(bits
βΎ β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) |
51 | 48, 50 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (bitsβ(β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) |
52 | 51, 31 | eqsstrdi 4037 |
. . . . . 6
β’ (π β (bitsβ(β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) β (0..^π)) |
53 | 41 | nn0zd 12584 |
. . . . . . 7
β’ (π β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β β€) |
54 | | bitsfzo 16376 |
. . . . . . 7
β’ (((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β β€ β§ π β β0) β ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β (0..^(2βπ)) β (bitsβ(β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) β (0..^π))) |
55 | 53, 19, 54 | syl2anc 585 |
. . . . . 6
β’ (π β ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β (0..^(2βπ)) β (bitsβ(β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) β (0..^π))) |
56 | 52, 55 | mpbird 257 |
. . . . 5
β’ (π β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β (0..^(2βπ))) |
57 | | elfzolt2 13641 |
. . . . 5
β’ ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β (0..^(2βπ)) β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) < (2βπ)) |
58 | 56, 57 | syl 17 |
. . . 4
β’ (π β (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) < (2βπ)) |
59 | | modid 13861 |
. . . 4
β’ ((((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β β β§ (2βπ) β β+)
β§ (0 β€ (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β§ (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) < (2βπ))) β ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) mod (2βπ)) = (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
60 | 42, 46, 47, 58, 59 | syl22anc 838 |
. . 3
β’ (π β ((β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) mod (2βπ)) = (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
61 | | inss1 4229 |
. . . . . . . 8
β’ ((π΄ sadd π΅) β© (0..^π)) β (π΄ sadd π΅) |
62 | | sadcl 16403 |
. . . . . . . . 9
β’ ((π΄ β β0
β§ π΅ β
β0) β (π΄ sadd π΅) β
β0) |
63 | 13, 16, 62 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄ sadd π΅) β
β0) |
64 | 61, 63 | sstrid 3994 |
. . . . . . 7
β’ (π β ((π΄ sadd π΅) β© (0..^π)) β
β0) |
65 | | inss2 4230 |
. . . . . . . 8
β’ ((π΄ sadd π΅) β© (0..^π)) β (0..^π) |
66 | | ssfi 9173 |
. . . . . . . 8
β’
(((0..^π) β Fin
β§ ((π΄ sadd π΅) β© (0..^π)) β (0..^π)) β ((π΄ sadd π΅) β© (0..^π)) β Fin) |
67 | 30, 65, 66 | sylancl 587 |
. . . . . . 7
β’ (π β ((π΄ sadd π΅) β© (0..^π)) β Fin) |
68 | | elfpw 9354 |
. . . . . . 7
β’ (((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin) β (((π΄ sadd
π΅) β© (0..^π)) β β0
β§ ((π΄ sadd π΅) β© (0..^π)) β Fin)) |
69 | 64, 67, 68 | sylanbrc 584 |
. . . . . 6
β’ (π β ((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin)) |
70 | 39 | ffvelcdmi 7086 |
. . . . . 6
β’ (((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin) β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β
β0) |
71 | 69, 70 | syl 17 |
. . . . 5
β’ (π β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β
β0) |
72 | 71 | nn0red 12533 |
. . . 4
β’ (π β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β β) |
73 | 71 | nn0ge0d 12535 |
. . . 4
β’ (π β 0 β€ (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) |
74 | 71 | fvresd 6912 |
. . . . . . . 8
β’ (π β ((bits βΎ
β0)β(β‘(bits
βΎ β0)β((π΄ sadd π΅) β© (0..^π)))) = (bitsβ(β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))))) |
75 | | f1ocnvfv2 7275 |
. . . . . . . . 9
β’ (((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β§ ((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin)) β ((bits βΎ β0)β(β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) = ((π΄ sadd π΅) β© (0..^π))) |
76 | 36, 69, 75 | sylancr 588 |
. . . . . . . 8
β’ (π β ((bits βΎ
β0)β(β‘(bits
βΎ β0)β((π΄ sadd π΅) β© (0..^π)))) = ((π΄ sadd π΅) β© (0..^π))) |
77 | 74, 76 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (bitsβ(β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) = ((π΄ sadd π΅) β© (0..^π))) |
78 | 77, 65 | eqsstrdi 4037 |
. . . . . 6
β’ (π β (bitsβ(β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) β (0..^π)) |
79 | 71 | nn0zd 12584 |
. . . . . . 7
β’ (π β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β β€) |
80 | | bitsfzo 16376 |
. . . . . . 7
β’ (((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β β€ β§ π β β0) β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β (0..^(2βπ)) β (bitsβ(β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) β (0..^π))) |
81 | 79, 19, 80 | syl2anc 585 |
. . . . . 6
β’ (π β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β (0..^(2βπ)) β (bitsβ(β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) β (0..^π))) |
82 | 78, 81 | mpbird 257 |
. . . . 5
β’ (π β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β (0..^(2βπ))) |
83 | | elfzolt2 13641 |
. . . . 5
β’ ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β (0..^(2βπ)) β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) < (2βπ)) |
84 | 82, 83 | syl 17 |
. . . 4
β’ (π β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) < (2βπ)) |
85 | | modid 13861 |
. . . 4
β’ ((((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β β β§ (2βπ) β β+)
β§ (0 β€ (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) β§ (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) < (2βπ))) β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) mod (2βπ)) = (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) |
86 | 72, 46, 73, 84, 85 | syl22anc 838 |
. . 3
β’ (π β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) mod (2βπ)) = (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π)))) |
87 | 24, 60, 86 | 3eqtr3rd 2782 |
. 2
β’ (π β (β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) = (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
88 | | f1of1 6833 |
. . . . 5
β’ (β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1-ontoββ0 β β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1ββ0) |
89 | 36, 37, 88 | mp2b 10 |
. . . 4
β’ β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1ββ0 |
90 | | f1fveq 7261 |
. . . 4
β’ ((β‘(bits βΎ
β0):(π« β0 β© Fin)β1-1ββ0 β§ (((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin) β§ (((π΄ β©
(0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (π« β0
β© Fin))) β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) = (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β ((π΄ sadd π΅) β© (0..^π)) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
91 | 89, 90 | mpan 689 |
. . 3
β’ ((((π΄ sadd π΅) β© (0..^π)) β (π« β0
β© Fin) β§ (((π΄ β©
(0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)) β (π« β0
β© Fin)) β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) = (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β ((π΄ sadd π΅) β© (0..^π)) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
92 | 69, 35, 91 | syl2anc 585 |
. 2
β’ (π β ((β‘(bits βΎ
β0)β((π΄ sadd π΅) β© (0..^π))) = (β‘(bits βΎ
β0)β(((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) β ((π΄ sadd π΅) β© (0..^π)) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π)))) |
93 | 87, 92 | mpbid 231 |
1
β’ (π β ((π΄ sadd π΅) β© (0..^π)) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) |