Step | Hyp | Ref
| Expression |
1 | | elmapi 8839 |
. . . . 5
β’ (π β (β0
βm (1...3)) β π:(1...3)βΆβ0) |
2 | | 3nn 12287 |
. . . . . 6
β’ 3 β
β |
3 | 2 | jm2.27dlem3 41735 |
. . . . 5
β’ 3 β
(1...3) |
4 | | ffvelcdm 7080 |
. . . . 5
β’ ((π:(1...3)βΆβ0 β§ 3
β (1...3)) β (πβ3) β
β0) |
5 | 1, 3, 4 | sylancl 586 |
. . . 4
β’ (π β (β0
βm (1...3)) β (πβ3) β
β0) |
6 | | expdiophlem1 41745 |
. . . 4
β’ ((πβ3) β
β0 β ((((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2))) β βπ β β0 βπ β β0
βπ β
β0 (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))))) |
7 | 5, 6 | syl 17 |
. . 3
β’ (π β (β0
βm (1...3)) β ((((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2))) β βπ β β0 βπ β β0
βπ β
β0 (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))))) |
8 | 7 | rabbiia 3436 |
. 2
β’ {π β (β0
βm (1...3)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))} = {π β (β0
βm (1...3)) β£ βπ β β0 βπ β β0
βπ β
β0 (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))))} |
9 | | 3nn0 12486 |
. . 3
β’ 3 β
β0 |
10 | | fvex 6901 |
. . . . . . . . 9
β’ (πβ5) β
V |
11 | | fvex 6901 |
. . . . . . . . 9
β’ (πβ6) β
V |
12 | | eqeq1 2736 |
. . . . . . . . . . . . . 14
β’ (π = (πβ5) β (π = (π Yrm (πβ2)) β (πβ5) = (π Yrm (πβ2)))) |
13 | 12 | anbi2d 629 |
. . . . . . . . . . . . 13
β’ (π = (πβ5) β ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β (π β
(β€β₯β2) β§ (πβ5) = (π Yrm (πβ2))))) |
14 | 13 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π = (πβ5) β§ π = (πβ6)) β ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β (π β
(β€β₯β2) β§ (πβ5) = (π Yrm (πβ2))))) |
15 | | eqeq1 2736 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ6) β (π = (π Xrm (πβ2)) β (πβ6) = (π Xrm (πβ2)))) |
16 | 15 | anbi2d 629 |
. . . . . . . . . . . . . 14
β’ (π = (πβ6) β ((π β (β€β₯β2)
β§ π = (π Xrm (πβ2))) β (π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))))) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π = (πβ5) β§ π = (πβ6)) β ((π β (β€β₯β2)
β§ π = (π Xrm (πβ2))) β (π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))))) |
18 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ5) β§ π = (πβ6)) β π = (πβ6)) |
19 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ5) β ((π β (πβ1)) Β· π) = ((π β (πβ1)) Β· (πβ5))) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ5) β§ π = (πβ6)) β ((π β (πβ1)) Β· π) = ((π β (πβ1)) Β· (πβ5))) |
21 | 18, 20 | oveq12d 7423 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ5) β§ π = (πβ6)) β (π β ((π β (πβ1)) Β· π)) = ((πβ6) β ((π β (πβ1)) Β· (πβ5)))) |
22 | 21 | oveq1d 7420 |
. . . . . . . . . . . . . . 15
β’ ((π = (πβ5) β§ π = (πβ6)) β ((π β ((π β (πβ1)) Β· π)) β (πβ3)) = (((πβ6) β ((π β (πβ1)) Β· (πβ5))) β (πβ3))) |
23 | 22 | breq2d 5159 |
. . . . . . . . . . . . . 14
β’ ((π = (πβ5) β§ π = (πβ6)) β (((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)) β ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
((π β (πβ1)) Β· (πβ5))) β (πβ3)))) |
24 | 23 | anbi2d 629 |
. . . . . . . . . . . . 13
β’ ((π = (πβ5) β§ π = (πβ6)) β (((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))) β ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))))) |
25 | 17, 24 | anbi12d 631 |
. . . . . . . . . . . 12
β’ ((π = (πβ5) β§ π = (πβ6)) β (((π β (β€β₯β2)
β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β·
π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· π)
Β· (πβ1))
β ((πβ1)β2)) β 1) β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))) β ((π β (β€β₯β2)
β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β·
π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· π)
Β· (πβ1))
β ((πβ1)β2)) β 1) β₯
(((πβ6) β
((π β (πβ1)) Β· (πβ5))) β (πβ3)))))) |
26 | 14, 25 | anbi12d 631 |
. . . . . . . . . . 11
β’ ((π = (πβ5) β§ π = (πβ6)) β (((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))) β ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))))))) |
27 | 26 | anbi2d 629 |
. . . . . . . . . 10
β’ ((π = (πβ5) β§ π = (πβ6)) β ((((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))) β (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3)))))))) |
28 | 27 | anbi2d 629 |
. . . . . . . . 9
β’ ((π = (πβ5) β§ π = (πβ6)) β ((((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))))))))) |
29 | 10, 11, 28 | sbc2ie 3859 |
. . . . . . . 8
β’
([(πβ5)
/ π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3)))))))) |
30 | 29 | sbcbii 3836 |
. . . . . . 7
β’
([(πβ4)
/ π][(πβ5) / π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))) β [(πβ4) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3)))))))) |
31 | 30 | sbcbii 3836 |
. . . . . 6
β’
([(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))) β [(π βΎ (1...3)) / π][(πβ4) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3)))))))) |
32 | | vex 3478 |
. . . . . . . 8
β’ π β V |
33 | 32 | resex 6027 |
. . . . . . 7
β’ (π βΎ (1...3)) β
V |
34 | | fvex 6901 |
. . . . . . 7
β’ (πβ4) β
V |
35 | | df-2 12271 |
. . . . . . . . . . . . . 14
β’ 2 = (1 +
1) |
36 | | df-3 12272 |
. . . . . . . . . . . . . . 15
β’ 3 = (2 +
1) |
37 | | ssid 4003 |
. . . . . . . . . . . . . . 15
β’ (1...3)
β (1...3) |
38 | 36, 37 | jm2.27dlem5 41737 |
. . . . . . . . . . . . . 14
β’ (1...2)
β (1...3) |
39 | 35, 38 | jm2.27dlem5 41737 |
. . . . . . . . . . . . 13
β’ (1...1)
β (1...3) |
40 | | 1nn 12219 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
41 | 40 | jm2.27dlem3 41735 |
. . . . . . . . . . . . 13
β’ 1 β
(1...1) |
42 | 39, 41 | sselii 3978 |
. . . . . . . . . . . 12
β’ 1 β
(1...3) |
43 | 42 | jm2.27dlem1 41733 |
. . . . . . . . . . 11
β’ (π = (π βΎ (1...3)) β (πβ1) = (πβ1)) |
44 | 43 | eleq1d 2818 |
. . . . . . . . . 10
β’ (π = (π βΎ (1...3)) β ((πβ1) β
(β€β₯β2) β (πβ1) β
(β€β₯β2))) |
45 | | 2nn 12281 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
46 | 45 | jm2.27dlem3 41735 |
. . . . . . . . . . . . 13
β’ 2 β
(1...2) |
47 | 46, 36, 45 | jm2.27dlem2 41734 |
. . . . . . . . . . . 12
β’ 2 β
(1...3) |
48 | 47 | jm2.27dlem1 41733 |
. . . . . . . . . . 11
β’ (π = (π βΎ (1...3)) β (πβ2) = (πβ2)) |
49 | 48 | eleq1d 2818 |
. . . . . . . . . 10
β’ (π = (π βΎ (1...3)) β ((πβ2) β β β (πβ2) β
β)) |
50 | 44, 49 | anbi12d 631 |
. . . . . . . . 9
β’ (π = (π βΎ (1...3)) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β ((πβ1) β
(β€β₯β2) β§ (πβ2) β β))) |
51 | 50 | adantr 481 |
. . . . . . . 8
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β ((πβ1) β
(β€β₯β2) β§ (πβ2) β β))) |
52 | 44 | adantr 481 |
. . . . . . . . . 10
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ1) β
(β€β₯β2) β (πβ1) β
(β€β₯β2))) |
53 | | id 22 |
. . . . . . . . . . 11
β’ (π = (πβ4) β π = (πβ4)) |
54 | 48 | oveq1d 7420 |
. . . . . . . . . . . 12
β’ (π = (π βΎ (1...3)) β ((πβ2) + 1) = ((πβ2) + 1)) |
55 | 43, 54 | oveq12d 7423 |
. . . . . . . . . . 11
β’ (π = (π βΎ (1...3)) β ((πβ1) Yrm ((πβ2) + 1)) = ((πβ1) Yrm ((πβ2) + 1))) |
56 | 53, 55 | eqeqan12rd 2747 |
. . . . . . . . . 10
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (π = ((πβ1) Yrm ((πβ2) + 1)) β (πβ4) = ((πβ1) Yrm ((πβ2) + 1)))) |
57 | 52, 56 | anbi12d 631 |
. . . . . . . . 9
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))))) |
58 | | eleq1 2821 |
. . . . . . . . . . . 12
β’ (π = (πβ4) β (π β (β€β₯β2)
β (πβ4) β
(β€β₯β2))) |
59 | 58 | adantl 482 |
. . . . . . . . . . 11
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (π β (β€β₯β2)
β (πβ4) β
(β€β₯β2))) |
60 | 53, 48 | oveqan12rd 7425 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (π Yrm (πβ2)) = ((πβ4) Yrm (πβ2))) |
61 | 60 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ5) = (π Yrm (πβ2)) β (πβ5) = ((πβ4) Yrm (πβ2)))) |
62 | 59, 61 | anbi12d 631 |
. . . . . . . . . 10
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β ((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))))) |
63 | 53, 48 | oveqan12rd 7425 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (π Xrm (πβ2)) = ((πβ4) Xrm (πβ2))) |
64 | 63 | eqeq2d 2743 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ6) = (π Xrm (πβ2)) β (πβ6) = ((πβ4) Xrm (πβ2)))) |
65 | 59, 64 | anbi12d 631 |
. . . . . . . . . . 11
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((π β (β€β₯β2)
β§ (πβ6) = (π Xrm (πβ2))) β ((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))))) |
66 | 3 | jm2.27dlem1 41733 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (1...3)) β (πβ3) = (πβ3)) |
67 | 66 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (πβ3) = (πβ3)) |
68 | | oveq2 7413 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ4) β (2 Β· π) = (2 Β· (πβ4))) |
69 | 68, 43 | oveqan12rd 7425 |
. . . . . . . . . . . . . . 15
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((2 Β· π) Β· (πβ1)) = ((2 Β· (πβ4)) Β· (πβ1))) |
70 | 43 | oveq1d 7420 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β ((πβ1)β2) = ((πβ1)β2)) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ1)β2) = ((πβ1)β2)) |
72 | 69, 71 | oveq12d 7423 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) = (((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2))) |
73 | 72 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) = ((((2
Β· (πβ4))
Β· (πβ1))
β ((πβ1)β2)) β
1)) |
74 | 67, 73 | breq12d 5160 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β (πβ3) < ((((2 Β·
(πβ4)) Β·
(πβ1)) β
((πβ1)β2))
β 1))) |
75 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β π = (πβ4)) |
76 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (πβ1) = (πβ1)) |
77 | 75, 76 | oveq12d 7423 |
. . . . . . . . . . . . . . . 16
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (π β (πβ1)) = ((πβ4) β (πβ1))) |
78 | 77 | oveq1d 7420 |
. . . . . . . . . . . . . . 15
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((π β (πβ1)) Β· (πβ5)) = (((πβ4) β (πβ1)) Β· (πβ5))) |
79 | 78 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ6) β ((π β (πβ1)) Β· (πβ5))) = ((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5)))) |
80 | 79, 67 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((πβ6) β ((π β (πβ1)) Β· (πβ5))) β (πβ3)) = (((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5))) β (πβ3))) |
81 | 73, 80 | breq12d 5160 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
((π β (πβ1)) Β· (πβ5))) β (πβ3)) β ((((2 Β·
(πβ4)) Β·
(πβ1)) β
((πβ1)β2))
β 1) β₯ (((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5))) β (πβ3)))) |
82 | 74, 81 | anbi12d 631 |
. . . . . . . . . . 11
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))) β ((πβ3) < ((((2 Β·
(πβ4)) Β·
(πβ1)) β
((πβ1)β2))
β 1) β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))) |
83 | 65, 82 | anbi12d 631 |
. . . . . . . . . 10
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((π β (β€β₯β2)
β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β·
π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· π)
Β· (πβ1))
β ((πβ1)β2)) β 1) β₯
(((πβ6) β
((π β (πβ1)) Β· (πβ5))) β (πβ3)))) β (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))) |
84 | 62, 83 | anbi12d 631 |
. . . . . . . . 9
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))))) β (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))))) |
85 | 57, 84 | anbi12d 631 |
. . . . . . . 8
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3)))))) β (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))))) |
86 | 51, 85 | anbi12d 631 |
. . . . . . 7
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))))))) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))))))) |
87 | 33, 34, 86 | sbc2ie 3859 |
. . . . . 6
β’
([(π βΎ
(1...3)) / π][(πβ4) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ (πβ5) = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ (πβ6) = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ (((πβ6)
β ((π β (πβ1)) Β· (πβ5))) β (πβ3))))))) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))))) |
88 | 31, 87 | bitri 274 |
. . . . 5
β’
([(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3))))))) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))))) |
89 | 88 | rabbii 3438 |
. . . 4
β’ {π β (β0
βm (1...6)) β£ [(π βΎ (1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))))} = {π β (β0
βm (1...6)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))))} |
90 | | 6nn0 12489 |
. . . . . . 7
β’ 6 β
β0 |
91 | | 2z 12590 |
. . . . . . 7
β’ 2 β
β€ |
92 | | ovex 7438 |
. . . . . . . 8
β’ (1...6)
β V |
93 | | df-4 12273 |
. . . . . . . . . . . 12
β’ 4 = (3 +
1) |
94 | | df-5 12274 |
. . . . . . . . . . . . 13
β’ 5 = (4 +
1) |
95 | | df-6 12275 |
. . . . . . . . . . . . . 14
β’ 6 = (5 +
1) |
96 | | ssid 4003 |
. . . . . . . . . . . . . 14
β’ (1...6)
β (1...6) |
97 | 95, 96 | jm2.27dlem5 41737 |
. . . . . . . . . . . . 13
β’ (1...5)
β (1...6) |
98 | 94, 97 | jm2.27dlem5 41737 |
. . . . . . . . . . . 12
β’ (1...4)
β (1...6) |
99 | 93, 98 | jm2.27dlem5 41737 |
. . . . . . . . . . 11
β’ (1...3)
β (1...6) |
100 | 36, 99 | jm2.27dlem5 41737 |
. . . . . . . . . 10
β’ (1...2)
β (1...6) |
101 | 35, 100 | jm2.27dlem5 41737 |
. . . . . . . . 9
β’ (1...1)
β (1...6) |
102 | 101, 41 | sselii 3978 |
. . . . . . . 8
β’ 1 β
(1...6) |
103 | | mzpproj 41460 |
. . . . . . . 8
β’ (((1...6)
β V β§ 1 β (1...6)) β (π β (β€ βm (1...6))
β¦ (πβ1)) β
(mzPolyβ(1...6))) |
104 | 92, 102, 103 | mp2an 690 |
. . . . . . 7
β’ (π β (β€
βm (1...6)) β¦ (πβ1)) β
(mzPolyβ(1...6)) |
105 | | eluzrabdioph 41529 |
. . . . . . 7
β’ ((6
β β0 β§ 2 β β€ β§ (π β (β€ βm (1...6))
β¦ (πβ1)) β
(mzPolyβ(1...6))) β {π β (β0
βm (1...6)) β£ (πβ1) β
(β€β₯β2)} β (Diophβ6)) |
106 | 90, 91, 104, 105 | mp3an 1461 |
. . . . . 6
β’ {π β (β0
βm (1...6)) β£ (πβ1) β
(β€β₯β2)} β (Diophβ6) |
107 | 100, 46 | sselii 3978 |
. . . . . . . 8
β’ 2 β
(1...6) |
108 | | mzpproj 41460 |
. . . . . . . 8
β’ (((1...6)
β V β§ 2 β (1...6)) β (π β (β€ βm (1...6))
β¦ (πβ2)) β
(mzPolyβ(1...6))) |
109 | 92, 107, 108 | mp2an 690 |
. . . . . . 7
β’ (π β (β€
βm (1...6)) β¦ (πβ2)) β
(mzPolyβ(1...6)) |
110 | | elnnrabdioph 41530 |
. . . . . . 7
β’ ((6
β β0 β§ (π β (β€ βm (1...6))
β¦ (πβ2)) β
(mzPolyβ(1...6))) β {π β (β0
βm (1...6)) β£ (πβ2) β β} β
(Diophβ6)) |
111 | 90, 109, 110 | mp2an 690 |
. . . . . 6
β’ {π β (β0
βm (1...6)) β£ (πβ2) β β} β
(Diophβ6) |
112 | | anrabdioph 41503 |
. . . . . 6
β’ (({π β (β0
βm (1...6)) β£ (πβ1) β
(β€β₯β2)} β (Diophβ6) β§ {π β (β0
βm (1...6)) β£ (πβ2) β β} β
(Diophβ6)) β {π
β (β0 βm (1...6)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ2) β β)} β
(Diophβ6)) |
113 | 106, 111,
112 | mp2an 690 |
. . . . 5
β’ {π β (β0
βm (1...6)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ2) β β)} β
(Diophβ6) |
114 | | elmapi 8839 |
. . . . . . . . . . 11
β’ (π β (β0
βm (1...6)) β π:(1...6)βΆβ0) |
115 | | ffvelcdm 7080 |
. . . . . . . . . . 11
β’ ((π:(1...6)βΆβ0 β§ 2
β (1...6)) β (πβ2) β
β0) |
116 | 114, 107,
115 | sylancl 586 |
. . . . . . . . . 10
β’ (π β (β0
βm (1...6)) β (πβ2) β
β0) |
117 | | peano2nn0 12508 |
. . . . . . . . . 10
β’ ((πβ2) β
β0 β ((πβ2) + 1) β
β0) |
118 | | oveq2 7413 |
. . . . . . . . . . . . 13
β’ (π = ((πβ2) + 1) β ((πβ1) Yrm π) = ((πβ1) Yrm ((πβ2) + 1))) |
119 | 118 | eqeq2d 2743 |
. . . . . . . . . . . 12
β’ (π = ((πβ2) + 1) β ((πβ4) = ((πβ1) Yrm π) β (πβ4) = ((πβ1) Yrm ((πβ2) + 1)))) |
120 | 119 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π = ((πβ2) + 1) β (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)) β ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))))) |
121 | 120 | ceqsrexv 3642 |
. . . . . . . . . 10
β’ (((πβ2) + 1) β
β0 β (βπ β β0 (π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π))) β ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))))) |
122 | 116, 117,
121 | 3syl 18 |
. . . . . . . . 9
β’ (π β (β0
βm (1...6)) β (βπ β β0 (π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π))) β ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))))) |
123 | 122 | bicomd 222 |
. . . . . . . 8
β’ (π β (β0
βm (1...6)) β (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β βπ β β0
(π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π))))) |
124 | 123 | rabbiia 3436 |
. . . . . . 7
β’ {π β (β0
βm (1...6)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1)))} = {π β (β0
βm (1...6)) β£ βπ β β0 (π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)))} |
125 | | vex 3478 |
. . . . . . . . . . . 12
β’ π β V |
126 | 125 | resex 6027 |
. . . . . . . . . . 11
β’ (π βΎ (1...6)) β
V |
127 | | fvex 6901 |
. . . . . . . . . . 11
β’ (πβ7) β
V |
128 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = (πβ7) β π = (πβ7)) |
129 | 107 | jm2.27dlem1 41733 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (1...6)) β (πβ2) = (πβ2)) |
130 | 129 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (1...6)) β ((πβ2) + 1) = ((πβ2) + 1)) |
131 | 128, 130 | eqeqan12rd 2747 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β (π = ((πβ2) + 1) β (πβ7) = ((πβ2) + 1))) |
132 | 102 | jm2.27dlem1 41733 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...6)) β (πβ1) = (πβ1)) |
133 | 132 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β (πβ1) = (πβ1)) |
134 | 133 | eleq1d 2818 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β ((πβ1) β
(β€β₯β2) β (πβ1) β
(β€β₯β2))) |
135 | | 4nn 12291 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
β |
136 | 135 | jm2.27dlem3 41735 |
. . . . . . . . . . . . . . . . 17
β’ 4 β
(1...4) |
137 | 98, 136 | sselii 3978 |
. . . . . . . . . . . . . . . 16
β’ 4 β
(1...6) |
138 | 137 | jm2.27dlem1 41733 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...6)) β (πβ4) = (πβ4)) |
139 | 138 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β (πβ4) = (πβ4)) |
140 | 132, 128 | oveqan12d 7424 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β ((πβ1) Yrm π) = ((πβ1) Yrm (πβ7))) |
141 | 139, 140 | eqeq12d 2748 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β ((πβ4) = ((πβ1) Yrm π) β (πβ4) = ((πβ1) Yrm (πβ7)))) |
142 | 134, 141 | anbi12d 631 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)) β ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7))))) |
143 | 131, 142 | anbi12d 631 |
. . . . . . . . . . 11
β’ ((π = (π βΎ (1...6)) β§ π = (πβ7)) β ((π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π))) β ((πβ7) = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7)))))) |
144 | 126, 127,
143 | sbc2ie 3859 |
. . . . . . . . . 10
β’
([(π βΎ
(1...6)) / π][(πβ7) / π](π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π))) β ((πβ7) = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7))))) |
145 | 144 | rabbii 3438 |
. . . . . . . . 9
β’ {π β (β0
βm (1...7)) β£ [(π βΎ (1...6)) / π][(πβ7) / π](π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)))} = {π β (β0
βm (1...7)) β£ ((πβ7) = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7))))} |
146 | | 7nn0 12490 |
. . . . . . . . . . 11
β’ 7 β
β0 |
147 | | ovex 7438 |
. . . . . . . . . . . 12
β’ (1...7)
β V |
148 | | 7nn 12300 |
. . . . . . . . . . . . 13
β’ 7 β
β |
149 | 148 | jm2.27dlem3 41735 |
. . . . . . . . . . . 12
β’ 7 β
(1...7) |
150 | | mzpproj 41460 |
. . . . . . . . . . . 12
β’ (((1...7)
β V β§ 7 β (1...7)) β (π β (β€ βm (1...7))
β¦ (πβ7)) β
(mzPolyβ(1...7))) |
151 | 147, 149,
150 | mp2an 690 |
. . . . . . . . . . 11
β’ (π β (β€
βm (1...7)) β¦ (πβ7)) β
(mzPolyβ(1...7)) |
152 | | df-7 12276 |
. . . . . . . . . . . . . 14
β’ 7 = (6 +
1) |
153 | | 6nn 12297 |
. . . . . . . . . . . . . 14
β’ 6 β
β |
154 | 107, 152,
153 | jm2.27dlem2 41734 |
. . . . . . . . . . . . 13
β’ 2 β
(1...7) |
155 | | mzpproj 41460 |
. . . . . . . . . . . . 13
β’ (((1...7)
β V β§ 2 β (1...7)) β (π β (β€ βm (1...7))
β¦ (πβ2)) β
(mzPolyβ(1...7))) |
156 | 147, 154,
155 | mp2an 690 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...7)) β¦ (πβ2)) β
(mzPolyβ(1...7)) |
157 | | 1z 12588 |
. . . . . . . . . . . . 13
β’ 1 β
β€ |
158 | | mzpconstmpt 41463 |
. . . . . . . . . . . . 13
β’ (((1...7)
β V β§ 1 β β€) β (π β (β€ βm (1...7))
β¦ 1) β (mzPolyβ(1...7))) |
159 | 147, 157,
158 | mp2an 690 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...7)) β¦ 1) β
(mzPolyβ(1...7)) |
160 | | mzpaddmpt 41464 |
. . . . . . . . . . . 12
β’ (((π β (β€
βm (1...7)) β¦ (πβ2)) β (mzPolyβ(1...7))
β§ (π β (β€
βm (1...7)) β¦ 1) β (mzPolyβ(1...7))) β
(π β (β€
βm (1...7)) β¦ ((πβ2) + 1)) β
(mzPolyβ(1...7))) |
161 | 156, 159,
160 | mp2an 690 |
. . . . . . . . . . 11
β’ (π β (β€
βm (1...7)) β¦ ((πβ2) + 1)) β
(mzPolyβ(1...7)) |
162 | | eqrabdioph 41500 |
. . . . . . . . . . 11
β’ ((7
β β0 β§ (π β (β€ βm (1...7))
β¦ (πβ7)) β
(mzPolyβ(1...7)) β§ (π β (β€ βm (1...7))
β¦ ((πβ2) + 1))
β (mzPolyβ(1...7))) β {π β (β0
βm (1...7)) β£ (πβ7) = ((πβ2) + 1)} β
(Diophβ7)) |
163 | 146, 151,
161, 162 | mp3an 1461 |
. . . . . . . . . 10
β’ {π β (β0
βm (1...7)) β£ (πβ7) = ((πβ2) + 1)} β
(Diophβ7) |
164 | | rmydioph 41738 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} β
(Diophβ3) |
165 | | simp1 1136 |
. . . . . . . . . . . . . 14
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β (πβ1) = (πβ1)) |
166 | 165 | eleq1d 2818 |
. . . . . . . . . . . . 13
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β ((πβ1) β
(β€β₯β2) β (πβ1) β
(β€β₯β2))) |
167 | | simp3 1138 |
. . . . . . . . . . . . . 14
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β (πβ3) = (πβ4)) |
168 | | simp2 1137 |
. . . . . . . . . . . . . . 15
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β (πβ2) = (πβ7)) |
169 | 165, 168 | oveq12d 7423 |
. . . . . . . . . . . . . 14
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β ((πβ1) Yrm (πβ2)) = ((πβ1) Yrm (πβ7))) |
170 | 167, 169 | eqeq12d 2748 |
. . . . . . . . . . . . 13
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β ((πβ3) = ((πβ1) Yrm (πβ2)) β (πβ4) = ((πβ1) Yrm (πβ7)))) |
171 | 166, 170 | anbi12d 631 |
. . . . . . . . . . . 12
β’ (((πβ1) = (πβ1) β§ (πβ2) = (πβ7) β§ (πβ3) = (πβ4)) β (((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2))) β ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7))))) |
172 | 102, 152,
153 | jm2.27dlem2 41734 |
. . . . . . . . . . . 12
β’ 1 β
(1...7) |
173 | 137, 152,
153 | jm2.27dlem2 41734 |
. . . . . . . . . . . 12
β’ 4 β
(1...7) |
174 | 171, 172,
149, 173 | rabren3dioph 41538 |
. . . . . . . . . . 11
β’ ((7
β β0 β§ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} β (Diophβ3)) β
{π β
(β0 βm (1...7)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7)))} β
(Diophβ7)) |
175 | 146, 164,
174 | mp2an 690 |
. . . . . . . . . 10
β’ {π β (β0
βm (1...7)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7)))} β
(Diophβ7) |
176 | | anrabdioph 41503 |
. . . . . . . . . 10
β’ (({π β (β0
βm (1...7)) β£ (πβ7) = ((πβ2) + 1)} β (Diophβ7) β§
{π β
(β0 βm (1...7)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7)))} β (Diophβ7)) β
{π β
(β0 βm (1...7)) β£ ((πβ7) = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7))))} β
(Diophβ7)) |
177 | 163, 175,
176 | mp2an 690 |
. . . . . . . . 9
β’ {π β (β0
βm (1...7)) β£ ((πβ7) = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm (πβ7))))} β
(Diophβ7) |
178 | 145, 177 | eqeltri 2829 |
. . . . . . . 8
β’ {π β (β0
βm (1...7)) β£ [(π βΎ (1...6)) / π][(πβ7) / π](π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)))} β (Diophβ7) |
179 | 152 | rexfrabdioph 41518 |
. . . . . . . 8
β’ ((6
β β0 β§ {π β (β0
βm (1...7)) β£ [(π βΎ (1...6)) / π][(πβ7) / π](π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)))} β (Diophβ7)) β {π β (β0
βm (1...6)) β£ βπ β β0 (π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)))} β (Diophβ6)) |
180 | 90, 178, 179 | mp2an 690 |
. . . . . . 7
β’ {π β (β0
βm (1...6)) β£ βπ β β0 (π = ((πβ2) + 1) β§ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm π)))} β (Diophβ6) |
181 | 124, 180 | eqeltri 2829 |
. . . . . 6
β’ {π β (β0
βm (1...6)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1)))} β
(Diophβ6) |
182 | | rmydioph 41738 |
. . . . . . . 8
β’ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} β
(Diophβ3) |
183 | | simp1 1136 |
. . . . . . . . . . 11
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β (πβ1) = (πβ4)) |
184 | 183 | eleq1d 2818 |
. . . . . . . . . 10
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β ((πβ1) β
(β€β₯β2) β (πβ4) β
(β€β₯β2))) |
185 | | simp3 1138 |
. . . . . . . . . . 11
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β (πβ3) = (πβ5)) |
186 | | simp2 1137 |
. . . . . . . . . . . 12
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β (πβ2) = (πβ2)) |
187 | 183, 186 | oveq12d 7423 |
. . . . . . . . . . 11
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β ((πβ1) Yrm (πβ2)) = ((πβ4) Yrm (πβ2))) |
188 | 185, 187 | eqeq12d 2748 |
. . . . . . . . . 10
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β ((πβ3) = ((πβ1) Yrm (πβ2)) β (πβ5) = ((πβ4) Yrm (πβ2)))) |
189 | 184, 188 | anbi12d 631 |
. . . . . . . . 9
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ5)) β (((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2))) β ((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))))) |
190 | | 5nn 12294 |
. . . . . . . . . . 11
β’ 5 β
β |
191 | 190 | jm2.27dlem3 41735 |
. . . . . . . . . 10
β’ 5 β
(1...5) |
192 | 191, 95, 190 | jm2.27dlem2 41734 |
. . . . . . . . 9
β’ 5 β
(1...6) |
193 | 189, 137,
107, 192 | rabren3dioph 41538 |
. . . . . . . 8
β’ ((6
β β0 β§ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} β (Diophβ3)) β
{π β
(β0 βm (1...6)) β£ ((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2)))} β
(Diophβ6)) |
194 | 90, 182, 193 | mp2an 690 |
. . . . . . 7
β’ {π β (β0
βm (1...6)) β£ ((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2)))} β
(Diophβ6) |
195 | | rmxdioph 41740 |
. . . . . . . . 9
β’ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Xrm (πβ2)))} β
(Diophβ3) |
196 | | simp1 1136 |
. . . . . . . . . . . 12
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β (πβ1) = (πβ4)) |
197 | 196 | eleq1d 2818 |
. . . . . . . . . . 11
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β ((πβ1) β
(β€β₯β2) β (πβ4) β
(β€β₯β2))) |
198 | | simp3 1138 |
. . . . . . . . . . . 12
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β (πβ3) = (πβ6)) |
199 | | simp2 1137 |
. . . . . . . . . . . . 13
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β (πβ2) = (πβ2)) |
200 | 196, 199 | oveq12d 7423 |
. . . . . . . . . . . 12
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β ((πβ1) Xrm (πβ2)) = ((πβ4) Xrm (πβ2))) |
201 | 198, 200 | eqeq12d 2748 |
. . . . . . . . . . 11
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β ((πβ3) = ((πβ1) Xrm (πβ2)) β (πβ6) = ((πβ4) Xrm (πβ2)))) |
202 | 197, 201 | anbi12d 631 |
. . . . . . . . . 10
β’ (((πβ1) = (πβ4) β§ (πβ2) = (πβ2) β§ (πβ3) = (πβ6)) β (((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Xrm (πβ2))) β ((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))))) |
203 | 153 | jm2.27dlem3 41735 |
. . . . . . . . . 10
β’ 6 β
(1...6) |
204 | 202, 137,
107, 203 | rabren3dioph 41538 |
. . . . . . . . 9
β’ ((6
β β0 β§ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Xrm (πβ2)))} β (Diophβ3)) β
{π β
(β0 βm (1...6)) β£ ((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2)))} β
(Diophβ6)) |
205 | 90, 195, 204 | mp2an 690 |
. . . . . . . 8
β’ {π β (β0
βm (1...6)) β£ ((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2)))} β
(Diophβ6) |
206 | 99, 3 | sselii 3978 |
. . . . . . . . . . 11
β’ 3 β
(1...6) |
207 | | mzpproj 41460 |
. . . . . . . . . . 11
β’ (((1...6)
β V β§ 3 β (1...6)) β (π β (β€ βm (1...6))
β¦ (πβ3)) β
(mzPolyβ(1...6))) |
208 | 92, 206, 207 | mp2an 690 |
. . . . . . . . . 10
β’ (π β (β€
βm (1...6)) β¦ (πβ3)) β
(mzPolyβ(1...6)) |
209 | | mzpconstmpt 41463 |
. . . . . . . . . . . . . . 15
β’ (((1...6)
β V β§ 2 β β€) β (π β (β€ βm (1...6))
β¦ 2) β (mzPolyβ(1...6))) |
210 | 92, 91, 209 | mp2an 690 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...6)) β¦ 2) β
(mzPolyβ(1...6)) |
211 | | mzpproj 41460 |
. . . . . . . . . . . . . . 15
β’ (((1...6)
β V β§ 4 β (1...6)) β (π β (β€ βm (1...6))
β¦ (πβ4)) β
(mzPolyβ(1...6))) |
212 | 92, 137, 211 | mp2an 690 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...6)) β¦ (πβ4)) β
(mzPolyβ(1...6)) |
213 | | mzpmulmpt 41465 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...6)) β¦ 2) β (mzPolyβ(1...6)) β§
(π β (β€
βm (1...6)) β¦ (πβ4)) β (mzPolyβ(1...6)))
β (π β (β€
βm (1...6)) β¦ (2 Β· (πβ4))) β
(mzPolyβ(1...6))) |
214 | 210, 212,
213 | mp2an 690 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...6)) β¦ (2 Β· (πβ4))) β
(mzPolyβ(1...6)) |
215 | | mzpmulmpt 41465 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...6)) β¦ (2 Β· (πβ4))) β (mzPolyβ(1...6))
β§ (π β (β€
βm (1...6)) β¦ (πβ1)) β (mzPolyβ(1...6)))
β (π β (β€
βm (1...6)) β¦ ((2 Β· (πβ4)) Β· (πβ1))) β
(mzPolyβ(1...6))) |
216 | 214, 104,
215 | mp2an 690 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...6)) β¦ ((2 Β· (πβ4)) Β· (πβ1))) β
(mzPolyβ(1...6)) |
217 | | 2nn0 12485 |
. . . . . . . . . . . . 13
β’ 2 β
β0 |
218 | | mzpexpmpt 41468 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...6)) β¦ (πβ1)) β (mzPolyβ(1...6))
β§ 2 β β0) β (π β (β€ βm (1...6))
β¦ ((πβ1)β2)) β
(mzPolyβ(1...6))) |
219 | 104, 217,
218 | mp2an 690 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...6)) β¦ ((πβ1)β2)) β
(mzPolyβ(1...6)) |
220 | | mzpsubmpt 41466 |
. . . . . . . . . . . 12
β’ (((π β (β€
βm (1...6)) β¦ ((2 Β· (πβ4)) Β· (πβ1))) β (mzPolyβ(1...6))
β§ (π β (β€
βm (1...6)) β¦ ((πβ1)β2)) β
(mzPolyβ(1...6))) β (π β (β€ βm (1...6))
β¦ (((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2))) β
(mzPolyβ(1...6))) |
221 | 216, 219,
220 | mp2an 690 |
. . . . . . . . . . 11
β’ (π β (β€
βm (1...6)) β¦ (((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2))) β
(mzPolyβ(1...6)) |
222 | | mzpconstmpt 41463 |
. . . . . . . . . . . 12
β’ (((1...6)
β V β§ 1 β β€) β (π β (β€ βm (1...6))
β¦ 1) β (mzPolyβ(1...6))) |
223 | 92, 157, 222 | mp2an 690 |
. . . . . . . . . . 11
β’ (π β (β€
βm (1...6)) β¦ 1) β
(mzPolyβ(1...6)) |
224 | | mzpsubmpt 41466 |
. . . . . . . . . . 11
β’ (((π β (β€
βm (1...6)) β¦ (((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2))) β
(mzPolyβ(1...6)) β§ (π β (β€ βm (1...6))
β¦ 1) β (mzPolyβ(1...6))) β (π β (β€ βm (1...6))
β¦ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)) β
(mzPolyβ(1...6))) |
225 | 221, 223,
224 | mp2an 690 |
. . . . . . . . . 10
β’ (π β (β€
βm (1...6)) β¦ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)) β
(mzPolyβ(1...6)) |
226 | | ltrabdioph 41531 |
. . . . . . . . . 10
β’ ((6
β β0 β§ (π β (β€ βm (1...6))
β¦ (πβ3)) β
(mzPolyβ(1...6)) β§ (π β (β€ βm (1...6))
β¦ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)) β
(mzPolyβ(1...6))) β {π β (β0
βm (1...6)) β£ (πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)}
β (Diophβ6)) |
227 | 90, 208, 225, 226 | mp3an 1461 |
. . . . . . . . 9
β’ {π β (β0
βm (1...6)) β£ (πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)}
β (Diophβ6) |
228 | | mzpproj 41460 |
. . . . . . . . . . . . 13
β’ (((1...6)
β V β§ 6 β (1...6)) β (π β (β€ βm (1...6))
β¦ (πβ6)) β
(mzPolyβ(1...6))) |
229 | 92, 203, 228 | mp2an 690 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...6)) β¦ (πβ6)) β
(mzPolyβ(1...6)) |
230 | | mzpsubmpt 41466 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...6)) β¦ (πβ4)) β (mzPolyβ(1...6))
β§ (π β (β€
βm (1...6)) β¦ (πβ1)) β (mzPolyβ(1...6)))
β (π β (β€
βm (1...6)) β¦ ((πβ4) β (πβ1))) β
(mzPolyβ(1...6))) |
231 | 212, 104,
230 | mp2an 690 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...6)) β¦ ((πβ4) β (πβ1))) β
(mzPolyβ(1...6)) |
232 | | mzpproj 41460 |
. . . . . . . . . . . . . 14
β’ (((1...6)
β V β§ 5 β (1...6)) β (π β (β€ βm (1...6))
β¦ (πβ5)) β
(mzPolyβ(1...6))) |
233 | 92, 192, 232 | mp2an 690 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...6)) β¦ (πβ5)) β
(mzPolyβ(1...6)) |
234 | | mzpmulmpt 41465 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...6)) β¦ ((πβ4) β (πβ1))) β (mzPolyβ(1...6))
β§ (π β (β€
βm (1...6)) β¦ (πβ5)) β (mzPolyβ(1...6)))
β (π β (β€
βm (1...6)) β¦ (((πβ4) β (πβ1)) Β· (πβ5))) β
(mzPolyβ(1...6))) |
235 | 231, 233,
234 | mp2an 690 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...6)) β¦ (((πβ4) β (πβ1)) Β· (πβ5))) β
(mzPolyβ(1...6)) |
236 | | mzpsubmpt 41466 |
. . . . . . . . . . . 12
β’ (((π β (β€
βm (1...6)) β¦ (πβ6)) β (mzPolyβ(1...6))
β§ (π β (β€
βm (1...6)) β¦ (((πβ4) β (πβ1)) Β· (πβ5))) β (mzPolyβ(1...6)))
β (π β (β€
βm (1...6)) β¦ ((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5)))) β
(mzPolyβ(1...6))) |
237 | 229, 235,
236 | mp2an 690 |
. . . . . . . . . . 11
β’ (π β (β€
βm (1...6)) β¦ ((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5)))) β
(mzPolyβ(1...6)) |
238 | | mzpsubmpt 41466 |
. . . . . . . . . . 11
β’ (((π β (β€
βm (1...6)) β¦ ((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5)))) β (mzPolyβ(1...6))
β§ (π β (β€
βm (1...6)) β¦ (πβ3)) β (mzPolyβ(1...6)))
β (π β (β€
βm (1...6)) β¦ (((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5))) β (πβ3))) β
(mzPolyβ(1...6))) |
239 | 237, 208,
238 | mp2an 690 |
. . . . . . . . . 10
β’ (π β (β€
βm (1...6)) β¦ (((πβ6) β (((πβ4) β (πβ1)) Β· (πβ5))) β (πβ3))) β
(mzPolyβ(1...6)) |
240 | | dvdsrabdioph 41533 |
. . . . . . . . . 10
β’ ((6
β β0 β§ (π β (β€ βm (1...6))
β¦ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)) β
(mzPolyβ(1...6)) β§ (π β (β€ βm (1...6))
β¦ (((πβ6)
β (((πβ4)
β (πβ1))
Β· (πβ5)))
β (πβ3)))
β (mzPolyβ(1...6))) β {π β (β0
βm (1...6)) β£ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))} β
(Diophβ6)) |
241 | 90, 225, 239, 240 | mp3an 1461 |
. . . . . . . . 9
β’ {π β (β0
βm (1...6)) β£ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))} β
(Diophβ6) |
242 | | anrabdioph 41503 |
. . . . . . . . 9
β’ (({π β (β0
βm (1...6)) β£ (πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)}
β (Diophβ6) β§ {π β (β0
βm (1...6)) β£ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))} β
(Diophβ6)) β {π
β (β0 βm (1...6)) β£ ((πβ3) < ((((2 Β·
(πβ4)) Β·
(πβ1)) β
((πβ1)β2))
β 1) β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))} β
(Diophβ6)) |
243 | 227, 241,
242 | mp2an 690 |
. . . . . . . 8
β’ {π β (β0
βm (1...6)) β£ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))} β
(Diophβ6) |
244 | | anrabdioph 41503 |
. . . . . . . 8
β’ (({π β (β0
βm (1...6)) β£ ((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2)))} β (Diophβ6) β§
{π β
(β0 βm (1...6)) β£ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))} β
(Diophβ6)) β {π
β (β0 βm (1...6)) β£ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))} β
(Diophβ6)) |
245 | 205, 243,
244 | mp2an 690 |
. . . . . . 7
β’ {π β (β0
βm (1...6)) β£ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))} β
(Diophβ6) |
246 | | anrabdioph 41503 |
. . . . . . 7
β’ (({π β (β0
βm (1...6)) β£ ((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2)))} β (Diophβ6) β§
{π β
(β0 βm (1...6)) β£ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))} β
(Diophβ6)) β {π
β (β0 βm (1...6)) β£ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))} β
(Diophβ6)) |
247 | 194, 245,
246 | mp2an 690 |
. . . . . 6
β’ {π β (β0
βm (1...6)) β£ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))} β
(Diophβ6) |
248 | | anrabdioph 41503 |
. . . . . 6
β’ (({π β (β0
βm (1...6)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1)))} β (Diophβ6)
β§ {π β
(β0 βm (1...6)) β£ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))} β
(Diophβ6)) β {π
β (β0 βm (1...6)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))))} β
(Diophβ6)) |
249 | 181, 247,
248 | mp2an 690 |
. . . . 5
β’ {π β (β0
βm (1...6)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))))} β
(Diophβ6) |
250 | | anrabdioph 41503 |
. . . . 5
β’ (({π β (β0
βm (1...6)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ2) β β)} β
(Diophβ6) β§ {π
β (β0 βm (1...6)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3))))))} β
(Diophβ6)) β {π
β (β0 βm (1...6)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))))} β
(Diophβ6)) |
251 | 113, 249,
250 | mp2an 690 |
. . . 4
β’ {π β (β0
βm (1...6)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ (πβ4) = ((πβ1) Yrm ((πβ2) + 1))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ5) = ((πβ4) Yrm (πβ2))) β§ (((πβ4) β
(β€β₯β2) β§ (πβ6) = ((πβ4) Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1)
β§ ((((2 Β· (πβ4)) Β· (πβ1)) β ((πβ1)β2)) β 1) β₯
(((πβ6) β
(((πβ4) β
(πβ1)) Β·
(πβ5))) β
(πβ3)))))))} β
(Diophβ6) |
252 | 89, 251 | eqeltri 2829 |
. . 3
β’ {π β (β0
βm (1...6)) β£ [(π βΎ (1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))))} β
(Diophβ6) |
253 | 93, 94, 95 | 3rexfrabdioph 41520 |
. . 3
β’ ((3
β β0 β§ {π β (β0
βm (1...6)) β£ [(π βΎ (1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π](((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))))} β (Diophβ6))
β {π β
(β0 βm (1...3)) β£ βπ β β0
βπ β
β0 βπ β β0 (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))))} β
(Diophβ3)) |
254 | 9, 252, 253 | mp2an 690 |
. 2
β’ {π β (β0
βm (1...3)) β£ βπ β β0 βπ β β0
βπ β
β0 (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (((πβ1) β
(β€β₯β2) β§ π = ((πβ1) Yrm ((πβ2) + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm (πβ2))) β§ ((π β
(β€β₯β2) β§ π = (π Xrm (πβ2))) β§ ((πβ3) < ((((2 Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1) β§ ((((2
Β· π) Β· (πβ1)) β ((πβ1)β2)) β 1)
β₯ ((π β ((π β (πβ1)) Β· π)) β (πβ3)))))))} β
(Diophβ3) |
255 | 8, 254 | eqeltri 2829 |
1
β’ {π β (β0
βm (1...3)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))} β
(Diophβ3) |