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