Step | Hyp | Ref
| Expression |
1 | | eulerpart.p |
. . . . 5
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
2 | | eulerpart.o |
. . . . 5
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
3 | | eulerpart.d |
. . . . 5
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
4 | | eulerpart.j |
. . . . 5
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
5 | | eulerpart.f |
. . . . 5
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
6 | | eulerpart.h |
. . . . 5
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
7 | | eulerpart.m |
. . . . 5
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
8 | | eulerpart.r |
. . . . 5
β’ π
= {π β£ (β‘π β β) β
Fin} |
9 | | eulerpart.t |
. . . . 5
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
10 | | eulerpart.g |
. . . . 5
β’ πΊ = (π β (π β© π
) β¦
((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemgv 32973 |
. . . 4
β’ (π΄ β (π β© π
) β (πΊβπ΄) = ((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))) |
12 | 11 | fveq1d 6844 |
. . 3
β’ (π΄ β (π β© π
) β ((πΊβπ΄)βπ΅) = (((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))βπ΅)) |
13 | 12 | adantr 481 |
. 2
β’ ((π΄ β (π β© π
) β§ π΅ β β) β ((πΊβπ΄)βπ΅) = (((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))βπ΅)) |
14 | | nnex 12159 |
. . 3
β’ β
β V |
15 | | imassrn 6024 |
. . . 4
β’ (πΉ β (πβ(bits β (π΄ βΎ π½)))) β ran πΉ |
16 | 4, 5 | oddpwdc 32954 |
. . . . 5
β’ πΉ:(π½ Γ β0)β1-1-ontoββ |
17 | | f1of 6784 |
. . . . 5
β’ (πΉ:(π½ Γ β0)β1-1-ontoββ β πΉ:(π½ Γ
β0)βΆβ) |
18 | | frn 6675 |
. . . . 5
β’ (πΉ:(π½ Γ β0)βΆβ
β ran πΉ β
β) |
19 | 16, 17, 18 | mp2b 10 |
. . . 4
β’ ran πΉ β
β |
20 | 15, 19 | sstri 3953 |
. . 3
β’ (πΉ β (πβ(bits β (π΄ βΎ π½)))) β β |
21 | | simpr 485 |
. . 3
β’ ((π΄ β (π β© π
) β§ π΅ β β) β π΅ β β) |
22 | | indfval 32615 |
. . 3
β’ ((β
β V β§ (πΉ β
(πβ(bits β
(π΄ βΎ π½)))) β β β§ π΅ β β) β
(((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))βπ΅) = if(π΅ β (πΉ β (πβ(bits β (π΄ βΎ π½)))), 1, 0)) |
23 | 14, 20, 21, 22 | mp3an12i 1465 |
. 2
β’ ((π΄ β (π β© π
) β§ π΅ β β) β
(((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))βπ΅) = if(π΅ β (πΉ β (πβ(bits β (π΄ βΎ π½)))), 1, 0)) |
24 | | ffn 6668 |
. . . . . 6
β’ (πΉ:(π½ Γ β0)βΆβ
β πΉ Fn (π½ Γ
β0)) |
25 | 16, 17, 24 | mp2b 10 |
. . . . 5
β’ πΉ Fn (π½ Γ
β0) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemmf 32975 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (bits β (π΄ βΎ π½)) β π») |
27 | 1, 2, 3, 4, 5, 6, 7 | eulerpartlem1 32967 |
. . . . . . . . . . 11
β’ π:π»β1-1-ontoβ(π« (π½ Γ β0) β©
Fin) |
28 | | f1of 6784 |
. . . . . . . . . . 11
β’ (π:π»β1-1-ontoβ(π« (π½ Γ β0) β© Fin)
β π:π»βΆ(π« (π½ Γ β0) β©
Fin)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . 10
β’ π:π»βΆ(π« (π½ Γ β0) β©
Fin) |
30 | 29 | ffvelcdmi 7034 |
. . . . . . . . 9
β’ ((bits
β (π΄ βΎ π½)) β π» β (πβ(bits β (π΄ βΎ π½))) β (π« (π½ Γ β0) β©
Fin)) |
31 | 26, 30 | syl 17 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β (πβ(bits β (π΄ βΎ π½))) β (π« (π½ Γ β0) β©
Fin)) |
32 | 31 | elin1d 4158 |
. . . . . . 7
β’ (π΄ β (π β© π
) β (πβ(bits β (π΄ βΎ π½))) β π« (π½ Γ
β0)) |
33 | 32 | adantr 481 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π΅ β β) β (πβ(bits β (π΄ βΎ π½))) β π« (π½ Γ
β0)) |
34 | 33 | elpwid 4569 |
. . . . 5
β’ ((π΄ β (π β© π
) β§ π΅ β β) β (πβ(bits β (π΄ βΎ π½))) β (π½ Γ
β0)) |
35 | | fvelimab 6914 |
. . . . 5
β’ ((πΉ Fn (π½ Γ β0) β§ (πβ(bits β (π΄ βΎ π½))) β (π½ Γ β0)) β (π΅ β (πΉ β (πβ(bits β (π΄ βΎ π½)))) β βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅)) |
36 | 25, 34, 35 | sylancr 587 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π΅ β β) β (π΅ β (πΉ β (πβ(bits β (π΄ βΎ π½)))) β βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅)) |
37 | 4 | ssrab3 4040 |
. . . . . . . . 9
β’ π½ β
β |
38 | | fveq1 6841 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (bits β (π΄ βΎ π½)) β (πβπ₯) = ((bits β (π΄ βΎ π½))βπ₯)) |
39 | 38 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (bits β (π΄ βΎ π½)) β (π¦ β (πβπ₯) β π¦ β ((bits β (π΄ βΎ π½))βπ₯))) |
40 | 39 | anbi2d 629 |
. . . . . . . . . . . . . . . . 17
β’ (π = (bits β (π΄ βΎ π½)) β ((π₯ β π½ β§ π¦ β (πβπ₯)) β (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯)))) |
41 | 40 | opabbidv 5171 |
. . . . . . . . . . . . . . . 16
β’ (π = (bits β (π΄ βΎ π½)) β {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))} = {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))}) |
42 | 14, 37 | ssexi 5279 |
. . . . . . . . . . . . . . . . . 18
β’ π½ β V |
43 | | abid2 2875 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π¦ β£ π¦ β ((bits β (π΄ βΎ π½))βπ₯)} = ((bits β (π΄ βΎ π½))βπ₯) |
44 | 43 | fvexi 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ {π¦ β£ π¦ β ((bits β (π΄ βΎ π½))βπ₯)} β V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π½ β {π¦ β£ π¦ β ((bits β (π΄ βΎ π½))βπ₯)} β V) |
46 | 42, 45 | opabex3 7900 |
. . . . . . . . . . . . . . . . 17
β’
{β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))} β V |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (π β© π
) β {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))} β V) |
48 | 7, 41, 26, 47 | fvmptd3 6971 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (π β© π
) β (πβ(bits β (π΄ βΎ π½))) = {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))}) |
49 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ = π‘ β§ π¦ = π) β π₯ = π‘) |
50 | 49 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π‘ β§ π¦ = π) β (π₯ β π½ β π‘ β π½)) |
51 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ = π‘ β§ π¦ = π) β π¦ = π) |
52 | 49 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ = π‘ β§ π¦ = π) β ((bits β (π΄ βΎ π½))βπ₯) = ((bits β (π΄ βΎ π½))βπ‘)) |
53 | 51, 52 | eleq12d 2831 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π‘ β§ π¦ = π) β (π¦ β ((bits β (π΄ βΎ π½))βπ₯) β π β ((bits β (π΄ βΎ π½))βπ‘))) |
54 | 50, 53 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π‘ β§ π¦ = π) β ((π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯)) β (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘)))) |
55 | 54 | cbvopabv 5178 |
. . . . . . . . . . . . . . 15
β’
{β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))} = {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))} |
56 | 48, 55 | eqtrdi 2792 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π β© π
) β (πβ(bits β (π΄ βΎ π½))) = {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))}) |
57 | 56 | eleq2d 2823 |
. . . . . . . . . . . . 13
β’ (π΄ β (π β© π
) β (π€ β (πβ(bits β (π΄ βΎ π½))) β π€ β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))})) |
58 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | eulerpartlemt0 32969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ β (π β© π
) β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) |
59 | 58 | simp1bi 1145 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β (π β© π
) β π΄ β (β0
βm β)) |
60 | | nn0ex 12419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β0 β V |
61 | 60, 14 | elmap 8809 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β (β0
βm β) β π΄:ββΆβ0) |
62 | 59, 61 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β (π β© π
) β π΄:ββΆβ0) |
63 | | ffun 6671 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄:ββΆβ0 β
Fun π΄) |
64 | | funres 6543 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Fun
π΄ β Fun (π΄ βΎ π½)) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β (π β© π
) β Fun (π΄ βΎ π½)) |
66 | | fssres 6708 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄:ββΆβ0 β§
π½ β β) β
(π΄ βΎ π½):π½βΆβ0) |
67 | 62, 37, 66 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β (π β© π
) β (π΄ βΎ π½):π½βΆβ0) |
68 | | fdm 6677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄ βΎ π½):π½βΆβ0 β dom
(π΄ βΎ π½) = π½) |
69 | 68 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ βΎ π½):π½βΆβ0 β (π‘ β dom (π΄ βΎ π½) β π‘ β π½)) |
70 | 67, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β (π β© π
) β (π‘ β dom (π΄ βΎ π½) β π‘ β π½)) |
71 | 70 | biimpar 478 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β (π β© π
) β§ π‘ β π½) β π‘ β dom (π΄ βΎ π½)) |
72 | | fvco 6939 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Fun
(π΄ βΎ π½) β§ π‘ β dom (π΄ βΎ π½)) β ((bits β (π΄ βΎ π½))βπ‘) = (bitsβ((π΄ βΎ π½)βπ‘))) |
73 | 65, 71, 72 | syl2an2r 683 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β (π β© π
) β§ π‘ β π½) β ((bits β (π΄ βΎ π½))βπ‘) = (bitsβ((π΄ βΎ π½)βπ‘))) |
74 | | fvres 6861 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ β π½ β ((π΄ βΎ π½)βπ‘) = (π΄βπ‘)) |
75 | 74 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ β π½ β (bitsβ((π΄ βΎ π½)βπ‘)) = (bitsβ(π΄βπ‘))) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β (π β© π
) β§ π‘ β π½) β (bitsβ((π΄ βΎ π½)βπ‘)) = (bitsβ(π΄βπ‘))) |
77 | 73, 76 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β (π β© π
) β§ π‘ β π½) β ((bits β (π΄ βΎ π½))βπ‘) = (bitsβ(π΄βπ‘))) |
78 | 77 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β (π β© π
) β§ π‘ β π½) β (π β ((bits β (π΄ βΎ π½))βπ‘) β π β (bitsβ(π΄βπ‘)))) |
79 | 78 | pm5.32da 579 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β (π β© π
) β ((π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘)) β (π‘ β π½ β§ π β (bitsβ(π΄βπ‘))))) |
80 | 79 | opabbidv 5171 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (π β© π
) β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))} = {β¨π‘, πβ© β£ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))}) |
81 | 80 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (π β© π
) β (π€ β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))} β π€ β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))})) |
82 | | elopab 5484 |
. . . . . . . . . . . . . . 15
β’ (π€ β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))} β βπ‘βπ(π€ = β¨π‘, πβ© β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘))))) |
83 | 81, 82 | bitrdi 286 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π β© π
) β (π€ β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))} β βπ‘βπ(π€ = β¨π‘, πβ© β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))))) |
84 | | ancom 461 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ = β¨π‘, πβ© β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β ((π‘ β π½ β§ π β (bitsβ(π΄βπ‘))) β§ π€ = β¨π‘, πβ©)) |
85 | | anass 469 |
. . . . . . . . . . . . . . . . 17
β’ (((π‘ β π½ β§ π β (bitsβ(π΄βπ‘))) β§ π€ = β¨π‘, πβ©) β (π‘ β π½ β§ (π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
86 | 84, 85 | bitri 274 |
. . . . . . . . . . . . . . . 16
β’ ((π€ = β¨π‘, πβ© β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β (π‘ β π½ β§ (π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
87 | 86 | 2exbii 1851 |
. . . . . . . . . . . . . . 15
β’
(βπ‘βπ(π€ = β¨π‘, πβ© β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β βπ‘βπ(π‘ β π½ β§ (π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
88 | | df-rex 3074 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(bitsβ(π΄βπ‘))π€ = β¨π‘, πβ© β βπ(π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©)) |
89 | 88 | anbi2i 623 |
. . . . . . . . . . . . . . . . 17
β’ ((π‘ β π½ β§ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©) β (π‘ β π½ β§ βπ(π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
90 | 89 | exbii 1850 |
. . . . . . . . . . . . . . . 16
β’
(βπ‘(π‘ β π½ β§ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©) β βπ‘(π‘ β π½ β§ βπ(π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
91 | | df-rex 3074 |
. . . . . . . . . . . . . . . 16
β’
(βπ‘ β
π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ© β βπ‘(π‘ β π½ β§ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©)) |
92 | | exdistr 1958 |
. . . . . . . . . . . . . . . 16
β’
(βπ‘βπ(π‘ β π½ β§ (π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©)) β βπ‘(π‘ β π½ β§ βπ(π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
93 | 90, 91, 92 | 3bitr4i 302 |
. . . . . . . . . . . . . . 15
β’
(βπ‘ β
π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ© β βπ‘βπ(π‘ β π½ β§ (π β (bitsβ(π΄βπ‘)) β§ π€ = β¨π‘, πβ©))) |
94 | 87, 93 | bitr4i 277 |
. . . . . . . . . . . . . 14
β’
(βπ‘βπ(π€ = β¨π‘, πβ© β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©) |
95 | 83, 94 | bitrdi 286 |
. . . . . . . . . . . . 13
β’ (π΄ β (π β© π
) β (π€ β {β¨π‘, πβ© β£ (π‘ β π½ β§ π β ((bits β (π΄ βΎ π½))βπ‘))} β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©)) |
96 | 57, 95 | bitrd 278 |
. . . . . . . . . . . 12
β’ (π΄ β (π β© π
) β (π€ β (πβ(bits β (π΄ βΎ π½))) β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©)) |
97 | 96 | biimpa 477 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©) |
98 | 97 | adantlr 713 |
. . . . . . . . . 10
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ©) |
99 | | fveq2 6842 |
. . . . . . . . . . . . . 14
β’ (π€ = β¨π‘, πβ© β (πΉβπ€) = (πΉββ¨π‘, πβ©)) |
100 | 99 | adantl 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β§ π€ = β¨π‘, πβ©) β (πΉβπ€) = (πΉββ¨π‘, πβ©)) |
101 | | bitsss 16306 |
. . . . . . . . . . . . . . . . 17
β’
(bitsβ(π΄βπ‘)) β
β0 |
102 | 101 | sseli 3940 |
. . . . . . . . . . . . . . . 16
β’ (π β (bitsβ(π΄βπ‘)) β π β β0) |
103 | 102 | anim2i 617 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β π½ β§ π β (bitsβ(π΄βπ‘))) β (π‘ β π½ β§ π β
β0)) |
104 | 103 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β§ π€ = β¨π‘, πβ©) β (π‘ β π½ β§ π β
β0)) |
105 | | opelxp 5669 |
. . . . . . . . . . . . . . 15
β’
(β¨π‘, πβ© β (π½ Γ β0) β (π‘ β π½ β§ π β
β0)) |
106 | 4, 5 | oddpwdcv 32955 |
. . . . . . . . . . . . . . . 16
β’
(β¨π‘, πβ© β (π½ Γ β0) β (πΉββ¨π‘, πβ©) = ((2β(2nd
ββ¨π‘, πβ©)) Β·
(1st ββ¨π‘, πβ©))) |
107 | | vex 3449 |
. . . . . . . . . . . . . . . . . . 19
β’ π‘ β V |
108 | | vex 3449 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
109 | 107, 108 | op2nd 7930 |
. . . . . . . . . . . . . . . . . 18
β’
(2nd ββ¨π‘, πβ©) = π |
110 | 109 | oveq2i 7368 |
. . . . . . . . . . . . . . . . 17
β’
(2β(2nd ββ¨π‘, πβ©)) = (2βπ) |
111 | 107, 108 | op1st 7929 |
. . . . . . . . . . . . . . . . 17
β’
(1st ββ¨π‘, πβ©) = π‘ |
112 | 110, 111 | oveq12i 7369 |
. . . . . . . . . . . . . . . 16
β’
((2β(2nd ββ¨π‘, πβ©)) Β· (1st
ββ¨π‘, πβ©)) = ((2βπ) Β· π‘) |
113 | 106, 112 | eqtrdi 2792 |
. . . . . . . . . . . . . . 15
β’
(β¨π‘, πβ© β (π½ Γ β0) β (πΉββ¨π‘, πβ©) = ((2βπ) Β· π‘)) |
114 | 105, 113 | sylbir 234 |
. . . . . . . . . . . . . 14
β’ ((π‘ β π½ β§ π β β0) β (πΉββ¨π‘, πβ©) = ((2βπ) Β· π‘)) |
115 | 104, 114 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β§ π€ = β¨π‘, πβ©) β (πΉββ¨π‘, πβ©) = ((2βπ) Β· π‘)) |
116 | 100, 115 | eqtr2d 2777 |
. . . . . . . . . . . 12
β’
(((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β§ π€ = β¨π‘, πβ©) β ((2βπ) Β· π‘) = (πΉβπ€)) |
117 | 116 | ex 413 |
. . . . . . . . . . 11
β’ ((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (π‘ β π½ β§ π β (bitsβ(π΄βπ‘)))) β (π€ = β¨π‘, πβ© β ((2βπ) Β· π‘) = (πΉβπ€))) |
118 | 117 | reximdvva 3202 |
. . . . . . . . . 10
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β (βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))π€ = β¨π‘, πβ© β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€))) |
119 | 98, 118 | mpd 15 |
. . . . . . . . 9
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€)) |
120 | | ssrexv 4011 |
. . . . . . . . 9
β’ (π½ β β β
(βπ‘ β π½ βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€))) |
121 | 37, 119, 120 | mpsyl 68 |
. . . . . . . 8
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€)) |
122 | 121 | adantr 481 |
. . . . . . 7
β’ ((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (πΉβπ€) = π΅) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€)) |
123 | | eqeq2 2748 |
. . . . . . . . . 10
β’ ((πΉβπ€) = π΅ β (((2βπ) Β· π‘) = (πΉβπ€) β ((2βπ) Β· π‘) = π΅)) |
124 | 123 | rexbidv 3175 |
. . . . . . . . 9
β’ ((πΉβπ€) = π΅ β (βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€) β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅)) |
125 | 124 | adantl 482 |
. . . . . . . 8
β’ ((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (πΉβπ€) = π΅) β (βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€) β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅)) |
126 | 125 | rexbidv 3175 |
. . . . . . 7
β’ ((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (πΉβπ€) = π΅) β (βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = (πΉβπ€) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅)) |
127 | 122, 126 | mpbid 231 |
. . . . . 6
β’ ((((π΄ β (π β© π
) β§ π΅ β β) β§ π€ β (πβ(bits β (π΄ βΎ π½)))) β§ (πΉβπ€) = π΅) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) |
128 | 127 | r19.29an 3155 |
. . . . 5
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) |
129 | | simp-5l 783 |
. . . . . . . 8
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β π΄ β (π β© π
)) |
130 | | simpllr 774 |
. . . . . . . 8
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β π₯ β π½) |
131 | | simplr 767 |
. . . . . . . . 9
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β π¦ β (bitsβ(π΄βπ₯))) |
132 | 68 | eleq2d 2823 |
. . . . . . . . . . . . . 14
β’ ((π΄ βΎ π½):π½βΆβ0 β (π₯ β dom (π΄ βΎ π½) β π₯ β π½)) |
133 | 67, 132 | syl 17 |
. . . . . . . . . . . . 13
β’ (π΄ β (π β© π
) β (π₯ β dom (π΄ βΎ π½) β π₯ β π½)) |
134 | 133 | biimpar 478 |
. . . . . . . . . . . 12
β’ ((π΄ β (π β© π
) β§ π₯ β π½) β π₯ β dom (π΄ βΎ π½)) |
135 | | fvco 6939 |
. . . . . . . . . . . 12
β’ ((Fun
(π΄ βΎ π½) β§ π₯ β dom (π΄ βΎ π½)) β ((bits β (π΄ βΎ π½))βπ₯) = (bitsβ((π΄ βΎ π½)βπ₯))) |
136 | 65, 134, 135 | syl2an2r 683 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π₯ β π½) β ((bits β (π΄ βΎ π½))βπ₯) = (bitsβ((π΄ βΎ π½)βπ₯))) |
137 | | fvres 6861 |
. . . . . . . . . . . . 13
β’ (π₯ β π½ β ((π΄ βΎ π½)βπ₯) = (π΄βπ₯)) |
138 | 137 | fveq2d 6846 |
. . . . . . . . . . . 12
β’ (π₯ β π½ β (bitsβ((π΄ βΎ π½)βπ₯)) = (bitsβ(π΄βπ₯))) |
139 | 138 | adantl 482 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π₯ β π½) β (bitsβ((π΄ βΎ π½)βπ₯)) = (bitsβ(π΄βπ₯))) |
140 | 136, 139 | eqtrd 2776 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ π₯ β π½) β ((bits β (π΄ βΎ π½))βπ₯) = (bitsβ(π΄βπ₯))) |
141 | 129, 130,
140 | syl2anc 584 |
. . . . . . . . 9
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β ((bits β (π΄ βΎ π½))βπ₯) = (bitsβ(π΄βπ₯))) |
142 | 131, 141 | eleqtrrd 2840 |
. . . . . . . 8
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β π¦ β ((bits β (π΄ βΎ π½))βπ₯)) |
143 | 48 | eleq2d 2823 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β (β¨π₯, π¦β© β (πβ(bits β (π΄ βΎ π½))) β β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))})) |
144 | | opabidw 5481 |
. . . . . . . . . 10
β’
(β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))} β (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))) |
145 | 143, 144 | bitrdi 286 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (β¨π₯, π¦β© β (πβ(bits β (π΄ βΎ π½))) β (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯)))) |
146 | 145 | biimpar 478 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ (π₯ β π½ β§ π¦ β ((bits β (π΄ βΎ π½))βπ₯))) β β¨π₯, π¦β© β (πβ(bits β (π΄ βΎ π½)))) |
147 | 129, 130,
142, 146 | syl12anc 835 |
. . . . . . 7
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β β¨π₯, π¦β© β (πβ(bits β (π΄ βΎ π½)))) |
148 | | simpr 485 |
. . . . . . . 8
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β ((2βπ¦) Β· π₯) = π΅) |
149 | 34 | ad4antr 730 |
. . . . . . . . 9
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β (πβ(bits β (π΄ βΎ π½))) β (π½ Γ
β0)) |
150 | 149, 147 | sseldd 3945 |
. . . . . . . 8
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β β¨π₯, π¦β© β (π½ Γ
β0)) |
151 | | opeq1 4830 |
. . . . . . . . . . . 12
β’ (π‘ = π₯ β β¨π‘, π¦β© = β¨π₯, π¦β©) |
152 | 151 | eleq1d 2822 |
. . . . . . . . . . 11
β’ (π‘ = π₯ β (β¨π‘, π¦β© β (π½ Γ β0) β
β¨π₯, π¦β© β (π½ Γ
β0))) |
153 | 151 | fveq2d 6846 |
. . . . . . . . . . . 12
β’ (π‘ = π₯ β (πΉββ¨π‘, π¦β©) = (πΉββ¨π₯, π¦β©)) |
154 | | oveq2 7365 |
. . . . . . . . . . . 12
β’ (π‘ = π₯ β ((2βπ¦) Β· π‘) = ((2βπ¦) Β· π₯)) |
155 | 153, 154 | eqeq12d 2752 |
. . . . . . . . . . 11
β’ (π‘ = π₯ β ((πΉββ¨π‘, π¦β©) = ((2βπ¦) Β· π‘) β (πΉββ¨π₯, π¦β©) = ((2βπ¦) Β· π₯))) |
156 | 152, 155 | imbi12d 344 |
. . . . . . . . . 10
β’ (π‘ = π₯ β ((β¨π‘, π¦β© β (π½ Γ β0) β (πΉββ¨π‘, π¦β©) = ((2βπ¦) Β· π‘)) β (β¨π₯, π¦β© β (π½ Γ β0) β (πΉββ¨π₯, π¦β©) = ((2βπ¦) Β· π₯)))) |
157 | | opeq2 4831 |
. . . . . . . . . . . . 13
β’ (π = π¦ β β¨π‘, πβ© = β¨π‘, π¦β©) |
158 | 157 | eleq1d 2822 |
. . . . . . . . . . . 12
β’ (π = π¦ β (β¨π‘, πβ© β (π½ Γ β0) β
β¨π‘, π¦β© β (π½ Γ
β0))) |
159 | 157 | fveq2d 6846 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (πΉββ¨π‘, πβ©) = (πΉββ¨π‘, π¦β©)) |
160 | | oveq2 7365 |
. . . . . . . . . . . . . 14
β’ (π = π¦ β (2βπ) = (2βπ¦)) |
161 | 160 | oveq1d 7372 |
. . . . . . . . . . . . 13
β’ (π = π¦ β ((2βπ) Β· π‘) = ((2βπ¦) Β· π‘)) |
162 | 159, 161 | eqeq12d 2752 |
. . . . . . . . . . . 12
β’ (π = π¦ β ((πΉββ¨π‘, πβ©) = ((2βπ) Β· π‘) β (πΉββ¨π‘, π¦β©) = ((2βπ¦) Β· π‘))) |
163 | 158, 162 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π = π¦ β ((β¨π‘, πβ© β (π½ Γ β0) β (πΉββ¨π‘, πβ©) = ((2βπ) Β· π‘)) β (β¨π‘, π¦β© β (π½ Γ β0) β (πΉββ¨π‘, π¦β©) = ((2βπ¦) Β· π‘)))) |
164 | 163, 113 | chvarvv 2002 |
. . . . . . . . . 10
β’
(β¨π‘, π¦β© β (π½ Γ β0) β (πΉββ¨π‘, π¦β©) = ((2βπ¦) Β· π‘)) |
165 | 156, 164 | chvarvv 2002 |
. . . . . . . . 9
β’
(β¨π₯, π¦β© β (π½ Γ β0) β (πΉββ¨π₯, π¦β©) = ((2βπ¦) Β· π₯)) |
166 | | eqeq2 2748 |
. . . . . . . . . 10
β’
(((2βπ¦)
Β· π₯) = π΅ β ((πΉββ¨π₯, π¦β©) = ((2βπ¦) Β· π₯) β (πΉββ¨π₯, π¦β©) = π΅)) |
167 | 166 | biimpa 477 |
. . . . . . . . 9
β’
((((2βπ¦)
Β· π₯) = π΅ β§ (πΉββ¨π₯, π¦β©) = ((2βπ¦) Β· π₯)) β (πΉββ¨π₯, π¦β©) = π΅) |
168 | 165, 167 | sylan2 593 |
. . . . . . . 8
β’
((((2βπ¦)
Β· π₯) = π΅ β§ β¨π₯, π¦β© β (π½ Γ β0)) β (πΉββ¨π₯, π¦β©) = π΅) |
169 | 148, 150,
168 | syl2anc 584 |
. . . . . . 7
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β (πΉββ¨π₯, π¦β©) = π΅) |
170 | | fveqeq2 6851 |
. . . . . . . 8
β’ (π€ = β¨π₯, π¦β© β ((πΉβπ€) = π΅ β (πΉββ¨π₯, π¦β©) = π΅)) |
171 | 170 | rspcev 3581 |
. . . . . . 7
β’
((β¨π₯, π¦β© β (πβ(bits β (π΄ βΎ π½))) β§ (πΉββ¨π₯, π¦β©) = π΅) β βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅) |
172 | 147, 169,
171 | syl2anc 584 |
. . . . . 6
β’
((((((π΄ β
(π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β§ π₯ β π½) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅) |
173 | | oveq2 7365 |
. . . . . . . . . . 11
β’ (π‘ = π₯ β ((2βπ) Β· π‘) = ((2βπ) Β· π₯)) |
174 | 173 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π‘ = π₯ β (((2βπ) Β· π‘) = π΅ β ((2βπ) Β· π₯) = π΅)) |
175 | 160 | oveq1d 7372 |
. . . . . . . . . . 11
β’ (π = π¦ β ((2βπ) Β· π₯) = ((2βπ¦) Β· π₯)) |
176 | 175 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = π¦ β (((2βπ) Β· π₯) = π΅ β ((2βπ¦) Β· π₯) = π΅)) |
177 | 174, 176 | sylan9bb 510 |
. . . . . . . . 9
β’ ((π‘ = π₯ β§ π = π¦) β (((2βπ) Β· π‘) = π΅ β ((2βπ¦) Β· π₯) = π΅)) |
178 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π‘ = π₯ β§ π = π¦) β π‘ = π₯) |
179 | 178 | fveq2d 6846 |
. . . . . . . . . 10
β’ ((π‘ = π₯ β§ π = π¦) β (π΄βπ‘) = (π΄βπ₯)) |
180 | 179 | fveq2d 6846 |
. . . . . . . . 9
β’ ((π‘ = π₯ β§ π = π¦) β (bitsβ(π΄βπ‘)) = (bitsβ(π΄βπ₯))) |
181 | 177, 180 | cbvrexdva2 3324 |
. . . . . . . 8
β’ (π‘ = π₯ β (βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅ β βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) |
182 | 181 | cbvrexvw 3226 |
. . . . . . 7
β’
(βπ‘ β
β βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅ β βπ₯ β β βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) |
183 | | nfv 1917 |
. . . . . . . . . . . . . 14
β’
β²π¦ π΄ β (π β© π
) |
184 | | nfv 1917 |
. . . . . . . . . . . . . . 15
β’
β²π¦ π₯ β β |
185 | | nfre1 3268 |
. . . . . . . . . . . . . . 15
β’
β²π¦βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅ |
186 | 184, 185 | nfan 1902 |
. . . . . . . . . . . . . 14
β’
β²π¦(π₯ β β β§
βπ¦ β
(bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) |
187 | 183, 186 | nfan 1902 |
. . . . . . . . . . . . 13
β’
β²π¦(π΄ β (π β© π
) β§ (π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) |
188 | | simplr 767 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β π₯ β β) |
189 | 62 | ffvelcdmda 7035 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β (π β© π
) β§ π₯ β β) β (π΄βπ₯) β
β0) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β (π΄βπ₯) β
β0) |
191 | | elnn0 12415 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄βπ₯) β β0 β ((π΄βπ₯) β β β¨ (π΄βπ₯) = 0)) |
192 | 190, 191 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β ((π΄βπ₯) β β β¨ (π΄βπ₯) = 0)) |
193 | | n0i 4293 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (bitsβ(π΄βπ₯)) β Β¬ (bitsβ(π΄βπ₯)) = β
) |
194 | 193 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β Β¬ (bitsβ(π΄βπ₯)) = β
) |
195 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄βπ₯) = 0 β (bitsβ(π΄βπ₯)) = (bitsβ0)) |
196 | | 0bits 16319 |
. . . . . . . . . . . . . . . . . . . 20
β’
(bitsβ0) = β
|
197 | 195, 196 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄βπ₯) = 0 β (bitsβ(π΄βπ₯)) = β
) |
198 | 194, 197 | nsyl 140 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β Β¬ (π΄βπ₯) = 0) |
199 | 192, 198 | olcnd 875 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β (π΄βπ₯) β β) |
200 | 58 | simp3bi 1147 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β π½) |
201 | 200 | sselda 3944 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ β (π β© π
) β§ π β (β‘π΄ β β)) β π β π½) |
202 | | breq2 5109 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π β (2 β₯ π§ β 2 β₯ π)) |
203 | 202 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = π β (Β¬ 2 β₯ π§ β Β¬ 2 β₯ π)) |
204 | 203, 4 | elrab2 3648 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π½ β (π β β β§ Β¬ 2 β₯ π)) |
205 | 204 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π½ β Β¬ 2 β₯ π) |
206 | 201, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β (π β© π
) β§ π β (β‘π΄ β β)) β Β¬ 2 β₯
π) |
207 | 206 | ralrimiva 3143 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β (π β© π
) β βπ β (β‘π΄ β β) Β¬ 2 β₯ π) |
208 | | ffn 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄:ββΆβ0 β
π΄ Fn
β) |
209 | | elpreima 7008 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄ Fn β β (π β (β‘π΄ β β) β (π β β β§ (π΄βπ) β β))) |
210 | 62, 208, 209 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ β (π β© π
) β (π β (β‘π΄ β β) β (π β β β§ (π΄βπ) β β))) |
211 | 210 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β (π β© π
) β ((π β (β‘π΄ β β) β Β¬ 2 β₯
π) β ((π β β β§ (π΄βπ) β β) β Β¬ 2 β₯
π))) |
212 | | impexp 451 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ (π΄βπ) β β) β Β¬ 2 β₯
π) β (π β β β ((π΄βπ) β β β Β¬ 2 β₯ π))) |
213 | 211, 212 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β (π β© π
) β ((π β (β‘π΄ β β) β Β¬ 2 β₯
π) β (π β β β ((π΄βπ) β β β Β¬ 2 β₯ π)))) |
214 | 213 | ralbidv2 3170 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β (π β© π
) β (βπ β (β‘π΄ β β) Β¬ 2 β₯ π β βπ β β ((π΄βπ) β β β Β¬ 2 β₯ π))) |
215 | 207, 214 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β (π β© π
) β βπ β β ((π΄βπ) β β β Β¬ 2 β₯ π)) |
216 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β (π΄βπ₯) = (π΄βπ)) |
217 | 216 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β ((π΄βπ₯) β β β (π΄βπ) β β)) |
218 | | breq2 5109 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β (2 β₯ π₯ β 2 β₯ π)) |
219 | 218 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β (Β¬ 2 β₯ π₯ β Β¬ 2 β₯ π)) |
220 | 217, 219 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β (((π΄βπ₯) β β β Β¬ 2 β₯ π₯) β ((π΄βπ) β β β Β¬ 2 β₯ π))) |
221 | 220 | cbvralvw 3225 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ₯ β
β ((π΄βπ₯) β β β Β¬ 2
β₯ π₯) β
βπ β β
((π΄βπ) β β β Β¬ 2
β₯ π)) |
222 | 215, 221 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β (π β© π
) β βπ₯ β β ((π΄βπ₯) β β β Β¬ 2 β₯ π₯)) |
223 | 222 | r19.21bi 3234 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β (π β© π
) β§ π₯ β β) β ((π΄βπ₯) β β β Β¬ 2 β₯ π₯)) |
224 | 223 | imp 407 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ (π΄βπ₯) β β) β Β¬ 2 β₯
π₯) |
225 | 199, 224 | syldan 591 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β Β¬ 2 β₯ π₯) |
226 | | breq2 5109 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π₯ β (2 β₯ π§ β 2 β₯ π₯)) |
227 | 226 | notbid 317 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π₯ β (Β¬ 2 β₯ π§ β Β¬ 2 β₯ π₯)) |
228 | 227, 4 | elrab2 3648 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π½ β (π₯ β β β§ Β¬ 2 β₯ π₯)) |
229 | 188, 225,
228 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β (π β© π
) β§ π₯ β β) β§ π¦ β (bitsβ(π΄βπ₯))) β π₯ β π½) |
230 | 229 | adantlrr 719 |
. . . . . . . . . . . . . 14
β’ (((π΄ β (π β© π
) β§ (π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) β§ π¦ β (bitsβ(π΄βπ₯))) β π₯ β π½) |
231 | 230 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (π β© π
) β§ (π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) β§ π¦ β (bitsβ(π΄βπ₯))) β§ ((2βπ¦) Β· π₯) = π΅) β π₯ β π½) |
232 | | simprr 771 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π β© π
) β§ (π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) β βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) |
233 | 187, 231,
232 | r19.29af 3251 |
. . . . . . . . . . . 12
β’ ((π΄ β (π β© π
) β§ (π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) β π₯ β π½) |
234 | 233, 232 | jca 512 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ (π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) β (π₯ β π½ β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) |
235 | 234 | ex 413 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β ((π₯ β β β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) β (π₯ β π½ β§ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅))) |
236 | 235 | reximdv2 3161 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (βπ₯ β β βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅ β βπ₯ β π½ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅)) |
237 | 236 | imp 407 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ βπ₯ β β βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) β βπ₯ β π½ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) |
238 | 237 | adantlr 713 |
. . . . . . 7
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ βπ₯ β β βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) β βπ₯ β π½ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) |
239 | 182, 238 | sylan2b 594 |
. . . . . 6
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β βπ₯ β π½ βπ¦ β (bitsβ(π΄βπ₯))((2βπ¦) Β· π₯) = π΅) |
240 | 172, 239 | r19.29vva 3207 |
. . . . 5
β’ (((π΄ β (π β© π
) β§ π΅ β β) β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅) β βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅) |
241 | 128, 240 | impbida 799 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π΅ β β) β (βπ€ β (πβ(bits β (π΄ βΎ π½)))(πΉβπ€) = π΅ β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅)) |
242 | 36, 241 | bitrd 278 |
. . 3
β’ ((π΄ β (π β© π
) β§ π΅ β β) β (π΅ β (πΉ β (πβ(bits β (π΄ βΎ π½)))) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅)) |
243 | 242 | ifbid 4509 |
. 2
β’ ((π΄ β (π β© π
) β§ π΅ β β) β if(π΅ β (πΉ β (πβ(bits β (π΄ βΎ π½)))), 1, 0) = if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅, 1, 0)) |
244 | 13, 23, 243 | 3eqtrd 2780 |
1
β’ ((π΄ β (π β© π
) β§ π΅ β β) β ((πΊβπ΄)βπ΅) = if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅, 1, 0)) |