Step | Hyp | Ref
| Expression |
1 | | mcubic.m |
. . . . . 6
โข (๐ โ ๐ = ((๐ตโ2) โ (3 ยท ๐ถ))) |
2 | | mcubic.b |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
3 | 2 | sqcld 14050 |
. . . . . . 7
โข (๐ โ (๐ตโ2) โ โ) |
4 | | 3cn 12235 |
. . . . . . . 8
โข 3 โ
โ |
5 | | mcubic.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ โ) |
6 | | mulcl 11136 |
. . . . . . . 8
โข ((3
โ โ โง ๐ถ
โ โ) โ (3 ยท ๐ถ) โ โ) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . . 7
โข (๐ โ (3 ยท ๐ถ) โ
โ) |
8 | 3, 7 | subcld 11513 |
. . . . . 6
โข (๐ โ ((๐ตโ2) โ (3 ยท ๐ถ)) โ
โ) |
9 | 1, 8 | eqeltrd 2838 |
. . . . 5
โข (๐ โ ๐ โ โ) |
10 | 4 | a1i 11 |
. . . . 5
โข (๐ โ 3 โ
โ) |
11 | | 3ne0 12260 |
. . . . . 6
โข 3 โ
0 |
12 | 11 | a1i 11 |
. . . . 5
โข (๐ โ 3 โ 0) |
13 | 9, 10, 12 | divcld 11932 |
. . . 4
โข (๐ โ (๐ / 3) โ โ) |
14 | 13 | negcld 11500 |
. . 3
โข (๐ โ -(๐ / 3) โ โ) |
15 | | mcubic.n |
. . . . 5
โข (๐ โ ๐ = (((2 ยท (๐ตโ3)) โ (9 ยท (๐ต ยท ๐ถ))) + (;27 ยท ๐ท))) |
16 | | 2cn 12229 |
. . . . . . . 8
โข 2 โ
โ |
17 | | 3nn0 12432 |
. . . . . . . . 9
โข 3 โ
โ0 |
18 | | expcl 13986 |
. . . . . . . . 9
โข ((๐ต โ โ โง 3 โ
โ0) โ (๐ตโ3) โ โ) |
19 | 2, 17, 18 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (๐ตโ3) โ โ) |
20 | | mulcl 11136 |
. . . . . . . 8
โข ((2
โ โ โง (๐ตโ3) โ โ) โ (2 ยท
(๐ตโ3)) โ
โ) |
21 | 16, 19, 20 | sylancr 588 |
. . . . . . 7
โข (๐ โ (2 ยท (๐ตโ3)) โ
โ) |
22 | | 9cn 12254 |
. . . . . . . 8
โข 9 โ
โ |
23 | 2, 5 | mulcld 11176 |
. . . . . . . 8
โข (๐ โ (๐ต ยท ๐ถ) โ โ) |
24 | | mulcl 11136 |
. . . . . . . 8
โข ((9
โ โ โง (๐ต
ยท ๐ถ) โ โ)
โ (9 ยท (๐ต
ยท ๐ถ)) โ
โ) |
25 | 22, 23, 24 | sylancr 588 |
. . . . . . 7
โข (๐ โ (9 ยท (๐ต ยท ๐ถ)) โ โ) |
26 | 21, 25 | subcld 11513 |
. . . . . 6
โข (๐ โ ((2 ยท (๐ตโ3)) โ (9 ยท
(๐ต ยท ๐ถ))) โ
โ) |
27 | | 2nn0 12431 |
. . . . . . . . 9
โข 2 โ
โ0 |
28 | | 7nn 12246 |
. . . . . . . . 9
โข 7 โ
โ |
29 | 27, 28 | decnncl 12639 |
. . . . . . . 8
โข ;27 โ โ |
30 | 29 | nncni 12164 |
. . . . . . 7
โข ;27 โ โ |
31 | | mcubic.d |
. . . . . . 7
โข (๐ โ ๐ท โ โ) |
32 | | mulcl 11136 |
. . . . . . 7
โข ((;27 โ โ โง ๐ท โ โ) โ (;27 ยท ๐ท) โ โ) |
33 | 30, 31, 32 | sylancr 588 |
. . . . . 6
โข (๐ โ (;27 ยท ๐ท) โ โ) |
34 | 26, 33 | addcld 11175 |
. . . . 5
โข (๐ โ (((2 ยท (๐ตโ3)) โ (9 ยท
(๐ต ยท ๐ถ))) + (;27 ยท ๐ท)) โ โ) |
35 | 15, 34 | eqeltrd 2838 |
. . . 4
โข (๐ โ ๐ โ โ) |
36 | 30 | a1i 11 |
. . . 4
โข (๐ โ ;27 โ โ) |
37 | 29 | nnne0i 12194 |
. . . . 5
โข ;27 โ 0 |
38 | 37 | a1i 11 |
. . . 4
โข (๐ โ ;27 โ 0) |
39 | 35, 36, 38 | divcld 11932 |
. . 3
โข (๐ โ (๐ / ;27) โ โ) |
40 | | mcubic.x |
. . . 4
โข (๐ โ ๐ โ โ) |
41 | 2, 10, 12 | divcld 11932 |
. . . 4
โข (๐ โ (๐ต / 3) โ โ) |
42 | 40, 41 | addcld 11175 |
. . 3
โข (๐ โ (๐ + (๐ต / 3)) โ โ) |
43 | | mcubic.t |
. . . . 5
โข (๐ โ ๐ โ โ) |
44 | 43, 10, 12 | divcld 11932 |
. . . 4
โข (๐ โ (๐ / 3) โ โ) |
45 | 44 | negcld 11500 |
. . 3
โข (๐ โ -(๐ / 3) โ โ) |
46 | | 3nn 12233 |
. . . . . 6
โข 3 โ
โ |
47 | 46 | a1i 11 |
. . . . 5
โข (๐ โ 3 โ
โ) |
48 | | n2dvds3 16254 |
. . . . . 6
โข ยฌ 2
โฅ 3 |
49 | 48 | a1i 11 |
. . . . 5
โข (๐ โ ยฌ 2 โฅ
3) |
50 | | oexpneg 16228 |
. . . . 5
โข (((๐ / 3) โ โ โง 3
โ โ โง ยฌ 2 โฅ 3) โ (-(๐ / 3)โ3) = -((๐ / 3)โ3)) |
51 | 44, 47, 49, 50 | syl3anc 1372 |
. . . 4
โข (๐ โ (-(๐ / 3)โ3) = -((๐ / 3)โ3)) |
52 | 17 | a1i 11 |
. . . . . . 7
โข (๐ โ 3 โ
โ0) |
53 | 43, 10, 12, 52 | expdivd 14066 |
. . . . . 6
โข (๐ โ ((๐ / 3)โ3) = ((๐โ3) / (3โ3))) |
54 | | mcubic.3 |
. . . . . . 7
โข (๐ โ (๐โ3) = ((๐ + ๐บ) / 2)) |
55 | | 3exp3 16965 |
. . . . . . . 8
โข
(3โ3) = ;27 |
56 | 55 | a1i 11 |
. . . . . . 7
โข (๐ โ (3โ3) = ;27) |
57 | 54, 56 | oveq12d 7376 |
. . . . . 6
โข (๐ โ ((๐โ3) / (3โ3)) = (((๐ + ๐บ) / 2) / ;27)) |
58 | | mcubic.g |
. . . . . . . . 9
โข (๐ โ ๐บ โ โ) |
59 | 35, 58 | addcld 11175 |
. . . . . . . 8
โข (๐ โ (๐ + ๐บ) โ โ) |
60 | | 2cnd 12232 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
61 | | 2ne0 12258 |
. . . . . . . . 9
โข 2 โ
0 |
62 | 61 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ 0) |
63 | 59, 60, 36, 62, 38 | divdiv32d 11957 |
. . . . . . 7
โข (๐ โ (((๐ + ๐บ) / 2) / ;27) = (((๐ + ๐บ) / ;27) / 2)) |
64 | 35, 58 | addcomd 11358 |
. . . . . . . . . 10
โข (๐ โ (๐ + ๐บ) = (๐บ + ๐)) |
65 | 64 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((๐ + ๐บ) / ;27) = ((๐บ + ๐) / ;27)) |
66 | 58, 35, 36, 38 | divdird 11970 |
. . . . . . . . 9
โข (๐ โ ((๐บ + ๐) / ;27) = ((๐บ / ;27) + (๐ / ;27))) |
67 | 65, 66 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((๐ + ๐บ) / ;27) = ((๐บ / ;27) + (๐ / ;27))) |
68 | 67 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ (((๐ + ๐บ) / ;27) / 2) = (((๐บ / ;27) + (๐ / ;27)) / 2)) |
69 | 58, 36, 38 | divcld 11932 |
. . . . . . . 8
โข (๐ โ (๐บ / ;27) โ โ) |
70 | 69, 39, 60, 62 | divdird 11970 |
. . . . . . 7
โข (๐ โ (((๐บ / ;27) + (๐ / ;27)) / 2) = (((๐บ / ;27) / 2) + ((๐ / ;27) / 2))) |
71 | 63, 68, 70 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ (((๐ + ๐บ) / 2) / ;27) = (((๐บ / ;27) / 2) + ((๐ / ;27) / 2))) |
72 | 53, 57, 71 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ ((๐ / 3)โ3) = (((๐บ / ;27) / 2) + ((๐ / ;27) / 2))) |
73 | 72 | negeqd 11396 |
. . . 4
โข (๐ โ -((๐ / 3)โ3) = -(((๐บ / ;27) / 2) + ((๐ / ;27) / 2))) |
74 | 69 | halfcld 12399 |
. . . . 5
โข (๐ โ ((๐บ / ;27) / 2) โ โ) |
75 | 39 | halfcld 12399 |
. . . . 5
โข (๐ โ ((๐ / ;27) / 2) โ โ) |
76 | 74, 75 | negdi2d 11527 |
. . . 4
โข (๐ โ -(((๐บ / ;27) / 2) + ((๐ / ;27) / 2)) = (-((๐บ / ;27) / 2) โ ((๐ / ;27) / 2))) |
77 | 51, 73, 76 | 3eqtrd 2781 |
. . 3
โข (๐ โ (-(๐ / 3)โ3) = (-((๐บ / ;27) / 2) โ ((๐ / ;27) / 2))) |
78 | 74 | negcld 11500 |
. . 3
โข (๐ โ -((๐บ / ;27) / 2) โ โ) |
79 | | sqneg 14022 |
. . . . 5
โข (((๐บ / ;27) / 2) โ โ โ (-((๐บ / ;27) / 2)โ2) = (((๐บ / ;27) / 2)โ2)) |
80 | 74, 79 | syl 17 |
. . . 4
โข (๐ โ (-((๐บ / ;27) / 2)โ2) = (((๐บ / ;27) / 2)โ2)) |
81 | 69, 60, 62 | sqdivd 14065 |
. . . 4
โข (๐ โ (((๐บ / ;27) / 2)โ2) = (((๐บ / ;27)โ2) / (2โ2))) |
82 | 39, 60, 62 | sqdivd 14065 |
. . . . . . . 8
โข (๐ โ (((๐ / ;27) / 2)โ2) = (((๐ / ;27)โ2) / (2โ2))) |
83 | 35, 36, 38 | sqdivd 14065 |
. . . . . . . . 9
โข (๐ โ ((๐ / ;27)โ2) = ((๐โ2) / (;27โ2))) |
84 | 83 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ (((๐ / ;27)โ2) / (2โ2)) = (((๐โ2) / (;27โ2)) / (2โ2))) |
85 | 82, 84 | eqtr2d 2778 |
. . . . . . 7
โข (๐ โ (((๐โ2) / (;27โ2)) / (2โ2)) = (((๐ / ;27) / 2)โ2)) |
86 | | 4cn 12239 |
. . . . . . . . . . . 12
โข 4 โ
โ |
87 | 86 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 4 โ
โ) |
88 | | expcl 13986 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
89 | 9, 17, 88 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ (๐โ3) โ โ) |
90 | 30 | sqcli 14086 |
. . . . . . . . . . . 12
โข (;27โ2) โ
โ |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (;27โ2) โ โ) |
92 | | sqne0 14029 |
. . . . . . . . . . . . 13
โข (;27 โ โ โ ((;27โ2) โ 0 โ ;27 โ 0)) |
93 | 36, 92 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((;27โ2) โ 0 โ ;27 โ 0)) |
94 | 38, 93 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ (;27โ2) โ 0) |
95 | 87, 89, 91, 94 | divassd 11967 |
. . . . . . . . . 10
โข (๐ โ ((4 ยท (๐โ3)) / (;27โ2)) = (4 ยท ((๐โ3) / (;27โ2)))) |
96 | 22 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 9 โ
โ) |
97 | | 9nn 12252 |
. . . . . . . . . . . . . . 15
โข 9 โ
โ |
98 | 97 | nnne0i 12194 |
. . . . . . . . . . . . . 14
โข 9 โ
0 |
99 | 98 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 9 โ 0) |
100 | 9, 96, 99, 52 | expdivd 14066 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ / 9)โ3) = ((๐โ3) / (9โ3))) |
101 | 16, 4 | mulcomi 11164 |
. . . . . . . . . . . . . . . 16
โข (2
ยท 3) = (3 ยท 2) |
102 | 101 | oveq2i 7369 |
. . . . . . . . . . . . . . 15
โข
(3โ(2 ยท 3)) = (3โ(3 ยท 2)) |
103 | | expmul 14014 |
. . . . . . . . . . . . . . . 16
โข ((3
โ โ โง 2 โ โ0 โง 3 โ
โ0) โ (3โ(2 ยท 3)) =
((3โ2)โ3)) |
104 | 4, 27, 17, 103 | mp3an 1462 |
. . . . . . . . . . . . . . 15
โข
(3โ(2 ยท 3)) = ((3โ2)โ3) |
105 | | expmul 14014 |
. . . . . . . . . . . . . . . 16
โข ((3
โ โ โง 3 โ โ0 โง 2 โ
โ0) โ (3โ(3 ยท 2)) =
((3โ3)โ2)) |
106 | 4, 17, 27, 105 | mp3an 1462 |
. . . . . . . . . . . . . . 15
โข
(3โ(3 ยท 2)) = ((3โ3)โ2) |
107 | 102, 104,
106 | 3eqtr3i 2773 |
. . . . . . . . . . . . . 14
โข
((3โ2)โ3) = ((3โ3)โ2) |
108 | | sq3 14103 |
. . . . . . . . . . . . . . 15
โข
(3โ2) = 9 |
109 | 108 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข
((3โ2)โ3) = (9โ3) |
110 | 55 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข
((3โ3)โ2) = (;27โ2) |
111 | 107, 109,
110 | 3eqtr3i 2773 |
. . . . . . . . . . . . 13
โข
(9โ3) = (;27โ2) |
112 | 111 | oveq2i 7369 |
. . . . . . . . . . . 12
โข ((๐โ3) / (9โ3)) = ((๐โ3) / (;27โ2)) |
113 | 100, 112 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ โ ((๐ / 9)โ3) = ((๐โ3) / (;27โ2))) |
114 | 113 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ โ (4 ยท ((๐ / 9)โ3)) = (4 ยท
((๐โ3) / (;27โ2)))) |
115 | 95, 114 | eqtr4d 2780 |
. . . . . . . . 9
โข (๐ โ ((4 ยท (๐โ3)) / (;27โ2)) = (4 ยท ((๐ / 9)โ3))) |
116 | 115 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ (((4 ยท (๐โ3)) / (;27โ2)) / (2โ2)) = ((4 ยท ((๐ / 9)โ3)) /
(2โ2))) |
117 | | sq2 14102 |
. . . . . . . . . 10
โข
(2โ2) = 4 |
118 | 117 | oveq2i 7369 |
. . . . . . . . 9
โข ((4
ยท ((๐ / 9)โ3))
/ (2โ2)) = ((4 ยท ((๐ / 9)โ3)) / 4) |
119 | 9, 96, 99 | divcld 11932 |
. . . . . . . . . . 11
โข (๐ โ (๐ / 9) โ โ) |
120 | | expcl 13986 |
. . . . . . . . . . 11
โข (((๐ / 9) โ โ โง 3
โ โ0) โ ((๐ / 9)โ3) โ
โ) |
121 | 119, 17, 120 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ((๐ / 9)โ3) โ
โ) |
122 | | 4ne0 12262 |
. . . . . . . . . . 11
โข 4 โ
0 |
123 | 122 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 4 โ 0) |
124 | 121, 87, 123 | divcan3d 11937 |
. . . . . . . . 9
โข (๐ โ ((4 ยท ((๐ / 9)โ3)) / 4) = ((๐ / 9)โ3)) |
125 | 118, 124 | eqtrid 2789 |
. . . . . . . 8
โข (๐ โ ((4 ยท ((๐ / 9)โ3)) / (2โ2)) =
((๐ /
9)โ3)) |
126 | 116, 125 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (((4 ยท (๐โ3)) / (;27โ2)) / (2โ2)) = ((๐ / 9)โ3)) |
127 | 85, 126 | oveq12d 7376 |
. . . . . 6
โข (๐ โ ((((๐โ2) / (;27โ2)) / (2โ2)) โ (((4 ยท
(๐โ3)) / (;27โ2)) / (2โ2))) = ((((๐ / ;27) / 2)โ2) โ ((๐ / 9)โ3))) |
128 | 35 | sqcld 14050 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ โ) |
129 | 128, 91, 94 | divcld 11932 |
. . . . . . 7
โข (๐ โ ((๐โ2) / (;27โ2)) โ โ) |
130 | | mulcl 11136 |
. . . . . . . . 9
โข ((4
โ โ โง (๐โ3) โ โ) โ (4 ยท
(๐โ3)) โ
โ) |
131 | 86, 89, 130 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (4 ยท (๐โ3)) โ
โ) |
132 | 131, 91, 94 | divcld 11932 |
. . . . . . 7
โข (๐ โ ((4 ยท (๐โ3)) / (;27โ2)) โ โ) |
133 | 16 | sqcli 14086 |
. . . . . . . 8
โข
(2โ2) โ โ |
134 | 133 | a1i 11 |
. . . . . . 7
โข (๐ โ (2โ2) โ
โ) |
135 | 117, 122 | eqnetri 3015 |
. . . . . . . 8
โข
(2โ2) โ 0 |
136 | 135 | a1i 11 |
. . . . . . 7
โข (๐ โ (2โ2) โ
0) |
137 | 129, 132,
134, 136 | divsubdird 11971 |
. . . . . 6
โข (๐ โ ((((๐โ2) / (;27โ2)) โ ((4 ยท (๐โ3)) / (;27โ2))) / (2โ2)) = ((((๐โ2) / (;27โ2)) / (2โ2)) โ (((4 ยท
(๐โ3)) / (;27โ2)) /
(2โ2)))) |
138 | 75 | sqcld 14050 |
. . . . . . 7
โข (๐ โ (((๐ / ;27) / 2)โ2) โ โ) |
139 | 138, 121 | negsubd 11519 |
. . . . . 6
โข (๐ โ ((((๐ / ;27) / 2)โ2) + -((๐ / 9)โ3)) = ((((๐ / ;27) / 2)โ2) โ ((๐ / 9)โ3))) |
140 | 127, 137,
139 | 3eqtr4d 2787 |
. . . . 5
โข (๐ โ ((((๐โ2) / (;27โ2)) โ ((4 ยท (๐โ3)) / (;27โ2))) / (2โ2)) = ((((๐ / ;27) / 2)โ2) + -((๐ / 9)โ3))) |
141 | 58, 36, 38 | sqdivd 14065 |
. . . . . . 7
โข (๐ โ ((๐บ / ;27)โ2) = ((๐บโ2) / (;27โ2))) |
142 | | mcubic.2 |
. . . . . . . 8
โข (๐ โ (๐บโ2) = ((๐โ2) โ (4 ยท (๐โ3)))) |
143 | 142 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ ((๐บโ2) / (;27โ2)) = (((๐โ2) โ (4 ยท (๐โ3))) / (;27โ2))) |
144 | 128, 131,
91, 94 | divsubdird 11971 |
. . . . . . 7
โข (๐ โ (((๐โ2) โ (4 ยท (๐โ3))) / (;27โ2)) = (((๐โ2) / (;27โ2)) โ ((4 ยท (๐โ3)) / (;27โ2)))) |
145 | 141, 143,
144 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ ((๐บ / ;27)โ2) = (((๐โ2) / (;27โ2)) โ ((4 ยท (๐โ3)) / (;27โ2)))) |
146 | 145 | oveq1d 7373 |
. . . . 5
โข (๐ โ (((๐บ / ;27)โ2) / (2โ2)) = ((((๐โ2) / (;27โ2)) โ ((4 ยท (๐โ3)) / (;27โ2))) / (2โ2))) |
147 | | oexpneg 16228 |
. . . . . . 7
โข (((๐ / 9) โ โ โง 3
โ โ โง ยฌ 2 โฅ 3) โ (-(๐ / 9)โ3) = -((๐ / 9)โ3)) |
148 | 119, 47, 49, 147 | syl3anc 1372 |
. . . . . 6
โข (๐ โ (-(๐ / 9)โ3) = -((๐ / 9)โ3)) |
149 | 148 | oveq2d 7374 |
. . . . 5
โข (๐ โ ((((๐ / ;27) / 2)โ2) + (-(๐ / 9)โ3)) = ((((๐ / ;27) / 2)โ2) + -((๐ / 9)โ3))) |
150 | 140, 146,
149 | 3eqtr4d 2787 |
. . . 4
โข (๐ โ (((๐บ / ;27)โ2) / (2โ2)) = ((((๐ / ;27) / 2)โ2) + (-(๐ / 9)โ3))) |
151 | 80, 81, 150 | 3eqtrd 2781 |
. . 3
โข (๐ โ (-((๐บ / ;27) / 2)โ2) = ((((๐ / ;27) / 2)โ2) + (-(๐ / 9)โ3))) |
152 | 9, 10, 10, 12, 12 | divdiv1d 11963 |
. . . . . 6
โข (๐ โ ((๐ / 3) / 3) = (๐ / (3 ยท 3))) |
153 | | 3t3e9 12321 |
. . . . . . 7
โข (3
ยท 3) = 9 |
154 | 153 | oveq2i 7369 |
. . . . . 6
โข (๐ / (3 ยท 3)) = (๐ / 9) |
155 | 152, 154 | eqtrdi 2793 |
. . . . 5
โข (๐ โ ((๐ / 3) / 3) = (๐ / 9)) |
156 | 155 | negeqd 11396 |
. . . 4
โข (๐ โ -((๐ / 3) / 3) = -(๐ / 9)) |
157 | 13, 10, 12 | divnegd 11945 |
. . . 4
โข (๐ โ -((๐ / 3) / 3) = (-(๐ / 3) / 3)) |
158 | 156, 157 | eqtr3d 2779 |
. . 3
โข (๐ โ -(๐ / 9) = (-(๐ / 3) / 3)) |
159 | | eqidd 2738 |
. . 3
โข (๐ โ ((๐ / ;27) / 2) = ((๐ / ;27) / 2)) |
160 | | mcubic.0 |
. . . . 5
โข (๐ โ ๐ โ 0) |
161 | 43, 10, 160, 12 | divne0d 11948 |
. . . 4
โข (๐ โ (๐ / 3) โ 0) |
162 | 44, 161 | negne0d 11511 |
. . 3
โข (๐ โ -(๐ / 3) โ 0) |
163 | 14, 39, 42, 45, 77, 78, 151, 158, 159, 162 | dcubic 26199 |
. 2
โข (๐ โ ((((๐ + (๐ต / 3))โ3) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = 0 โ โ๐ โ โ ((๐โ3) = 1 โง (๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3))))))) |
164 | | binom3 14128 |
. . . . . . 7
โข ((๐ โ โ โง (๐ต / 3) โ โ) โ
((๐ + (๐ต / 3))โ3) = (((๐โ3) + (3 ยท ((๐โ2) ยท (๐ต / 3)))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)))) |
165 | 40, 41, 164 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ + (๐ต / 3))โ3) = (((๐โ3) + (3 ยท ((๐โ2) ยท (๐ต / 3)))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)))) |
166 | 40 | sqcld 14050 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) โ โ) |
167 | 10, 166, 41 | mul12d 11365 |
. . . . . . . . 9
โข (๐ โ (3 ยท ((๐โ2) ยท (๐ต / 3))) = ((๐โ2) ยท (3 ยท (๐ต / 3)))) |
168 | 2, 10, 12 | divcan2d 11934 |
. . . . . . . . . 10
โข (๐ โ (3 ยท (๐ต / 3)) = ๐ต) |
169 | 168 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ ((๐โ2) ยท (3 ยท (๐ต / 3))) = ((๐โ2) ยท ๐ต)) |
170 | 166, 2 | mulcomd 11177 |
. . . . . . . . 9
โข (๐ โ ((๐โ2) ยท ๐ต) = (๐ต ยท (๐โ2))) |
171 | 167, 169,
170 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ (3 ยท ((๐โ2) ยท (๐ต / 3))) = (๐ต ยท (๐โ2))) |
172 | 171 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ ((๐โ3) + (3 ยท ((๐โ2) ยท (๐ต / 3)))) = ((๐โ3) + (๐ต ยท (๐โ2)))) |
173 | 172 | oveq1d 7373 |
. . . . . 6
โข (๐ โ (((๐โ3) + (3 ยท ((๐โ2) ยท (๐ต / 3)))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3))) = (((๐โ3) + (๐ต ยท (๐โ2))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)))) |
174 | 165, 173 | eqtrd 2777 |
. . . . 5
โข (๐ โ ((๐ + (๐ต / 3))โ3) = (((๐โ3) + (๐ต ยท (๐โ2))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)))) |
175 | 174 | oveq1d 7373 |
. . . 4
โข (๐ โ (((๐ + (๐ต / 3))โ3) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = ((((๐โ3) + (๐ต ยท (๐โ2))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3))) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27)))) |
176 | | expcl 13986 |
. . . . . . 7
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
177 | 40, 17, 176 | sylancl 587 |
. . . . . 6
โข (๐ โ (๐โ3) โ โ) |
178 | 2, 166 | mulcld 11176 |
. . . . . 6
โข (๐ โ (๐ต ยท (๐โ2)) โ โ) |
179 | 177, 178 | addcld 11175 |
. . . . 5
โข (๐ โ ((๐โ3) + (๐ต ยท (๐โ2))) โ โ) |
180 | 41 | sqcld 14050 |
. . . . . . . 8
โข (๐ โ ((๐ต / 3)โ2) โ
โ) |
181 | 40, 180 | mulcld 11176 |
. . . . . . 7
โข (๐ โ (๐ ยท ((๐ต / 3)โ2)) โ
โ) |
182 | 10, 181 | mulcld 11176 |
. . . . . 6
โข (๐ โ (3 ยท (๐ ยท ((๐ต / 3)โ2))) โ
โ) |
183 | | expcl 13986 |
. . . . . . 7
โข (((๐ต / 3) โ โ โง 3
โ โ0) โ ((๐ต / 3)โ3) โ
โ) |
184 | 41, 17, 183 | sylancl 587 |
. . . . . 6
โข (๐ โ ((๐ต / 3)โ3) โ
โ) |
185 | 182, 184 | addcld 11175 |
. . . . 5
โข (๐ โ ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) โ
โ) |
186 | 14, 42 | mulcld 11176 |
. . . . . 6
โข (๐ โ (-(๐ / 3) ยท (๐ + (๐ต / 3))) โ โ) |
187 | 186, 39 | addcld 11175 |
. . . . 5
โข (๐ โ ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27)) โ โ) |
188 | 179, 185,
187 | addassd 11178 |
. . . 4
โข (๐ โ ((((๐โ3) + (๐ต ยท (๐โ2))) + ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3))) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = (((๐โ3) + (๐ต ยท (๐โ2))) + (((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))))) |
189 | 14, 40, 41 | adddid 11180 |
. . . . . . . . . 10
โข (๐ โ (-(๐ / 3) ยท (๐ + (๐ต / 3))) = ((-(๐ / 3) ยท ๐) + (-(๐ / 3) ยท (๐ต / 3)))) |
190 | 189 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27)) = (((-(๐ / 3) ยท ๐) + (-(๐ / 3) ยท (๐ต / 3))) + (๐ / ;27))) |
191 | 14, 40 | mulcld 11176 |
. . . . . . . . . 10
โข (๐ โ (-(๐ / 3) ยท ๐) โ โ) |
192 | 14, 41 | mulcld 11176 |
. . . . . . . . . 10
โข (๐ โ (-(๐ / 3) ยท (๐ต / 3)) โ โ) |
193 | 191, 192,
39 | addassd 11178 |
. . . . . . . . 9
โข (๐ โ (((-(๐ / 3) ยท ๐) + (-(๐ / 3) ยท (๐ต / 3))) + (๐ / ;27)) = ((-(๐ / 3) ยท ๐) + ((-(๐ / 3) ยท (๐ต / 3)) + (๐ / ;27)))) |
194 | 1 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ / 3) = (((๐ตโ2) โ (3 ยท ๐ถ)) / 3)) |
195 | 3, 7, 10, 12 | divsubdird 11971 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ตโ2) โ (3 ยท ๐ถ)) / 3) = (((๐ตโ2) / 3) โ ((3 ยท ๐ถ) / 3))) |
196 | 5, 10, 12 | divcan3d 11937 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((3 ยท ๐ถ) / 3) = ๐ถ) |
197 | 196 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ตโ2) / 3) โ ((3 ยท ๐ถ) / 3)) = (((๐ตโ2) / 3) โ ๐ถ)) |
198 | 194, 195,
197 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / 3) = (((๐ตโ2) / 3) โ ๐ถ)) |
199 | 198 | negeqd 11396 |
. . . . . . . . . . . . 13
โข (๐ โ -(๐ / 3) = -(((๐ตโ2) / 3) โ ๐ถ)) |
200 | 3, 10, 12 | divcld 11932 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ตโ2) / 3) โ
โ) |
201 | 200, 5 | negsubdi2d 11529 |
. . . . . . . . . . . . 13
โข (๐ โ -(((๐ตโ2) / 3) โ ๐ถ) = (๐ถ โ ((๐ตโ2) / 3))) |
202 | 199, 201 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ -(๐ / 3) = (๐ถ โ ((๐ตโ2) / 3))) |
203 | 202 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ (-(๐ / 3) ยท ๐) = ((๐ถ โ ((๐ตโ2) / 3)) ยท ๐)) |
204 | 5, 200, 40 | subdird 11613 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ โ ((๐ตโ2) / 3)) ยท ๐) = ((๐ถ ยท ๐) โ (((๐ตโ2) / 3) ยท ๐))) |
205 | 200, 40 | mulcomd 11177 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ตโ2) / 3) ยท ๐) = (๐ ยท ((๐ตโ2) / 3))) |
206 | 4 | sqvali 14085 |
. . . . . . . . . . . . . . . . . 18
โข
(3โ2) = (3 ยท 3) |
207 | 206 | oveq2i 7369 |
. . . . . . . . . . . . . . . . 17
โข ((๐ตโ2) / (3โ2)) = ((๐ตโ2) / (3 ยท
3)) |
208 | 2, 10, 12 | sqdivd 14065 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ต / 3)โ2) = ((๐ตโ2) / (3โ2))) |
209 | 3, 10, 10, 12, 12 | divdiv1d 11963 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((๐ตโ2) / 3) / 3) = ((๐ตโ2) / (3 ยท 3))) |
210 | 207, 208,
209 | 3eqtr4a 2803 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ต / 3)โ2) = (((๐ตโ2) / 3) / 3)) |
211 | 210 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ (3 ยท ((๐ต / 3)โ2)) = (3 ยท
(((๐ตโ2) / 3) /
3))) |
212 | 200, 10, 12 | divcan2d 11934 |
. . . . . . . . . . . . . . 15
โข (๐ โ (3 ยท (((๐ตโ2) / 3) / 3)) = ((๐ตโ2) / 3)) |
213 | 211, 212 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (3 ยท ((๐ต / 3)โ2)) = ((๐ตโ2) / 3)) |
214 | 213 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท (3 ยท ((๐ต / 3)โ2))) = (๐ ยท ((๐ตโ2) / 3))) |
215 | 40, 10, 180 | mul12d 11365 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท (3 ยท ((๐ต / 3)โ2))) = (3 ยท (๐ ยท ((๐ต / 3)โ2)))) |
216 | 205, 214,
215 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ตโ2) / 3) ยท ๐) = (3 ยท (๐ ยท ((๐ต / 3)โ2)))) |
217 | 216 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ ยท ๐) โ (((๐ตโ2) / 3) ยท ๐)) = ((๐ถ ยท ๐) โ (3 ยท (๐ ยท ((๐ต / 3)โ2))))) |
218 | 203, 204,
217 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (๐ โ (-(๐ / 3) ยท ๐) = ((๐ถ ยท ๐) โ (3 ยท (๐ ยท ((๐ต / 3)โ2))))) |
219 | 202 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ (-(๐ / 3) ยท (๐ต / 3)) = ((๐ถ โ ((๐ตโ2) / 3)) ยท (๐ต / 3))) |
220 | 5, 200, 41 | subdird 11613 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ โ ((๐ตโ2) / 3)) ยท (๐ต / 3)) = ((๐ถ ยท (๐ต / 3)) โ (((๐ตโ2) / 3) ยท (๐ต / 3)))) |
221 | 5, 2, 10, 12 | divassd 11967 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ถ ยท ๐ต) / 3) = (๐ถ ยท (๐ต / 3))) |
222 | 5, 2 | mulcomd 11177 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ถ ยท ๐ต) = (๐ต ยท ๐ถ)) |
223 | 222 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ถ ยท ๐ต) / 3) = ((๐ต ยท ๐ถ) / 3)) |
224 | 221, 223 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ถ ยท (๐ต / 3)) = ((๐ต ยท ๐ถ) / 3)) |
225 | 3, 10, 2, 10, 12, 12 | divmuldivd 11973 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ตโ2) / 3) ยท (๐ต / 3)) = (((๐ตโ2) ยท ๐ต) / (3 ยท 3))) |
226 | | df-3 12218 |
. . . . . . . . . . . . . . . . . 18
โข 3 = (2 +
1) |
227 | 226 | oveq2i 7369 |
. . . . . . . . . . . . . . . . 17
โข (๐ตโ3) = (๐ตโ(2 + 1)) |
228 | | expp1 13975 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต โ โ โง 2 โ
โ0) โ (๐ตโ(2 + 1)) = ((๐ตโ2) ยท ๐ต)) |
229 | 2, 27, 228 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ตโ(2 + 1)) = ((๐ตโ2) ยท ๐ต)) |
230 | 227, 229 | eqtr2id 2790 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ตโ2) ยท ๐ต) = (๐ตโ3)) |
231 | 153 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (3 ยท 3) =
9) |
232 | 230, 231 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ตโ2) ยท ๐ต) / (3 ยท 3)) = ((๐ตโ3) / 9)) |
233 | 225, 232 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ตโ2) / 3) ยท (๐ต / 3)) = ((๐ตโ3) / 9)) |
234 | 224, 233 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ ยท (๐ต / 3)) โ (((๐ตโ2) / 3) ยท (๐ต / 3))) = (((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9))) |
235 | 219, 220,
234 | 3eqtrd 2781 |
. . . . . . . . . . . 12
โข (๐ โ (-(๐ / 3) ยท (๐ต / 3)) = (((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9))) |
236 | 15 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ / ;27) = ((((2 ยท (๐ตโ3)) โ (9 ยท (๐ต ยท ๐ถ))) + (;27 ยท ๐ท)) / ;27)) |
237 | 26, 33, 36, 38 | divdird 11970 |
. . . . . . . . . . . . 13
โข (๐ โ ((((2 ยท (๐ตโ3)) โ (9 ยท
(๐ต ยท ๐ถ))) + (;27 ยท ๐ท)) / ;27) = ((((2 ยท (๐ตโ3)) โ (9 ยท (๐ต ยท ๐ถ))) / ;27) + ((;27 ยท ๐ท) / ;27))) |
238 | 21, 25, 36, 38 | divsubdird 11971 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท (๐ตโ3)) โ (9 ยท
(๐ต ยท ๐ถ))) / ;27) = (((2 ยท (๐ตโ3)) / ;27) โ ((9 ยท (๐ต ยท ๐ถ)) / ;27))) |
239 | | 9t3e27 12742 |
. . . . . . . . . . . . . . . . . 18
โข (9
ยท 3) = ;27 |
240 | 239 | oveq2i 7369 |
. . . . . . . . . . . . . . . . 17
โข ((9
ยท (๐ต ยท ๐ถ)) / (9 ยท 3)) = ((9
ยท (๐ต ยท ๐ถ)) / ;27) |
241 | 23, 10, 96, 12, 99 | divcan5d 11958 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((9 ยท (๐ต ยท ๐ถ)) / (9 ยท 3)) = ((๐ต ยท ๐ถ) / 3)) |
242 | 240, 241 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((9 ยท (๐ต ยท ๐ถ)) / ;27) = ((๐ต ยท ๐ถ) / 3)) |
243 | 242 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท (๐ตโ3)) / ;27) โ ((9 ยท (๐ต ยท ๐ถ)) / ;27)) = (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3))) |
244 | 238, 243 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท (๐ตโ3)) โ (9 ยท
(๐ต ยท ๐ถ))) / ;27) = (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3))) |
245 | 31, 36, 38 | divcan3d 11937 |
. . . . . . . . . . . . . 14
โข (๐ โ ((;27 ยท ๐ท) / ;27) = ๐ท) |
246 | 244, 245 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ ((((2 ยท (๐ตโ3)) โ (9 ยท
(๐ต ยท ๐ถ))) / ;27) + ((;27 ยท ๐ท) / ;27)) = ((((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)) + ๐ท)) |
247 | 236, 237,
246 | 3eqtrd 2781 |
. . . . . . . . . . . 12
โข (๐ โ (๐ / ;27) = ((((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)) + ๐ท)) |
248 | 235, 247 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ โ ((-(๐ / 3) ยท (๐ต / 3)) + (๐ / ;27)) = ((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + ((((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)) + ๐ท))) |
249 | 19, 96, 99 | divcld 11932 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ตโ3) / 9) โ
โ) |
250 | 21, 36, 38 | divcld 11932 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท (๐ตโ3)) / ;27) โ โ) |
251 | 249, 250 | negsubdi2d 11529 |
. . . . . . . . . . . . . 14
โข (๐ โ -(((๐ตโ3) / 9) โ ((2 ยท (๐ตโ3)) / ;27)) = (((2 ยท (๐ตโ3)) / ;27) โ ((๐ตโ3) / 9))) |
252 | 2, 10, 12, 52 | expdivd 14066 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ต / 3)โ3) = ((๐ตโ3) / (3โ3))) |
253 | 55 | oveq2i 7369 |
. . . . . . . . . . . . . . . . 17
โข ((๐ตโ3) / (3โ3)) = ((๐ตโ3) / ;27) |
254 | | ax-1cn 11110 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 1 โ
โ |
255 | | 2p1e3 12296 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (2 + 1) =
3 |
256 | 4, 16, 254, 255 | subaddrii 11491 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (3
โ 2) = 1 |
257 | 256 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((3
โ 2) ยท (๐ตโ3)) = (1 ยท (๐ตโ3)) |
258 | 19 | mulid2d 11174 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (1 ยท (๐ตโ3)) = (๐ตโ3)) |
259 | 257, 258 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((3 โ 2) ยท
(๐ตโ3)) = (๐ตโ3)) |
260 | 10, 60, 19 | subdird 11613 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((3 โ 2) ยท
(๐ตโ3)) = ((3 ยท
(๐ตโ3)) โ (2
ยท (๐ตโ3)))) |
261 | 259, 260 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ตโ3) = ((3 ยท (๐ตโ3)) โ (2 ยท (๐ตโ3)))) |
262 | 261 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ตโ3) / ;27) = (((3 ยท (๐ตโ3)) โ (2 ยท (๐ตโ3))) / ;27)) |
263 | | mulcl 11136 |
. . . . . . . . . . . . . . . . . . . 20
โข ((3
โ โ โง (๐ตโ3) โ โ) โ (3 ยท
(๐ตโ3)) โ
โ) |
264 | 4, 19, 263 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (3 ยท (๐ตโ3)) โ
โ) |
265 | 264, 21, 36, 38 | divsubdird 11971 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((3 ยท (๐ตโ3)) โ (2 ยท
(๐ตโ3))) / ;27) = (((3 ยท (๐ตโ3)) / ;27) โ ((2 ยท (๐ตโ3)) / ;27))) |
266 | 262, 265 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ตโ3) / ;27) = (((3 ยท (๐ตโ3)) / ;27) โ ((2 ยท (๐ตโ3)) / ;27))) |
267 | 253, 266 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ตโ3) / (3โ3)) = (((3 ยท
(๐ตโ3)) / ;27) โ ((2 ยท (๐ตโ3)) / ;27))) |
268 | 22, 4, 239 | mulcomli 11165 |
. . . . . . . . . . . . . . . . . . 19
โข (3
ยท 9) = ;27 |
269 | 268 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . 18
โข ((3
ยท (๐ตโ3)) / (3
ยท 9)) = ((3 ยท (๐ตโ3)) / ;27) |
270 | 19, 96, 10, 99, 12 | divcan5d 11958 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((3 ยท (๐ตโ3)) / (3 ยท 9)) =
((๐ตโ3) /
9)) |
271 | 269, 270 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((3 ยท (๐ตโ3)) / ;27) = ((๐ตโ3) / 9)) |
272 | 271 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((3 ยท (๐ตโ3)) / ;27) โ ((2 ยท (๐ตโ3)) / ;27)) = (((๐ตโ3) / 9) โ ((2 ยท (๐ตโ3)) / ;27))) |
273 | 252, 267,
272 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ต / 3)โ3) = (((๐ตโ3) / 9) โ ((2 ยท (๐ตโ3)) / ;27))) |
274 | 273 | negeqd 11396 |
. . . . . . . . . . . . . 14
โข (๐ โ -((๐ต / 3)โ3) = -(((๐ตโ3) / 9) โ ((2 ยท (๐ตโ3)) / ;27))) |
275 | 23, 10, 12 | divcld 11932 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ต ยท ๐ถ) / 3) โ โ) |
276 | 275, 249,
250 | npncan3d 11549 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3))) = (((2 ยท (๐ตโ3)) / ;27) โ ((๐ตโ3) / 9))) |
277 | 251, 274,
276 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
โข (๐ โ -((๐ต / 3)โ3) = ((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)))) |
278 | 277 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ (-((๐ต / 3)โ3) + ๐ท) = (((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3))) + ๐ท)) |
279 | 184 | negcld 11500 |
. . . . . . . . . . . . 13
โข (๐ โ -((๐ต / 3)โ3) โ
โ) |
280 | 279, 31 | addcomd 11358 |
. . . . . . . . . . . 12
โข (๐ โ (-((๐ต / 3)โ3) + ๐ท) = (๐ท + -((๐ต / 3)โ3))) |
281 | 235, 192 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) โ
โ) |
282 | 250, 275 | subcld 11513 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)) โ โ) |
283 | 281, 282,
31 | addassd 11178 |
. . . . . . . . . . . 12
โข (๐ โ (((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + (((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3))) + ๐ท) = ((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + ((((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)) + ๐ท))) |
284 | 278, 280,
283 | 3eqtr3d 2785 |
. . . . . . . . . . 11
โข (๐ โ (๐ท + -((๐ต / 3)โ3)) = ((((๐ต ยท ๐ถ) / 3) โ ((๐ตโ3) / 9)) + ((((2 ยท (๐ตโ3)) / ;27) โ ((๐ต ยท ๐ถ) / 3)) + ๐ท))) |
285 | 31, 184 | negsubd 11519 |
. . . . . . . . . . 11
โข (๐ โ (๐ท + -((๐ต / 3)โ3)) = (๐ท โ ((๐ต / 3)โ3))) |
286 | 248, 284,
285 | 3eqtr2d 2783 |
. . . . . . . . . 10
โข (๐ โ ((-(๐ / 3) ยท (๐ต / 3)) + (๐ / ;27)) = (๐ท โ ((๐ต / 3)โ3))) |
287 | 218, 286 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ โ ((-(๐ / 3) ยท ๐) + ((-(๐ / 3) ยท (๐ต / 3)) + (๐ / ;27))) = (((๐ถ ยท ๐) โ (3 ยท (๐ ยท ((๐ต / 3)โ2)))) + (๐ท โ ((๐ต / 3)โ3)))) |
288 | 190, 193,
287 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27)) = (((๐ถ ยท ๐) โ (3 ยท (๐ ยท ((๐ต / 3)โ2)))) + (๐ท โ ((๐ต / 3)โ3)))) |
289 | 5, 40 | mulcld 11176 |
. . . . . . . . 9
โข (๐ โ (๐ถ ยท ๐) โ โ) |
290 | 289, 31, 182, 184 | addsub4d 11560 |
. . . . . . . 8
โข (๐ โ (((๐ถ ยท ๐) + ๐ท) โ ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3))) = (((๐ถ ยท ๐) โ (3 ยท (๐ ยท ((๐ต / 3)โ2)))) + (๐ท โ ((๐ต / 3)โ3)))) |
291 | 288, 290 | eqtr4d 2780 |
. . . . . . 7
โข (๐ โ ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27)) = (((๐ถ ยท ๐) + ๐ท) โ ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)))) |
292 | 291 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = (((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) + (((๐ถ ยท ๐) + ๐ท) โ ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3))))) |
293 | 289, 31 | addcld 11175 |
. . . . . . 7
โข (๐ โ ((๐ถ ยท ๐) + ๐ท) โ โ) |
294 | 185, 293 | pncan3d 11516 |
. . . . . 6
โข (๐ โ (((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) + (((๐ถ ยท ๐) + ๐ท) โ ((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)))) = ((๐ถ ยท ๐) + ๐ท)) |
295 | 292, 294 | eqtrd 2777 |
. . . . 5
โข (๐ โ (((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = ((๐ถ ยท ๐) + ๐ท)) |
296 | 295 | oveq2d 7374 |
. . . 4
โข (๐ โ (((๐โ3) + (๐ต ยท (๐โ2))) + (((3 ยท (๐ ยท ((๐ต / 3)โ2))) + ((๐ต / 3)โ3)) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27)))) = (((๐โ3) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท))) |
297 | 175, 188,
296 | 3eqtrd 2781 |
. . 3
โข (๐ โ (((๐ + (๐ต / 3))โ3) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = (((๐โ3) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท))) |
298 | 297 | eqeq1d 2739 |
. 2
โข (๐ โ ((((๐ + (๐ต / 3))โ3) + ((-(๐ / 3) ยท (๐ + (๐ต / 3))) + (๐ / ;27))) = 0 โ (((๐โ3) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0)) |
299 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ3) = (0โ3)) |
300 | | 0exp 14004 |
. . . . . . . . 9
โข (3 โ
โ โ (0โ3) = 0) |
301 | 46, 300 | ax-mp 5 |
. . . . . . . 8
โข
(0โ3) = 0 |
302 | 299, 301 | eqtrdi 2793 |
. . . . . . 7
โข (๐ = 0 โ (๐โ3) = 0) |
303 | | 0ne1 12225 |
. . . . . . . 8
โข 0 โ
1 |
304 | 303 | a1i 11 |
. . . . . . 7
โข (๐ = 0 โ 0 โ
1) |
305 | 302, 304 | eqnetrd 3012 |
. . . . . 6
โข (๐ = 0 โ (๐โ3) โ 1) |
306 | 305 | necon2i 2979 |
. . . . 5
โข ((๐โ3) = 1 โ ๐ โ 0) |
307 | | eqcom 2744 |
. . . . . . . 8
โข (๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) โ -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) = ๐) |
308 | 2 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ต โ โ) |
309 | | simprl 770 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
310 | 43 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
311 | 309, 310 | mulcld 11176 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท ๐) โ โ) |
312 | 9 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
313 | | simprr 772 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ 0) |
314 | 160 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ 0) |
315 | 309, 310,
313, 314 | mulne0d 11808 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท ๐) โ 0) |
316 | 312, 311,
315 | divcld 11932 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / (๐ ยท ๐)) โ โ) |
317 | 311, 316 | addcld 11175 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) + (๐ / (๐ ยท ๐))) โ โ) |
318 | 4 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ 3 โ
โ) |
319 | 11 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ 3 โ 0) |
320 | 308, 317,
318, 319 | divdird 11970 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต + ((๐ ยท ๐) + (๐ / (๐ ยท ๐)))) / 3) = ((๐ต / 3) + (((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3))) |
321 | 308, 311,
316 | addassd 11178 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) = (๐ต + ((๐ ยท ๐) + (๐ / (๐ ยท ๐))))) |
322 | 321 | oveq1d 7373 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) = ((๐ต + ((๐ ยท ๐) + (๐ / (๐ ยท ๐)))) / 3)) |
323 | 41 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ต / 3) โ โ) |
324 | 317, 318,
319 | divcld 11932 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ โ) |
325 | 323, 324 | subnegd 11520 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ต / 3) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3)) = ((๐ต / 3) + (((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3))) |
326 | 320, 322,
325 | 3eqtr4d 2787 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) = ((๐ต / 3) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3))) |
327 | 326 | negeqd 11396 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) = -((๐ต / 3) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3))) |
328 | 324 | negcld 11500 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ โ) |
329 | 323, 328 | negsubdi2d 11529 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -((๐ต / 3) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3)) = (-(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ (๐ต / 3))) |
330 | 327, 329 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) = (-(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ (๐ต / 3))) |
331 | 330 | eqeq1d 2739 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (-(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) = ๐ โ (-(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ (๐ต / 3)) = ๐)) |
332 | 307, 331 | bitrid 283 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3) โ (-(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ (๐ต / 3)) = ๐)) |
333 | 40 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ โ) |
334 | 328, 323,
333 | subadd2d 11532 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((-(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ (๐ต / 3)) = ๐ โ (๐ + (๐ต / 3)) = -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3))) |
335 | 311, 316,
318, 319 | divdird 11970 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) = (((๐ ยท ๐) / 3) + ((๐ / (๐ ยท ๐)) / 3))) |
336 | 335 | negeqd 11396 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) = -(((๐ ยท ๐) / 3) + ((๐ / (๐ ยท ๐)) / 3))) |
337 | 311, 318,
319 | divcld 11932 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) / 3) โ โ) |
338 | 316, 318,
319 | divcld 11932 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / (๐ ยท ๐)) / 3) โ โ) |
339 | 337, 338 | negdi2d 11527 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -(((๐ ยท ๐) / 3) + ((๐ / (๐ ยท ๐)) / 3)) = (-((๐ ยท ๐) / 3) โ ((๐ / (๐ ยท ๐)) / 3))) |
340 | 309, 310,
318, 319 | divassd 11967 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) / 3) = (๐ ยท (๐ / 3))) |
341 | 340 | negeqd 11396 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -((๐ ยท ๐) / 3) = -(๐ ยท (๐ / 3))) |
342 | 44 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / 3) โ โ) |
343 | 309, 342 | mulneg2d 11610 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท -(๐ / 3)) = -(๐ ยท (๐ / 3))) |
344 | 341, 343 | eqtr4d 2780 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -((๐ ยท ๐) / 3) = (๐ ยท -(๐ / 3))) |
345 | 312, 311,
318, 315, 319 | divdiv32d 11957 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / (๐ ยท ๐)) / 3) = ((๐ / 3) / (๐ ยท ๐))) |
346 | 13 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / 3) โ โ) |
347 | 346, 311,
318, 315, 319 | divcan7d 11960 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ / 3) / 3) / ((๐ ยท ๐) / 3)) = ((๐ / 3) / (๐ ยท ๐))) |
348 | 155 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ / 3) / 3) / ((๐ ยท ๐) / 3)) = ((๐ / 9) / ((๐ ยท ๐) / 3))) |
349 | 348 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ / 3) / 3) / ((๐ ยท ๐) / 3)) = ((๐ / 9) / ((๐ ยท ๐) / 3))) |
350 | 345, 347,
349 | 3eqtr2d 2783 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / (๐ ยท ๐)) / 3) = ((๐ / 9) / ((๐ ยท ๐) / 3))) |
351 | 119 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (๐ / 9) โ โ) |
352 | 311, 318,
315, 319 | divne0d 11948 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) / 3) โ 0) |
353 | 351, 337,
352 | div2negd 11947 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (-(๐ / 9) / -((๐ ยท ๐) / 3)) = ((๐ / 9) / ((๐ ยท ๐) / 3))) |
354 | 344 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (-(๐ / 9) / -((๐ ยท ๐) / 3)) = (-(๐ / 9) / (๐ ยท -(๐ / 3)))) |
355 | 350, 353,
354 | 3eqtr2d 2783 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / (๐ ยท ๐)) / 3) = (-(๐ / 9) / (๐ ยท -(๐ / 3)))) |
356 | 344, 355 | oveq12d 7376 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ (-((๐ ยท ๐) / 3) โ ((๐ / (๐ ยท ๐)) / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3))))) |
357 | 336, 339,
356 | 3eqtrd 2781 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3))))) |
358 | 357 | eqeq2d 2748 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ + (๐ต / 3)) = -(((๐ ยท ๐) + (๐ / (๐ ยท ๐))) / 3) โ (๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3)))))) |
359 | 332, 334,
358 | 3bitrrd 306 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3)))) โ ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3))) |
360 | 359 | anassrs 469 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ๐ โ 0) โ ((๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3)))) โ ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3))) |
361 | 306, 360 | sylan2 594 |
. . . 4
โข (((๐ โง ๐ โ โ) โง (๐โ3) = 1) โ ((๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3)))) โ ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3))) |
362 | 361 | pm5.32da 580 |
. . 3
โข ((๐ โง ๐ โ โ) โ (((๐โ3) = 1 โง (๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3))))) โ ((๐โ3) = 1 โง ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3)))) |
363 | 362 | rexbidva 3174 |
. 2
โข (๐ โ (โ๐ โ โ ((๐โ3) = 1 โง (๐ + (๐ต / 3)) = ((๐ ยท -(๐ / 3)) โ (-(๐ / 9) / (๐ ยท -(๐ / 3))))) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3)))) |
364 | 163, 298,
363 | 3bitr3d 309 |
1
โข (๐ โ ((((๐โ3) + (๐ต ยท (๐โ2))) + ((๐ถ ยท ๐) + ๐ท)) = 0 โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = -(((๐ต + (๐ ยท ๐)) + (๐ / (๐ ยท ๐))) / 3)))) |