Step | Hyp | Ref
| Expression |
1 | | dcubic.3 |
. . . . . . 7
โข (๐ โ (๐โ3) = (๐บ โ ๐)) |
2 | 1 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((๐โ3)โ2) = ((๐บ โ ๐)โ2)) |
3 | | dcubic.g |
. . . . . . 7
โข (๐ โ ๐บ โ โ) |
4 | | dcubic.n |
. . . . . . . 8
โข (๐ โ ๐ = (๐ / 2)) |
5 | | dcubic.d |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
6 | 5 | halfcld 12405 |
. . . . . . . 8
โข (๐ โ (๐ / 2) โ โ) |
7 | 4, 6 | eqeltrd 2838 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
8 | | binom2sub 14130 |
. . . . . . 7
โข ((๐บ โ โ โง ๐ โ โ) โ ((๐บ โ ๐)โ2) = (((๐บโ2) โ (2 ยท (๐บ ยท ๐))) + (๐โ2))) |
9 | 3, 7, 8 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐บ โ ๐)โ2) = (((๐บโ2) โ (2 ยท (๐บ ยท ๐))) + (๐โ2))) |
10 | | dcubic.2 |
. . . . . . . 8
โข (๐ โ (๐บโ2) = ((๐โ2) + (๐โ3))) |
11 | | 2cnd 12238 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
12 | 11, 3, 7 | mul12d 11371 |
. . . . . . . . 9
โข (๐ โ (2 ยท (๐บ ยท ๐)) = (๐บ ยท (2 ยท ๐))) |
13 | 4 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) = (2 ยท (๐ / 2))) |
14 | | 2ne0 12264 |
. . . . . . . . . . . . 13
โข 2 โ
0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ 0) |
16 | 5, 11, 15 | divcan2d 11940 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (๐ / 2)) = ๐) |
17 | 13, 16 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) = ๐) |
18 | 17 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (๐บ ยท (2 ยท ๐)) = (๐บ ยท ๐)) |
19 | 3, 5 | mulcomd 11183 |
. . . . . . . . 9
โข (๐ โ (๐บ ยท ๐) = (๐ ยท ๐บ)) |
20 | 12, 18, 19 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ (2 ยท (๐บ ยท ๐)) = (๐ ยท ๐บ)) |
21 | 10, 20 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ ((๐บโ2) โ (2 ยท (๐บ ยท ๐))) = (((๐โ2) + (๐โ3)) โ (๐ ยท ๐บ))) |
22 | 21 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (((๐บโ2) โ (2 ยท (๐บ ยท ๐))) + (๐โ2)) = ((((๐โ2) + (๐โ3)) โ (๐ ยท ๐บ)) + (๐โ2))) |
23 | 2, 9, 22 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ ((๐โ3)โ2) = ((((๐โ2) + (๐โ3)) โ (๐ ยท ๐บ)) + (๐โ2))) |
24 | 7 | sqcld 14056 |
. . . . . . 7
โข (๐ โ (๐โ2) โ โ) |
25 | | dcubic.m |
. . . . . . . . 9
โข (๐ โ ๐ = (๐ / 3)) |
26 | | dcubic.c |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
27 | | 3cn 12241 |
. . . . . . . . . . 11
โข 3 โ
โ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 3 โ
โ) |
29 | | 3ne0 12266 |
. . . . . . . . . . 11
โข 3 โ
0 |
30 | 29 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 3 โ 0) |
31 | 26, 28, 30 | divcld 11938 |
. . . . . . . . 9
โข (๐ โ (๐ / 3) โ โ) |
32 | 25, 31 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
33 | | 3nn0 12438 |
. . . . . . . 8
โข 3 โ
โ0 |
34 | | expcl 13992 |
. . . . . . . 8
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
35 | 32, 33, 34 | sylancl 587 |
. . . . . . 7
โข (๐ โ (๐โ3) โ โ) |
36 | 24, 35 | addcld 11181 |
. . . . . 6
โข (๐ โ ((๐โ2) + (๐โ3)) โ โ) |
37 | 5, 3 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ ยท ๐บ) โ โ) |
38 | 36, 24, 37 | addsubd 11540 |
. . . . 5
โข (๐ โ ((((๐โ2) + (๐โ3)) + (๐โ2)) โ (๐ ยท ๐บ)) = ((((๐โ2) + (๐โ3)) โ (๐ ยท ๐บ)) + (๐โ2))) |
39 | 24, 35, 24 | add32d 11389 |
. . . . . . 7
โข (๐ โ (((๐โ2) + (๐โ3)) + (๐โ2)) = (((๐โ2) + (๐โ2)) + (๐โ3))) |
40 | 24 | 2timesd 12403 |
. . . . . . . 8
โข (๐ โ (2 ยท (๐โ2)) = ((๐โ2) + (๐โ2))) |
41 | 40 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((2 ยท (๐โ2)) + (๐โ3)) = (((๐โ2) + (๐โ2)) + (๐โ3))) |
42 | 39, 41 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ (((๐โ2) + (๐โ3)) + (๐โ2)) = ((2 ยท (๐โ2)) + (๐โ3))) |
43 | 42 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((((๐โ2) + (๐โ3)) + (๐โ2)) โ (๐ ยท ๐บ)) = (((2 ยท (๐โ2)) + (๐โ3)) โ (๐ ยท ๐บ))) |
44 | 23, 38, 43 | 3eqtr2d 2783 |
. . . 4
โข (๐ โ ((๐โ3)โ2) = (((2 ยท (๐โ2)) + (๐โ3)) โ (๐ ยท ๐บ))) |
45 | 5, 3, 7 | subdid 11618 |
. . . . . . 7
โข (๐ โ (๐ ยท (๐บ โ ๐)) = ((๐ ยท ๐บ) โ (๐ ยท ๐))) |
46 | 1 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (๐ ยท (๐โ3)) = (๐ ยท (๐บ โ ๐))) |
47 | 7 | sqvald 14055 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
48 | 47 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (2 ยท (๐โ2)) = (2 ยท (๐ ยท ๐))) |
49 | 11, 7, 7 | mulassd 11185 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) ยท ๐) = (2 ยท (๐ ยท ๐))) |
50 | 17 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) ยท ๐) = (๐ ยท ๐)) |
51 | 48, 49, 50 | 3eqtr2d 2783 |
. . . . . . . 8
โข (๐ โ (2 ยท (๐โ2)) = (๐ ยท ๐)) |
52 | 51 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ ((๐ ยท ๐บ) โ (2 ยท (๐โ2))) = ((๐ ยท ๐บ) โ (๐ ยท ๐))) |
53 | 45, 46, 52 | 3eqtr4d 2787 |
. . . . . 6
โข (๐ โ (๐ ยท (๐โ3)) = ((๐ ยท ๐บ) โ (2 ยท (๐โ2)))) |
54 | 53 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((๐ ยท (๐โ3)) โ (๐โ3)) = (((๐ ยท ๐บ) โ (2 ยท (๐โ2))) โ (๐โ3))) |
55 | | 2cn 12235 |
. . . . . . 7
โข 2 โ
โ |
56 | | mulcl 11142 |
. . . . . . 7
โข ((2
โ โ โง (๐โ2) โ โ) โ (2 ยท
(๐โ2)) โ
โ) |
57 | 55, 24, 56 | sylancr 588 |
. . . . . 6
โข (๐ โ (2 ยท (๐โ2)) โ
โ) |
58 | 37, 57, 35 | subsub4d 11550 |
. . . . 5
โข (๐ โ (((๐ ยท ๐บ) โ (2 ยท (๐โ2))) โ (๐โ3)) = ((๐ ยท ๐บ) โ ((2 ยท (๐โ2)) + (๐โ3)))) |
59 | 54, 58 | eqtrd 2777 |
. . . 4
โข (๐ โ ((๐ ยท (๐โ3)) โ (๐โ3)) = ((๐ ยท ๐บ) โ ((2 ยท (๐โ2)) + (๐โ3)))) |
60 | 44, 59 | oveq12d 7380 |
. . 3
โข (๐ โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = ((((2 ยท (๐โ2)) + (๐โ3)) โ (๐ ยท ๐บ)) + ((๐ ยท ๐บ) โ ((2 ยท (๐โ2)) + (๐โ3))))) |
61 | 57, 35 | addcld 11181 |
. . . 4
โข (๐ โ ((2 ยท (๐โ2)) + (๐โ3)) โ โ) |
62 | | npncan2 11435 |
. . . 4
โข ((((2
ยท (๐โ2)) +
(๐โ3)) โ โ
โง (๐ ยท ๐บ) โ โ) โ ((((2
ยท (๐โ2)) +
(๐โ3)) โ (๐ ยท ๐บ)) + ((๐ ยท ๐บ) โ ((2 ยท (๐โ2)) + (๐โ3)))) = 0) |
63 | 61, 37, 62 | syl2anc 585 |
. . 3
โข (๐ โ ((((2 ยท (๐โ2)) + (๐โ3)) โ (๐ ยท ๐บ)) + ((๐ ยท ๐บ) โ ((2 ยท (๐โ2)) + (๐โ3)))) = 0) |
64 | 60, 63 | eqtrd 2777 |
. 2
โข (๐ โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = 0) |
65 | | dcubic.x |
. . 3
โข (๐ โ ๐ โ โ) |
66 | | dcubic.t |
. . 3
โข (๐ โ ๐ โ โ) |
67 | | dcubic.0 |
. . 3
โข (๐ โ ๐ โ 0) |
68 | | dcubic1.x |
. . 3
โข (๐ โ ๐ = (๐ โ (๐ / ๐))) |
69 | 26, 5, 65, 66, 1, 3, 10, 25, 4, 67, 66, 67, 68 | dcubic1lem 26209 |
. 2
โข (๐ โ (((๐โ3) + ((๐ ยท ๐) + ๐)) = 0 โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = 0)) |
70 | 64, 69 | mpbird 257 |
1
โข (๐ โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) |