Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . 5
β’ 2 β
β |
2 | 1 | a1i 11 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β 2 β
β) |
3 | | bitsss 16313 |
. . . . 5
β’
(bitsβ(π΄βπ‘)) β
β0 |
4 | | simprr 772 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β π β (bitsβ(π΄βπ‘))) |
5 | 3, 4 | sselid 3947 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β π β β0) |
6 | 2, 5 | reexpcld 14075 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (2βπ) β β) |
7 | | simprl 770 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β π‘ β β) |
8 | 7 | nnred 12175 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β π‘ β β) |
9 | 6, 8 | remulcld 11192 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((2βπ) Β· π‘) β β) |
10 | | eulerpartlems.r |
. . . . . . . 8
β’ π
= {π β£ (β‘π β β) β
Fin} |
11 | | eulerpartlems.s |
. . . . . . . 8
β’ π = (π β ((β0
βm β) β© π
) β¦ Ξ£π β β ((πβπ) Β· π)) |
12 | 10, 11 | eulerpartlemelr 32997 |
. . . . . . 7
β’ (π΄ β ((β0
βm β) β© π
) β (π΄:ββΆβ0 β§
(β‘π΄ β β) β
Fin)) |
13 | 12 | simpld 496 |
. . . . . 6
β’ (π΄ β ((β0
βm β) β© π
) β π΄:ββΆβ0) |
14 | 13 | ffvelcdmda 7040 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β (π΄βπ‘) β
β0) |
15 | 14 | adantrr 716 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (π΄βπ‘) β
β0) |
16 | 15 | nn0red 12481 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (π΄βπ‘) β β) |
17 | 16, 8 | remulcld 11192 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((π΄βπ‘) Β· π‘) β β) |
18 | 10, 11 | eulerpartlemsf 32999 |
. . . . 5
β’ π:((β0
βm β) β© π
)βΆβ0 |
19 | 18 | ffvelcdmi 7039 |
. . . 4
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) β
β0) |
20 | 19 | adantr 482 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (πβπ΄) β
β0) |
21 | 20 | nn0red 12481 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (πβπ΄) β β) |
22 | 14 | nn0red 12481 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β (π΄βπ‘) β β) |
23 | 22 | adantrr 716 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (π΄βπ‘) β β) |
24 | 7 | nnrpd 12962 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β π‘ β β+) |
25 | 24 | rprege0d 12971 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (π‘ β β β§ 0 β€ π‘)) |
26 | | bitsfi 16324 |
. . . . . 6
β’ ((π΄βπ‘) β β0 β
(bitsβ(π΄βπ‘)) β Fin) |
27 | 15, 26 | syl 17 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (bitsβ(π΄βπ‘)) β Fin) |
28 | 1 | a1i 11 |
. . . . . 6
β’ (((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β§ π β (bitsβ(π΄βπ‘))) β 2 β β) |
29 | 3 | a1i 11 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (bitsβ(π΄βπ‘)) β
β0) |
30 | 29 | sselda 3949 |
. . . . . 6
β’ (((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β§ π β (bitsβ(π΄βπ‘))) β π β β0) |
31 | 28, 30 | reexpcld 14075 |
. . . . 5
β’ (((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β§ π β (bitsβ(π΄βπ‘))) β (2βπ) β β) |
32 | | 0le2 12262 |
. . . . . . 7
β’ 0 β€
2 |
33 | 32 | a1i 11 |
. . . . . 6
β’ (((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β§ π β (bitsβ(π΄βπ‘))) β 0 β€ 2) |
34 | 28, 30, 33 | expge0d 14076 |
. . . . 5
β’ (((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β§ π β (bitsβ(π΄βπ‘))) β 0 β€ (2βπ)) |
35 | 4 | snssd 4774 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β {π} β (bitsβ(π΄βπ‘))) |
36 | 27, 31, 34, 35 | fsumless 15688 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β Ξ£π β {π} (2βπ) β€ Ξ£π β (bitsβ(π΄βπ‘))(2βπ)) |
37 | 6 | recnd 11190 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (2βπ) β β) |
38 | | oveq2 7370 |
. . . . . 6
β’ (π = π β (2βπ) = (2βπ)) |
39 | 38 | sumsn 15638 |
. . . . 5
β’ ((π β (bitsβ(π΄βπ‘)) β§ (2βπ) β β) β Ξ£π β {π} (2βπ) = (2βπ)) |
40 | 4, 37, 39 | syl2anc 585 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β Ξ£π β {π} (2βπ) = (2βπ)) |
41 | | bitsinv1 16329 |
. . . . 5
β’ ((π΄βπ‘) β β0 β
Ξ£π β
(bitsβ(π΄βπ‘))(2βπ) = (π΄βπ‘)) |
42 | 15, 41 | syl 17 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β Ξ£π β (bitsβ(π΄βπ‘))(2βπ) = (π΄βπ‘)) |
43 | 36, 40, 42 | 3brtr3d 5141 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β (2βπ) β€ (π΄βπ‘)) |
44 | | lemul1a 12016 |
. . 3
β’
((((2βπ) β
β β§ (π΄βπ‘) β β β§ (π‘ β β β§ 0 β€ π‘)) β§ (2βπ) β€ (π΄βπ‘)) β ((2βπ) Β· π‘) β€ ((π΄βπ‘) Β· π‘)) |
45 | 6, 23, 25, 43, 44 | syl31anc 1374 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((2βπ) Β· π‘) β€ ((π΄βπ‘) Β· π‘)) |
46 | | fzfid 13885 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (1...(πβπ΄))) β (1...(πβπ΄)) β Fin) |
47 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β (1...(πβπ΄)) β π β β) |
48 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((π΄:ββΆβ0 β§
π β β) β
(π΄βπ) β
β0) |
49 | 13, 47, 48 | syl2an 597 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β (π΄βπ) β
β0) |
50 | 49 | nn0red 12481 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β (π΄βπ) β β) |
51 | 47 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β π β β) |
52 | 51 | nnred 12175 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β π β β) |
53 | 50, 52 | remulcld 11192 |
. . . . . . . 8
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β ((π΄βπ) Β· π) β β) |
54 | 53 | adantlr 714 |
. . . . . . 7
β’ (((π΄ β ((β0
βm β) β© π
) β§ π‘ β (1...(πβπ΄))) β§ π β (1...(πβπ΄))) β ((π΄βπ) Β· π) β β) |
55 | 49 | nn0ge0d 12483 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β 0 β€ (π΄βπ)) |
56 | | 0red 11165 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β 0 β
β) |
57 | 51 | nngt0d 12209 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β 0 < π) |
58 | 56, 52, 57 | ltled 11310 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β 0 β€ π) |
59 | 50, 52, 55, 58 | mulge0d 11739 |
. . . . . . . 8
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β 0 β€ ((π΄βπ) Β· π)) |
60 | 59 | adantlr 714 |
. . . . . . 7
β’ (((π΄ β ((β0
βm β) β© π
) β§ π‘ β (1...(πβπ΄))) β§ π β (1...(πβπ΄))) β 0 β€ ((π΄βπ) Β· π)) |
61 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π‘ β (π΄βπ) = (π΄βπ‘)) |
62 | | id 22 |
. . . . . . . 8
β’ (π = π‘ β π = π‘) |
63 | 61, 62 | oveq12d 7380 |
. . . . . . 7
β’ (π = π‘ β ((π΄βπ) Β· π) = ((π΄βπ‘) Β· π‘)) |
64 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (1...(πβπ΄))) β π‘ β (1...(πβπ΄))) |
65 | 46, 54, 60, 63, 64 | fsumge1 15689 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (1...(πβπ΄))) β ((π΄βπ‘) Β· π‘) β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
66 | 65 | adantlr 714 |
. . . . 5
β’ (((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β§ π‘ β (1...(πβπ΄))) β ((π΄βπ‘) Β· π‘) β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
67 | | eldif 3925 |
. . . . . . 7
β’ (π‘ β (β β
(1...(πβπ΄))) β (π‘ β β β§ Β¬ π‘ β (1...(πβπ΄)))) |
68 | | nndiffz1 31731 |
. . . . . . . . . . . . . 14
β’ ((πβπ΄) β β0 β (β
β (1...(πβπ΄))) =
(β€β₯β((πβπ΄) + 1))) |
69 | 68 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ ((πβπ΄) β β0 β (π‘ β (β β
(1...(πβπ΄))) β π‘ β (β€β₯β((πβπ΄) + 1)))) |
70 | 19, 69 | syl 17 |
. . . . . . . . . . . 12
β’ (π΄ β ((β0
βm β) β© π
) β (π‘ β (β β (1...(πβπ΄))) β π‘ β (β€β₯β((πβπ΄) + 1)))) |
71 | 70 | pm5.32i 576 |
. . . . . . . . . . 11
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (π΄ β ((β0
βm β) β© π
) β§ π‘ β (β€β₯β((πβπ΄) + 1)))) |
72 | 10, 11 | eulerpartlems 33000 |
. . . . . . . . . . 11
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β€β₯β((πβπ΄) + 1))) β (π΄βπ‘) = 0) |
73 | 71, 72 | sylbi 216 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (π΄βπ‘) = 0) |
74 | 73 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β ((π΄βπ‘) Β· π‘) = (0 Β· π‘)) |
75 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β π‘ β (β β (1...(πβπ΄)))) |
76 | 75 | eldifad 3927 |
. . . . . . . . . . 11
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β π‘ β β) |
77 | 76 | nncnd 12176 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β π‘ β β) |
78 | 77 | mul02d 11360 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (0 Β· π‘) = 0) |
79 | 74, 78 | eqtrd 2777 |
. . . . . . . 8
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β ((π΄βπ‘) Β· π‘) = 0) |
80 | | fzfid 13885 |
. . . . . . . . . 10
β’ (π΄ β ((β0
βm β) β© π
) β (1...(πβπ΄)) β Fin) |
81 | 80, 53, 59 | fsumge0 15687 |
. . . . . . . . 9
β’ (π΄ β ((β0
βm β) β© π
) β 0 β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
82 | 81 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β 0 β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
83 | 79, 82 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β ((π΄βπ‘) Β· π‘) β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
84 | 67, 83 | sylan2br 596 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ Β¬ π‘ β (1...(πβπ΄)))) β ((π΄βπ‘) Β· π‘) β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
85 | 84 | anassrs 469 |
. . . . 5
β’ (((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β§ Β¬ π‘ β (1...(πβπ΄))) β ((π΄βπ‘) Β· π‘) β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
86 | 66, 85 | pm2.61dan 812 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β ((π΄βπ‘) Β· π‘) β€ Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
87 | 10, 11 | eulerpartlemsv3 33001 |
. . . . 5
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
88 | 87 | adantr 482 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β (πβπ΄) = Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |
89 | 86, 88 | breqtrrd 5138 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β ((π΄βπ‘) Β· π‘) β€ (πβπ΄)) |
90 | 89 | adantrr 716 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((π΄βπ‘) Β· π‘) β€ (πβπ΄)) |
91 | 9, 17, 21, 45, 90 | letrd 11319 |
1
β’ ((π΄ β ((β0
βm β) β© π
) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((2βπ) Β· π‘) β€ (πβπ΄)) |