Step | Hyp | Ref
| Expression |
1 | | df-rab 3411 |
. . . . . 6
β’ {π β (β0
βm (1...π))
β£ βπ β
β0 [π / π£][π / π’]π} = {π β£ (π β (β0
βm (1...π))
β§ βπ β
β0 [π / π£][π / π’]π)} |
2 | | dfsbcq 3746 |
. . . . . . . . . . 11
β’ (π = π β ([π / π£][π / π’]π β [π / π£][π / π’]π)) |
3 | 2 | cbvrexvw 3229 |
. . . . . . . . . 10
β’
(βπ β
β0 [π / π£][π / π’]π β βπ β β0 [π / π£][π / π’]π) |
4 | 3 | anbi2i 624 |
. . . . . . . . 9
β’ ((π β (β0
βm (1...π))
β§ βπ β
β0 [π / π£][π / π’]π) β (π β (β0
βm (1...π))
β§ βπ β
β0 [π / π£][π / π’]π)) |
5 | | r19.42v 3188 |
. . . . . . . . 9
β’
(βπ β
β0 (π
β (β0 βm (1...π)) β§ [π / π£][π / π’]π) β (π β (β0
βm (1...π))
β§ βπ β
β0 [π / π£][π / π’]π)) |
6 | 4, 5 | bitr4i 278 |
. . . . . . . 8
β’ ((π β (β0
βm (1...π))
β§ βπ β
β0 [π / π£][π / π’]π) β βπ β β0 (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) |
7 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β π β
β0) |
8 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β π β (β0
βm (1...π))) |
9 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β π β β0) |
10 | | rexrabdioph.1 |
. . . . . . . . . . . . . 14
β’ π = (π + 1) |
11 | 10 | mapfzcons 41068 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π β
(β0 βm (1...π)) β§ π β β0) β (π βͺ {β¨π, πβ©}) β (β0
βm (1...π))) |
12 | 7, 8, 9, 11 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β (π βͺ {β¨π, πβ©}) β (β0
βm (1...π))) |
13 | 12 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) β (π βͺ {β¨π, πβ©}) β (β0
βm (1...π))) |
14 | 10 | mapfzcons2 41071 |
. . . . . . . . . . . . . . . 16
β’ ((π β (β0
βm (1...π))
β§ π β
β0) β ((π βͺ {β¨π, πβ©})βπ) = π) |
15 | 8, 9, 14 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β ((π βͺ {β¨π, πβ©})βπ) = π) |
16 | 15 | eqcomd 2743 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β π = ((π βͺ {β¨π, πβ©})βπ)) |
17 | 10 | mapfzcons1 41069 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β0
βm (1...π))
β ((π βͺ
{β¨π, πβ©}) βΎ (1...π)) = π) |
18 | 17 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β ((π βͺ {β¨π, πβ©}) βΎ (1...π)) = π) |
19 | 18 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β π = ((π βͺ {β¨π, πβ©}) βΎ (1...π))) |
20 | 19 | sbceq1d 3749 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β ([π / π’]π β [((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π)) |
21 | 16, 20 | sbceqbid 3751 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β ([π / π£][π / π’]π β [((π βͺ {β¨π, πβ©})βπ) / π£][((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π)) |
22 | 21 | biimpd 228 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
β0) β§ π β (β0
βm (1...π))) β ([π / π£][π / π’]π β [((π βͺ {β¨π, πβ©})βπ) / π£][((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π)) |
23 | 22 | impr 456 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) β [((π βͺ {β¨π, πβ©})βπ) / π£][((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π) |
24 | 19 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) β π = ((π βͺ {β¨π, πβ©}) βΎ (1...π))) |
25 | | fveq1 6846 |
. . . . . . . . . . . . . 14
β’ (π = (π βͺ {β¨π, πβ©}) β (πβπ) = ((π βͺ {β¨π, πβ©})βπ)) |
26 | | reseq1 5936 |
. . . . . . . . . . . . . . 15
β’ (π = (π βͺ {β¨π, πβ©}) β (π βΎ (1...π)) = ((π βͺ {β¨π, πβ©}) βΎ (1...π))) |
27 | 26 | sbceq1d 3749 |
. . . . . . . . . . . . . 14
β’ (π = (π βͺ {β¨π, πβ©}) β ([(π βΎ (1...π)) / π’]π β [((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π)) |
28 | 25, 27 | sbceqbid 3751 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ {β¨π, πβ©}) β ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β [((π βͺ {β¨π, πβ©})βπ) / π£][((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π)) |
29 | 26 | eqeq2d 2748 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ {β¨π, πβ©}) β (π = (π βΎ (1...π)) β π = ((π βͺ {β¨π, πβ©}) βΎ (1...π)))) |
30 | 28, 29 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = (π βͺ {β¨π, πβ©}) β (([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π))) β ([((π βͺ {β¨π, πβ©})βπ) / π£][((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π β§ π = ((π βͺ {β¨π, πβ©}) βΎ (1...π))))) |
31 | 30 | rspcev 3584 |
. . . . . . . . . . 11
β’ (((π βͺ {β¨π, πβ©}) β (β0
βm (1...π))
β§ ([((π βͺ
{β¨π, πβ©})βπ) / π£][((π βͺ {β¨π, πβ©}) βΎ (1...π)) / π’]π β§ π = ((π βͺ {β¨π, πβ©}) βΎ (1...π)))) β βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) |
32 | 13, 23, 24, 31 | syl12anc 836 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β
β0) β§ (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) β βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) |
33 | 32 | rexlimdva2 3155 |
. . . . . . . . 9
β’ (π β β0
β (βπ β
β0 (π
β (β0 βm (1...π)) β§ [π / π£][π / π’]π) β βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π))))) |
34 | | elmapi 8794 |
. . . . . . . . . . . . 13
β’ (π β (β0
βm (1...π))
β π:(1...π)βΆβ0) |
35 | | nn0p1nn 12459 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β) |
36 | 10, 35 | eqeltrid 2842 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
37 | | elfz1end 13478 |
. . . . . . . . . . . . . 14
β’ (π β β β π β (1...π)) |
38 | 36, 37 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β (1...π)) |
39 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((π:(1...π)βΆβ0 β§ π β (1...π)) β (πβπ) β
β0) |
40 | 34, 38, 39 | syl2anr 598 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β
(β0 βm (1...π))) β (πβπ) β
β0) |
41 | 40 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β (πβπ) β
β0) |
42 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β π = (π βΎ (1...π))) |
43 | 10 | mapfzcons1cl 41070 |
. . . . . . . . . . . . 13
β’ (π β (β0
βm (1...π))
β (π βΎ
(1...π)) β
(β0 βm (1...π))) |
44 | 43 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β (π βΎ (1...π)) β (β0
βm (1...π))) |
45 | 42, 44 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β π β (β0
βm (1...π))) |
46 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β [(πβπ) / π£][(π βΎ (1...π)) / π’]π) |
47 | | dfsbcq 3746 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (1...π)) β ([π / π’]π β [(π βΎ (1...π)) / π’]π)) |
48 | 47 | sbcbidv 3803 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (1...π)) β ([(πβπ) / π£][π / π’]π β [(πβπ) / π£][(π βΎ (1...π)) / π’]π)) |
49 | 48 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β ([(πβπ) / π£][π / π’]π β [(πβπ) / π£][(π βΎ (1...π)) / π’]π)) |
50 | 46, 49 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β [(πβπ) / π£][π / π’]π) |
51 | | dfsbcq 3746 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ([π / π£][π / π’]π β [(πβπ) / π£][π / π’]π)) |
52 | 51 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((π β (β0
βm (1...π))
β§ [π / π£][π / π’]π) β (π β (β0
βm (1...π))
β§ [(πβπ) / π£][π / π’]π))) |
53 | 52 | rspcev 3584 |
. . . . . . . . . . 11
β’ (((πβπ) β β0 β§ (π β (β0
βm (1...π))
β§ [(πβπ) / π£][π / π’]π)) β βπ β β0 (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) |
54 | 41, 45, 50, 53 | syl12anc 836 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β
(β0 βm (1...π))) β§ ([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) β βπ β β0 (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π)) |
55 | 54 | rexlimdva2 3155 |
. . . . . . . . 9
β’ (π β β0
β (βπ β
(β0 βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π))) β βπ β β0 (π β (β0
βm (1...π))
β§ [π / π£][π / π’]π))) |
56 | 33, 55 | impbid 211 |
. . . . . . . 8
β’ (π β β0
β (βπ β
β0 (π
β (β0 βm (1...π)) β§ [π / π£][π / π’]π) β βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π))))) |
57 | 6, 56 | bitrid 283 |
. . . . . . 7
β’ (π β β0
β ((π β
(β0 βm (1...π)) β§ βπ β β0 [π / π£][π / π’]π) β βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π))))) |
58 | 57 | abbidv 2806 |
. . . . . 6
β’ (π β β0
β {π β£ (π β (β0
βm (1...π))
β§ βπ β
β0 [π / π£][π / π’]π)} = {π β£ βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))}) |
59 | 1, 58 | eqtrid 2789 |
. . . . 5
β’ (π β β0
β {π β
(β0 βm (1...π)) β£ βπ β β0 [π / π£][π / π’]π} = {π β£ βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))}) |
60 | | nfcv 2908 |
. . . . . 6
β’
β²π’(β0 βm
(1...π)) |
61 | | nfcv 2908 |
. . . . . 6
β’
β²π(β0 βm
(1...π)) |
62 | | nfv 1918 |
. . . . . 6
β’
β²πβπ£ β β0
π |
63 | | nfcv 2908 |
. . . . . . 7
β’
β²π’β0 |
64 | | nfcv 2908 |
. . . . . . . 8
β’
β²π’π |
65 | | nfsbc1v 3764 |
. . . . . . . 8
β’
β²π’[π / π’]π |
66 | 64, 65 | nfsbcw 3766 |
. . . . . . 7
β’
β²π’[π / π£][π / π’]π |
67 | 63, 66 | nfrexw 3299 |
. . . . . 6
β’
β²π’βπ β β0
[π / π£][π / π’]π |
68 | | sbceq1a 3755 |
. . . . . . . 8
β’ (π’ = π β (π β [π / π’]π)) |
69 | 68 | rexbidv 3176 |
. . . . . . 7
β’ (π’ = π β (βπ£ β β0 π β βπ£ β β0 [π / π’]π)) |
70 | | nfv 1918 |
. . . . . . . 8
β’
β²π[π / π’]π |
71 | | nfsbc1v 3764 |
. . . . . . . 8
β’
β²π£[π / π£][π / π’]π |
72 | | sbceq1a 3755 |
. . . . . . . 8
β’ (π£ = π β ([π / π’]π β [π / π£][π / π’]π)) |
73 | 70, 71, 72 | cbvrexw 3293 |
. . . . . . 7
β’
(βπ£ β
β0 [π / π’]π β βπ β β0 [π / π£][π / π’]π) |
74 | 69, 73 | bitrdi 287 |
. . . . . 6
β’ (π’ = π β (βπ£ β β0 π β βπ β β0 [π / π£][π / π’]π)) |
75 | 60, 61, 62, 67, 74 | cbvrabw 3442 |
. . . . 5
β’ {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 π} =
{π β
(β0 βm (1...π)) β£ βπ β β0 [π / π£][π / π’]π} |
76 | | fveq1 6846 |
. . . . . . . 8
β’ (π‘ = π β (π‘βπ) = (πβπ)) |
77 | | reseq1 5936 |
. . . . . . . . 9
β’ (π‘ = π β (π‘ βΎ (1...π)) = (π βΎ (1...π))) |
78 | 77 | sbceq1d 3749 |
. . . . . . . 8
β’ (π‘ = π β ([(π‘ βΎ (1...π)) / π’]π β [(π βΎ (1...π)) / π’]π)) |
79 | 76, 78 | sbceqbid 3751 |
. . . . . . 7
β’ (π‘ = π β ([(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π β [(πβπ) / π£][(π βΎ (1...π)) / π’]π)) |
80 | 79 | rexrab 3659 |
. . . . . 6
β’
(βπ β
{π‘ β
(β0 βm (1...π)) β£ [(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π}π = (π βΎ (1...π)) β βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))) |
81 | 80 | abbii 2807 |
. . . . 5
β’ {π β£ βπ β {π‘ β (β0
βm (1...π))
β£ [(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π}π = (π βΎ (1...π))} = {π β£ βπ β (β0
βm (1...π))([(πβπ) / π£][(π βΎ (1...π)) / π’]π β§ π = (π βΎ (1...π)))} |
82 | 59, 75, 81 | 3eqtr4g 2802 |
. . . 4
β’ (π β β0
β {π’ β
(β0 βm (1...π)) β£ βπ£ β β0 π} = {π β£ βπ β {π‘ β (β0
βm (1...π))
β£ [(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π}π = (π βΎ (1...π))}) |
83 | | fvex 6860 |
. . . . . . . 8
β’ (π‘βπ) β V |
84 | | vex 3452 |
. . . . . . . . 9
β’ π‘ β V |
85 | 84 | resex 5990 |
. . . . . . . 8
β’ (π‘ βΎ (1...π)) β V |
86 | | rexrabdioph.2 |
. . . . . . . . 9
β’ (π£ = (π‘βπ) β (π β π)) |
87 | | rexrabdioph.3 |
. . . . . . . . 9
β’ (π’ = (π‘ βΎ (1...π)) β (π β π)) |
88 | 86, 87 | sylan9bb 511 |
. . . . . . . 8
β’ ((π£ = (π‘βπ) β§ π’ = (π‘ βΎ (1...π))) β (π β π)) |
89 | 83, 85, 88 | sbc2ie 3827 |
. . . . . . 7
β’
([(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π β π) |
90 | 89 | rabbii 3416 |
. . . . . 6
β’ {π‘ β (β0
βm (1...π))
β£ [(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π} = {π‘ β (β0
βm (1...π))
β£ π} |
91 | 90 | rexeqi 3315 |
. . . . 5
β’
(βπ β
{π‘ β
(β0 βm (1...π)) β£ [(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π}π = (π βΎ (1...π)) β βπ β {π‘ β (β0
βm (1...π))
β£ π}π = (π βΎ (1...π))) |
92 | 91 | abbii 2807 |
. . . 4
β’ {π β£ βπ β {π‘ β (β0
βm (1...π))
β£ [(π‘βπ) / π£][(π‘ βΎ (1...π)) / π’]π}π = (π βΎ (1...π))} = {π β£ βπ β {π‘ β (β0
βm (1...π))
β£ π}π = (π βΎ (1...π))} |
93 | 82, 92 | eqtrdi 2793 |
. . 3
β’ (π β β0
β {π’ β
(β0 βm (1...π)) β£ βπ£ β β0 π} = {π β£ βπ β {π‘ β (β0
βm (1...π))
β£ π}π = (π βΎ (1...π))}) |
94 | 93 | adantr 482 |
. 2
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π)) β£ π} β (Diophβπ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 π} =
{π β£ βπ β {π‘ β (β0
βm (1...π))
β£ π}π = (π βΎ (1...π))}) |
95 | | simpl 484 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π)) β£ π} β (Diophβπ)) β π β
β0) |
96 | | nn0z 12531 |
. . . . . 6
β’ (π β β0
β π β
β€) |
97 | | uzid 12785 |
. . . . . 6
β’ (π β β€ β π β
(β€β₯βπ)) |
98 | | peano2uz 12833 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
99 | 96, 97, 98 | 3syl 18 |
. . . . 5
β’ (π β β0
β (π + 1) β
(β€β₯βπ)) |
100 | 10, 99 | eqeltrid 2842 |
. . . 4
β’ (π β β0
β π β
(β€β₯βπ)) |
101 | 100 | adantr 482 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π)) β£ π} β (Diophβπ)) β π β (β€β₯βπ)) |
102 | | simpr 486 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π)) β£ π} β (Diophβπ)) β {π‘ β (β0
βm (1...π))
β£ π} β
(Diophβπ)) |
103 | | diophrex 41127 |
. . 3
β’ ((π β β0
β§ π β
(β€β₯βπ) β§ {π‘ β (β0
βm (1...π))
β£ π} β
(Diophβπ)) β
{π β£ βπ β {π‘ β (β0
βm (1...π))
β£ π}π = (π βΎ (1...π))} β (Diophβπ)) |
104 | 95, 101, 102, 103 | syl3anc 1372 |
. 2
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π)) β£ π} β (Diophβπ)) β {π β£ βπ β {π‘ β (β0
βm (1...π))
β£ π}π = (π βΎ (1...π))} β (Diophβπ)) |
105 | 94, 104 | eqeltrd 2838 |
1
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π)) β£ π} β (Diophβπ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 π} β
(Diophβπ)) |