Step | Hyp | Ref
| Expression |
1 | | elmapi 8794 |
. . . . . . 7
β’ (π β (β0
βm (1...3)) β π:(1...3)βΆβ0) |
2 | | 2nn 12233 |
. . . . . . . . 9
β’ 2 β
β |
3 | 2 | jm2.27dlem3 41364 |
. . . . . . . 8
β’ 2 β
(1...2) |
4 | | df-3 12224 |
. . . . . . . 8
β’ 3 = (2 +
1) |
5 | 3, 4, 2 | jm2.27dlem2 41363 |
. . . . . . 7
β’ 2 β
(1...3) |
6 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((π:(1...3)βΆβ0 β§ 2
β (1...3)) β (πβ2) β
β0) |
7 | 1, 5, 6 | sylancl 587 |
. . . . . 6
β’ (π β (β0
βm (1...3)) β (πβ2) β
β0) |
8 | | elnn0 12422 |
. . . . . 6
β’ ((πβ2) β
β0 β ((πβ2) β β β¨ (πβ2) = 0)) |
9 | 7, 8 | sylib 217 |
. . . . 5
β’ (π β (β0
βm (1...3)) β ((πβ2) β β β¨ (πβ2) = 0)) |
10 | | iba 529 |
. . . . . . 7
β’ (((πβ2) β β β¨
(πβ2) = 0) β
((πβ3) = ((πβ1) Yrm (πβ2)) β ((πβ3) = ((πβ1) Yrm (πβ2)) β§ ((πβ2) β β β¨ (πβ2) =
0)))) |
11 | | andi 1007 |
. . . . . . 7
β’ (((πβ3) = ((πβ1) Yrm (πβ2)) β§ ((πβ2) β β β¨ (πβ2) = 0)) β (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0))) |
12 | 10, 11 | bitrdi 287 |
. . . . . 6
β’ (((πβ2) β β β¨
(πβ2) = 0) β
((πβ3) = ((πβ1) Yrm (πβ2)) β (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0)))) |
13 | 12 | anbi2d 630 |
. . . . 5
β’ (((πβ2) β β β¨
(πβ2) = 0) β
(((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2))) β ((πβ1) β
(β€β₯β2) β§ (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0))))) |
14 | 9, 13 | syl 17 |
. . . 4
β’ (π β (β0
βm (1...3)) β (((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2))) β ((πβ1) β
(β€β₯β2) β§ (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0))))) |
15 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β (πβ1) β
(β€β₯β2)) |
16 | | nnz 12527 |
. . . . . . . . . . . . . 14
β’ ((πβ2) β β β
(πβ2) β
β€) |
17 | 16 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β (πβ2) β
β€) |
18 | | frmy 41267 |
. . . . . . . . . . . . . 14
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
19 | 18 | fovcl 7489 |
. . . . . . . . . . . . 13
β’ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β€) β ((πβ1) Yrm (πβ2)) β
β€) |
20 | 15, 17, 19 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ1) Yrm (πβ2)) β
β€) |
21 | | rmy0 41282 |
. . . . . . . . . . . . . 14
β’ ((πβ1) β
(β€β₯β2) β ((πβ1) Yrm 0) =
0) |
22 | 21 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ1) Yrm 0) =
0) |
23 | | nngt0 12191 |
. . . . . . . . . . . . . . 15
β’ ((πβ2) β β β
0 < (πβ2)) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β 0 <
(πβ2)) |
25 | | 0zd 12518 |
. . . . . . . . . . . . . . 15
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β 0 β
β€) |
26 | | ltrmy 41305 |
. . . . . . . . . . . . . . 15
β’ (((πβ1) β
(β€β₯β2) β§ 0 β β€ β§ (πβ2) β β€) β
(0 < (πβ2) β
((πβ1) Yrm
0) < ((πβ1)
Yrm (πβ2)))) |
27 | 15, 25, 17, 26 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β (0 <
(πβ2) β ((πβ1) Yrm 0) <
((πβ1) Yrm
(πβ2)))) |
28 | 24, 27 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ1) Yrm 0) <
((πβ1) Yrm
(πβ2))) |
29 | 22, 28 | eqbrtrrd 5134 |
. . . . . . . . . . . 12
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β 0 <
((πβ1) Yrm
(πβ2))) |
30 | | elnnz 12516 |
. . . . . . . . . . . 12
β’ (((πβ1) Yrm (πβ2)) β β β
(((πβ1)
Yrm (πβ2))
β β€ β§ 0 < ((πβ1) Yrm (πβ2)))) |
31 | 20, 29, 30 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ1) Yrm (πβ2)) β
β) |
32 | | eleq1 2826 |
. . . . . . . . . . 11
β’ ((πβ3) = ((πβ1) Yrm (πβ2)) β ((πβ3) β β β ((πβ1) Yrm (πβ2)) β
β)) |
33 | 31, 32 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ3) = ((πβ1) Yrm (πβ2)) β (πβ3) β β)) |
34 | 33 | pm4.71rd 564 |
. . . . . . . . 9
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ3) = ((πβ1) Yrm (πβ2)) β ((πβ3) β β β§ (πβ3) = ((πβ1) Yrm (πβ2))))) |
35 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β§ (πβ3) β β) β
(πβ1) β
(β€β₯β2)) |
36 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β§ (πβ3) β β) β
(πβ2) β
β) |
37 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β§ (πβ3) β β) β
(πβ3) β
β) |
38 | | jm2.27 41361 |
. . . . . . . . . . 11
β’ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β β§ (πβ3) β β) β
((πβ3) = ((πβ1) Yrm (πβ2)) β βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))))) |
39 | 35, 36, 37, 38 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β§ (πβ3) β β) β
((πβ3) = ((πβ1) Yrm (πβ2)) β βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))))) |
40 | 39 | pm5.32da 580 |
. . . . . . . . 9
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β (((πβ3) β β β§
(πβ3) = ((πβ1) Yrm (πβ2))) β ((πβ3) β β β§
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 βπ β β0
ββ β
β0 (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))))) |
41 | 34, 40 | bitrd 279 |
. . . . . . . 8
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) β β) β ((πβ3) = ((πβ1) Yrm (πβ2)) β ((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))))) |
42 | 41 | ex 414 |
. . . . . . 7
β’ ((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β ((πβ2) β β β ((πβ3) = ((πβ1) Yrm (πβ2)) β ((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))))))) |
43 | 42 | pm5.32rd 579 |
. . . . . 6
β’ ((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β (((πβ3) β β β§
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 βπ β β0
ββ β
β0 (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β))) |
44 | | oveq2 7370 |
. . . . . . . . . . 11
β’ ((πβ2) = 0 β ((πβ1) Yrm (πβ2)) = ((πβ1) Yrm
0)) |
45 | 44 | adantl 483 |
. . . . . . . . . 10
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) = 0) β ((πβ1) Yrm (πβ2)) = ((πβ1) Yrm 0)) |
46 | 21 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) = 0) β ((πβ1) Yrm 0) =
0) |
47 | 45, 46 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) = 0) β ((πβ1) Yrm (πβ2)) = 0) |
48 | 47 | eqeq2d 2748 |
. . . . . . . 8
β’ (((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β§ (πβ2) = 0) β ((πβ3) = ((πβ1) Yrm (πβ2)) β (πβ3) = 0)) |
49 | 48 | ex 414 |
. . . . . . 7
β’ ((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β ((πβ2) = 0 β ((πβ3) = ((πβ1) Yrm (πβ2)) β (πβ3) = 0))) |
50 | 49 | pm5.32rd 579 |
. . . . . 6
β’ ((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0) β ((πβ3) = 0 β§ (πβ2) = 0))) |
51 | 43, 50 | orbi12d 918 |
. . . . 5
β’ ((π β (β0
βm (1...3)) β§ (πβ1) β
(β€β₯β2)) β ((((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0)) β ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) =
0)))) |
52 | 51 | pm5.32da 580 |
. . . 4
β’ (π β (β0
βm (1...3)) β (((πβ1) β
(β€β₯β2) β§ (((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1) Yrm (πβ2)) β§ (πβ2) = 0))) β ((πβ1) β
(β€β₯β2) β§ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) =
0))))) |
53 | 14, 52 | bitrd 279 |
. . 3
β’ (π β (β0
βm (1...3)) β (((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2))) β ((πβ1) β
(β€β₯β2) β§ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) =
0))))) |
54 | 53 | rabbiia 3414 |
. 2
β’ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} = {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) =
0)))} |
55 | | 3nn0 12438 |
. . . 4
β’ 3 β
β0 |
56 | | 2z 12542 |
. . . 4
β’ 2 β
β€ |
57 | | ovex 7395 |
. . . . 5
β’ (1...3)
β V |
58 | | 1nn 12171 |
. . . . . . . 8
β’ 1 β
β |
59 | 58 | jm2.27dlem3 41364 |
. . . . . . 7
β’ 1 β
(1...1) |
60 | | df-2 12223 |
. . . . . . 7
β’ 2 = (1 +
1) |
61 | 59, 60, 58 | jm2.27dlem2 41363 |
. . . . . 6
β’ 1 β
(1...2) |
62 | 61, 4, 2 | jm2.27dlem2 41363 |
. . . . 5
β’ 1 β
(1...3) |
63 | | mzpproj 41089 |
. . . . 5
β’ (((1...3)
β V β§ 1 β (1...3)) β (π β (β€ βm (1...3))
β¦ (πβ1)) β
(mzPolyβ(1...3))) |
64 | 57, 62, 63 | mp2an 691 |
. . . 4
β’ (π β (β€
βm (1...3)) β¦ (πβ1)) β
(mzPolyβ(1...3)) |
65 | | eluzrabdioph 41158 |
. . . 4
β’ ((3
β β0 β§ 2 β β€ β§ (π β (β€ βm (1...3))
β¦ (πβ1)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ1) β
(β€β₯β2)} β (Diophβ3)) |
66 | 55, 56, 64, 65 | mp3an 1462 |
. . 3
β’ {π β (β0
βm (1...3)) β£ (πβ1) β
(β€β₯β2)} β (Diophβ3) |
67 | | 3nn 12239 |
. . . . . . . . 9
β’ 3 β
β |
68 | 67 | jm2.27dlem3 41364 |
. . . . . . . 8
β’ 3 β
(1...3) |
69 | | mzpproj 41089 |
. . . . . . . 8
β’ (((1...3)
β V β§ 3 β (1...3)) β (π β (β€ βm (1...3))
β¦ (πβ3)) β
(mzPolyβ(1...3))) |
70 | 57, 68, 69 | mp2an 691 |
. . . . . . 7
β’ (π β (β€
βm (1...3)) β¦ (πβ3)) β
(mzPolyβ(1...3)) |
71 | | elnnrabdioph 41159 |
. . . . . . 7
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ3)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ3) β β} β
(Diophβ3)) |
72 | 55, 70, 71 | mp2an 691 |
. . . . . 6
β’ {π β (β0
βm (1...3)) β£ (πβ3) β β} β
(Diophβ3) |
73 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ (πβ8) β
V |
74 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ (πβ9) β
V |
75 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ (πβ;10) β V |
76 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ9) β (πβ2) = ((πβ9)β2)) |
77 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πβ8) β (πβ2) = ((πβ8)β2)) |
78 | 77 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ8) β (((πβ2) β 1) Β· (πβ2)) = (((πβ2) β 1) Β·
((πβ8)β2))) |
79 | 76, 78 | oveqan12rd 7382 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = (πβ8) β§ π = (πβ9)) β ((πβ2) β (((πβ2) β 1) Β· (πβ2))) = (((πβ9)β2) β
(((πβ2) β 1)
Β· ((πβ8)β2)))) |
80 | 79 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = (πβ8) β§ π = (πβ9)) β (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β (((πβ9)β2) β
(((πβ2) β 1)
Β· ((πβ8)β2))) = 1)) |
81 | 80 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = (πβ8) β§ π = (πβ9) β§ β = (πβ;10)) β (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β (((πβ9)β2) β
(((πβ2) β 1)
Β· ((πβ8)β2))) = 1)) |
82 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β = (πβ;10) β (β + 1) = ((πβ;10) + 1)) |
83 | 82 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β = (πβ;10) β ((β + 1) Β· (2 Β· ((πβ3)β2))) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))) |
84 | 83 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = (πβ;10) β (π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))))) |
85 | 84 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = (πβ8) β§ π = (πβ9) β§ β = (πβ;10)) β (π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))))) |
86 | 81, 85 | 3anbi12d 1438 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = (πβ8) β§ π = (πβ9) β§ β = (πβ;10)) β ((((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1))) β ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1))))) |
87 | 86 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ8) β§ π = (πβ9) β§ β = (πβ;10)) β (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β ((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))))) |
88 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ8) β (π β (πβ3)) = ((πβ8) β (πβ3))) |
89 | 88 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβ8) β (π β₯ (π β (πβ3)) β π β₯ ((πβ8) β (πβ3)))) |
90 | 89 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ8) β (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β ((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))))) |
91 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ8) β (π β (πβ2)) = ((πβ8) β (πβ2))) |
92 | 91 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβ8) β ((2 Β· (πβ3)) β₯ (π β (πβ2)) β (2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)))) |
93 | 92 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ8) β (((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)) β ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) |
94 | 90, 93 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ8) β ((((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))) β (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
95 | 94 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ8) β§ π = (πβ9) β§ β = (πβ;10)) β ((((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))) β (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
96 | 87, 95 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ8) β§ π = (πβ9) β§ β = (πβ;10)) β ((((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))))) |
97 | 73, 74, 75, 96 | sbc3ie 3830 |
. . . . . . . . . . . . . . 15
β’
([(πβ8)
/ π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
98 | 97 | sbcbii 3804 |
. . . . . . . . . . . . . 14
β’
([(πβ7)
/ π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β [(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
99 | 98 | sbcbii 3804 |
. . . . . . . . . . . . 13
β’
([(πβ6)
/ π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β [(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
100 | 99 | sbcbii 3804 |
. . . . . . . . . . . 12
β’
([(πβ5)
/ π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β [(πβ5) / π][(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
101 | 100 | sbcbii 3804 |
. . . . . . . . . . 11
β’
([(πβ4)
/ π][(πβ5) / π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β [(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
102 | 101 | sbcbii 3804 |
. . . . . . . . . 10
β’
([(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β [(π βΎ (1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
103 | | fvex 6860 |
. . . . . . . . . . . . 13
β’ (πβ5) β
V |
104 | | fvex 6860 |
. . . . . . . . . . . . 13
β’ (πβ6) β
V |
105 | | fvex 6860 |
. . . . . . . . . . . . 13
β’ (πβ7) β
V |
106 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ6) β (πβ2) = ((πβ6)β2)) |
107 | 106 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (πβ2) = ((πβ6)β2)) |
108 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβ5) β (πβ2) = ((πβ5)β2)) |
109 | 108 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ5) β ((((πβ1)β2) β 1) Β· (πβ2)) = ((((πβ1)β2) β 1)
Β· ((πβ5)β2))) |
110 | 109 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β ((((πβ1)β2) β 1) Β· (πβ2)) = ((((πβ1)β2) β 1)
Β· ((πβ5)β2))) |
111 | 107, 110 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β ((πβ2) β ((((πβ1)β2) β 1) Β· (πβ2))) = (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2)))) |
112 | 111 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (((πβ2) β ((((πβ1)β2) β 1) Β· (πβ2))) = 1 β (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1)) |
113 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ7) β (π β (β€β₯β2)
β (πβ7) β
(β€β₯β2))) |
114 | 113 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (π β (β€β₯β2)
β (πβ7) β
(β€β₯β2))) |
115 | 112, 114 | 3anbi23d 1440 |
. . . . . . . . . . . . . . 15
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β ((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β (((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)))) |
116 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβ7) β (πβ2) = ((πβ7)β2)) |
117 | 116 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβ7) β ((πβ2) β 1) = (((πβ7)β2) β
1)) |
118 | 117 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ7) β (((πβ2) β 1) Β· ((πβ8)β2)) = ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) |
119 | 118 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ7) β (((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) =
(((πβ9)β2)
β ((((πβ7)β2) β 1) Β· ((πβ8)β2)))) |
120 | 119 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ7) β ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1)) |
121 | 120 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1)) |
122 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ5) β (π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))))) |
123 | 122 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))))) |
124 | | simp2 1138 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β π = (πβ6)) |
125 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ7) β (π β (πβ1)) = ((πβ7) β (πβ1))) |
126 | 125 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (π β (πβ1)) = ((πβ7) β (πβ1))) |
127 | 124, 126 | breq12d 5123 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (π β₯ (π β (πβ1)) β (πβ6) β₯ ((πβ7) β (πβ1)))) |
128 | 121, 123,
127 | 3anbi123d 1437 |
. . . . . . . . . . . . . . 15
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1))) β ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))))) |
129 | 115, 128 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β ((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))))) |
130 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ7) β (π β 1) = ((πβ7) β 1)) |
131 | 130 | breq2d 5122 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ7) β ((2 Β· (πβ3)) β₯ (π β 1) β (2 Β·
(πβ3)) β₯
((πβ7) β
1))) |
132 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ6) β (π β₯ ((πβ8) β (πβ3)) β (πβ6) β₯ ((πβ8) β (πβ3)))) |
133 | 131, 132 | bi2anan9r 639 |
. . . . . . . . . . . . . . . 16
β’ ((π = (πβ6) β§ π = (πβ7)) β (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β ((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))))) |
134 | 133 | anbi1d 631 |
. . . . . . . . . . . . . . 15
β’ ((π = (πβ6) β§ π = (πβ7)) β ((((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))) β (((2 Β·
(πβ3)) β₯
((πβ7) β 1)
β§ (πβ6) β₯
((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
135 | 134 | 3adant1 1131 |
. . . . . . . . . . . . . 14
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β ((((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))) β (((2 Β·
(πβ3)) β₯
((πβ7) β 1)
β§ (πβ6) β₯
((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
136 | 129, 135 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ ((π = (πβ5) β§ π = (πβ6) β§ π = (πβ7)) β ((((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) β (((((πβ2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))))) |
137 | 103, 104,
105, 136 | sbc3ie 3830 |
. . . . . . . . . . . 12
β’
([(πβ5)
/ π][(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) β (((((πβ2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
138 | 137 | sbcbii 3804 |
. . . . . . . . . . 11
β’
([(πβ4)
/ π][(πβ5) / π][(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) β
[(πβ4) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
139 | 138 | sbcbii 3804 |
. . . . . . . . . 10
β’
([(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ ((((πβ9)β2) β (((πβ2) β 1) Β·
((πβ8)β2))) = 1
β§ π = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ ((πβ8) β (πβ3))) β§ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) β
[(π βΎ (1...3))
/ π][(πβ4) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
140 | | vex 3452 |
. . . . . . . . . . . 12
β’ π β V |
141 | 140 | resex 5990 |
. . . . . . . . . . 11
β’ (π βΎ (1...3)) β
V |
142 | | fvex 6860 |
. . . . . . . . . . 11
β’ (πβ4) β
V |
143 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ4) β (πβ2) = ((πβ4)β2)) |
144 | 62 | jm2.27dlem1 41362 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βΎ (1...3)) β (πβ1) = (πβ1)) |
145 | 144 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βΎ (1...3)) β ((πβ1)β2) = ((πβ1)β2)) |
146 | 145 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ (1...3)) β (((πβ1)β2) β 1) =
(((πβ1)β2)
β 1)) |
147 | 68 | jm2.27dlem1 41362 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βΎ (1...3)) β (πβ3) = (πβ3)) |
148 | 147 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ (1...3)) β ((πβ3)β2) = ((πβ3)β2)) |
149 | 146, 148 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2)) = ((((πβ1)β2) β 1) Β· ((πβ3)β2))) |
150 | 143, 149 | oveqan12rd 7382 |
. . . . . . . . . . . . . . 15
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = (((πβ4)β2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2)))) |
151 | 150 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β
(((πβ4)β2)
β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) =
1)) |
152 | 146 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ (1...3)) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2)) = ((((πβ1)β2) β 1) Β· ((πβ5)β2))) |
153 | 152 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2)))) |
154 | 153 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1)) |
155 | 154 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2))) = 1 β (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1)) |
156 | 151, 155 | 3anbi12d 1438 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β ((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)))) |
157 | 148 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ (1...3)) β (2 Β· ((πβ3)β2)) = (2 Β·
((πβ3)β2))) |
158 | 157 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))) |
159 | 158 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))))) |
160 | 144 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β ((πβ7) β (πβ1)) = ((πβ7) β (πβ1))) |
161 | 160 | breq2d 5122 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((πβ6) β₯ ((πβ7) β (πβ1)) β (πβ6) β₯ ((πβ7) β (πβ1)))) |
162 | 159, 161 | 3anbi23d 1440 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (1...3)) β (((((πβ9)β2) β
((((πβ7)β2)
β 1) Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))) β ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))))) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))) β ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))))) |
164 | 156, 163 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β (((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))))) |
165 | 147 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β (2 Β· (πβ3)) = (2 Β· (πβ3))) |
166 | 165 | breq1d 5120 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((2 Β· (πβ3)) β₯ ((πβ7) β 1) β (2
Β· (πβ3))
β₯ ((πβ7)
β 1))) |
167 | 147 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β ((πβ8) β (πβ3)) = ((πβ8) β (πβ3))) |
168 | 167 | breq2d 5122 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((πβ6) β₯ ((πβ8) β (πβ3)) β (πβ6) β₯ ((πβ8) β (πβ3)))) |
169 | 166, 168 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (1...3)) β (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β ((2 Β·
(πβ3)) β₯
((πβ7) β 1)
β§ (πβ6) β₯
((πβ8) β (πβ3))))) |
170 | 5 | jm2.27dlem1 41362 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π βΎ (1...3)) β (πβ2) = (πβ2)) |
171 | 170 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βΎ (1...3)) β ((πβ8) β (πβ2)) = ((πβ8) β (πβ2))) |
172 | 165, 171 | breq12d 5123 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β (2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)))) |
173 | 170, 147 | breq12d 5123 |
. . . . . . . . . . . . . . 15
β’ (π = (π βΎ (1...3)) β ((πβ2) β€ (πβ3) β (πβ2) β€ (πβ3))) |
174 | 172, 173 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (1...3)) β (((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)) β ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) |
175 | 169, 174 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (1...3)) β ((((2 Β·
(πβ3)) β₯
((πβ7) β 1)
β§ (πβ6) β₯
((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))) β (((2 Β·
(πβ3)) β₯
((πβ7) β 1)
β§ (πβ6) β₯
((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
176 | 175 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))) β (((2 Β·
(πβ3)) β₯
((πβ7) β 1)
β§ (πβ6) β₯
((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
177 | 164, 176 | anbi12d 632 |
. . . . . . . . . . 11
β’ ((π = (π βΎ (1...3)) β§ π = (πβ4)) β ((((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) β ((((((πβ4)β2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))))) |
178 | 141, 142,
177 | sbc2ie 3827 |
. . . . . . . . . 10
β’
([(π βΎ
(1...3)) / π][(πβ4) / π](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
(((πβ6)β2)
β ((((πβ1)β2) β 1) Β· ((πβ5)β2))) = 1 β§
(πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))) β ((((((πβ4)β2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
179 | 102, 139,
178 | 3bitri 297 |
. . . . . . . . 9
β’
([(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))) β ((((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))) |
180 | 179 | rabbii 3416 |
. . . . . . . 8
β’ {π β (β0
βm (1...;10))
β£ [(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))} = {π β (β0
βm (1...;10))
β£ ((((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))} |
181 | | 10nn0 12643 |
. . . . . . . . . . . 12
β’ ;10 β
β0 |
182 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’
(1...;10) β
V |
183 | | df-5 12226 |
. . . . . . . . . . . . . . . . 17
β’ 5 = (4 +
1) |
184 | | df-6 12227 |
. . . . . . . . . . . . . . . . . 18
β’ 6 = (5 +
1) |
185 | | df-7 12228 |
. . . . . . . . . . . . . . . . . . 19
β’ 7 = (6 +
1) |
186 | | df-8 12229 |
. . . . . . . . . . . . . . . . . . . 20
β’ 8 = (7 +
1) |
187 | | df-9 12230 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 9 = (8 +
1) |
188 | | 9p1e10 12627 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (9 + 1) =
;10 |
189 | 188 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ;10 = (9 + 1) |
190 | | ssid 3971 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(1...;10) β
(1...;10) |
191 | 189, 190 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1...9)
β (1...;10) |
192 | 187, 191 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1...8)
β (1...;10) |
193 | 186, 192 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . . 19
β’ (1...7)
β (1...;10) |
194 | 185, 193 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . 18
β’ (1...6)
β (1...;10) |
195 | 184, 194 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . 17
β’ (1...5)
β (1...;10) |
196 | 183, 195 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . 16
β’ (1...4)
β (1...;10) |
197 | | 4nn 12243 |
. . . . . . . . . . . . . . . . 17
β’ 4 β
β |
198 | 197 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . . . 16
β’ 4 β
(1...4) |
199 | 196, 198 | sselii 3946 |
. . . . . . . . . . . . . . 15
β’ 4 β
(1...;10) |
200 | | mzpproj 41089 |
. . . . . . . . . . . . . . 15
β’
(((1...;10) β V β§
4 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ4)) β
(mzPolyβ(1...;10))) |
201 | 182, 199,
200 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ (πβ4)) β
(mzPolyβ(1...;10)) |
202 | | 2nn0 12437 |
. . . . . . . . . . . . . 14
β’ 2 β
β0 |
203 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (πβ4)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ4)β2)) β
(mzPolyβ(1...;10))) |
204 | 201, 202,
203 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((πβ4)β2)) β
(mzPolyβ(1...;10)) |
205 | | df-4 12225 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 4 = (3 +
1) |
206 | 205, 196 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1...3)
β (1...;10) |
207 | 4, 206 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . . 19
β’ (1...2)
β (1...;10) |
208 | 60, 207 | jm2.27dlem5 41366 |
. . . . . . . . . . . . . . . . . 18
β’ (1...1)
β (1...;10) |
209 | 208, 59 | sselii 3946 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
(1...;10) |
210 | | mzpproj 41089 |
. . . . . . . . . . . . . . . . 17
β’
(((1...;10) β V β§
1 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ1)) β
(mzPolyβ(1...;10))) |
211 | 182, 209,
210 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’ (π β (β€
βm (1...;10))
β¦ (πβ1)) β
(mzPolyβ(1...;10)) |
212 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . . . 16
β’ (((π β (β€
βm (1...;10))
β¦ (πβ1)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ1)β2)) β
(mzPolyβ(1...;10))) |
213 | 211, 202,
212 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm (1...;10))
β¦ ((πβ1)β2)) β
(mzPolyβ(1...;10)) |
214 | | 1z 12540 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β€ |
215 | | mzpconstmpt 41092 |
. . . . . . . . . . . . . . . 16
β’
(((1...;10) β V β§
1 β β€) β (π
β (β€ βm (1...;10)) β¦ 1) β (mzPolyβ(1...;10))) |
216 | 182, 214,
215 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10)) |
217 | | mzpsubmpt 41095 |
. . . . . . . . . . . . . . 15
β’ (((π β (β€
βm (1...;10))
β¦ ((πβ1)β2)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10))) β (π β (β€ βm
(1...;10)) β¦ (((πβ1)β2) β 1))
β (mzPolyβ(1...;10))) |
218 | 213, 216,
217 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ (((πβ1)β2) β 1)) β
(mzPolyβ(1...;10)) |
219 | 206, 68 | sselii 3946 |
. . . . . . . . . . . . . . . 16
β’ 3 β
(1...;10) |
220 | | mzpproj 41089 |
. . . . . . . . . . . . . . . 16
β’
(((1...;10) β V β§
3 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ3)) β
(mzPolyβ(1...;10))) |
221 | 182, 219,
220 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm (1...;10))
β¦ (πβ3)) β
(mzPolyβ(1...;10)) |
222 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . . 15
β’ (((π β (β€
βm (1...;10))
β¦ (πβ3)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ3)β2)) β
(mzPolyβ(1...;10))) |
223 | 221, 202,
222 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ ((πβ3)β2)) β
(mzPolyβ(1...;10)) |
224 | | mzpmulmpt 41094 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (((πβ1)β2) β 1)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((πβ3)β2)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((((πβ1)β2) β 1) Β· ((πβ3)β2))) β
(mzPolyβ(1...;10))) |
225 | 218, 223,
224 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((((πβ1)β2) β 1) Β· ((πβ3)β2))) β
(mzPolyβ(1...;10)) |
226 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ ((πβ4)β2)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((((πβ1)β2) β 1) Β· ((πβ3)β2))) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ (((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2)))) β
(mzPolyβ(1...;10))) |
227 | 204, 225,
226 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ (((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2)))) β
(mzPolyβ(1...;10)) |
228 | | eqrabdioph 41129 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2)))) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10))) β {π β (β0
βm (1...;10))
β£ (((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1} β
(Diophβ;10)) |
229 | 181, 227,
216, 228 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1} β
(Diophβ;10) |
230 | | 6nn 12249 |
. . . . . . . . . . . . . . . . 17
β’ 6 β
β |
231 | 230 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . . . 16
β’ 6 β
(1...6) |
232 | 194, 231 | sselii 3946 |
. . . . . . . . . . . . . . 15
β’ 6 β
(1...;10) |
233 | | mzpproj 41089 |
. . . . . . . . . . . . . . 15
β’
(((1...;10) β V β§
6 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ6)) β
(mzPolyβ(1...;10))) |
234 | 182, 232,
233 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ (πβ6)) β
(mzPolyβ(1...;10)) |
235 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (πβ6)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ6)β2)) β
(mzPolyβ(1...;10))) |
236 | 234, 202,
235 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((πβ6)β2)) β
(mzPolyβ(1...;10)) |
237 | | 5nn 12246 |
. . . . . . . . . . . . . . . . . 18
β’ 5 β
β |
238 | 237 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . . . . 17
β’ 5 β
(1...5) |
239 | 195, 238 | sselii 3946 |
. . . . . . . . . . . . . . . 16
β’ 5 β
(1...;10) |
240 | | mzpproj 41089 |
. . . . . . . . . . . . . . . 16
β’
(((1...;10) β V β§
5 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ5)) β
(mzPolyβ(1...;10))) |
241 | 182, 239,
240 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm (1...;10))
β¦ (πβ5)) β
(mzPolyβ(1...;10)) |
242 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . . 15
β’ (((π β (β€
βm (1...;10))
β¦ (πβ5)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ5)β2)) β
(mzPolyβ(1...;10))) |
243 | 241, 202,
242 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ ((πβ5)β2)) β
(mzPolyβ(1...;10)) |
244 | | mzpmulmpt 41094 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (((πβ1)β2) β 1)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((πβ5)β2)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((((πβ1)β2) β 1) Β· ((πβ5)β2))) β
(mzPolyβ(1...;10))) |
245 | 218, 243,
244 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((((πβ1)β2) β 1) Β· ((πβ5)β2))) β
(mzPolyβ(1...;10)) |
246 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ ((πβ6)β2)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((((πβ1)β2) β 1) Β· ((πβ5)β2))) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2)))) β
(mzPolyβ(1...;10))) |
247 | 236, 245,
246 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2)))) β
(mzPolyβ(1...;10)) |
248 | | eqrabdioph 41129 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2)))) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10))) β {π β (β0
βm (1...;10))
β£ (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2))) = 1} β
(Diophβ;10)) |
249 | 181, 247,
216, 248 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2))) = 1} β
(Diophβ;10) |
250 | | 7nn 12252 |
. . . . . . . . . . . . . . 15
β’ 7 β
β |
251 | 250 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . 14
β’ 7 β
(1...7) |
252 | 193, 251 | sselii 3946 |
. . . . . . . . . . . . 13
β’ 7 β
(1...;10) |
253 | | mzpproj 41089 |
. . . . . . . . . . . . 13
β’
(((1...;10) β V β§
7 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ7)) β
(mzPolyβ(1...;10))) |
254 | 182, 252,
253 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ (πβ7)) β
(mzPolyβ(1...;10)) |
255 | | eluzrabdioph 41158 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§ 2
β β€ β§ (π
β (β€ βm (1...;10)) β¦ (πβ7)) β (mzPolyβ(1...;10))) β {π β (β0
βm (1...;10))
β£ (πβ7) β
(β€β₯β2)} β (Diophβ;10)) |
256 | 181, 56, 254, 255 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (πβ7) β
(β€β₯β2)} β (Diophβ;10) |
257 | | 3anrabdioph 41134 |
. . . . . . . . . . 11
β’ (({π β (β0
βm (1...;10))
β£ (((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1} β
(Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (((πβ6)β2) β ((((πβ1)β2) β 1)
Β· ((πβ5)β2))) = 1} β
(Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (πβ7) β
(β€β₯β2)} β (Diophβ;10)) β {π β (β0
βm (1...;10))
β£ ((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2))} β (Diophβ;10)) |
258 | 229, 249,
256, 257 | mp3an 1462 |
. . . . . . . . . 10
β’ {π β (β0
βm (1...;10))
β£ ((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2))} β (Diophβ;10) |
259 | | 9nn 12258 |
. . . . . . . . . . . . . . . . 17
β’ 9 β
β |
260 | 259 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . . . 16
β’ 9 β
(1...9) |
261 | 260, 189,
259 | jm2.27dlem2 41363 |
. . . . . . . . . . . . . . 15
β’ 9 β
(1...;10) |
262 | | mzpproj 41089 |
. . . . . . . . . . . . . . 15
β’
(((1...;10) β V β§
9 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ9)) β
(mzPolyβ(1...;10))) |
263 | 182, 261,
262 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ (πβ9)) β
(mzPolyβ(1...;10)) |
264 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (πβ9)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ9)β2)) β
(mzPolyβ(1...;10))) |
265 | 263, 202,
264 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((πβ9)β2)) β
(mzPolyβ(1...;10)) |
266 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . . . 16
β’ (((π β (β€
βm (1...;10))
β¦ (πβ7)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ7)β2)) β
(mzPolyβ(1...;10))) |
267 | 254, 202,
266 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm (1...;10))
β¦ ((πβ7)β2)) β
(mzPolyβ(1...;10)) |
268 | | mzpsubmpt 41095 |
. . . . . . . . . . . . . . 15
β’ (((π β (β€
βm (1...;10))
β¦ ((πβ7)β2)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10))) β (π β (β€ βm
(1...;10)) β¦ (((πβ7)β2) β 1))
β (mzPolyβ(1...;10))) |
269 | 267, 216,
268 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ (((πβ7)β2) β 1)) β
(mzPolyβ(1...;10)) |
270 | | 8nn 12255 |
. . . . . . . . . . . . . . . . . 18
β’ 8 β
β |
271 | 270 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . . . . 17
β’ 8 β
(1...8) |
272 | 192, 271 | sselii 3946 |
. . . . . . . . . . . . . . . 16
β’ 8 β
(1...;10) |
273 | | mzpproj 41089 |
. . . . . . . . . . . . . . . 16
β’
(((1...;10) β V β§
8 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ8)) β
(mzPolyβ(1...;10))) |
274 | 182, 272,
273 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π β (β€
βm (1...;10))
β¦ (πβ8)) β
(mzPolyβ(1...;10)) |
275 | | mzpexpmpt 41097 |
. . . . . . . . . . . . . . 15
β’ (((π β (β€
βm (1...;10))
β¦ (πβ8)) β
(mzPolyβ(1...;10)) β§ 2
β β0) β (π β (β€ βm
(1...;10)) β¦ ((πβ8)β2)) β
(mzPolyβ(1...;10))) |
276 | 274, 202,
275 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ ((πβ8)β2)) β
(mzPolyβ(1...;10)) |
277 | | mzpmulmpt 41094 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (((πβ7)β2) β 1)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((πβ8)β2)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((((πβ7)β2) β 1) Β· ((πβ8)β2))) β
(mzPolyβ(1...;10))) |
278 | 269, 276,
277 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((((πβ7)β2) β 1) Β· ((πβ8)β2))) β
(mzPolyβ(1...;10)) |
279 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ ((πβ9)β2)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((((πβ7)β2) β 1) Β· ((πβ8)β2))) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2)))) β
(mzPolyβ(1...;10))) |
280 | 265, 278,
279 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2)))) β
(mzPolyβ(1...;10)) |
281 | | eqrabdioph 41129 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2)))) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10))) β {π β (β0
βm (1...;10))
β£ (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1} β
(Diophβ;10)) |
282 | 181, 280,
216, 281 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1} β
(Diophβ;10) |
283 | | 10nn 12641 |
. . . . . . . . . . . . . . . 16
β’ ;10 β β |
284 | 283 | jm2.27dlem3 41364 |
. . . . . . . . . . . . . . 15
β’ ;10 β (1...;10) |
285 | | mzpproj 41089 |
. . . . . . . . . . . . . . 15
β’
(((1...;10) β V β§
;10 β (1...;10)) β (π β (β€ βm
(1...;10)) β¦ (πβ;10)) β (mzPolyβ(1...;10))) |
286 | 182, 284,
285 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ (πβ;10)) β (mzPolyβ(1...;10)) |
287 | | mzpaddmpt 41093 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ (πβ;10)) β (mzPolyβ(1...;10)) β§ (π β (β€ βm
(1...;10)) β¦ 1) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((πβ;10) + 1)) β
(mzPolyβ(1...;10))) |
288 | 286, 216,
287 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ ((πβ;10) + 1)) β
(mzPolyβ(1...;10)) |
289 | | mzpconstmpt 41092 |
. . . . . . . . . . . . . . 15
β’
(((1...;10) β V β§
2 β β€) β (π
β (β€ βm (1...;10)) β¦ 2) β (mzPolyβ(1...;10))) |
290 | 182, 56, 289 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (β€
βm (1...;10))
β¦ 2) β (mzPolyβ(1...;10)) |
291 | | mzpmulmpt 41094 |
. . . . . . . . . . . . . 14
β’ (((π β (β€
βm (1...;10))
β¦ 2) β (mzPolyβ(1...;10)) β§ (π β (β€ βm
(1...;10)) β¦ ((πβ3)β2)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ (2 Β· ((πβ3)β2))) β
(mzPolyβ(1...;10))) |
292 | 290, 223,
291 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ (2 Β· ((πβ3)β2))) β
(mzPolyβ(1...;10)) |
293 | | mzpmulmpt 41094 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ ((πβ;10) + 1)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ (2 Β· ((πβ3)β2))) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))) β
(mzPolyβ(1...;10))) |
294 | 288, 292,
293 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))) β
(mzPolyβ(1...;10)) |
295 | | eqrabdioph 41129 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (πβ5)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))) β
(mzPolyβ(1...;10))) β
{π β
(β0 βm (1...;10)) β£ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))} β
(Diophβ;10)) |
296 | 181, 241,
294, 295 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (πβ5) =
(((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))} β
(Diophβ;10) |
297 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ (πβ7)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ (πβ1)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((πβ7)
β (πβ1)))
β (mzPolyβ(1...;10))) |
298 | 254, 211,
297 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ ((πβ7)
β (πβ1)))
β (mzPolyβ(1...;10)) |
299 | | dvdsrabdioph 41162 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (πβ6)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((πβ7)
β (πβ1)))
β (mzPolyβ(1...;10)))
β {π β
(β0 βm (1...;10)) β£ (πβ6) β₯ ((πβ7) β (πβ1))} β (Diophβ;10)) |
300 | 181, 234,
298, 299 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (πβ6) β₯
((πβ7) β (πβ1))} β
(Diophβ;10) |
301 | | 3anrabdioph 41134 |
. . . . . . . . . . 11
β’ (({π β (β0
βm (1...;10))
β£ (((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1} β
(Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (πβ5) =
(((πβ;10) + 1) Β· (2 Β· ((πβ3)β2)))} β
(Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (πβ6) β₯
((πβ7) β (πβ1))} β
(Diophβ;10)) β {π β (β0
βm (1...;10))
β£ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))} β (Diophβ;10)) |
302 | 282, 296,
300, 301 | mp3an 1462 |
. . . . . . . . . 10
β’ {π β (β0
βm (1...;10))
β£ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))} β (Diophβ;10) |
303 | | anrabdioph 41132 |
. . . . . . . . . 10
β’ (({π β (β0
βm (1...;10))
β£ ((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2))} β (Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))} β (Diophβ;10)) β {π β (β0
βm (1...;10))
β£ (((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))))} β (Diophβ;10)) |
304 | 258, 302,
303 | mp2an 691 |
. . . . . . . . 9
β’ {π β (β0
βm (1...;10))
β£ (((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))))} β (Diophβ;10) |
305 | | mzpmulmpt 41094 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ 2) β (mzPolyβ(1...;10)) β§ (π β (β€ βm
(1...;10)) β¦ (πβ3)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ (2 Β· (πβ3))) β (mzPolyβ(1...;10))) |
306 | 290, 221,
305 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ (2 Β· (πβ3))) β (mzPolyβ(1...;10)) |
307 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ (πβ7)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ 1) β (mzPolyβ(1...;10))) β (π β (β€ βm
(1...;10)) β¦ ((πβ7) β 1)) β
(mzPolyβ(1...;10))) |
308 | 254, 216,
307 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ ((πβ7)
β 1)) β (mzPolyβ(1...;10)) |
309 | | dvdsrabdioph 41162 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (2 Β· (πβ3))) β (mzPolyβ(1...;10)) β§ (π β (β€ βm
(1...;10)) β¦ ((πβ7) β 1)) β
(mzPolyβ(1...;10))) β
{π β
(β0 βm (1...;10)) β£ (2 Β· (πβ3)) β₯ ((πβ7) β 1)} β
(Diophβ;10)) |
310 | 181, 306,
308, 309 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (2 Β· (πβ3)) β₯ ((πβ7) β 1)} β
(Diophβ;10) |
311 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ (πβ8)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ (πβ3)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((πβ8)
β (πβ3)))
β (mzPolyβ(1...;10))) |
312 | 274, 221,
311 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ ((πβ8)
β (πβ3)))
β (mzPolyβ(1...;10)) |
313 | | dvdsrabdioph 41162 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (πβ6)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ ((πβ8)
β (πβ3)))
β (mzPolyβ(1...;10)))
β {π β
(β0 βm (1...;10)) β£ (πβ6) β₯ ((πβ8) β (πβ3))} β (Diophβ;10)) |
314 | 181, 234,
312, 313 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (πβ6) β₯
((πβ8) β (πβ3))} β
(Diophβ;10) |
315 | | anrabdioph 41132 |
. . . . . . . . . . 11
β’ (({π β (β0
βm (1...;10))
β£ (2 Β· (πβ3)) β₯ ((πβ7) β 1)} β
(Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (πβ6) β₯
((πβ8) β (πβ3))} β
(Diophβ;10)) β {π β (β0
βm (1...;10))
β£ ((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§ (πβ6) β₯ ((πβ8) β (πβ3)))} β
(Diophβ;10)) |
316 | 310, 314,
315 | mp2an 691 |
. . . . . . . . . 10
β’ {π β (β0
βm (1...;10))
β£ ((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§ (πβ6) β₯ ((πβ8) β (πβ3)))} β
(Diophβ;10) |
317 | 207, 3 | sselii 3946 |
. . . . . . . . . . . . . 14
β’ 2 β
(1...;10) |
318 | | mzpproj 41089 |
. . . . . . . . . . . . . 14
β’
(((1...;10) β V β§
2 β (1...;10)) β (π β (β€
βm (1...;10))
β¦ (πβ2)) β
(mzPolyβ(1...;10))) |
319 | 182, 317,
318 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (β€
βm (1...;10))
β¦ (πβ2)) β
(mzPolyβ(1...;10)) |
320 | | mzpsubmpt 41095 |
. . . . . . . . . . . . 13
β’ (((π β (β€
βm (1...;10))
β¦ (πβ8)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ (πβ2)) β
(mzPolyβ(1...;10))) β
(π β (β€
βm (1...;10))
β¦ ((πβ8)
β (πβ2)))
β (mzPolyβ(1...;10))) |
321 | 274, 319,
320 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π β (β€
βm (1...;10))
β¦ ((πβ8)
β (πβ2)))
β (mzPolyβ(1...;10)) |
322 | | dvdsrabdioph 41162 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (2 Β· (πβ3))) β (mzPolyβ(1...;10)) β§ (π β (β€ βm
(1...;10)) β¦ ((πβ8) β (πβ2))) β
(mzPolyβ(1...;10))) β
{π β
(β0 βm (1...;10)) β£ (2 Β· (πβ3)) β₯ ((πβ8) β (πβ2))} β (Diophβ;10)) |
323 | 181, 306,
321, 322 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (2 Β· (πβ3)) β₯ ((πβ8) β (πβ2))} β (Diophβ;10) |
324 | | lerabdioph 41157 |
. . . . . . . . . . . 12
β’ ((;10 β β0 β§
(π β (β€
βm (1...;10))
β¦ (πβ2)) β
(mzPolyβ(1...;10)) β§
(π β (β€
βm (1...;10))
β¦ (πβ3)) β
(mzPolyβ(1...;10))) β
{π β
(β0 βm (1...;10)) β£ (πβ2) β€ (πβ3)} β (Diophβ;10)) |
325 | 181, 319,
221, 324 | mp3an 1462 |
. . . . . . . . . . 11
β’ {π β (β0
βm (1...;10))
β£ (πβ2) β€
(πβ3)} β
(Diophβ;10) |
326 | | anrabdioph 41132 |
. . . . . . . . . . 11
β’ (({π β (β0
βm (1...;10))
β£ (2 Β· (πβ3)) β₯ ((πβ8) β (πβ2))} β (Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (πβ2) β€
(πβ3)} β
(Diophβ;10)) β {π β (β0
βm (1...;10))
β£ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))} β (Diophβ;10)) |
327 | 323, 325,
326 | mp2an 691 |
. . . . . . . . . 10
β’ {π β (β0
βm (1...;10))
β£ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))} β (Diophβ;10) |
328 | | anrabdioph 41132 |
. . . . . . . . . 10
β’ (({π β (β0
βm (1...;10))
β£ ((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§ (πβ6) β₯ ((πβ8) β (πβ3)))} β
(Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ ((2 Β· (πβ3)) β₯ ((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))} β (Diophβ;10)) β {π β (β0
βm (1...;10))
β£ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§ (πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))} β
(Diophβ;10)) |
329 | 316, 327,
328 | mp2an 691 |
. . . . . . . . 9
β’ {π β (β0
βm (1...;10))
β£ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§ (πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))} β
(Diophβ;10) |
330 | | anrabdioph 41132 |
. . . . . . . . 9
β’ (({π β (β0
βm (1...;10))
β£ (((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1))))} β (Diophβ;10) β§ {π β (β0
βm (1...;10))
β£ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§ (πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3)))} β
(Diophβ;10)) β {π β (β0
βm (1...;10))
β£ ((((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))} β
(Diophβ;10)) |
331 | 304, 329,
330 | mp2an 691 |
. . . . . . . 8
β’ {π β (β0
βm (1...;10))
β£ ((((((πβ4)β2) β ((((πβ1)β2) β 1)
Β· ((πβ3)β2))) = 1 β§ (((πβ6)β2) β
((((πβ1)β2)
β 1) Β· ((πβ5)β2))) = 1 β§ (πβ7) β
(β€β₯β2)) β§ ((((πβ9)β2) β ((((πβ7)β2) β 1)
Β· ((πβ8)β2))) = 1 β§ (πβ5) = (((πβ;10) + 1) Β· (2 Β· ((πβ3)β2))) β§ (πβ6) β₯ ((πβ7) β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ ((πβ7) β 1) β§
(πβ6) β₯ ((πβ8) β (πβ3))) β§ ((2 Β·
(πβ3)) β₯
((πβ8) β (πβ2)) β§ (πβ2) β€ (πβ3))))} β
(Diophβ;10) |
332 | 180, 331 | eqeltri 2834 |
. . . . . . 7
β’ {π β (β0
βm (1...;10))
β£ [(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))} β (Diophβ;10) |
333 | 205, 183,
184, 185, 186, 187, 189 | 7rexfrabdioph 41152 |
. . . . . . 7
β’ ((3
β β0 β§ {π β (β0
βm (1...;10))
β£ [(π βΎ
(1...3)) / π][(πβ4) / π][(πβ5) / π][(πβ6) / π][(πβ7) / π][(πβ8) / π][(πβ9) / π][(πβ;10) / β](((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))} β (Diophβ;10)) β {π β (β0
βm (1...3)) β£ βπ β β0 βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 ββ
β β0 (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))} β
(Diophβ3)) |
334 | 55, 332, 333 | mp2an 691 |
. . . . . 6
β’ {π β (β0
βm (1...3)) β£ βπ β β0 βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 ββ
β β0 (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))} β
(Diophβ3) |
335 | | anrabdioph 41132 |
. . . . . 6
β’ (({π β (β0
βm (1...3)) β£ (πβ3) β β} β
(Diophβ3) β§ {π
β (β0 βm (1...3)) β£ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))} β (Diophβ3)) β
{π β
(β0 βm (1...3)) β£ ((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))))} β
(Diophβ3)) |
336 | 72, 334, 335 | mp2an 691 |
. . . . 5
β’ {π β (β0
βm (1...3)) β£ ((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))))} β
(Diophβ3) |
337 | | mzpproj 41089 |
. . . . . . 7
β’ (((1...3)
β V β§ 2 β (1...3)) β (π β (β€ βm (1...3))
β¦ (πβ2)) β
(mzPolyβ(1...3))) |
338 | 57, 5, 337 | mp2an 691 |
. . . . . 6
β’ (π β (β€
βm (1...3)) β¦ (πβ2)) β
(mzPolyβ(1...3)) |
339 | | elnnrabdioph 41159 |
. . . . . 6
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ2)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ2) β β} β
(Diophβ3)) |
340 | 55, 338, 339 | mp2an 691 |
. . . . 5
β’ {π β (β0
βm (1...3)) β£ (πβ2) β β} β
(Diophβ3) |
341 | | anrabdioph 41132 |
. . . . 5
β’ (({π β (β0
βm (1...3)) β£ ((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3)))))} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ (πβ2) β β} β
(Diophβ3)) β {π
β (β0 βm (1...3)) β£ (((πβ3) β β β§
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 βπ β β0
ββ β
β0 (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β)} β
(Diophβ3)) |
342 | 336, 340,
341 | mp2an 691 |
. . . 4
β’ {π β (β0
βm (1...3)) β£ (((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β)} β
(Diophβ3) |
343 | | eq0rabdioph 41128 |
. . . . . 6
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ3)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ3) = 0} β
(Diophβ3)) |
344 | 55, 70, 343 | mp2an 691 |
. . . . 5
β’ {π β (β0
βm (1...3)) β£ (πβ3) = 0} β
(Diophβ3) |
345 | | eq0rabdioph 41128 |
. . . . . 6
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ2)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ2) = 0} β
(Diophβ3)) |
346 | 55, 338, 345 | mp2an 691 |
. . . . 5
β’ {π β (β0
βm (1...3)) β£ (πβ2) = 0} β
(Diophβ3) |
347 | | anrabdioph 41132 |
. . . . 5
β’ (({π β (β0
βm (1...3)) β£ (πβ3) = 0} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ (πβ2) = 0} β (Diophβ3)) β
{π β
(β0 βm (1...3)) β£ ((πβ3) = 0 β§ (πβ2) = 0)} β
(Diophβ3)) |
348 | 344, 346,
347 | mp2an 691 |
. . . 4
β’ {π β (β0
βm (1...3)) β£ ((πβ3) = 0 β§ (πβ2) = 0)} β
(Diophβ3) |
349 | | orrabdioph 41133 |
. . . 4
β’ (({π β (β0
βm (1...3)) β£ (((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β)} β
(Diophβ3) β§ {π
β (β0 βm (1...3)) β£ ((πβ3) = 0 β§ (πβ2) = 0)} β
(Diophβ3)) β {π
β (β0 βm (1...3)) β£ ((((πβ3) β β β§
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 βπ β β0
ββ β
β0 (((((πβ2) β ((((πβ1)β2) β 1) Β· ((πβ3)β2))) = 1 β§
((πβ2) β
((((πβ1)β2)
β 1) Β· (πβ2))) = 1 β§ π β (β€β₯β2))
β§ (((πβ2) β
(((πβ2) β 1)
Β· (πβ2))) = 1
β§ π = ((β + 1) Β· (2 Β·
((πβ3)β2)))
β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) = 0))} β
(Diophβ3)) |
350 | 342, 348,
349 | mp2an 691 |
. . 3
β’ {π β (β0
βm (1...3)) β£ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) = 0))} β
(Diophβ3) |
351 | | anrabdioph 41132 |
. . 3
β’ (({π β (β0
βm (1...3)) β£ (πβ1) β
(β€β₯β2)} β (Diophβ3) β§ {π β (β0
βm (1...3)) β£ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) = 0))} β
(Diophβ3)) β {π
β (β0 βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) = 0)))} β
(Diophβ3)) |
352 | 66, 350, 351 | mp2an 691 |
. 2
β’ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ ((((πβ3) β β β§ βπ β β0
βπ β
β0 βπ β β0 βπ β β0
βπ β
β0 βπ β β0 ββ β β0
(((((πβ2) β
((((πβ1)β2)
β 1) Β· ((πβ3)β2))) = 1 β§ ((πβ2) β ((((πβ1)β2) β 1)
Β· (πβ2))) = 1
β§ π β
(β€β₯β2)) β§ (((πβ2) β (((πβ2) β 1) Β· (πβ2))) = 1 β§ π = ((β + 1) Β· (2 Β· ((πβ3)β2))) β§ π β₯ (π β (πβ1)))) β§ (((2 Β· (πβ3)) β₯ (π β 1) β§ π β₯ (π β (πβ3))) β§ ((2 Β· (πβ3)) β₯ (π β (πβ2)) β§ (πβ2) β€ (πβ3))))) β§ (πβ2) β β) β¨ ((πβ3) = 0 β§ (πβ2) = 0)))} β
(Diophβ3) |
353 | 54, 352 | eqeltri 2834 |
1
β’ {π β (β0
βm (1...3)) β£ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} β
(Diophβ3) |