Step | Hyp | Ref
| Expression |
1 | | bitsss 16311 |
. . . . . 6
β’
(bitsβπ΄)
β β0 |
2 | | bitsss 16311 |
. . . . . 6
β’
(bitsβπ΅)
β β0 |
3 | | sadcl 16347 |
. . . . . 6
β’
(((bitsβπ΄)
β β0 β§ (bitsβπ΅) β β0) β
((bitsβπ΄) sadd
(bitsβπ΅)) β
β0) |
4 | 1, 2, 3 | mp2an 691 |
. . . . 5
β’
((bitsβπ΄) sadd
(bitsβπ΅)) β
β0 |
5 | 4 | sseli 3941 |
. . . 4
β’ (π β ((bitsβπ΄) sadd (bitsβπ΅)) β π β β0) |
6 | 5 | a1i 11 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€) β (π β ((bitsβπ΄) sadd (bitsβπ΅)) β π β
β0)) |
7 | | bitsss 16311 |
. . . . 5
β’
(bitsβ(π΄ +
π΅)) β
β0 |
8 | 7 | sseli 3941 |
. . . 4
β’ (π β (bitsβ(π΄ + π΅)) β π β β0) |
9 | 8 | a1i 11 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€) β (π β (bitsβ(π΄ + π΅)) β π β
β0)) |
10 | | eqid 2733 |
. . . . . . . . 9
β’
seq0((π β
2o, π β
β0 β¦ if(cadd(π β (bitsβπ΄), π β (bitsβπ΅), β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β 1)))) =
seq0((π β
2o, π β
β0 β¦ if(cadd(π β (bitsβπ΄), π β (bitsβπ΅), β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β
1)))) |
11 | | eqid 2733 |
. . . . . . . . 9
β’ β‘(bits βΎ β0) = β‘(bits βΎ
β0) |
12 | | simpll 766 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π΄ β
β€) |
13 | | simplr 768 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π΅ β
β€) |
14 | | simpr 486 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β
β0) |
15 | | 1nn0 12434 |
. . . . . . . . . . 11
β’ 1 β
β0 |
16 | 15 | a1i 11 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β 1 β β0) |
17 | 14, 16 | nn0addcld 12482 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π + 1) β
β0) |
18 | 10, 11, 12, 13, 17 | sadaddlem 16351 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((bitsβπ΄)
sadd (bitsβπ΅)) β©
(0..^(π + 1))) =
(bitsβ((π΄ + π΅) mod (2β(π + 1))))) |
19 | 12, 13 | zaddcld 12616 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π΄ + π΅) β
β€) |
20 | | bitsmod 16321 |
. . . . . . . . 9
β’ (((π΄ + π΅) β β€ β§ (π + 1) β β0) β
(bitsβ((π΄ + π΅) mod (2β(π + 1)))) = ((bitsβ(π΄ + π΅)) β© (0..^(π + 1)))) |
21 | 19, 17, 20 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (bitsβ((π΄ +
π΅) mod (2β(π + 1)))) = ((bitsβ(π΄ + π΅)) β© (0..^(π + 1)))) |
22 | 18, 21 | eqtrd 2773 |
. . . . . . 7
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (((bitsβπ΄)
sadd (bitsβπ΅)) β©
(0..^(π + 1))) =
((bitsβ(π΄ + π΅)) β© (0..^(π + 1)))) |
23 | 22 | eleq2d 2820 |
. . . . . 6
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
(((bitsβπ΄) sadd
(bitsβπ΅)) β©
(0..^(π + 1))) β π β ((bitsβ(π΄ + π΅)) β© (0..^(π + 1))))) |
24 | | elin 3927 |
. . . . . 6
β’ (π β (((bitsβπ΄) sadd (bitsβπ΅)) β© (0..^(π + 1))) β (π β ((bitsβπ΄) sadd (bitsβπ΅)) β§ π β (0..^(π + 1)))) |
25 | | elin 3927 |
. . . . . 6
β’ (π β ((bitsβ(π΄ + π΅)) β© (0..^(π + 1))) β (π β (bitsβ(π΄ + π΅)) β§ π β (0..^(π + 1)))) |
26 | 23, 24, 25 | 3bitr3g 313 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β ((π β
((bitsβπ΄) sadd
(bitsβπ΅)) β§ π β (0..^(π + 1))) β (π β (bitsβ(π΄ + π΅)) β§ π β (0..^(π + 1))))) |
27 | | nn0uz 12810 |
. . . . . . . . 9
β’
β0 = (β€β₯β0) |
28 | 14, 27 | eleqtrdi 2844 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β
(β€β₯β0)) |
29 | | eluzfz2 13455 |
. . . . . . . 8
β’ (π β
(β€β₯β0) β π β (0...π)) |
30 | 28, 29 | syl 17 |
. . . . . . 7
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β (0...π)) |
31 | 14 | nn0zd 12530 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β
β€) |
32 | | fzval3 13647 |
. . . . . . . 8
β’ (π β β€ β
(0...π) = (0..^(π + 1))) |
33 | 31, 32 | syl 17 |
. . . . . . 7
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (0...π) =
(0..^(π +
1))) |
34 | 30, 33 | eleqtrd 2836 |
. . . . . 6
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β π β (0..^(π + 1))) |
35 | 34 | biantrud 533 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
((bitsβπ΄) sadd
(bitsβπ΅)) β
(π β
((bitsβπ΄) sadd
(bitsβπ΅)) β§ π β (0..^(π + 1))))) |
36 | 34 | biantrud 533 |
. . . . 5
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
(bitsβ(π΄ + π΅)) β (π β (bitsβ(π΄ + π΅)) β§ π β (0..^(π + 1))))) |
37 | 26, 35, 36 | 3bitr4d 311 |
. . . 4
β’ (((π΄ β β€ β§ π΅ β β€) β§ π β β0)
β (π β
((bitsβπ΄) sadd
(bitsβπ΅)) β
π β (bitsβ(π΄ + π΅)))) |
38 | 37 | ex 414 |
. . 3
β’ ((π΄ β β€ β§ π΅ β β€) β (π β β0
β (π β
((bitsβπ΄) sadd
(bitsβπ΅)) β
π β (bitsβ(π΄ + π΅))))) |
39 | 6, 9, 38 | pm5.21ndd 381 |
. 2
β’ ((π΄ β β€ β§ π΅ β β€) β (π β ((bitsβπ΄) sadd (bitsβπ΅)) β π β (bitsβ(π΄ + π΅)))) |
40 | 39 | eqrdv 2731 |
1
β’ ((π΄ β β€ β§ π΅ β β€) β
((bitsβπ΄) sadd
(bitsβπ΅)) =
(bitsβ(π΄ + π΅))) |