Step | Hyp | Ref
| Expression |
1 | | pm4.42 1053 |
. . . 4
β’ ((πβ3) = ((πβ1)β(πβ2)) β (((πβ3) = ((πβ1)β(πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1)β(πβ2)) β§ Β¬ (πβ2) β β))) |
2 | | ancom 462 |
. . . . . 6
β’ (((πβ3) = ((πβ1)β(πβ2)) β§ (πβ2) β β) β ((πβ2) β β β§
(πβ3) = ((πβ1)β(πβ2)))) |
3 | | elmapi 8790 |
. . . . . . . . . . . . 13
β’ (π β (β0
βm (1...3)) β π:(1...3)βΆβ0) |
4 | | df-2 12221 |
. . . . . . . . . . . . . . 15
β’ 2 = (1 +
1) |
5 | | df-3 12222 |
. . . . . . . . . . . . . . . 16
β’ 3 = (2 +
1) |
6 | | ssid 3967 |
. . . . . . . . . . . . . . . 16
β’ (1...3)
β (1...3) |
7 | 5, 6 | jm2.27dlem5 41380 |
. . . . . . . . . . . . . . 15
β’ (1...2)
β (1...3) |
8 | 4, 7 | jm2.27dlem5 41380 |
. . . . . . . . . . . . . 14
β’ (1...1)
β (1...3) |
9 | | 1nn 12169 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
10 | 9 | jm2.27dlem3 41378 |
. . . . . . . . . . . . . 14
β’ 1 β
(1...1) |
11 | 8, 10 | sselii 3942 |
. . . . . . . . . . . . 13
β’ 1 β
(1...3) |
12 | | ffvelcdm 7033 |
. . . . . . . . . . . . 13
β’ ((π:(1...3)βΆβ0 β§ 1
β (1...3)) β (πβ1) β
β0) |
13 | 3, 11, 12 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β (β0
βm (1...3)) β (πβ1) β
β0) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (πβ1) β
β0) |
15 | | elnn0 12420 |
. . . . . . . . . . 11
β’ ((πβ1) β
β0 β ((πβ1) β β β¨ (πβ1) = 0)) |
16 | 14, 15 | sylib 217 |
. . . . . . . . . 10
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ1) β β β¨
(πβ1) =
0)) |
17 | | elnn1uz2 12855 |
. . . . . . . . . . . 12
β’ ((πβ1) β β β
((πβ1) = 1 β¨
(πβ1) β
(β€β₯β2))) |
18 | 17 | biimpi 215 |
. . . . . . . . . . 11
β’ ((πβ1) β β β
((πβ1) = 1 β¨
(πβ1) β
(β€β₯β2))) |
19 | 18 | orim1i 909 |
. . . . . . . . . 10
β’ (((πβ1) β β β¨
(πβ1) = 0) β
(((πβ1) = 1 β¨
(πβ1) β
(β€β₯β2)) β¨ (πβ1) = 0)) |
20 | 16, 19 | syl 17 |
. . . . . . . . 9
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (((πβ1) = 1 β¨ (πβ1) β
(β€β₯β2)) β¨ (πβ1) = 0)) |
21 | 20 | biantrurd 534 |
. . . . . . . 8
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ3) = ((πβ1)β(πβ2)) β ((((πβ1) = 1 β¨ (πβ1) β
(β€β₯β2)) β¨ (πβ1) = 0) β§ (πβ3) = ((πβ1)β(πβ2))))) |
22 | | andir 1008 |
. . . . . . . . . 10
β’
(((((πβ1) = 1
β¨ (πβ1) β
(β€β₯β2)) β¨ (πβ1) = 0) β§ (πβ3) = ((πβ1)β(πβ2))) β ((((πβ1) = 1 β¨ (πβ1) β
(β€β₯β2)) β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) = 0 β§ (πβ3) = ((πβ1)β(πβ2))))) |
23 | | andir 1008 |
. . . . . . . . . . 11
β’ ((((πβ1) = 1 β¨ (πβ1) β
(β€β₯β2)) β§ (πβ3) = ((πβ1)β(πβ2))) β (((πβ1) = 1 β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1)β(πβ2))))) |
24 | 23 | orbi1i 913 |
. . . . . . . . . 10
β’
(((((πβ1) = 1
β¨ (πβ1) β
(β€β₯β2)) β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) = 0 β§ (πβ3) = ((πβ1)β(πβ2)))) β ((((πβ1) = 1 β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = ((πβ1)β(πβ2))))) |
25 | 22, 24 | bitri 275 |
. . . . . . . . 9
β’
(((((πβ1) = 1
β¨ (πβ1) β
(β€β₯β2)) β¨ (πβ1) = 0) β§ (πβ3) = ((πβ1)β(πβ2))) β ((((πβ1) = 1 β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = ((πβ1)β(πβ2))))) |
26 | | nnz 12525 |
. . . . . . . . . . . . . . . 16
β’ ((πβ2) β β β
(πβ2) β
β€) |
27 | | 1exp 14003 |
. . . . . . . . . . . . . . . 16
β’ ((πβ2) β β€ β
(1β(πβ2)) =
1) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((πβ2) β β β
(1β(πβ2)) =
1) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β
(1β(πβ2)) =
1) |
30 | 29 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ3) = (1β(πβ2)) β (πβ3) = 1)) |
31 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ ((πβ1) = 1 β ((πβ1)β(πβ2)) = (1β(πβ2))) |
32 | 31 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ ((πβ1) = 1 β ((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = (1β(πβ2)))) |
33 | 32 | bibi1d 344 |
. . . . . . . . . . . . 13
β’ ((πβ1) = 1 β (((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = 1) β ((πβ3) = (1β(πβ2)) β (πβ3) = 1))) |
34 | 30, 33 | syl5ibrcom 247 |
. . . . . . . . . . . 12
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ1) = 1 β ((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = 1))) |
35 | 34 | pm5.32d 578 |
. . . . . . . . . . 11
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (((πβ1) = 1 β§ (πβ3) = ((πβ1)β(πβ2))) β ((πβ1) = 1 β§ (πβ3) = 1))) |
36 | | iba 529 |
. . . . . . . . . . . . 13
β’ ((πβ2) β β β
((πβ1) β
(β€β₯β2) β ((πβ1) β
(β€β₯β2) β§ (πβ2) β β))) |
37 | 36 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ1) β
(β€β₯β2) β ((πβ1) β
(β€β₯β2) β§ (πβ2) β β))) |
38 | 37 | anbi1d 631 |
. . . . . . . . . . 11
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1)β(πβ2))) β (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2))))) |
39 | 35, 38 | orbi12d 918 |
. . . . . . . . . 10
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((((πβ1) = 1 β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1)β(πβ2)))) β (((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))))) |
40 | | 0exp 14009 |
. . . . . . . . . . . . . 14
β’ ((πβ2) β β β
(0β(πβ2)) =
0) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β
(0β(πβ2)) =
0) |
42 | 41 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ3) = (0β(πβ2)) β (πβ3) = 0)) |
43 | | oveq1 7365 |
. . . . . . . . . . . . . 14
β’ ((πβ1) = 0 β ((πβ1)β(πβ2)) = (0β(πβ2))) |
44 | 43 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ ((πβ1) = 0 β ((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = (0β(πβ2)))) |
45 | 44 | bibi1d 344 |
. . . . . . . . . . . 12
β’ ((πβ1) = 0 β (((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = 0) β ((πβ3) = (0β(πβ2)) β (πβ3) = 0))) |
46 | 42, 45 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ1) = 0 β ((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = 0))) |
47 | 46 | pm5.32d 578 |
. . . . . . . . . 10
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (((πβ1) = 0 β§ (πβ3) = ((πβ1)β(πβ2))) β ((πβ1) = 0 β§ (πβ3) = 0))) |
48 | 39, 47 | orbi12d 918 |
. . . . . . . . 9
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (((((πβ1) = 1 β§ (πβ3) = ((πβ1)β(πβ2))) β¨ ((πβ1) β
(β€β₯β2) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = ((πβ1)β(πβ2)))) β ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0)))) |
49 | 25, 48 | bitrid 283 |
. . . . . . . 8
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β (((((πβ1) = 1 β¨ (πβ1) β
(β€β₯β2)) β¨ (πβ1) = 0) β§ (πβ3) = ((πβ1)β(πβ2))) β ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0)))) |
50 | 21, 49 | bitrd 279 |
. . . . . . 7
β’ ((π β (β0
βm (1...3)) β§ (πβ2) β β) β ((πβ3) = ((πβ1)β(πβ2)) β ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0)))) |
51 | 50 | pm5.32da 580 |
. . . . . 6
β’ (π β (β0
βm (1...3)) β (((πβ2) β β β§ (πβ3) = ((πβ1)β(πβ2))) β ((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))))) |
52 | 2, 51 | bitrid 283 |
. . . . 5
β’ (π β (β0
βm (1...3)) β (((πβ3) = ((πβ1)β(πβ2)) β§ (πβ2) β β) β ((πβ2) β β β§
((((πβ1) = 1 β§
(πβ3) = 1) β¨
(((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))))) |
53 | | ancom 462 |
. . . . . 6
β’ (((πβ3) = ((πβ1)β(πβ2)) β§ Β¬ (πβ2) β β) β (Β¬
(πβ2) β β
β§ (πβ3) = ((πβ1)β(πβ2)))) |
54 | | 2nn 12231 |
. . . . . . . . . . . 12
β’ 2 β
β |
55 | 54 | jm2.27dlem3 41378 |
. . . . . . . . . . 11
β’ 2 β
(1...2) |
56 | 7, 55 | sselii 3942 |
. . . . . . . . . 10
β’ 2 β
(1...3) |
57 | | ffvelcdm 7033 |
. . . . . . . . . 10
β’ ((π:(1...3)βΆβ0 β§ 2
β (1...3)) β (πβ2) β
β0) |
58 | 3, 56, 57 | sylancl 587 |
. . . . . . . . 9
β’ (π β (β0
βm (1...3)) β (πβ2) β
β0) |
59 | | elnn0 12420 |
. . . . . . . . . . 11
β’ ((πβ2) β
β0 β ((πβ2) β β β¨ (πβ2) = 0)) |
60 | | pm2.53 850 |
. . . . . . . . . . 11
β’ (((πβ2) β β β¨
(πβ2) = 0) β
(Β¬ (πβ2) β
β β (πβ2)
= 0)) |
61 | 59, 60 | sylbi 216 |
. . . . . . . . . 10
β’ ((πβ2) β
β0 β (Β¬ (πβ2) β β β (πβ2) = 0)) |
62 | | 0nnn 12194 |
. . . . . . . . . . 11
β’ Β¬ 0
β β |
63 | | eleq1 2822 |
. . . . . . . . . . 11
β’ ((πβ2) = 0 β ((πβ2) β β β
0 β β)) |
64 | 62, 63 | mtbiri 327 |
. . . . . . . . . 10
β’ ((πβ2) = 0 β Β¬
(πβ2) β
β) |
65 | 61, 64 | impbid1 224 |
. . . . . . . . 9
β’ ((πβ2) β
β0 β (Β¬ (πβ2) β β β (πβ2) = 0)) |
66 | 58, 65 | syl 17 |
. . . . . . . 8
β’ (π β (β0
βm (1...3)) β (Β¬ (πβ2) β β β (πβ2) = 0)) |
67 | 66 | anbi1d 631 |
. . . . . . 7
β’ (π β (β0
βm (1...3)) β ((Β¬ (πβ2) β β β§ (πβ3) = ((πβ1)β(πβ2))) β ((πβ2) = 0 β§ (πβ3) = ((πβ1)β(πβ2))))) |
68 | 13 | nn0cnd 12480 |
. . . . . . . . . . 11
β’ (π β (β0
βm (1...3)) β (πβ1) β β) |
69 | 68 | exp0d 14051 |
. . . . . . . . . 10
β’ (π β (β0
βm (1...3)) β ((πβ1)β0) = 1) |
70 | 69 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π β (β0
βm (1...3)) β ((πβ3) = ((πβ1)β0) β (πβ3) = 1)) |
71 | | oveq2 7366 |
. . . . . . . . . . 11
β’ ((πβ2) = 0 β ((πβ1)β(πβ2)) = ((πβ1)β0)) |
72 | 71 | eqeq2d 2744 |
. . . . . . . . . 10
β’ ((πβ2) = 0 β ((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = ((πβ1)β0))) |
73 | 72 | bibi1d 344 |
. . . . . . . . 9
β’ ((πβ2) = 0 β (((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = 1) β ((πβ3) = ((πβ1)β0) β (πβ3) = 1))) |
74 | 70, 73 | syl5ibrcom 247 |
. . . . . . . 8
β’ (π β (β0
βm (1...3)) β ((πβ2) = 0 β ((πβ3) = ((πβ1)β(πβ2)) β (πβ3) = 1))) |
75 | 74 | pm5.32d 578 |
. . . . . . 7
β’ (π β (β0
βm (1...3)) β (((πβ2) = 0 β§ (πβ3) = ((πβ1)β(πβ2))) β ((πβ2) = 0 β§ (πβ3) = 1))) |
76 | 67, 75 | bitrd 279 |
. . . . . 6
β’ (π β (β0
βm (1...3)) β ((Β¬ (πβ2) β β β§ (πβ3) = ((πβ1)β(πβ2))) β ((πβ2) = 0 β§ (πβ3) = 1))) |
77 | 53, 76 | bitrid 283 |
. . . . 5
β’ (π β (β0
βm (1...3)) β (((πβ3) = ((πβ1)β(πβ2)) β§ Β¬ (πβ2) β β) β ((πβ2) = 0 β§ (πβ3) =
1))) |
78 | 52, 77 | orbi12d 918 |
. . . 4
β’ (π β (β0
βm (1...3)) β ((((πβ3) = ((πβ1)β(πβ2)) β§ (πβ2) β β) β¨ ((πβ3) = ((πβ1)β(πβ2)) β§ Β¬ (πβ2) β β)) β (((πβ2) β β β§
((((πβ1) = 1 β§
(πβ3) = 1) β¨
(((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))) β¨ ((πβ2) = 0 β§ (πβ3) = 1)))) |
79 | 1, 78 | bitrid 283 |
. . 3
β’ (π β (β0
βm (1...3)) β ((πβ3) = ((πβ1)β(πβ2)) β (((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))) β¨ ((πβ2) = 0 β§ (πβ3) = 1)))) |
80 | 79 | rabbiia 3410 |
. 2
β’ {π β (β0
βm (1...3)) β£ (πβ3) = ((πβ1)β(πβ2))} = {π β (β0
βm (1...3)) β£ (((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))) β¨ ((πβ2) = 0 β§ (πβ3) = 1))} |
81 | | 3nn0 12436 |
. . . . 5
β’ 3 β
β0 |
82 | | ovex 7391 |
. . . . . 6
β’ (1...3)
β V |
83 | | mzpproj 41103 |
. . . . . 6
β’ (((1...3)
β V β§ 2 β (1...3)) β (π β (β€ βm (1...3))
β¦ (πβ2)) β
(mzPolyβ(1...3))) |
84 | 82, 56, 83 | mp2an 691 |
. . . . 5
β’ (π β (β€
βm (1...3)) β¦ (πβ2)) β
(mzPolyβ(1...3)) |
85 | | elnnrabdioph 41173 |
. . . . 5
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ2)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ2) β β} β
(Diophβ3)) |
86 | 81, 84, 85 | mp2an 691 |
. . . 4
β’ {π β (β0
βm (1...3)) β£ (πβ2) β β} β
(Diophβ3) |
87 | | mzpproj 41103 |
. . . . . . . . 9
β’ (((1...3)
β V β§ 1 β (1...3)) β (π β (β€ βm (1...3))
β¦ (πβ1)) β
(mzPolyβ(1...3))) |
88 | 82, 11, 87 | mp2an 691 |
. . . . . . . 8
β’ (π β (β€
βm (1...3)) β¦ (πβ1)) β
(mzPolyβ(1...3)) |
89 | | 1z 12538 |
. . . . . . . . 9
β’ 1 β
β€ |
90 | | mzpconstmpt 41106 |
. . . . . . . . 9
β’ (((1...3)
β V β§ 1 β β€) β (π β (β€ βm (1...3))
β¦ 1) β (mzPolyβ(1...3))) |
91 | 82, 89, 90 | mp2an 691 |
. . . . . . . 8
β’ (π β (β€
βm (1...3)) β¦ 1) β
(mzPolyβ(1...3)) |
92 | | eqrabdioph 41143 |
. . . . . . . 8
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ1)) β
(mzPolyβ(1...3)) β§ (π β (β€ βm (1...3))
β¦ 1) β (mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ1) = 1} β
(Diophβ3)) |
93 | 81, 88, 91, 92 | mp3an 1462 |
. . . . . . 7
β’ {π β (β0
βm (1...3)) β£ (πβ1) = 1} β
(Diophβ3) |
94 | | 3nn 12237 |
. . . . . . . . . 10
β’ 3 β
β |
95 | 94 | jm2.27dlem3 41378 |
. . . . . . . . 9
β’ 3 β
(1...3) |
96 | | mzpproj 41103 |
. . . . . . . . 9
β’ (((1...3)
β V β§ 3 β (1...3)) β (π β (β€ βm (1...3))
β¦ (πβ3)) β
(mzPolyβ(1...3))) |
97 | 82, 95, 96 | mp2an 691 |
. . . . . . . 8
β’ (π β (β€
βm (1...3)) β¦ (πβ3)) β
(mzPolyβ(1...3)) |
98 | | eqrabdioph 41143 |
. . . . . . . 8
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ3)) β
(mzPolyβ(1...3)) β§ (π β (β€ βm (1...3))
β¦ 1) β (mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ3) = 1} β
(Diophβ3)) |
99 | 81, 97, 91, 98 | mp3an 1462 |
. . . . . . 7
β’ {π β (β0
βm (1...3)) β£ (πβ3) = 1} β
(Diophβ3) |
100 | | anrabdioph 41146 |
. . . . . . 7
β’ (({π β (β0
βm (1...3)) β£ (πβ1) = 1} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ (πβ3) = 1} β (Diophβ3)) β
{π β
(β0 βm (1...3)) β£ ((πβ1) = 1 β§ (πβ3) = 1)} β
(Diophβ3)) |
101 | 93, 99, 100 | mp2an 691 |
. . . . . 6
β’ {π β (β0
βm (1...3)) β£ ((πβ1) = 1 β§ (πβ3) = 1)} β
(Diophβ3) |
102 | | expdiophlem2 41389 |
. . . . . 6
β’ {π β (β0
βm (1...3)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))} β
(Diophβ3) |
103 | | orrabdioph 41147 |
. . . . . 6
β’ (({π β (β0
βm (1...3)) β£ ((πβ1) = 1 β§ (πβ3) = 1)} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))} β (Diophβ3)) β
{π β
(β0 βm (1...3)) β£ (((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2))))} β
(Diophβ3)) |
104 | 101, 102,
103 | mp2an 691 |
. . . . 5
β’ {π β (β0
βm (1...3)) β£ (((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2))))} β
(Diophβ3) |
105 | | eq0rabdioph 41142 |
. . . . . . 7
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ1)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ1) = 0} β
(Diophβ3)) |
106 | 81, 88, 105 | mp2an 691 |
. . . . . 6
β’ {π β (β0
βm (1...3)) β£ (πβ1) = 0} β
(Diophβ3) |
107 | | eq0rabdioph 41142 |
. . . . . . 7
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ3)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ3) = 0} β
(Diophβ3)) |
108 | 81, 97, 107 | mp2an 691 |
. . . . . 6
β’ {π β (β0
βm (1...3)) β£ (πβ3) = 0} β
(Diophβ3) |
109 | | anrabdioph 41146 |
. . . . . 6
β’ (({π β (β0
βm (1...3)) β£ (πβ1) = 0} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ (πβ3) = 0} β (Diophβ3)) β
{π β
(β0 βm (1...3)) β£ ((πβ1) = 0 β§ (πβ3) = 0)} β
(Diophβ3)) |
110 | 106, 108,
109 | mp2an 691 |
. . . . 5
β’ {π β (β0
βm (1...3)) β£ ((πβ1) = 0 β§ (πβ3) = 0)} β
(Diophβ3) |
111 | | orrabdioph 41147 |
. . . . 5
β’ (({π β (β0
βm (1...3)) β£ (((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2))))} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ ((πβ1) = 0 β§ (πβ3) = 0)} β (Diophβ3))
β {π β
(β0 βm (1...3)) β£ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))} β
(Diophβ3)) |
112 | 104, 110,
111 | mp2an 691 |
. . . 4
β’ {π β (β0
βm (1...3)) β£ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))} β
(Diophβ3) |
113 | | anrabdioph 41146 |
. . . 4
β’ (({π β (β0
βm (1...3)) β£ (πβ2) β β} β
(Diophβ3) β§ {π
β (β0 βm (1...3)) β£ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))} β (Diophβ3))
β {π β
(β0 βm (1...3)) β£ ((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0)))} β
(Diophβ3)) |
114 | 86, 112, 113 | mp2an 691 |
. . 3
β’ {π β (β0
βm (1...3)) β£ ((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0)))} β
(Diophβ3) |
115 | | eq0rabdioph 41142 |
. . . . 5
β’ ((3
β β0 β§ (π β (β€ βm (1...3))
β¦ (πβ2)) β
(mzPolyβ(1...3))) β {π β (β0
βm (1...3)) β£ (πβ2) = 0} β
(Diophβ3)) |
116 | 81, 84, 115 | mp2an 691 |
. . . 4
β’ {π β (β0
βm (1...3)) β£ (πβ2) = 0} β
(Diophβ3) |
117 | | anrabdioph 41146 |
. . . 4
β’ (({π β (β0
βm (1...3)) β£ (πβ2) = 0} β (Diophβ3) β§
{π β
(β0 βm (1...3)) β£ (πβ3) = 1} β (Diophβ3)) β
{π β
(β0 βm (1...3)) β£ ((πβ2) = 0 β§ (πβ3) = 1)} β
(Diophβ3)) |
118 | 116, 99, 117 | mp2an 691 |
. . 3
β’ {π β (β0
βm (1...3)) β£ ((πβ2) = 0 β§ (πβ3) = 1)} β
(Diophβ3) |
119 | | orrabdioph 41147 |
. . 3
β’ (({π β (β0
βm (1...3)) β£ ((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0)))} β (Diophβ3)
β§ {π β
(β0 βm (1...3)) β£ ((πβ2) = 0 β§ (πβ3) = 1)} β (Diophβ3))
β {π β
(β0 βm (1...3)) β£ (((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))) β¨ ((πβ2) = 0 β§ (πβ3) = 1))} β
(Diophβ3)) |
120 | 114, 118,
119 | mp2an 691 |
. 2
β’ {π β (β0
βm (1...3)) β£ (((πβ2) β β β§ ((((πβ1) = 1 β§ (πβ3) = 1) β¨ (((πβ1) β
(β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))) β¨ ((πβ1) = 0 β§ (πβ3) = 0))) β¨ ((πβ2) = 0 β§ (πβ3) = 1))} β
(Diophβ3) |
121 | 80, 120 | eqeltri 2830 |
1
β’ {π β (β0
βm (1...3)) β£ (πβ3) = ((πβ1)β(πβ2))} β
(Diophβ3) |