Step | Hyp | Ref
| Expression |
1 | | cubic2.a |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
2 | | cubic2.x |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
3 | | 3nn0 12438 |
. . . . . . . 8
โข 3 โ
โ0 |
4 | | expcl 13992 |
. . . . . . . 8
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
5 | 2, 3, 4 | sylancl 587 |
. . . . . . 7
โข (๐ โ (๐โ3) โ โ) |
6 | 1, 5 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ด ยท (๐โ3)) โ โ) |
7 | | cubic2.b |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
8 | 2 | sqcld 14056 |
. . . . . . 7
โข (๐ โ (๐โ2) โ โ) |
9 | 7, 8 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ต ยท (๐โ2)) โ โ) |
10 | 6, 9 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) โ โ) |
11 | | cubic2.c |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
12 | 11, 2 | mulcld 11182 |
. . . . . 6
โข (๐ โ (๐ถ ยท ๐) โ โ) |
13 | | cubic2.d |
. . . . . 6
โข (๐ โ ๐ท โ โ) |
14 | 12, 13 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐ถ ยท ๐) + ๐ท) โ โ) |
15 | 10, 14 | addcld 11181 |
. . . 4
โข (๐ โ (((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) โ โ) |
16 | | cubic2.z |
. . . 4
โข (๐ โ ๐ด โ 0) |
17 | 15, 1, 16 | diveq0ad 11948 |
. . 3
โข (๐ โ (((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) / ๐ด) = 0 โ (((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0)) |
18 | 10, 14, 1, 16 | divdird 11976 |
. . . . 5
โข (๐ โ ((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) / ๐ด) = ((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) / ๐ด) + (((๐ถ ยท ๐) + ๐ท) / ๐ด))) |
19 | 6, 9, 1, 16 | divdird 11976 |
. . . . . . 7
โข (๐ โ (((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) / ๐ด) = (((๐ด ยท (๐โ3)) / ๐ด) + ((๐ต ยท (๐โ2)) / ๐ด))) |
20 | 5, 1, 16 | divcan3d 11943 |
. . . . . . . 8
โข (๐ โ ((๐ด ยท (๐โ3)) / ๐ด) = (๐โ3)) |
21 | 7, 8, 1, 16 | div23d 11975 |
. . . . . . . 8
โข (๐ โ ((๐ต ยท (๐โ2)) / ๐ด) = ((๐ต / ๐ด) ยท (๐โ2))) |
22 | 20, 21 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ (((๐ด ยท (๐โ3)) / ๐ด) + ((๐ต ยท (๐โ2)) / ๐ด)) = ((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2)))) |
23 | 19, 22 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) / ๐ด) = ((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2)))) |
24 | 12, 13, 1, 16 | divdird 11976 |
. . . . . . 7
โข (๐ โ (((๐ถ ยท ๐) + ๐ท) / ๐ด) = (((๐ถ ยท ๐) / ๐ด) + (๐ท / ๐ด))) |
25 | 11, 2, 1, 16 | div23d 11975 |
. . . . . . . 8
โข (๐ โ ((๐ถ ยท ๐) / ๐ด) = ((๐ถ / ๐ด) ยท ๐)) |
26 | 25 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (((๐ถ ยท ๐) / ๐ด) + (๐ท / ๐ด)) = (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด))) |
27 | 24, 26 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (((๐ถ ยท ๐) + ๐ท) / ๐ด) = (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด))) |
28 | 23, 27 | oveq12d 7380 |
. . . . 5
โข (๐ โ ((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) / ๐ด) + (((๐ถ ยท ๐) + ๐ท) / ๐ด)) = (((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2))) + (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด)))) |
29 | 18, 28 | eqtrd 2777 |
. . . 4
โข (๐ โ ((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) / ๐ด) = (((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2))) + (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด)))) |
30 | 29 | eqeq1d 2739 |
. . 3
โข (๐ โ (((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) / ๐ด) = 0 โ (((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2))) + (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด))) = 0)) |
31 | 17, 30 | bitr3d 281 |
. 2
โข (๐ โ ((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0 โ (((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2))) + (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด))) = 0)) |
32 | 7, 1, 16 | divcld 11938 |
. . 3
โข (๐ โ (๐ต / ๐ด) โ โ) |
33 | 11, 1, 16 | divcld 11938 |
. . 3
โข (๐ โ (๐ถ / ๐ด) โ โ) |
34 | 13, 1, 16 | divcld 11938 |
. . 3
โข (๐ โ (๐ท / ๐ด) โ โ) |
35 | | cubic2.t |
. . . 4
โข (๐ โ ๐ โ โ) |
36 | 35, 1, 16 | divcld 11938 |
. . 3
โข (๐ โ (๐ / ๐ด) โ โ) |
37 | 3 | a1i 11 |
. . . . 5
โข (๐ โ 3 โ
โ0) |
38 | 35, 1, 16, 37 | expdivd 14072 |
. . . 4
โข (๐ โ ((๐ / ๐ด)โ3) = ((๐โ3) / (๐ดโ3))) |
39 | | cubic2.3 |
. . . . 5
โข (๐ โ (๐โ3) = ((๐ + ๐บ) / 2)) |
40 | 39 | oveq1d 7377 |
. . . 4
โข (๐ โ ((๐โ3) / (๐ดโ3)) = (((๐ + ๐บ) / 2) / (๐ดโ3))) |
41 | | cubic2.n |
. . . . . . . 8
โข (๐ โ ๐ = (((2 ยท (๐ตโ3)) โ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) + (;27 ยท ((๐ดโ2) ยท ๐ท)))) |
42 | | 2cn 12235 |
. . . . . . . . . . 11
โข 2 โ
โ |
43 | | expcl 13992 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง 3 โ
โ0) โ (๐ตโ3) โ โ) |
44 | 7, 3, 43 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ (๐ตโ3) โ โ) |
45 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((2
โ โ โง (๐ตโ3) โ โ) โ (2 ยท
(๐ตโ3)) โ
โ) |
46 | 42, 44, 45 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (2 ยท (๐ตโ3)) โ
โ) |
47 | | 9cn 12260 |
. . . . . . . . . . . 12
โข 9 โ
โ |
48 | | mulcl 11142 |
. . . . . . . . . . . 12
โข ((9
โ โ โง ๐ด
โ โ) โ (9 ยท ๐ด) โ โ) |
49 | 47, 1, 48 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (9 ยท ๐ด) โ
โ) |
50 | 7, 11 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ (๐ต ยท ๐ถ) โ โ) |
51 | 49, 50 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) โ โ) |
52 | 46, 51 | subcld 11519 |
. . . . . . . . 9
โข (๐ โ ((2 ยท (๐ตโ3)) โ ((9 ยท
๐ด) ยท (๐ต ยท ๐ถ))) โ โ) |
53 | | 2nn0 12437 |
. . . . . . . . . . . 12
โข 2 โ
โ0 |
54 | | 7nn 12252 |
. . . . . . . . . . . 12
โข 7 โ
โ |
55 | 53, 54 | decnncl 12645 |
. . . . . . . . . . 11
โข ;27 โ โ |
56 | 55 | nncni 12170 |
. . . . . . . . . 10
โข ;27 โ โ |
57 | 1 | sqcld 14056 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ2) โ โ) |
58 | 57, 13 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((๐ดโ2) ยท ๐ท) โ โ) |
59 | | mulcl 11142 |
. . . . . . . . . 10
โข ((;27 โ โ โง ((๐ดโ2) ยท ๐ท) โ โ) โ (;27 ยท ((๐ดโ2) ยท ๐ท)) โ โ) |
60 | 56, 58, 59 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ (;27 ยท ((๐ดโ2) ยท ๐ท)) โ โ) |
61 | 52, 60 | addcld 11181 |
. . . . . . . 8
โข (๐ โ (((2 ยท (๐ตโ3)) โ ((9 ยท
๐ด) ยท (๐ต ยท ๐ถ))) + (;27 ยท ((๐ดโ2) ยท ๐ท))) โ โ) |
62 | 41, 61 | eqeltrd 2838 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
63 | | cubic2.g |
. . . . . . 7
โข (๐ โ ๐บ โ โ) |
64 | 62, 63 | addcld 11181 |
. . . . . 6
โข (๐ โ (๐ + ๐บ) โ โ) |
65 | | 2cnd 12238 |
. . . . . 6
โข (๐ โ 2 โ
โ) |
66 | | expcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ3) โ โ) |
67 | 1, 3, 66 | sylancl 587 |
. . . . . 6
โข (๐ โ (๐ดโ3) โ โ) |
68 | | 2ne0 12264 |
. . . . . . 7
โข 2 โ
0 |
69 | 68 | a1i 11 |
. . . . . 6
โข (๐ โ 2 โ 0) |
70 | | 3z 12543 |
. . . . . . . 8
โข 3 โ
โค |
71 | 70 | a1i 11 |
. . . . . . 7
โข (๐ โ 3 โ
โค) |
72 | 1, 16, 71 | expne0d 14064 |
. . . . . 6
โข (๐ โ (๐ดโ3) โ 0) |
73 | 64, 65, 67, 69, 72 | divdiv32d 11963 |
. . . . 5
โข (๐ โ (((๐ + ๐บ) / 2) / (๐ดโ3)) = (((๐ + ๐บ) / (๐ดโ3)) / 2)) |
74 | 62, 63, 67, 72 | divdird 11976 |
. . . . . 6
โข (๐ โ ((๐ + ๐บ) / (๐ดโ3)) = ((๐ / (๐ดโ3)) + (๐บ / (๐ดโ3)))) |
75 | 74 | oveq1d 7377 |
. . . . 5
โข (๐ โ (((๐ + ๐บ) / (๐ดโ3)) / 2) = (((๐ / (๐ดโ3)) + (๐บ / (๐ดโ3))) / 2)) |
76 | 73, 75 | eqtrd 2777 |
. . . 4
โข (๐ โ (((๐ + ๐บ) / 2) / (๐ดโ3)) = (((๐ / (๐ดโ3)) + (๐บ / (๐ดโ3))) / 2)) |
77 | 38, 40, 76 | 3eqtrd 2781 |
. . 3
โข (๐ โ ((๐ / ๐ด)โ3) = (((๐ / (๐ดโ3)) + (๐บ / (๐ดโ3))) / 2)) |
78 | 63, 67, 72 | divcld 11938 |
. . 3
โข (๐ โ (๐บ / (๐ดโ3)) โ โ) |
79 | 63, 67, 72 | sqdivd 14071 |
. . . 4
โข (๐ โ ((๐บ / (๐ดโ3))โ2) = ((๐บโ2) / ((๐ดโ3)โ2))) |
80 | | cubic2.2 |
. . . . 5
โข (๐ โ (๐บโ2) = ((๐โ2) โ (4 ยท (๐โ3)))) |
81 | 80 | oveq1d 7377 |
. . . 4
โข (๐ โ ((๐บโ2) / ((๐ดโ3)โ2)) = (((๐โ2) โ (4 ยท (๐โ3))) / ((๐ดโ3)โ2))) |
82 | 62 | sqcld 14056 |
. . . . . 6
โข (๐ โ (๐โ2) โ โ) |
83 | | 4cn 12245 |
. . . . . . 7
โข 4 โ
โ |
84 | | cubic2.m |
. . . . . . . . 9
โข (๐ โ ๐ = ((๐ตโ2) โ (3 ยท (๐ด ยท ๐ถ)))) |
85 | 7 | sqcld 14056 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ2) โ โ) |
86 | | 3cn 12241 |
. . . . . . . . . . 11
โข 3 โ
โ |
87 | 1, 11 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
88 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((3
โ โ โง (๐ด
ยท ๐ถ) โ โ)
โ (3 ยท (๐ด
ยท ๐ถ)) โ
โ) |
89 | 86, 87, 88 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (3 ยท (๐ด ยท ๐ถ)) โ โ) |
90 | 85, 89 | subcld 11519 |
. . . . . . . . 9
โข (๐ โ ((๐ตโ2) โ (3 ยท (๐ด ยท ๐ถ))) โ โ) |
91 | 84, 90 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
92 | | expcl 13992 |
. . . . . . . 8
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
93 | 91, 3, 92 | sylancl 587 |
. . . . . . 7
โข (๐ โ (๐โ3) โ โ) |
94 | | mulcl 11142 |
. . . . . . 7
โข ((4
โ โ โง (๐โ3) โ โ) โ (4 ยท
(๐โ3)) โ
โ) |
95 | 83, 93, 94 | sylancr 588 |
. . . . . 6
โข (๐ โ (4 ยท (๐โ3)) โ
โ) |
96 | 67 | sqcld 14056 |
. . . . . 6
โข (๐ โ ((๐ดโ3)โ2) โ
โ) |
97 | | sqne0 14035 |
. . . . . . . 8
โข ((๐ดโ3) โ โ โ
(((๐ดโ3)โ2) โ 0
โ (๐ดโ3) โ
0)) |
98 | 67, 97 | syl 17 |
. . . . . . 7
โข (๐ โ (((๐ดโ3)โ2) โ 0 โ (๐ดโ3) โ
0)) |
99 | 72, 98 | mpbird 257 |
. . . . . 6
โข (๐ โ ((๐ดโ3)โ2) โ 0) |
100 | 82, 95, 96, 99 | divsubdird 11977 |
. . . . 5
โข (๐ โ (((๐โ2) โ (4 ยท (๐โ3))) / ((๐ดโ3)โ2)) = (((๐โ2) / ((๐ดโ3)โ2)) โ ((4 ยท
(๐โ3)) / ((๐ดโ3)โ2)))) |
101 | 62, 67, 72 | sqdivd 14071 |
. . . . . 6
โข (๐ โ ((๐ / (๐ดโ3))โ2) = ((๐โ2) / ((๐ดโ3)โ2))) |
102 | | 2z 12542 |
. . . . . . . . . . . 12
โข 2 โ
โค |
103 | 102 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โค) |
104 | 1, 16, 103 | expne0d 14064 |
. . . . . . . . . 10
โข (๐ โ (๐ดโ2) โ 0) |
105 | 91, 57, 104, 37 | expdivd 14072 |
. . . . . . . . 9
โข (๐ โ ((๐ / (๐ดโ2))โ3) = ((๐โ3) / ((๐ดโ2)โ3))) |
106 | 42, 86 | mulcomi 11170 |
. . . . . . . . . . . 12
โข (2
ยท 3) = (3 ยท 2) |
107 | 106 | oveq2i 7373 |
. . . . . . . . . . 11
โข (๐ดโ(2 ยท 3)) = (๐ดโ(3 ยท
2)) |
108 | 53 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ0) |
109 | 1, 37, 108 | expmuld 14061 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ(2 ยท 3)) = ((๐ดโ2)โ3)) |
110 | 1, 108, 37 | expmuld 14061 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ(3 ยท 2)) = ((๐ดโ3)โ2)) |
111 | 107, 109,
110 | 3eqtr3a 2801 |
. . . . . . . . . 10
โข (๐ โ ((๐ดโ2)โ3) = ((๐ดโ3)โ2)) |
112 | 111 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ ((๐โ3) / ((๐ดโ2)โ3)) = ((๐โ3) / ((๐ดโ3)โ2))) |
113 | 105, 112 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((๐ / (๐ดโ2))โ3) = ((๐โ3) / ((๐ดโ3)โ2))) |
114 | 113 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (4 ยท ((๐ / (๐ดโ2))โ3)) = (4 ยท ((๐โ3) / ((๐ดโ3)โ2)))) |
115 | 83 | a1i 11 |
. . . . . . . 8
โข (๐ โ 4 โ
โ) |
116 | 115, 93, 96, 99 | divassd 11973 |
. . . . . . 7
โข (๐ โ ((4 ยท (๐โ3)) / ((๐ดโ3)โ2)) = (4 ยท ((๐โ3) / ((๐ดโ3)โ2)))) |
117 | 114, 116 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ (4 ยท ((๐ / (๐ดโ2))โ3)) = ((4 ยท (๐โ3)) / ((๐ดโ3)โ2))) |
118 | 101, 117 | oveq12d 7380 |
. . . . 5
โข (๐ โ (((๐ / (๐ดโ3))โ2) โ (4 ยท
((๐ / (๐ดโ2))โ3))) = (((๐โ2) / ((๐ดโ3)โ2)) โ ((4 ยท
(๐โ3)) / ((๐ดโ3)โ2)))) |
119 | 100, 118 | eqtr4d 2780 |
. . . 4
โข (๐ โ (((๐โ2) โ (4 ยท (๐โ3))) / ((๐ดโ3)โ2)) = (((๐ / (๐ดโ3))โ2) โ (4 ยท
((๐ / (๐ดโ2))โ3)))) |
120 | 79, 81, 119 | 3eqtrd 2781 |
. . 3
โข (๐ โ ((๐บ / (๐ดโ3))โ2) = (((๐ / (๐ดโ3))โ2) โ (4 ยท
((๐ / (๐ดโ2))โ3)))) |
121 | 85, 89, 57, 104 | divsubdird 11977 |
. . . 4
โข (๐ โ (((๐ตโ2) โ (3 ยท (๐ด ยท ๐ถ))) / (๐ดโ2)) = (((๐ตโ2) / (๐ดโ2)) โ ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ2)))) |
122 | 84 | oveq1d 7377 |
. . . 4
โข (๐ โ (๐ / (๐ดโ2)) = (((๐ตโ2) โ (3 ยท (๐ด ยท ๐ถ))) / (๐ดโ2))) |
123 | 7, 1, 16 | sqdivd 14071 |
. . . . 5
โข (๐ โ ((๐ต / ๐ด)โ2) = ((๐ตโ2) / (๐ดโ2))) |
124 | 1 | sqvald 14055 |
. . . . . . . . 9
โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
125 | 124 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((๐ด ยท ๐ถ) / (๐ดโ2)) = ((๐ด ยท ๐ถ) / (๐ด ยท ๐ด))) |
126 | 11, 1, 1, 16, 16 | divcan5d 11964 |
. . . . . . . 8
โข (๐ โ ((๐ด ยท ๐ถ) / (๐ด ยท ๐ด)) = (๐ถ / ๐ด)) |
127 | 125, 126 | eqtr2d 2778 |
. . . . . . 7
โข (๐ โ (๐ถ / ๐ด) = ((๐ด ยท ๐ถ) / (๐ดโ2))) |
128 | 127 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (3 ยท (๐ถ / ๐ด)) = (3 ยท ((๐ด ยท ๐ถ) / (๐ดโ2)))) |
129 | 86 | a1i 11 |
. . . . . . 7
โข (๐ โ 3 โ
โ) |
130 | 129, 87, 57, 104 | divassd 11973 |
. . . . . 6
โข (๐ โ ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ2)) = (3 ยท ((๐ด ยท ๐ถ) / (๐ดโ2)))) |
131 | 128, 130 | eqtr4d 2780 |
. . . . 5
โข (๐ โ (3 ยท (๐ถ / ๐ด)) = ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ2))) |
132 | 123, 131 | oveq12d 7380 |
. . . 4
โข (๐ โ (((๐ต / ๐ด)โ2) โ (3 ยท (๐ถ / ๐ด))) = (((๐ตโ2) / (๐ดโ2)) โ ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ2)))) |
133 | 121, 122,
132 | 3eqtr4d 2787 |
. . 3
โข (๐ โ (๐ / (๐ดโ2)) = (((๐ต / ๐ด)โ2) โ (3 ยท (๐ถ / ๐ด)))) |
134 | 52, 60, 67, 72 | divdird 11976 |
. . . 4
โข (๐ โ ((((2 ยท (๐ตโ3)) โ ((9 ยท
๐ด) ยท (๐ต ยท ๐ถ))) + (;27 ยท ((๐ดโ2) ยท ๐ท))) / (๐ดโ3)) = ((((2 ยท (๐ตโ3)) โ ((9 ยท
๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ3)) + ((;27 ยท ((๐ดโ2) ยท ๐ท)) / (๐ดโ3)))) |
135 | 41 | oveq1d 7377 |
. . . 4
โข (๐ โ (๐ / (๐ดโ3)) = ((((2 ยท (๐ตโ3)) โ ((9 ยท
๐ด) ยท (๐ต ยท ๐ถ))) + (;27 ยท ((๐ดโ2) ยท ๐ท))) / (๐ดโ3))) |
136 | 7, 1, 16, 37 | expdivd 14072 |
. . . . . . . . 9
โข (๐ โ ((๐ต / ๐ด)โ3) = ((๐ตโ3) / (๐ดโ3))) |
137 | 136 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ (2 ยท ((๐ต / ๐ด)โ3)) = (2 ยท ((๐ตโ3) / (๐ดโ3)))) |
138 | 65, 44, 67, 72 | divassd 11973 |
. . . . . . . 8
โข (๐ โ ((2 ยท (๐ตโ3)) / (๐ดโ3)) = (2 ยท ((๐ตโ3) / (๐ดโ3)))) |
139 | 137, 138 | eqtr4d 2780 |
. . . . . . 7
โข (๐ โ (2 ยท ((๐ต / ๐ด)โ3)) = ((2 ยท (๐ตโ3)) / (๐ดโ3))) |
140 | 47 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 9 โ
โ) |
141 | 1, 50 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (๐ด ยท (๐ต ยท ๐ถ)) โ โ) |
142 | 140, 141,
67, 72 | divassd 11973 |
. . . . . . . 8
โข (๐ โ ((9 ยท (๐ด ยท (๐ต ยท ๐ถ))) / (๐ดโ3)) = (9 ยท ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ3)))) |
143 | 140, 1, 50 | mulassd 11185 |
. . . . . . . . 9
โข (๐ โ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) = (9 ยท (๐ด ยท (๐ต ยท ๐ถ)))) |
144 | 143 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ3)) = ((9 ยท (๐ด ยท (๐ต ยท ๐ถ))) / (๐ดโ3))) |
145 | 50, 57, 1, 104, 16 | divcan5d 11964 |
. . . . . . . . . 10
โข (๐ โ ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ด ยท (๐ดโ2))) = ((๐ต ยท ๐ถ) / (๐ดโ2))) |
146 | | df-3 12224 |
. . . . . . . . . . . . . 14
โข 3 = (2 +
1) |
147 | 146 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข (๐ดโ3) = (๐ดโ(2 + 1)) |
148 | | expp1 13981 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 2 โ
โ0) โ (๐ดโ(2 + 1)) = ((๐ดโ2) ยท ๐ด)) |
149 | 1, 53, 148 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ดโ(2 + 1)) = ((๐ดโ2) ยท ๐ด)) |
150 | 147, 149 | eqtrid 2789 |
. . . . . . . . . . . 12
โข (๐ โ (๐ดโ3) = ((๐ดโ2) ยท ๐ด)) |
151 | 57, 1 | mulcomd 11183 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ดโ2) ยท ๐ด) = (๐ด ยท (๐ดโ2))) |
152 | 150, 151 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ3) = (๐ด ยท (๐ดโ2))) |
153 | 152 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ3)) = ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ด ยท (๐ดโ2)))) |
154 | 7, 1, 11, 1, 16, 16 | divmuldivd 11979 |
. . . . . . . . . . 11
โข (๐ โ ((๐ต / ๐ด) ยท (๐ถ / ๐ด)) = ((๐ต ยท ๐ถ) / (๐ด ยท ๐ด))) |
155 | 124 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ ((๐ต ยท ๐ถ) / (๐ดโ2)) = ((๐ต ยท ๐ถ) / (๐ด ยท ๐ด))) |
156 | 154, 155 | eqtr4d 2780 |
. . . . . . . . . 10
โข (๐ โ ((๐ต / ๐ด) ยท (๐ถ / ๐ด)) = ((๐ต ยท ๐ถ) / (๐ดโ2))) |
157 | 145, 153,
156 | 3eqtr4rd 2788 |
. . . . . . . . 9
โข (๐ โ ((๐ต / ๐ด) ยท (๐ถ / ๐ด)) = ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ3))) |
158 | 157 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด))) = (9 ยท ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ3)))) |
159 | 142, 144,
158 | 3eqtr4rd 2788 |
. . . . . . 7
โข (๐ โ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด))) = (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ3))) |
160 | 139, 159 | oveq12d 7380 |
. . . . . 6
โข (๐ โ ((2 ยท ((๐ต / ๐ด)โ3)) โ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) = (((2 ยท (๐ตโ3)) / (๐ดโ3)) โ (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ3)))) |
161 | 46, 51, 67, 72 | divsubdird 11977 |
. . . . . 6
โข (๐ โ (((2 ยท (๐ตโ3)) โ ((9 ยท
๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ3)) = (((2 ยท (๐ตโ3)) / (๐ดโ3)) โ (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ3)))) |
162 | 160, 161 | eqtr4d 2780 |
. . . . 5
โข (๐ โ ((2 ยท ((๐ต / ๐ด)โ3)) โ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) = (((2 ยท (๐ตโ3)) โ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ3))) |
163 | 150 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ (((๐ดโ2) ยท ๐ท) / (๐ดโ3)) = (((๐ดโ2) ยท ๐ท) / ((๐ดโ2) ยท ๐ด))) |
164 | 13, 1, 57, 16, 104 | divcan5d 11964 |
. . . . . . . 8
โข (๐ โ (((๐ดโ2) ยท ๐ท) / ((๐ดโ2) ยท ๐ด)) = (๐ท / ๐ด)) |
165 | 163, 164 | eqtr2d 2778 |
. . . . . . 7
โข (๐ โ (๐ท / ๐ด) = (((๐ดโ2) ยท ๐ท) / (๐ดโ3))) |
166 | 165 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (;27 ยท (๐ท / ๐ด)) = (;27 ยท (((๐ดโ2) ยท ๐ท) / (๐ดโ3)))) |
167 | 56 | a1i 11 |
. . . . . . 7
โข (๐ โ ;27 โ โ) |
168 | 167, 58, 67, 72 | divassd 11973 |
. . . . . 6
โข (๐ โ ((;27 ยท ((๐ดโ2) ยท ๐ท)) / (๐ดโ3)) = (;27 ยท (((๐ดโ2) ยท ๐ท) / (๐ดโ3)))) |
169 | 166, 168 | eqtr4d 2780 |
. . . . 5
โข (๐ โ (;27 ยท (๐ท / ๐ด)) = ((;27 ยท ((๐ดโ2) ยท ๐ท)) / (๐ดโ3))) |
170 | 162, 169 | oveq12d 7380 |
. . . 4
โข (๐ โ (((2 ยท ((๐ต / ๐ด)โ3)) โ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) + (;27 ยท (๐ท / ๐ด))) = ((((2 ยท (๐ตโ3)) โ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ3)) + ((;27 ยท ((๐ดโ2) ยท ๐ท)) / (๐ดโ3)))) |
171 | 134, 135,
170 | 3eqtr4d 2787 |
. . 3
โข (๐ โ (๐ / (๐ดโ3)) = (((2 ยท ((๐ต / ๐ด)โ3)) โ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) + (;27 ยท (๐ท / ๐ด)))) |
172 | | cubic2.0 |
. . . 4
โข (๐ โ ๐ โ 0) |
173 | 35, 1, 172, 16 | divne0d 11954 |
. . 3
โข (๐ โ (๐ / ๐ด) โ 0) |
174 | 32, 33, 34, 2, 36, 77, 78, 120, 133, 171, 173 | mcubic 26213 |
. 2
โข (๐ โ ((((๐โ3) + ((๐ต / ๐ด) ยท (๐โ2))) + (((๐ถ / ๐ด) ยท ๐) + (๐ท / ๐ด))) = 0 โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3)))) |
175 | | oveq1 7369 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ3) = (0โ3)) |
176 | | 3nn 12239 |
. . . . . . . . 9
โข 3 โ
โ |
177 | | 0exp 14010 |
. . . . . . . . 9
โข (3 โ
โ โ (0โ3) = 0) |
178 | 176, 177 | ax-mp 5 |
. . . . . . . 8
โข
(0โ3) = 0 |
179 | 175, 178 | eqtrdi 2793 |
. . . . . . 7
โข (๐ = 0 โ (๐โ3) = 0) |
180 | | 0ne1 12231 |
. . . . . . . 8
โข 0 โ
1 |
181 | 180 | a1i 11 |
. . . . . . 7
โข (๐ = 0 โ 0 โ
1) |
182 | 179, 181 | eqnetrd 3012 |
. . . . . 6
โข (๐ = 0 โ (๐โ3) โ 1) |
183 | 182 | necon2i 2979 |
. . . . 5
โข ((๐โ3) = 1 โ ๐ โ 0) |
184 | | simprl 770 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
185 | 35 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
186 | 1 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ด โ โ) |
187 | 16 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ด โ 0) |
188 | 184, 185,
186, 187 | divassd 11973 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) / ๐ด) = (๐ ยท (๐ / ๐ด))) |
189 | 188 | eqcomd 2743 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท (๐ / ๐ด)) = ((๐ ยท ๐) / ๐ด)) |
190 | 189 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) = ((๐ต / ๐ด) + ((๐ ยท ๐) / ๐ด))) |
191 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ต โ โ) |
192 | 184, 185 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท ๐) โ โ) |
193 | 191, 192,
186, 187 | divdird 11976 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต + (๐ ยท ๐)) / ๐ด) = ((๐ต / ๐ด) + ((๐ ยท ๐) / ๐ด))) |
194 | 190, 193 | eqtr4d 2780 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) = ((๐ต + (๐ ยท ๐)) / ๐ด)) |
195 | 91 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
196 | 195, 186,
187 | divcld 11938 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / ๐ด) โ โ) |
197 | | simprr 772 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ 0) |
198 | 172 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ 0) |
199 | 184, 185,
197, 198 | mulne0d 11814 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท ๐) โ 0) |
200 | 196, 192,
186, 199, 187 | divcan7d 11966 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ / ๐ด) / ๐ด) / ((๐ ยท ๐) / ๐ด)) = ((๐ / ๐ด) / (๐ ยท ๐))) |
201 | 195, 186,
186, 187, 187 | divdiv1d 11969 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / ๐ด) / ๐ด) = (๐ / (๐ด ยท ๐ด))) |
202 | 186 | sqvald 14055 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ดโ2) = (๐ด ยท ๐ด)) |
203 | 202 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / (๐ดโ2)) = (๐ / (๐ด ยท ๐ด))) |
204 | 201, 203 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / ๐ด) / ๐ด) = (๐ / (๐ดโ2))) |
205 | 204, 188 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ / ๐ด) / ๐ด) / ((๐ ยท ๐) / ๐ด)) = ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) |
206 | 195, 186,
192, 187, 199 | divdiv32d 11963 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / ๐ด) / (๐ ยท ๐)) = ((๐ / (๐ ยท ๐)) / ๐ด)) |
207 | 200, 205,
206 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด))) = ((๐ / (๐ ยท ๐)) / ๐ด)) |
208 | 194, 207 | oveq12d 7380 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) = (((๐ต + (๐ ยท ๐)) / ๐ด) + ((๐ / (๐ ยท ๐)) / ๐ด))) |
209 | 191, 192 | addcld 11181 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ต + (๐ ยท ๐)) โ โ) |
210 | 195, 192,
199 | divcld 11938 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / (๐ ยท ๐)) โ โ) |
211 | 209, 210,
186, 187 | divdird 11976 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / ๐ด) = (((๐ต + (๐ ยท ๐)) / ๐ด) + ((๐ / (๐ ยท ๐)) / ๐ด))) |
212 | 208, 211 | eqtr4d 2780 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) = (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / ๐ด)) |
213 | 212 | oveq1d 7377 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3) = ((((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / ๐ด) / 3)) |
214 | 209, 210 | addcld 11181 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) โ โ) |
215 | 86 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ 3 โ
โ) |
216 | | 3ne0 12266 |
. . . . . . . . . . 11
โข 3 โ
0 |
217 | 216 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ 3 โ 0) |
218 | 214, 186,
215, 187, 217 | divdiv1d 11969 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / ๐ด) / 3) = (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (๐ด ยท 3))) |
219 | | mulcom 11144 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 3 โ
โ) โ (๐ด ยท
3) = (3 ยท ๐ด)) |
220 | 186, 86, 219 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ด ยท 3) = (3 ยท ๐ด)) |
221 | 220 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (๐ด ยท 3)) = (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด))) |
222 | 213, 218,
221 | 3eqtrd 2781 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3) = (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด))) |
223 | 222 | negeqd 11402 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3) = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด))) |
224 | 223 | eqeq2d 2748 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ = -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3) โ ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด)))) |
225 | 224 | anassrs 469 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ๐ โ 0) โ (๐ = -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3) โ ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด)))) |
226 | 183, 225 | sylan2 594 |
. . . 4
โข (((๐ โง ๐ โ โ) โง (๐โ3) = 1) โ (๐ = -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3) โ ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด)))) |
227 | 226 | pm5.32da 580 |
. . 3
โข ((๐ โง ๐ โ โ) โ (((๐โ3) = 1 โง ๐ = -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3)) โ ((๐โ3) = 1 โง ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด))))) |
228 | 227 | rexbidva 3174 |
. 2
โข (๐ โ (โ๐ โ โ ((๐โ3) = 1 โง ๐ = -((((๐ต / ๐ด) + (๐ ยท (๐ / ๐ด))) + ((๐ / (๐ดโ2)) / (๐ ยท (๐ / ๐ด)))) / 3)) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด))))) |
229 | 31, 174, 228 | 3bitrd 305 |
1
โข (๐ โ ((((๐ด ยท (๐โ3)) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0 โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / (3 ยท ๐ด))))) |