Step | Hyp | Ref
| Expression |
1 | | quart.a |
. . . 4
โข (๐ โ ๐ด โ โ) |
2 | | quart.b |
. . . 4
โข (๐ โ ๐ต โ โ) |
3 | | quart.c |
. . . 4
โข (๐ โ ๐ถ โ โ) |
4 | | quart.d |
. . . 4
โข (๐ โ ๐ท โ โ) |
5 | | quart.p |
. . . 4
โข (๐ โ ๐ = (๐ต โ ((3 / 8) ยท (๐ดโ2)))) |
6 | | quart.q |
. . . 4
โข (๐ โ ๐ = ((๐ถ โ ((๐ด ยท ๐ต) / 2)) + ((๐ดโ3) / 8))) |
7 | | quart.r |
. . . 4
โข (๐ โ ๐
= ((๐ท โ ((๐ถ ยท ๐ด) / 4)) + ((((๐ดโ2) ยท ๐ต) / ;16) โ ((3 / ;;256)
ยท (๐ดโ4))))) |
8 | | quart.x |
. . . 4
โข (๐ โ ๐ โ โ) |
9 | | quart.e |
. . . . . 6
โข (๐ โ ๐ธ = -(๐ด / 4)) |
10 | 9 | oveq2d 7425 |
. . . . 5
โข (๐ โ (๐ โ ๐ธ) = (๐ โ -(๐ด / 4))) |
11 | | 4cn 12297 |
. . . . . . . 8
โข 4 โ
โ |
12 | 11 | a1i 11 |
. . . . . . 7
โข (๐ โ 4 โ
โ) |
13 | | 4ne0 12320 |
. . . . . . . 8
โข 4 โ
0 |
14 | 13 | a1i 11 |
. . . . . . 7
โข (๐ โ 4 โ 0) |
15 | 1, 12, 14 | divcld 11990 |
. . . . . 6
โข (๐ โ (๐ด / 4) โ โ) |
16 | 8, 15 | subnegd 11578 |
. . . . 5
โข (๐ โ (๐ โ -(๐ด / 4)) = (๐ + (๐ด / 4))) |
17 | 10, 16 | eqtrd 2773 |
. . . 4
โข (๐ โ (๐ โ ๐ธ) = (๐ + (๐ด / 4))) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 17 | quart1 26361 |
. . 3
โข (๐ โ (((๐โ4) + (๐ด ยท (๐โ3))) + ((๐ต ยท (๐โ2)) + ((๐ถ ยท ๐) + ๐ท))) = ((((๐ โ ๐ธ)โ4) + (๐ ยท ((๐ โ ๐ธ)โ2))) + ((๐ ยท (๐ โ ๐ธ)) + ๐
))) |
19 | 18 | eqeq1d 2735 |
. 2
โข (๐ โ ((((๐โ4) + (๐ด ยท (๐โ3))) + ((๐ต ยท (๐โ2)) + ((๐ถ ยท ๐) + ๐ท))) = 0 โ ((((๐ โ ๐ธ)โ4) + (๐ ยท ((๐ โ ๐ธ)โ2))) + ((๐ ยท (๐ โ ๐ธ)) + ๐
)) = 0)) |
20 | 1, 2, 3, 4, 5, 6, 7 | quart1cl 26359 |
. . . 4
โข (๐ โ (๐ โ โ โง ๐ โ โ โง ๐
โ โ)) |
21 | 20 | simp1d 1143 |
. . 3
โข (๐ โ ๐ โ โ) |
22 | 20 | simp2d 1144 |
. . 3
โข (๐ โ ๐ โ โ) |
23 | 15 | negcld 11558 |
. . . . 5
โข (๐ โ -(๐ด / 4) โ โ) |
24 | 9, 23 | eqeltrd 2834 |
. . . 4
โข (๐ โ ๐ธ โ โ) |
25 | 8, 24 | subcld 11571 |
. . 3
โข (๐ โ (๐ โ ๐ธ) โ โ) |
26 | | quart.u |
. . . . 5
โข (๐ โ ๐ = ((๐โ2) + (;12 ยท ๐
))) |
27 | | quart.v |
. . . . 5
โข (๐ โ ๐ = ((-(2 ยท (๐โ3)) โ (;27 ยท (๐โ2))) + (;72 ยท (๐ ยท ๐
)))) |
28 | | quart.w |
. . . . 5
โข (๐ โ ๐ = (โโ((๐โ2) โ (4 ยท (๐โ3))))) |
29 | | quart.s |
. . . . 5
โข (๐ โ ๐ = ((โโ๐) / 2)) |
30 | | quart.m |
. . . . 5
โข (๐ โ ๐ = -((((2 ยท ๐) + ๐) + (๐ / ๐)) / 3)) |
31 | | quart.t |
. . . . 5
โข (๐ โ ๐ = (((๐ + ๐) / 2)โ๐(1 /
3))) |
32 | | quart.t0 |
. . . . 5
โข (๐ โ ๐ โ 0) |
33 | 1, 2, 3, 4, 1, 9, 5, 6, 7, 26,
27, 28, 29, 30, 31, 32 | quartlem3 26364 |
. . . 4
โข (๐ โ (๐ โ โ โง ๐ โ โ โง ๐ โ โ)) |
34 | 33 | simp1d 1143 |
. . 3
โข (๐ โ ๐ โ โ) |
35 | 29 | oveq2d 7425 |
. . . . . 6
โข (๐ โ (2 ยท ๐) = (2 ยท
((โโ๐) /
2))) |
36 | 33 | simp2d 1144 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
37 | 36 | sqrtcld 15384 |
. . . . . . 7
โข (๐ โ (โโ๐) โ
โ) |
38 | | 2cnd 12290 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
39 | | 2ne0 12316 |
. . . . . . . 8
โข 2 โ
0 |
40 | 39 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ 0) |
41 | 37, 38, 40 | divcan2d 11992 |
. . . . . 6
โข (๐ โ (2 ยท
((โโ๐) / 2)) =
(โโ๐)) |
42 | 35, 41 | eqtrd 2773 |
. . . . 5
โข (๐ โ (2 ยท ๐) = (โโ๐)) |
43 | 42 | oveq1d 7424 |
. . . 4
โข (๐ โ ((2 ยท ๐)โ2) =
((โโ๐)โ2)) |
44 | 36 | sqsqrtd 15386 |
. . . 4
โข (๐ โ ((โโ๐)โ2) = ๐) |
45 | 43, 44 | eqtr2d 2774 |
. . 3
โข (๐ โ ๐ = ((2 ยท ๐)โ2)) |
46 | | quart.m0 |
. . 3
โข (๐ โ ๐ โ 0) |
47 | | quart.i |
. . . . 5
โข (๐ โ ๐ผ = (โโ((-(๐โ2) โ (๐ / 2)) + ((๐ / 4) / ๐)))) |
48 | | quart.j |
. . . . 5
โข (๐ โ ๐ฝ = (โโ((-(๐โ2) โ (๐ / 2)) โ ((๐ / 4) / ๐)))) |
49 | 1, 2, 3, 4, 1, 9, 5, 6, 7, 26,
27, 28, 29, 30, 31, 32, 46, 47, 48 | quartlem4 26365 |
. . . 4
โข (๐ โ (๐ โ 0 โง ๐ผ โ โ โง ๐ฝ โ โ)) |
50 | 49 | simp2d 1144 |
. . 3
โข (๐ โ ๐ผ โ โ) |
51 | 47 | oveq1d 7424 |
. . . 4
โข (๐ โ (๐ผโ2) = ((โโ((-(๐โ2) โ (๐ / 2)) + ((๐ / 4) / ๐)))โ2)) |
52 | 34 | sqcld 14109 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ โ) |
53 | 52 | negcld 11558 |
. . . . . . 7
โข (๐ โ -(๐โ2) โ โ) |
54 | 21 | halfcld 12457 |
. . . . . . 7
โข (๐ โ (๐ / 2) โ โ) |
55 | 53, 54 | subcld 11571 |
. . . . . 6
โข (๐ โ (-(๐โ2) โ (๐ / 2)) โ โ) |
56 | 22, 12, 14 | divcld 11990 |
. . . . . . 7
โข (๐ โ (๐ / 4) โ โ) |
57 | 49 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
58 | 56, 34, 57 | divcld 11990 |
. . . . . 6
โข (๐ โ ((๐ / 4) / ๐) โ โ) |
59 | 55, 58 | addcld 11233 |
. . . . 5
โข (๐ โ ((-(๐โ2) โ (๐ / 2)) + ((๐ / 4) / ๐)) โ โ) |
60 | 59 | sqsqrtd 15386 |
. . . 4
โข (๐ โ ((โโ((-(๐โ2) โ (๐ / 2)) + ((๐ / 4) / ๐)))โ2) = ((-(๐โ2) โ (๐ / 2)) + ((๐ / 4) / ๐))) |
61 | 51, 60 | eqtrd 2773 |
. . 3
โข (๐ โ (๐ผโ2) = ((-(๐โ2) โ (๐ / 2)) + ((๐ / 4) / ๐))) |
62 | 20 | simp3d 1145 |
. . 3
โข (๐ โ ๐
โ โ) |
63 | | 1cnd 11209 |
. . . . 5
โข (๐ โ 1 โ
โ) |
64 | | 3z 12595 |
. . . . . 6
โข 3 โ
โค |
65 | | 1exp 14057 |
. . . . . 6
โข (3 โ
โค โ (1โ3) = 1) |
66 | 64, 65 | mp1i 13 |
. . . . 5
โข (๐ โ (1โ3) =
1) |
67 | 33 | simp3d 1145 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
68 | 67 | mullidd 11232 |
. . . . . . . . . 10
โข (๐ โ (1 ยท ๐) = ๐) |
69 | 68 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) + (1 ยท ๐)) = ((2 ยท ๐) + ๐)) |
70 | 68 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ โ (๐ / (1 ยท ๐)) = (๐ / ๐)) |
71 | 69, 70 | oveq12d 7427 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) = (((2 ยท ๐) + ๐) + (๐ / ๐))) |
72 | 71 | oveq1d 7424 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3) = ((((2 ยท ๐) + ๐) + (๐ / ๐)) / 3)) |
73 | 72 | negeqd 11454 |
. . . . . 6
โข (๐ โ -((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3) = -((((2 ยท ๐) + ๐) + (๐ / ๐)) / 3)) |
74 | 30, 73 | eqtr4d 2776 |
. . . . 5
โข (๐ โ ๐ = -((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3)) |
75 | | oveq1 7416 |
. . . . . . . 8
โข (๐ฅ = 1 โ (๐ฅโ3) = (1โ3)) |
76 | 75 | eqeq1d 2735 |
. . . . . . 7
โข (๐ฅ = 1 โ ((๐ฅโ3) = 1 โ (1โ3) =
1)) |
77 | | oveq1 7416 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (๐ฅ ยท ๐) = (1 ยท ๐)) |
78 | 77 | oveq2d 7425 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ((2 ยท ๐) + (๐ฅ ยท ๐)) = ((2 ยท ๐) + (1 ยท ๐))) |
79 | 77 | oveq2d 7425 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ (๐ / (๐ฅ ยท ๐)) = (๐ / (1 ยท ๐))) |
80 | 78, 79 | oveq12d 7427 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ (((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) = (((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐)))) |
81 | 80 | oveq1d 7424 |
. . . . . . . . 9
โข (๐ฅ = 1 โ ((((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3) = ((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3)) |
82 | 81 | negeqd 11454 |
. . . . . . . 8
โข (๐ฅ = 1 โ -((((2 ยท
๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3) = -((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3)) |
83 | 82 | eqeq2d 2744 |
. . . . . . 7
โข (๐ฅ = 1 โ (๐ = -((((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3) โ ๐ = -((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3))) |
84 | 76, 83 | anbi12d 632 |
. . . . . 6
โข (๐ฅ = 1 โ (((๐ฅโ3) = 1 โง ๐ = -((((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3)) โ ((1โ3) = 1 โง ๐ = -((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3)))) |
85 | 84 | rspcev 3613 |
. . . . 5
โข ((1
โ โ โง ((1โ3) = 1 โง ๐ = -((((2 ยท ๐) + (1 ยท ๐)) + (๐ / (1 ยท ๐))) / 3))) โ โ๐ฅ โ โ ((๐ฅโ3) = 1 โง ๐ = -((((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3))) |
86 | 63, 66, 74, 85 | syl12anc 836 |
. . . 4
โข (๐ โ โ๐ฅ โ โ ((๐ฅโ3) = 1 โง ๐ = -((((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3))) |
87 | | 2cn 12287 |
. . . . . 6
โข 2 โ
โ |
88 | | mulcl 11194 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
89 | 87, 21, 88 | sylancr 588 |
. . . . 5
โข (๐ โ (2 ยท ๐) โ
โ) |
90 | 21 | sqcld 14109 |
. . . . . 6
โข (๐ โ (๐โ2) โ โ) |
91 | | mulcl 11194 |
. . . . . . 7
โข ((4
โ โ โง ๐
โ โ) โ (4 ยท ๐
) โ โ) |
92 | 11, 62, 91 | sylancr 588 |
. . . . . 6
โข (๐ โ (4 ยท ๐
) โ
โ) |
93 | 90, 92 | subcld 11571 |
. . . . 5
โข (๐ โ ((๐โ2) โ (4 ยท ๐
)) โ
โ) |
94 | 22 | sqcld 14109 |
. . . . . 6
โข (๐ โ (๐โ2) โ โ) |
95 | 94 | negcld 11558 |
. . . . 5
โข (๐ โ -(๐โ2) โ โ) |
96 | 31 | oveq1d 7424 |
. . . . . 6
โข (๐ โ (๐โ3) = ((((๐ + ๐) / 2)โ๐(1 /
3))โ3)) |
97 | 1, 2, 3, 4, 1, 9, 5, 6, 7, 26,
27, 28 | quartlem2 26363 |
. . . . . . . . . 10
โข (๐ โ (๐ โ โ โง ๐ โ โ โง ๐ โ โ)) |
98 | 97 | simp2d 1144 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
99 | 97 | simp3d 1145 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
100 | 98, 99 | addcld 11233 |
. . . . . . . 8
โข (๐ โ (๐ + ๐) โ โ) |
101 | 100 | halfcld 12457 |
. . . . . . 7
โข (๐ โ ((๐ + ๐) / 2) โ โ) |
102 | | 3nn 12291 |
. . . . . . 7
โข 3 โ
โ |
103 | | cxproot 26198 |
. . . . . . 7
โข ((((๐ + ๐) / 2) โ โ โง 3 โ
โ) โ ((((๐ +
๐) /
2)โ๐(1 / 3))โ3) = ((๐ + ๐) / 2)) |
104 | 101, 102,
103 | sylancl 587 |
. . . . . 6
โข (๐ โ ((((๐ + ๐) / 2)โ๐(1 /
3))โ3) = ((๐ + ๐) / 2)) |
105 | 96, 104 | eqtrd 2773 |
. . . . 5
โข (๐ โ (๐โ3) = ((๐ + ๐) / 2)) |
106 | 28 | oveq1d 7424 |
. . . . . 6
โข (๐ โ (๐โ2) = ((โโ((๐โ2) โ (4 ยท
(๐โ3))))โ2)) |
107 | 98 | sqcld 14109 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ โ) |
108 | 97 | simp1d 1143 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
109 | | 3nn0 12490 |
. . . . . . . . . 10
โข 3 โ
โ0 |
110 | | expcl 14045 |
. . . . . . . . . 10
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
111 | 108, 109,
110 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (๐โ3) โ โ) |
112 | | mulcl 11194 |
. . . . . . . . 9
โข ((4
โ โ โง (๐โ3) โ โ) โ (4 ยท
(๐โ3)) โ
โ) |
113 | 11, 111, 112 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (4 ยท (๐โ3)) โ
โ) |
114 | 107, 113 | subcld 11571 |
. . . . . . 7
โข (๐ โ ((๐โ2) โ (4 ยท (๐โ3))) โ
โ) |
115 | 114 | sqsqrtd 15386 |
. . . . . 6
โข (๐ โ ((โโ((๐โ2) โ (4 ยท
(๐โ3))))โ2) =
((๐โ2) โ (4
ยท (๐โ3)))) |
116 | 106, 115 | eqtrd 2773 |
. . . . 5
โข (๐ โ (๐โ2) = ((๐โ2) โ (4 ยท (๐โ3)))) |
117 | 21, 22, 62, 26, 27 | quartlem1 26362 |
. . . . . 6
โข (๐ โ (๐ = (((2 ยท ๐)โ2) โ (3 ยท ((๐โ2) โ (4 ยท
๐
)))) โง ๐ = (((2 ยท ((2 ยท
๐)โ3)) โ (9
ยท ((2 ยท ๐)
ยท ((๐โ2)
โ (4 ยท ๐
)))))
+ (;27 ยท -(๐โ2))))) |
118 | 117 | simpld 496 |
. . . . 5
โข (๐ โ ๐ = (((2 ยท ๐)โ2) โ (3 ยท ((๐โ2) โ (4 ยท
๐
))))) |
119 | 117 | simprd 497 |
. . . . 5
โข (๐ โ ๐ = (((2 ยท ((2 ยท ๐)โ3)) โ (9 ยท
((2 ยท ๐) ยท
((๐โ2) โ (4
ยท ๐
))))) + (;27 ยท -(๐โ2)))) |
120 | 89, 93, 95, 36, 67, 105, 99, 116, 118, 119, 32 | mcubic 26352 |
. . . 4
โข (๐ โ ((((๐โ3) + ((2 ยท ๐) ยท (๐โ2))) + ((((๐โ2) โ (4 ยท ๐
)) ยท ๐) + -(๐โ2))) = 0 โ โ๐ฅ โ โ ((๐ฅโ3) = 1 โง ๐ = -((((2 ยท ๐) + (๐ฅ ยท ๐)) + (๐ / (๐ฅ ยท ๐))) / 3)))) |
121 | 86, 120 | mpbird 257 |
. . 3
โข (๐ โ (((๐โ3) + ((2 ยท ๐) ยท (๐โ2))) + ((((๐โ2) โ (4 ยท ๐
)) ยท ๐) + -(๐โ2))) = 0) |
122 | 49 | simp3d 1145 |
. . 3
โข (๐ โ ๐ฝ โ โ) |
123 | 48 | oveq1d 7424 |
. . . 4
โข (๐ โ (๐ฝโ2) = ((โโ((-(๐โ2) โ (๐ / 2)) โ ((๐ / 4) / ๐)))โ2)) |
124 | 55, 58 | subcld 11571 |
. . . . 5
โข (๐ โ ((-(๐โ2) โ (๐ / 2)) โ ((๐ / 4) / ๐)) โ โ) |
125 | 124 | sqsqrtd 15386 |
. . . 4
โข (๐ โ ((โโ((-(๐โ2) โ (๐ / 2)) โ ((๐ / 4) / ๐)))โ2) = ((-(๐โ2) โ (๐ / 2)) โ ((๐ / 4) / ๐))) |
126 | 123, 125 | eqtrd 2773 |
. . 3
โข (๐ โ (๐ฝโ2) = ((-(๐โ2) โ (๐ / 2)) โ ((๐ / 4) / ๐))) |
127 | 21, 22, 25, 34, 45, 46, 50, 61, 62, 121, 122, 126 | dquart 26358 |
. 2
โข (๐ โ (((((๐ โ ๐ธ)โ4) + (๐ ยท ((๐ โ ๐ธ)โ2))) + ((๐ ยท (๐ โ ๐ธ)) + ๐
)) = 0 โ (((๐ โ ๐ธ) = (-๐ + ๐ผ) โจ (๐ โ ๐ธ) = (-๐ โ ๐ผ)) โจ ((๐ โ ๐ธ) = (๐ + ๐ฝ) โจ (๐ โ ๐ธ) = (๐ โ ๐ฝ))))) |
128 | 34 | negcld 11558 |
. . . . . . . 8
โข (๐ โ -๐ โ โ) |
129 | 128, 50 | addcld 11233 |
. . . . . . 7
โข (๐ โ (-๐ + ๐ผ) โ โ) |
130 | 8, 24, 129 | subaddd 11589 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ธ) = (-๐ + ๐ผ) โ (๐ธ + (-๐ + ๐ผ)) = ๐)) |
131 | 24, 34 | negsubd 11577 |
. . . . . . . . 9
โข (๐ โ (๐ธ + -๐) = (๐ธ โ ๐)) |
132 | 131 | oveq1d 7424 |
. . . . . . . 8
โข (๐ โ ((๐ธ + -๐) + ๐ผ) = ((๐ธ โ ๐) + ๐ผ)) |
133 | 24, 128, 50 | addassd 11236 |
. . . . . . . 8
โข (๐ โ ((๐ธ + -๐) + ๐ผ) = (๐ธ + (-๐ + ๐ผ))) |
134 | 132, 133 | eqtr3d 2775 |
. . . . . . 7
โข (๐ โ ((๐ธ โ ๐) + ๐ผ) = (๐ธ + (-๐ + ๐ผ))) |
135 | 134 | eqeq1d 2735 |
. . . . . 6
โข (๐ โ (((๐ธ โ ๐) + ๐ผ) = ๐ โ (๐ธ + (-๐ + ๐ผ)) = ๐)) |
136 | 130, 135 | bitr4d 282 |
. . . . 5
โข (๐ โ ((๐ โ ๐ธ) = (-๐ + ๐ผ) โ ((๐ธ โ ๐) + ๐ผ) = ๐)) |
137 | | eqcom 2740 |
. . . . 5
โข (((๐ธ โ ๐) + ๐ผ) = ๐ โ ๐ = ((๐ธ โ ๐) + ๐ผ)) |
138 | 136, 137 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ โ ๐ธ) = (-๐ + ๐ผ) โ ๐ = ((๐ธ โ ๐) + ๐ผ))) |
139 | 128, 50 | subcld 11571 |
. . . . . . 7
โข (๐ โ (-๐ โ ๐ผ) โ โ) |
140 | 8, 24, 139 | subaddd 11589 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ธ) = (-๐ โ ๐ผ) โ (๐ธ + (-๐ โ ๐ผ)) = ๐)) |
141 | 131 | oveq1d 7424 |
. . . . . . . 8
โข (๐ โ ((๐ธ + -๐) โ ๐ผ) = ((๐ธ โ ๐) โ ๐ผ)) |
142 | 24, 128, 50 | addsubassd 11591 |
. . . . . . . 8
โข (๐ โ ((๐ธ + -๐) โ ๐ผ) = (๐ธ + (-๐ โ ๐ผ))) |
143 | 141, 142 | eqtr3d 2775 |
. . . . . . 7
โข (๐ โ ((๐ธ โ ๐) โ ๐ผ) = (๐ธ + (-๐ โ ๐ผ))) |
144 | 143 | eqeq1d 2735 |
. . . . . 6
โข (๐ โ (((๐ธ โ ๐) โ ๐ผ) = ๐ โ (๐ธ + (-๐ โ ๐ผ)) = ๐)) |
145 | 140, 144 | bitr4d 282 |
. . . . 5
โข (๐ โ ((๐ โ ๐ธ) = (-๐ โ ๐ผ) โ ((๐ธ โ ๐) โ ๐ผ) = ๐)) |
146 | | eqcom 2740 |
. . . . 5
โข (((๐ธ โ ๐) โ ๐ผ) = ๐ โ ๐ = ((๐ธ โ ๐) โ ๐ผ)) |
147 | 145, 146 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ โ ๐ธ) = (-๐ โ ๐ผ) โ ๐ = ((๐ธ โ ๐) โ ๐ผ))) |
148 | 138, 147 | orbi12d 918 |
. . 3
โข (๐ โ (((๐ โ ๐ธ) = (-๐ + ๐ผ) โจ (๐ โ ๐ธ) = (-๐ โ ๐ผ)) โ (๐ = ((๐ธ โ ๐) + ๐ผ) โจ ๐ = ((๐ธ โ ๐) โ ๐ผ)))) |
149 | 34, 122 | addcld 11233 |
. . . . . . 7
โข (๐ โ (๐ + ๐ฝ) โ โ) |
150 | 8, 24, 149 | subaddd 11589 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ธ) = (๐ + ๐ฝ) โ (๐ธ + (๐ + ๐ฝ)) = ๐)) |
151 | 24, 34, 122 | addassd 11236 |
. . . . . . 7
โข (๐ โ ((๐ธ + ๐) + ๐ฝ) = (๐ธ + (๐ + ๐ฝ))) |
152 | 151 | eqeq1d 2735 |
. . . . . 6
โข (๐ โ (((๐ธ + ๐) + ๐ฝ) = ๐ โ (๐ธ + (๐ + ๐ฝ)) = ๐)) |
153 | 150, 152 | bitr4d 282 |
. . . . 5
โข (๐ โ ((๐ โ ๐ธ) = (๐ + ๐ฝ) โ ((๐ธ + ๐) + ๐ฝ) = ๐)) |
154 | | eqcom 2740 |
. . . . 5
โข (((๐ธ + ๐) + ๐ฝ) = ๐ โ ๐ = ((๐ธ + ๐) + ๐ฝ)) |
155 | 153, 154 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ โ ๐ธ) = (๐ + ๐ฝ) โ ๐ = ((๐ธ + ๐) + ๐ฝ))) |
156 | 34, 122 | subcld 11571 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ฝ) โ โ) |
157 | 8, 24, 156 | subaddd 11589 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ธ) = (๐ โ ๐ฝ) โ (๐ธ + (๐ โ ๐ฝ)) = ๐)) |
158 | 24, 34, 122 | addsubassd 11591 |
. . . . . . 7
โข (๐ โ ((๐ธ + ๐) โ ๐ฝ) = (๐ธ + (๐ โ ๐ฝ))) |
159 | 158 | eqeq1d 2735 |
. . . . . 6
โข (๐ โ (((๐ธ + ๐) โ ๐ฝ) = ๐ โ (๐ธ + (๐ โ ๐ฝ)) = ๐)) |
160 | 157, 159 | bitr4d 282 |
. . . . 5
โข (๐ โ ((๐ โ ๐ธ) = (๐ โ ๐ฝ) โ ((๐ธ + ๐) โ ๐ฝ) = ๐)) |
161 | | eqcom 2740 |
. . . . 5
โข (((๐ธ + ๐) โ ๐ฝ) = ๐ โ ๐ = ((๐ธ + ๐) โ ๐ฝ)) |
162 | 160, 161 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ โ ๐ธ) = (๐ โ ๐ฝ) โ ๐ = ((๐ธ + ๐) โ ๐ฝ))) |
163 | 155, 162 | orbi12d 918 |
. . 3
โข (๐ โ (((๐ โ ๐ธ) = (๐ + ๐ฝ) โจ (๐ โ ๐ธ) = (๐ โ ๐ฝ)) โ (๐ = ((๐ธ + ๐) + ๐ฝ) โจ ๐ = ((๐ธ + ๐) โ ๐ฝ)))) |
164 | 148, 163 | orbi12d 918 |
. 2
โข (๐ โ ((((๐ โ ๐ธ) = (-๐ + ๐ผ) โจ (๐ โ ๐ธ) = (-๐ โ ๐ผ)) โจ ((๐ โ ๐ธ) = (๐ + ๐ฝ) โจ (๐ โ ๐ธ) = (๐ โ ๐ฝ))) โ ((๐ = ((๐ธ โ ๐) + ๐ผ) โจ ๐ = ((๐ธ โ ๐) โ ๐ผ)) โจ (๐ = ((๐ธ + ๐) + ๐ฝ) โจ ๐ = ((๐ธ + ๐) โ ๐ฝ))))) |
165 | 19, 127, 164 | 3bitrd 305 |
1
โข (๐ โ ((((๐โ4) + (๐ด ยท (๐โ3))) + ((๐ต ยท (๐โ2)) + ((๐ถ ยท ๐) + ๐ท))) = 0 โ ((๐ = ((๐ธ โ ๐) + ๐ผ) โจ ๐ = ((๐ธ โ ๐) โ ๐ผ)) โจ (๐ = ((๐ธ + ๐) + ๐ฝ) โจ ๐ = ((๐ธ + ๐) โ ๐ฝ))))) |