Step | Hyp | Ref
| Expression |
1 | | rabdiophlem1 40659 |
. . . 4
β’ ((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β βπ‘ β
(β0 βm (1...π))π΄ β β€) |
2 | | rabdiophlem1 40659 |
. . . 4
β’ ((π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π))
β βπ‘ β
(β0 βm (1...π))π΅ β β€) |
3 | | divides 16006 |
. . . . . . 7
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ β₯ π΅ β βπ β β€ (π Β· π΄) = π΅)) |
4 | | oveq1 7310 |
. . . . . . . . 9
β’ (π = π β (π Β· π΄) = (π Β· π΄)) |
5 | 4 | eqeq1d 2738 |
. . . . . . . 8
β’ (π = π β ((π Β· π΄) = π΅ β (π Β· π΄) = π΅)) |
6 | | oveq1 7310 |
. . . . . . . . 9
β’ (π = -π β (π Β· π΄) = (-π Β· π΄)) |
7 | 6 | eqeq1d 2738 |
. . . . . . . 8
β’ (π = -π β ((π Β· π΄) = π΅ β (-π Β· π΄) = π΅)) |
8 | 5, 7 | rexzrexnn0 40662 |
. . . . . . 7
β’
(βπ β
β€ (π Β· π΄) = π΅ β βπ β β0 ((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)) |
9 | 3, 8 | bitrdi 288 |
. . . . . 6
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ β₯ π΅ β βπ β β0 ((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅))) |
10 | 9 | ralimi 3083 |
. . . . 5
β’
(βπ‘ β
(β0 βm (1...π))(π΄ β β€ β§ π΅ β β€) β βπ‘ β (β0
βm (1...π))(π΄ β₯ π΅ β βπ β β0 ((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅))) |
11 | | r19.26 3111 |
. . . . 5
β’
(βπ‘ β
(β0 βm (1...π))(π΄ β β€ β§ π΅ β β€) β (βπ‘ β (β0
βm (1...π))π΄ β β€ β§ βπ‘ β (β0
βm (1...π))π΅ β β€)) |
12 | | rabbi 3328 |
. . . . 5
β’
(βπ‘ β
(β0 βm (1...π))(π΄ β₯ π΅ β βπ β β0 ((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)) β {π‘ β (β0
βm (1...π))
β£ π΄ β₯ π΅} = {π‘ β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)}) |
13 | 10, 11, 12 | 3imtr3i 292 |
. . . 4
β’
((βπ‘ β
(β0 βm (1...π))π΄ β β€ β§ βπ‘ β (β0
βm (1...π))π΅ β β€) β {π‘ β (β0
βm (1...π))
β£ π΄ β₯ π΅} = {π‘ β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)}) |
14 | 1, 2, 13 | syl2an 597 |
. . 3
β’ (((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ β₯ π΅} = {π‘ β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)}) |
15 | 14 | 3adant1 1130 |
. 2
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ β₯ π΅} = {π‘ β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)}) |
16 | | nfcv 2905 |
. . . 4
β’
β²π‘(β0 βm
(1...π)) |
17 | | nfcv 2905 |
. . . 4
β’
β²π(β0 βm
(1...π)) |
18 | | nfv 1915 |
. . . 4
β’
β²πβπ β β0
((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅) |
19 | | nfcv 2905 |
. . . . 5
β’
β²π‘β0 |
20 | | nfcv 2905 |
. . . . . . . 8
β’
β²π‘π |
21 | | nfcv 2905 |
. . . . . . . 8
β’
β²π‘
Β· |
22 | | nfcsb1v 3862 |
. . . . . . . 8
β’
β²π‘β¦π / π‘β¦π΄ |
23 | 20, 21, 22 | nfov 7333 |
. . . . . . 7
β’
β²π‘(π Β· β¦π / π‘β¦π΄) |
24 | | nfcsb1v 3862 |
. . . . . . 7
β’
β²π‘β¦π / π‘β¦π΅ |
25 | 23, 24 | nfeq 2918 |
. . . . . 6
β’
β²π‘(π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ |
26 | | nfcv 2905 |
. . . . . . . 8
β’
β²π‘-π |
27 | 26, 21, 22 | nfov 7333 |
. . . . . . 7
β’
β²π‘(-π Β· β¦π / π‘β¦π΄) |
28 | 27, 24 | nfeq 2918 |
. . . . . 6
β’
β²π‘(-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ |
29 | 25, 28 | nfor 1905 |
. . . . 5
β’
β²π‘((π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅) |
30 | 19, 29 | nfrex 3301 |
. . . 4
β’
β²π‘βπ β β0
((π Β·
β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅) |
31 | | csbeq1a 3851 |
. . . . . . . 8
β’ (π‘ = π β π΄ = β¦π / π‘β¦π΄) |
32 | 31 | oveq2d 7319 |
. . . . . . 7
β’ (π‘ = π β (π Β· π΄) = (π Β· β¦π / π‘β¦π΄)) |
33 | | csbeq1a 3851 |
. . . . . . 7
β’ (π‘ = π β π΅ = β¦π / π‘β¦π΅) |
34 | 32, 33 | eqeq12d 2752 |
. . . . . 6
β’ (π‘ = π β ((π Β· π΄) = π΅ β (π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)) |
35 | 31 | oveq2d 7319 |
. . . . . . 7
β’ (π‘ = π β (-π Β· π΄) = (-π Β· β¦π / π‘β¦π΄)) |
36 | 35, 33 | eqeq12d 2752 |
. . . . . 6
β’ (π‘ = π β ((-π Β· π΄) = π΅ β (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)) |
37 | 34, 36 | orbi12d 917 |
. . . . 5
β’ (π‘ = π β (((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅) β ((π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅))) |
38 | 37 | rexbidv 3172 |
. . . 4
β’ (π‘ = π β (βπ β β0 ((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅) β βπ β β0 ((π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅))) |
39 | 16, 17, 18, 30, 38 | cbvrabw 3431 |
. . 3
β’ {π‘ β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)} = {π β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· β¦π /
π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)} |
40 | | simp1 1136 |
. . . 4
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β π β
β0) |
41 | | peano2nn0 12315 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β0) |
42 | 41 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π + 1) β
β0) |
43 | | ovex 7336 |
. . . . . . . . . 10
β’
(1...(π + 1)) β
V |
44 | | nn0p1nn 12314 |
. . . . . . . . . . 11
β’ (π β β0
β (π + 1) β
β) |
45 | | elfz1end 13328 |
. . . . . . . . . . 11
β’ ((π + 1) β β β
(π + 1) β (1...(π + 1))) |
46 | 44, 45 | sylib 217 |
. . . . . . . . . 10
β’ (π β β0
β (π + 1) β
(1...(π +
1))) |
47 | | mzpproj 40595 |
. . . . . . . . . 10
β’
(((1...(π + 1))
β V β§ (π + 1)
β (1...(π + 1)))
β (π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
48 | 43, 46, 47 | sylancr 588 |
. . . . . . . . 9
β’ (π β β0
β (π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
49 | 48 | adantr 482 |
. . . . . . . 8
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
50 | | eqid 2736 |
. . . . . . . . 9
β’ (π + 1) = (π + 1) |
51 | 50 | rabdiophlem2 40660 |
. . . . . . . 8
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΄) β (mzPolyβ(1...(π + 1)))) |
52 | | mzpmulmpt 40600 |
. . . . . . . 8
β’ (((π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1))) β§ (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΄) β (mzPolyβ(1...(π + 1)))) β (π β (β€
βm (1...(π
+ 1))) β¦ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1)))) |
53 | 49, 51, 52 | syl2anc 585 |
. . . . . . 7
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1)))) |
54 | 53 | 3adant3 1132 |
. . . . . 6
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1)))) |
55 | 50 | rabdiophlem2 40660 |
. . . . . . 7
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΅) β (mzPolyβ(1...(π + 1)))) |
56 | 55 | 3adant2 1131 |
. . . . . 6
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΅) β (mzPolyβ(1...(π + 1)))) |
57 | | eqrabdioph 40635 |
. . . . . 6
β’ (((π + 1) β β0
β§ (π β (β€
βm (1...(π
+ 1))) β¦ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1))) β§ (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΅) β (mzPolyβ(1...(π + 1)))) β {π β (β0
βm (1...(π
+ 1))) β£ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅} β (Diophβ(π + 1))) |
58 | 42, 54, 56, 57 | syl3anc 1371 |
. . . . 5
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π β
(β0 βm (1...(π + 1))) β£ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅} β (Diophβ(π + 1))) |
59 | | mzpnegmpt 40602 |
. . . . . . . . 9
β’ ((π β (β€
βm (1...(π
+ 1))) β¦ (πβ(π + 1))) β (mzPolyβ(1...(π + 1))) β (π β (β€
βm (1...(π
+ 1))) β¦ -(πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
60 | 49, 59 | syl 17 |
. . . . . . . 8
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ -(πβ(π + 1))) β (mzPolyβ(1...(π + 1)))) |
61 | | mzpmulmpt 40600 |
. . . . . . . 8
β’ (((π β (β€
βm (1...(π
+ 1))) β¦ -(πβ(π + 1))) β (mzPolyβ(1...(π + 1))) β§ (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΄) β (mzPolyβ(1...(π + 1)))) β (π β (β€
βm (1...(π
+ 1))) β¦ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1)))) |
62 | 60, 51, 61 | syl2anc 585 |
. . . . . . 7
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1)))) |
63 | 62 | 3adant3 1132 |
. . . . . 6
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π β (β€
βm (1...(π
+ 1))) β¦ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1)))) |
64 | | eqrabdioph 40635 |
. . . . . 6
β’ (((π + 1) β β0
β§ (π β (β€
βm (1...(π
+ 1))) β¦ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) β (mzPolyβ(1...(π + 1))) β§ (π β (β€
βm (1...(π
+ 1))) β¦ β¦(π βΎ (1...π)) / π‘β¦π΅) β (mzPolyβ(1...(π + 1)))) β {π β (β0
βm (1...(π
+ 1))) β£ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅} β (Diophβ(π + 1))) |
65 | 42, 63, 56, 64 | syl3anc 1371 |
. . . . 5
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π β
(β0 βm (1...(π + 1))) β£ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅} β (Diophβ(π + 1))) |
66 | | orrabdioph 40639 |
. . . . 5
β’ (({π β (β0
βm (1...(π
+ 1))) β£ ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅} β (Diophβ(π + 1)) β§ {π β (β0
βm (1...(π
+ 1))) β£ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅} β (Diophβ(π + 1))) β {π β (β0
βm (1...(π
+ 1))) β£ (((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅ β¨ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅)} β (Diophβ(π + 1))) |
67 | 58, 65, 66 | syl2anc 585 |
. . . 4
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π β
(β0 βm (1...(π + 1))) β£ (((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅ β¨ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅)} β (Diophβ(π + 1))) |
68 | | oveq1 7310 |
. . . . . . 7
β’ (π = (πβ(π + 1)) β (π Β· β¦π / π‘β¦π΄) = ((πβ(π + 1)) Β· β¦π / π‘β¦π΄)) |
69 | 68 | eqeq1d 2738 |
. . . . . 6
β’ (π = (πβ(π + 1)) β ((π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β ((πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)) |
70 | | negeq 11255 |
. . . . . . . 8
β’ (π = (πβ(π + 1)) β -π = -(πβ(π + 1))) |
71 | 70 | oveq1d 7318 |
. . . . . . 7
β’ (π = (πβ(π + 1)) β (-π Β· β¦π / π‘β¦π΄) = (-(πβ(π + 1)) Β· β¦π / π‘β¦π΄)) |
72 | 71 | eqeq1d 2738 |
. . . . . 6
β’ (π = (πβ(π + 1)) β ((-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β (-(πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)) |
73 | 69, 72 | orbi12d 917 |
. . . . 5
β’ (π = (πβ(π + 1)) β (((π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅) β (((πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-(πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅))) |
74 | | csbeq1 3840 |
. . . . . . . 8
β’ (π = (π βΎ (1...π)) β β¦π / π‘β¦π΄ = β¦(π βΎ (1...π)) / π‘β¦π΄) |
75 | 74 | oveq2d 7319 |
. . . . . . 7
β’ (π = (π βΎ (1...π)) β ((πβ(π + 1)) Β· β¦π / π‘β¦π΄) = ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) |
76 | | csbeq1 3840 |
. . . . . . 7
β’ (π = (π βΎ (1...π)) β β¦π / π‘β¦π΅ = β¦(π βΎ (1...π)) / π‘β¦π΅) |
77 | 75, 76 | eqeq12d 2752 |
. . . . . 6
β’ (π = (π βΎ (1...π)) β (((πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β ((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅)) |
78 | 74 | oveq2d 7319 |
. . . . . . 7
β’ (π = (π βΎ (1...π)) β (-(πβ(π + 1)) Β· β¦π / π‘β¦π΄) = (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄)) |
79 | 78, 76 | eqeq12d 2752 |
. . . . . 6
β’ (π = (π βΎ (1...π)) β ((-(πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅)) |
80 | 77, 79 | orbi12d 917 |
. . . . 5
β’ (π = (π βΎ (1...π)) β ((((πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-(πβ(π + 1)) Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅) β (((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅ β¨ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅))) |
81 | 50, 73, 80 | rexrabdioph 40652 |
. . . 4
β’ ((π β β0
β§ {π β
(β0 βm (1...(π + 1))) β£ (((πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅ β¨ (-(πβ(π + 1)) Β· β¦(π βΎ (1...π)) / π‘β¦π΄) = β¦(π βΎ (1...π)) / π‘β¦π΅)} β (Diophβ(π + 1))) β {π β (β0
βm (1...π))
β£ βπ β
β0 ((π
Β· β¦π /
π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)} β (Diophβπ)) |
82 | 40, 67, 81 | syl2anc 585 |
. . 3
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π β
(β0 βm (1...π)) β£ βπ β β0 ((π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅ β¨ (-π Β· β¦π / π‘β¦π΄) = β¦π / π‘β¦π΅)} β (Diophβπ)) |
83 | 39, 82 | eqeltrid 2841 |
. 2
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ βπ β β0 ((π Β· π΄) = π΅ β¨ (-π Β· π΄) = π΅)} β (Diophβπ)) |
84 | 15, 83 | eqeltrd 2837 |
1
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ β₯ π΅} β (Diophβπ)) |