Step |
Hyp |
Ref |
Expression |
1 |
|
quart1.a |
|- ( ph -> A e. CC ) |
2 |
|
quart1.b |
|- ( ph -> B e. CC ) |
3 |
|
quart1.c |
|- ( ph -> C e. CC ) |
4 |
|
quart1.d |
|- ( ph -> D e. CC ) |
5 |
|
quart1.p |
|- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) |
6 |
|
quart1.q |
|- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ) |
7 |
|
quart1.r |
|- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) |
8 |
|
quart1.x |
|- ( ph -> X e. CC ) |
9 |
|
quart1.y |
|- ( ph -> Y = ( X + ( A / 4 ) ) ) |
10 |
9
|
oveq1d |
|- ( ph -> ( Y ^ 4 ) = ( ( X + ( A / 4 ) ) ^ 4 ) ) |
11 |
|
4cn |
|- 4 e. CC |
12 |
11
|
a1i |
|- ( ph -> 4 e. CC ) |
13 |
|
4ne0 |
|- 4 =/= 0 |
14 |
13
|
a1i |
|- ( ph -> 4 =/= 0 ) |
15 |
1 12 14
|
divcld |
|- ( ph -> ( A / 4 ) e. CC ) |
16 |
|
binom4 |
|- ( ( X e. CC /\ ( A / 4 ) e. CC ) -> ( ( X + ( A / 4 ) ) ^ 4 ) = ( ( ( X ^ 4 ) + ( 4 x. ( ( X ^ 3 ) x. ( A / 4 ) ) ) ) + ( ( 6 x. ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) + ( ( A / 4 ) ^ 4 ) ) ) ) ) |
17 |
8 15 16
|
syl2anc |
|- ( ph -> ( ( X + ( A / 4 ) ) ^ 4 ) = ( ( ( X ^ 4 ) + ( 4 x. ( ( X ^ 3 ) x. ( A / 4 ) ) ) ) + ( ( 6 x. ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) + ( ( A / 4 ) ^ 4 ) ) ) ) ) |
18 |
|
3nn0 |
|- 3 e. NN0 |
19 |
|
expcl |
|- ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC ) |
20 |
8 18 19
|
sylancl |
|- ( ph -> ( X ^ 3 ) e. CC ) |
21 |
12 20 15
|
mul12d |
|- ( ph -> ( 4 x. ( ( X ^ 3 ) x. ( A / 4 ) ) ) = ( ( X ^ 3 ) x. ( 4 x. ( A / 4 ) ) ) ) |
22 |
1 12 14
|
divcan2d |
|- ( ph -> ( 4 x. ( A / 4 ) ) = A ) |
23 |
22
|
oveq2d |
|- ( ph -> ( ( X ^ 3 ) x. ( 4 x. ( A / 4 ) ) ) = ( ( X ^ 3 ) x. A ) ) |
24 |
20 1
|
mulcomd |
|- ( ph -> ( ( X ^ 3 ) x. A ) = ( A x. ( X ^ 3 ) ) ) |
25 |
21 23 24
|
3eqtrd |
|- ( ph -> ( 4 x. ( ( X ^ 3 ) x. ( A / 4 ) ) ) = ( A x. ( X ^ 3 ) ) ) |
26 |
25
|
oveq2d |
|- ( ph -> ( ( X ^ 4 ) + ( 4 x. ( ( X ^ 3 ) x. ( A / 4 ) ) ) ) = ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) ) |
27 |
|
6nn |
|- 6 e. NN |
28 |
27
|
nncni |
|- 6 e. CC |
29 |
28
|
a1i |
|- ( ph -> 6 e. CC ) |
30 |
15
|
sqcld |
|- ( ph -> ( ( A / 4 ) ^ 2 ) e. CC ) |
31 |
8
|
sqcld |
|- ( ph -> ( X ^ 2 ) e. CC ) |
32 |
29 30 31
|
mulassd |
|- ( ph -> ( ( 6 x. ( ( A / 4 ) ^ 2 ) ) x. ( X ^ 2 ) ) = ( 6 x. ( ( ( A / 4 ) ^ 2 ) x. ( X ^ 2 ) ) ) ) |
33 |
|
3cn |
|- 3 e. CC |
34 |
|
2cn |
|- 2 e. CC |
35 |
|
3t2e6 |
|- ( 3 x. 2 ) = 6 |
36 |
33 34 35
|
mulcomli |
|- ( 2 x. 3 ) = 6 |
37 |
|
8cn |
|- 8 e. CC |
38 |
|
8t2e16 |
|- ( 8 x. 2 ) = ; 1 6 |
39 |
37 34 38
|
mulcomli |
|- ( 2 x. 8 ) = ; 1 6 |
40 |
36 39
|
oveq12i |
|- ( ( 2 x. 3 ) / ( 2 x. 8 ) ) = ( 6 / ; 1 6 ) |
41 |
|
8nn |
|- 8 e. NN |
42 |
41
|
nnne0i |
|- 8 =/= 0 |
43 |
37 42
|
pm3.2i |
|- ( 8 e. CC /\ 8 =/= 0 ) |
44 |
|
2cnne0 |
|- ( 2 e. CC /\ 2 =/= 0 ) |
45 |
|
divcan5 |
|- ( ( 3 e. CC /\ ( 8 e. CC /\ 8 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. 3 ) / ( 2 x. 8 ) ) = ( 3 / 8 ) ) |
46 |
33 43 44 45
|
mp3an |
|- ( ( 2 x. 3 ) / ( 2 x. 8 ) ) = ( 3 / 8 ) |
47 |
40 46
|
eqtr3i |
|- ( 6 / ; 1 6 ) = ( 3 / 8 ) |
48 |
47
|
oveq2i |
|- ( ( A ^ 2 ) x. ( 6 / ; 1 6 ) ) = ( ( A ^ 2 ) x. ( 3 / 8 ) ) |
49 |
1
|
sqcld |
|- ( ph -> ( A ^ 2 ) e. CC ) |
50 |
|
1nn0 |
|- 1 e. NN0 |
51 |
50 27
|
decnncl |
|- ; 1 6 e. NN |
52 |
51
|
nncni |
|- ; 1 6 e. CC |
53 |
52
|
a1i |
|- ( ph -> ; 1 6 e. CC ) |
54 |
51
|
nnne0i |
|- ; 1 6 =/= 0 |
55 |
54
|
a1i |
|- ( ph -> ; 1 6 =/= 0 ) |
56 |
49 29 53 55
|
div12d |
|- ( ph -> ( ( A ^ 2 ) x. ( 6 / ; 1 6 ) ) = ( 6 x. ( ( A ^ 2 ) / ; 1 6 ) ) ) |
57 |
48 56
|
eqtr3id |
|- ( ph -> ( ( A ^ 2 ) x. ( 3 / 8 ) ) = ( 6 x. ( ( A ^ 2 ) / ; 1 6 ) ) ) |
58 |
33 37 42
|
divcli |
|- ( 3 / 8 ) e. CC |
59 |
|
mulcom |
|- ( ( ( 3 / 8 ) e. CC /\ ( A ^ 2 ) e. CC ) -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) = ( ( A ^ 2 ) x. ( 3 / 8 ) ) ) |
60 |
58 49 59
|
sylancr |
|- ( ph -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) = ( ( A ^ 2 ) x. ( 3 / 8 ) ) ) |
61 |
1 12 14
|
sqdivd |
|- ( ph -> ( ( A / 4 ) ^ 2 ) = ( ( A ^ 2 ) / ( 4 ^ 2 ) ) ) |
62 |
11
|
sqvali |
|- ( 4 ^ 2 ) = ( 4 x. 4 ) |
63 |
|
4t4e16 |
|- ( 4 x. 4 ) = ; 1 6 |
64 |
62 63
|
eqtri |
|- ( 4 ^ 2 ) = ; 1 6 |
65 |
64
|
oveq2i |
|- ( ( A ^ 2 ) / ( 4 ^ 2 ) ) = ( ( A ^ 2 ) / ; 1 6 ) |
66 |
61 65
|
eqtrdi |
|- ( ph -> ( ( A / 4 ) ^ 2 ) = ( ( A ^ 2 ) / ; 1 6 ) ) |
67 |
66
|
oveq2d |
|- ( ph -> ( 6 x. ( ( A / 4 ) ^ 2 ) ) = ( 6 x. ( ( A ^ 2 ) / ; 1 6 ) ) ) |
68 |
57 60 67
|
3eqtr4d |
|- ( ph -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) = ( 6 x. ( ( A / 4 ) ^ 2 ) ) ) |
69 |
68
|
oveq1d |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) = ( ( 6 x. ( ( A / 4 ) ^ 2 ) ) x. ( X ^ 2 ) ) ) |
70 |
31 30
|
mulcomd |
|- ( ph -> ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) = ( ( ( A / 4 ) ^ 2 ) x. ( X ^ 2 ) ) ) |
71 |
70
|
oveq2d |
|- ( ph -> ( 6 x. ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) ) = ( 6 x. ( ( ( A / 4 ) ^ 2 ) x. ( X ^ 2 ) ) ) ) |
72 |
32 69 71
|
3eqtr4rd |
|- ( ph -> ( 6 x. ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) ) = ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) ) |
73 |
|
expcl |
|- ( ( ( A / 4 ) e. CC /\ 3 e. NN0 ) -> ( ( A / 4 ) ^ 3 ) e. CC ) |
74 |
15 18 73
|
sylancl |
|- ( ph -> ( ( A / 4 ) ^ 3 ) e. CC ) |
75 |
12 8 74
|
mul12d |
|- ( ph -> ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) = ( X x. ( 4 x. ( ( A / 4 ) ^ 3 ) ) ) ) |
76 |
12 74
|
mulcld |
|- ( ph -> ( 4 x. ( ( A / 4 ) ^ 3 ) ) e. CC ) |
77 |
8 76
|
mulcomd |
|- ( ph -> ( X x. ( 4 x. ( ( A / 4 ) ^ 3 ) ) ) = ( ( 4 x. ( ( A / 4 ) ^ 3 ) ) x. X ) ) |
78 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
79 |
78
|
oveq2i |
|- ( 4 ^ 3 ) = ( 4 ^ ( 2 + 1 ) ) |
80 |
|
2nn0 |
|- 2 e. NN0 |
81 |
|
expp1 |
|- ( ( 4 e. CC /\ 2 e. NN0 ) -> ( 4 ^ ( 2 + 1 ) ) = ( ( 4 ^ 2 ) x. 4 ) ) |
82 |
11 80 81
|
mp2an |
|- ( 4 ^ ( 2 + 1 ) ) = ( ( 4 ^ 2 ) x. 4 ) |
83 |
64
|
oveq1i |
|- ( ( 4 ^ 2 ) x. 4 ) = ( ; 1 6 x. 4 ) |
84 |
79 82 83
|
3eqtri |
|- ( 4 ^ 3 ) = ( ; 1 6 x. 4 ) |
85 |
84
|
oveq2i |
|- ( ( A ^ 3 ) / ( 4 ^ 3 ) ) = ( ( A ^ 3 ) / ( ; 1 6 x. 4 ) ) |
86 |
18
|
a1i |
|- ( ph -> 3 e. NN0 ) |
87 |
1 12 14 86
|
expdivd |
|- ( ph -> ( ( A / 4 ) ^ 3 ) = ( ( A ^ 3 ) / ( 4 ^ 3 ) ) ) |
88 |
|
expcl |
|- ( ( A e. CC /\ 3 e. NN0 ) -> ( A ^ 3 ) e. CC ) |
89 |
1 18 88
|
sylancl |
|- ( ph -> ( A ^ 3 ) e. CC ) |
90 |
89 53 12 55 14
|
divdiv1d |
|- ( ph -> ( ( ( A ^ 3 ) / ; 1 6 ) / 4 ) = ( ( A ^ 3 ) / ( ; 1 6 x. 4 ) ) ) |
91 |
85 87 90
|
3eqtr4a |
|- ( ph -> ( ( A / 4 ) ^ 3 ) = ( ( ( A ^ 3 ) / ; 1 6 ) / 4 ) ) |
92 |
91
|
oveq2d |
|- ( ph -> ( 4 x. ( ( A / 4 ) ^ 3 ) ) = ( 4 x. ( ( ( A ^ 3 ) / ; 1 6 ) / 4 ) ) ) |
93 |
38
|
oveq2i |
|- ( ( A ^ 3 ) / ( 8 x. 2 ) ) = ( ( A ^ 3 ) / ; 1 6 ) |
94 |
37
|
a1i |
|- ( ph -> 8 e. CC ) |
95 |
34
|
a1i |
|- ( ph -> 2 e. CC ) |
96 |
42
|
a1i |
|- ( ph -> 8 =/= 0 ) |
97 |
|
2ne0 |
|- 2 =/= 0 |
98 |
97
|
a1i |
|- ( ph -> 2 =/= 0 ) |
99 |
89 94 95 96 98
|
divdiv1d |
|- ( ph -> ( ( ( A ^ 3 ) / 8 ) / 2 ) = ( ( A ^ 3 ) / ( 8 x. 2 ) ) ) |
100 |
89 53 55
|
divcld |
|- ( ph -> ( ( A ^ 3 ) / ; 1 6 ) e. CC ) |
101 |
100 12 14
|
divcan2d |
|- ( ph -> ( 4 x. ( ( ( A ^ 3 ) / ; 1 6 ) / 4 ) ) = ( ( A ^ 3 ) / ; 1 6 ) ) |
102 |
93 99 101
|
3eqtr4a |
|- ( ph -> ( ( ( A ^ 3 ) / 8 ) / 2 ) = ( 4 x. ( ( ( A ^ 3 ) / ; 1 6 ) / 4 ) ) ) |
103 |
92 102
|
eqtr4d |
|- ( ph -> ( 4 x. ( ( A / 4 ) ^ 3 ) ) = ( ( ( A ^ 3 ) / 8 ) / 2 ) ) |
104 |
103
|
oveq1d |
|- ( ph -> ( ( 4 x. ( ( A / 4 ) ^ 3 ) ) x. X ) = ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) ) |
105 |
75 77 104
|
3eqtrd |
|- ( ph -> ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) = ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) ) |
106 |
|
4nn0 |
|- 4 e. NN0 |
107 |
106
|
a1i |
|- ( ph -> 4 e. NN0 ) |
108 |
1 12 14 107
|
expdivd |
|- ( ph -> ( ( A / 4 ) ^ 4 ) = ( ( A ^ 4 ) / ( 4 ^ 4 ) ) ) |
109 |
|
expmul |
|- ( ( 2 e. CC /\ 2 e. NN0 /\ 4 e. NN0 ) -> ( 2 ^ ( 2 x. 4 ) ) = ( ( 2 ^ 2 ) ^ 4 ) ) |
110 |
34 80 106 109
|
mp3an |
|- ( 2 ^ ( 2 x. 4 ) ) = ( ( 2 ^ 2 ) ^ 4 ) |
111 |
|
4t2e8 |
|- ( 4 x. 2 ) = 8 |
112 |
11 34 111
|
mulcomli |
|- ( 2 x. 4 ) = 8 |
113 |
112
|
oveq2i |
|- ( 2 ^ ( 2 x. 4 ) ) = ( 2 ^ 8 ) |
114 |
110 113
|
eqtr3i |
|- ( ( 2 ^ 2 ) ^ 4 ) = ( 2 ^ 8 ) |
115 |
|
sq2 |
|- ( 2 ^ 2 ) = 4 |
116 |
115
|
oveq1i |
|- ( ( 2 ^ 2 ) ^ 4 ) = ( 4 ^ 4 ) |
117 |
114 116
|
eqtr3i |
|- ( 2 ^ 8 ) = ( 4 ^ 4 ) |
118 |
|
2exp8 |
|- ( 2 ^ 8 ) = ; ; 2 5 6 |
119 |
117 118
|
eqtr3i |
|- ( 4 ^ 4 ) = ; ; 2 5 6 |
120 |
119
|
oveq2i |
|- ( ( A ^ 4 ) / ( 4 ^ 4 ) ) = ( ( A ^ 4 ) / ; ; 2 5 6 ) |
121 |
108 120
|
eqtrdi |
|- ( ph -> ( ( A / 4 ) ^ 4 ) = ( ( A ^ 4 ) / ; ; 2 5 6 ) ) |
122 |
105 121
|
oveq12d |
|- ( ph -> ( ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) + ( ( A / 4 ) ^ 4 ) ) = ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) |
123 |
72 122
|
oveq12d |
|- ( ph -> ( ( 6 x. ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) + ( ( A / 4 ) ^ 4 ) ) ) = ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) ) |
124 |
26 123
|
oveq12d |
|- ( ph -> ( ( ( X ^ 4 ) + ( 4 x. ( ( X ^ 3 ) x. ( A / 4 ) ) ) ) + ( ( 6 x. ( ( X ^ 2 ) x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( 4 x. ( X x. ( ( A / 4 ) ^ 3 ) ) ) + ( ( A / 4 ) ^ 4 ) ) ) ) = ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) ) ) |
125 |
10 17 124
|
3eqtrd |
|- ( ph -> ( Y ^ 4 ) = ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) ) ) |
126 |
125
|
oveq1d |
|- ( ph -> ( ( Y ^ 4 ) + ( P x. ( Y ^ 2 ) ) ) = ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) ) + ( P x. ( Y ^ 2 ) ) ) ) |
127 |
|
expcl |
|- ( ( X e. CC /\ 4 e. NN0 ) -> ( X ^ 4 ) e. CC ) |
128 |
8 106 127
|
sylancl |
|- ( ph -> ( X ^ 4 ) e. CC ) |
129 |
1 20
|
mulcld |
|- ( ph -> ( A x. ( X ^ 3 ) ) e. CC ) |
130 |
128 129
|
addcld |
|- ( ph -> ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) e. CC ) |
131 |
|
mulcl |
|- ( ( ( 3 / 8 ) e. CC /\ ( A ^ 2 ) e. CC ) -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) e. CC ) |
132 |
58 49 131
|
sylancr |
|- ( ph -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) e. CC ) |
133 |
132 31
|
mulcld |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) e. CC ) |
134 |
89 94 96
|
divcld |
|- ( ph -> ( ( A ^ 3 ) / 8 ) e. CC ) |
135 |
134
|
halfcld |
|- ( ph -> ( ( ( A ^ 3 ) / 8 ) / 2 ) e. CC ) |
136 |
135 8
|
mulcld |
|- ( ph -> ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) e. CC ) |
137 |
|
expcl |
|- ( ( A e. CC /\ 4 e. NN0 ) -> ( A ^ 4 ) e. CC ) |
138 |
1 106 137
|
sylancl |
|- ( ph -> ( A ^ 4 ) e. CC ) |
139 |
|
5nn0 |
|- 5 e. NN0 |
140 |
80 139
|
deccl |
|- ; 2 5 e. NN0 |
141 |
140 27
|
decnncl |
|- ; ; 2 5 6 e. NN |
142 |
141
|
nncni |
|- ; ; 2 5 6 e. CC |
143 |
142
|
a1i |
|- ( ph -> ; ; 2 5 6 e. CC ) |
144 |
141
|
nnne0i |
|- ; ; 2 5 6 =/= 0 |
145 |
144
|
a1i |
|- ( ph -> ; ; 2 5 6 =/= 0 ) |
146 |
138 143 145
|
divcld |
|- ( ph -> ( ( A ^ 4 ) / ; ; 2 5 6 ) e. CC ) |
147 |
136 146
|
addcld |
|- ( ph -> ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) e. CC ) |
148 |
133 147
|
addcld |
|- ( ph -> ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) e. CC ) |
149 |
1 2 3 4 5 6 7
|
quart1cl |
|- ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) ) |
150 |
149
|
simp1d |
|- ( ph -> P e. CC ) |
151 |
8 15
|
addcld |
|- ( ph -> ( X + ( A / 4 ) ) e. CC ) |
152 |
9 151
|
eqeltrd |
|- ( ph -> Y e. CC ) |
153 |
152
|
sqcld |
|- ( ph -> ( Y ^ 2 ) e. CC ) |
154 |
150 153
|
mulcld |
|- ( ph -> ( P x. ( Y ^ 2 ) ) e. CC ) |
155 |
130 148 154
|
addassd |
|- ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) ) + ( P x. ( Y ^ 2 ) ) ) = ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) ) ) |
156 |
126 155
|
eqtrd |
|- ( ph -> ( ( Y ^ 4 ) + ( P x. ( Y ^ 2 ) ) ) = ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) ) ) |
157 |
156
|
oveq1d |
|- ( ph -> ( ( ( Y ^ 4 ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) ) + ( ( Q x. Y ) + R ) ) ) |
158 |
148 154
|
addcld |
|- ( ph -> ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) e. CC ) |
159 |
149
|
simp2d |
|- ( ph -> Q e. CC ) |
160 |
159 152
|
mulcld |
|- ( ph -> ( Q x. Y ) e. CC ) |
161 |
149
|
simp3d |
|- ( ph -> R e. CC ) |
162 |
160 161
|
addcld |
|- ( ph -> ( ( Q x. Y ) + R ) e. CC ) |
163 |
130 158 162
|
addassd |
|- ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) ) ) |
164 |
9
|
oveq1d |
|- ( ph -> ( Y ^ 2 ) = ( ( X + ( A / 4 ) ) ^ 2 ) ) |
165 |
|
binom2 |
|- ( ( X e. CC /\ ( A / 4 ) e. CC ) -> ( ( X + ( A / 4 ) ) ^ 2 ) = ( ( ( X ^ 2 ) + ( 2 x. ( X x. ( A / 4 ) ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) |
166 |
8 15 165
|
syl2anc |
|- ( ph -> ( ( X + ( A / 4 ) ) ^ 2 ) = ( ( ( X ^ 2 ) + ( 2 x. ( X x. ( A / 4 ) ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) |
167 |
8 15
|
mulcld |
|- ( ph -> ( X x. ( A / 4 ) ) e. CC ) |
168 |
|
mulcl |
|- ( ( 2 e. CC /\ ( X x. ( A / 4 ) ) e. CC ) -> ( 2 x. ( X x. ( A / 4 ) ) ) e. CC ) |
169 |
34 167 168
|
sylancr |
|- ( ph -> ( 2 x. ( X x. ( A / 4 ) ) ) e. CC ) |
170 |
31 169 30
|
addassd |
|- ( ph -> ( ( ( X ^ 2 ) + ( 2 x. ( X x. ( A / 4 ) ) ) ) + ( ( A / 4 ) ^ 2 ) ) = ( ( X ^ 2 ) + ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) |
171 |
164 166 170
|
3eqtrd |
|- ( ph -> ( Y ^ 2 ) = ( ( X ^ 2 ) + ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) |
172 |
171
|
oveq2d |
|- ( ph -> ( P x. ( Y ^ 2 ) ) = ( P x. ( ( X ^ 2 ) + ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) |
173 |
169 30
|
addcld |
|- ( ph -> ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) e. CC ) |
174 |
150 31 173
|
adddid |
|- ( ph -> ( P x. ( ( X ^ 2 ) + ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) = ( ( P x. ( X ^ 2 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) |
175 |
172 174
|
eqtrd |
|- ( ph -> ( P x. ( Y ^ 2 ) ) = ( ( P x. ( X ^ 2 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) |
176 |
175
|
oveq2d |
|- ( ph -> ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) = ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( ( P x. ( X ^ 2 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) ) |
177 |
150 31
|
mulcld |
|- ( ph -> ( P x. ( X ^ 2 ) ) e. CC ) |
178 |
150 173
|
mulcld |
|- ( ph -> ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) e. CC ) |
179 |
133 147 177 178
|
add4d |
|- ( ph -> ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( ( P x. ( X ^ 2 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) = ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( P x. ( X ^ 2 ) ) ) + ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) ) |
180 |
132 150 31
|
adddird |
|- ( ph -> ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) + P ) x. ( X ^ 2 ) ) = ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( P x. ( X ^ 2 ) ) ) ) |
181 |
5
|
oveq2d |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) + P ) = ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) + ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) ) |
182 |
132 2
|
pncan3d |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) + ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) = B ) |
183 |
181 182
|
eqtrd |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) + P ) = B ) |
184 |
183
|
oveq1d |
|- ( ph -> ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) + P ) x. ( X ^ 2 ) ) = ( B x. ( X ^ 2 ) ) ) |
185 |
180 184
|
eqtr3d |
|- ( ph -> ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( P x. ( X ^ 2 ) ) ) = ( B x. ( X ^ 2 ) ) ) |
186 |
185
|
oveq1d |
|- ( ph -> ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( P x. ( X ^ 2 ) ) ) + ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) = ( ( B x. ( X ^ 2 ) ) + ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) ) |
187 |
176 179 186
|
3eqtrd |
|- ( ph -> ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) = ( ( B x. ( X ^ 2 ) ) + ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) ) |
188 |
187
|
oveq1d |
|- ( ph -> ( ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( ( B x. ( X ^ 2 ) ) + ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) + ( ( Q x. Y ) + R ) ) ) |
189 |
2 31
|
mulcld |
|- ( ph -> ( B x. ( X ^ 2 ) ) e. CC ) |
190 |
147 178
|
addcld |
|- ( ph -> ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) e. CC ) |
191 |
189 190 162
|
addassd |
|- ( ph -> ( ( ( B x. ( X ^ 2 ) ) + ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( B x. ( X ^ 2 ) ) + ( ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) + ( ( Q x. Y ) + R ) ) ) ) |
192 |
1 2
|
mulcld |
|- ( ph -> ( A x. B ) e. CC ) |
193 |
192
|
halfcld |
|- ( ph -> ( ( A x. B ) / 2 ) e. CC ) |
194 |
193 134
|
subcld |
|- ( ph -> ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) e. CC ) |
195 |
194 8
|
mulcld |
|- ( ph -> ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) e. CC ) |
196 |
150 30
|
mulcld |
|- ( ph -> ( P x. ( ( A / 4 ) ^ 2 ) ) e. CC ) |
197 |
146 196
|
addcld |
|- ( ph -> ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) e. CC ) |
198 |
159 8
|
mulcld |
|- ( ph -> ( Q x. X ) e. CC ) |
199 |
159 15
|
mulcld |
|- ( ph -> ( Q x. ( A / 4 ) ) e. CC ) |
200 |
199 161
|
addcld |
|- ( ph -> ( ( Q x. ( A / 4 ) ) + R ) e. CC ) |
201 |
195 197 198 200
|
add4d |
|- ( ph -> ( ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) + ( ( Q x. X ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) = ( ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( Q x. X ) ) + ( ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) ) |
202 |
150 169 30
|
adddid |
|- ( ph -> ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) = ( ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) |
203 |
202
|
oveq2d |
|- ( ph -> ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) = ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) ) |
204 |
150 169
|
mulcld |
|- ( ph -> ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) e. CC ) |
205 |
136 146 204 196
|
add4d |
|- ( ph -> ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) = ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) ) + ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) ) |
206 |
1 95 95 98 98
|
divdiv1d |
|- ( ph -> ( ( A / 2 ) / 2 ) = ( A / ( 2 x. 2 ) ) ) |
207 |
|
2t2e4 |
|- ( 2 x. 2 ) = 4 |
208 |
207
|
oveq2i |
|- ( A / ( 2 x. 2 ) ) = ( A / 4 ) |
209 |
206 208
|
eqtrdi |
|- ( ph -> ( ( A / 2 ) / 2 ) = ( A / 4 ) ) |
210 |
209
|
oveq2d |
|- ( ph -> ( 2 x. ( ( A / 2 ) / 2 ) ) = ( 2 x. ( A / 4 ) ) ) |
211 |
1
|
halfcld |
|- ( ph -> ( A / 2 ) e. CC ) |
212 |
211 95 98
|
divcan2d |
|- ( ph -> ( 2 x. ( ( A / 2 ) / 2 ) ) = ( A / 2 ) ) |
213 |
210 212
|
eqtr3d |
|- ( ph -> ( 2 x. ( A / 4 ) ) = ( A / 2 ) ) |
214 |
213
|
oveq2d |
|- ( ph -> ( X x. ( 2 x. ( A / 4 ) ) ) = ( X x. ( A / 2 ) ) ) |
215 |
8 211
|
mulcomd |
|- ( ph -> ( X x. ( A / 2 ) ) = ( ( A / 2 ) x. X ) ) |
216 |
214 215
|
eqtrd |
|- ( ph -> ( X x. ( 2 x. ( A / 4 ) ) ) = ( ( A / 2 ) x. X ) ) |
217 |
216
|
oveq2d |
|- ( ph -> ( P x. ( X x. ( 2 x. ( A / 4 ) ) ) ) = ( P x. ( ( A / 2 ) x. X ) ) ) |
218 |
95 8 15
|
mul12d |
|- ( ph -> ( 2 x. ( X x. ( A / 4 ) ) ) = ( X x. ( 2 x. ( A / 4 ) ) ) ) |
219 |
218
|
oveq2d |
|- ( ph -> ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) = ( P x. ( X x. ( 2 x. ( A / 4 ) ) ) ) ) |
220 |
150 211 8
|
mulassd |
|- ( ph -> ( ( P x. ( A / 2 ) ) x. X ) = ( P x. ( ( A / 2 ) x. X ) ) ) |
221 |
217 219 220
|
3eqtr4d |
|- ( ph -> ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) = ( ( P x. ( A / 2 ) ) x. X ) ) |
222 |
221
|
oveq2d |
|- ( ph -> ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) ) = ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( P x. ( A / 2 ) ) x. X ) ) ) |
223 |
150 211
|
mulcld |
|- ( ph -> ( P x. ( A / 2 ) ) e. CC ) |
224 |
135 223 8
|
adddird |
|- ( ph -> ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( P x. ( A / 2 ) ) ) x. X ) = ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( P x. ( A / 2 ) ) x. X ) ) ) |
225 |
5
|
oveq1d |
|- ( ph -> ( P x. ( A / 2 ) ) = ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( A / 2 ) ) ) |
226 |
2 132 211
|
subdird |
|- ( ph -> ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( A / 2 ) ) = ( ( B x. ( A / 2 ) ) - ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( A / 2 ) ) ) ) |
227 |
2 1 95 98
|
divassd |
|- ( ph -> ( ( B x. A ) / 2 ) = ( B x. ( A / 2 ) ) ) |
228 |
2 1
|
mulcomd |
|- ( ph -> ( B x. A ) = ( A x. B ) ) |
229 |
228
|
oveq1d |
|- ( ph -> ( ( B x. A ) / 2 ) = ( ( A x. B ) / 2 ) ) |
230 |
227 229
|
eqtr3d |
|- ( ph -> ( B x. ( A / 2 ) ) = ( ( A x. B ) / 2 ) ) |
231 |
78
|
oveq2i |
|- ( A ^ 3 ) = ( A ^ ( 2 + 1 ) ) |
232 |
|
expp1 |
|- ( ( A e. CC /\ 2 e. NN0 ) -> ( A ^ ( 2 + 1 ) ) = ( ( A ^ 2 ) x. A ) ) |
233 |
1 80 232
|
sylancl |
|- ( ph -> ( A ^ ( 2 + 1 ) ) = ( ( A ^ 2 ) x. A ) ) |
234 |
231 233
|
syl5eq |
|- ( ph -> ( A ^ 3 ) = ( ( A ^ 2 ) x. A ) ) |
235 |
234
|
oveq2d |
|- ( ph -> ( ( 3 / 8 ) x. ( A ^ 3 ) ) = ( ( 3 / 8 ) x. ( ( A ^ 2 ) x. A ) ) ) |
236 |
33
|
a1i |
|- ( ph -> 3 e. CC ) |
237 |
236 89 94 96
|
div23d |
|- ( ph -> ( ( 3 x. ( A ^ 3 ) ) / 8 ) = ( ( 3 / 8 ) x. ( A ^ 3 ) ) ) |
238 |
58
|
a1i |
|- ( ph -> ( 3 / 8 ) e. CC ) |
239 |
238 49 1
|
mulassd |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. A ) = ( ( 3 / 8 ) x. ( ( A ^ 2 ) x. A ) ) ) |
240 |
235 237 239
|
3eqtr4rd |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. A ) = ( ( 3 x. ( A ^ 3 ) ) / 8 ) ) |
241 |
236 89 94 96
|
divassd |
|- ( ph -> ( ( 3 x. ( A ^ 3 ) ) / 8 ) = ( 3 x. ( ( A ^ 3 ) / 8 ) ) ) |
242 |
240 241
|
eqtrd |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. A ) = ( 3 x. ( ( A ^ 3 ) / 8 ) ) ) |
243 |
242
|
oveq1d |
|- ( ph -> ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. A ) / 2 ) = ( ( 3 x. ( ( A ^ 3 ) / 8 ) ) / 2 ) ) |
244 |
132 1 95 98
|
divassd |
|- ( ph -> ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. A ) / 2 ) = ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( A / 2 ) ) ) |
245 |
236 134 95 98
|
divassd |
|- ( ph -> ( ( 3 x. ( ( A ^ 3 ) / 8 ) ) / 2 ) = ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) |
246 |
243 244 245
|
3eqtr3d |
|- ( ph -> ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( A / 2 ) ) = ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) |
247 |
230 246
|
oveq12d |
|- ( ph -> ( ( B x. ( A / 2 ) ) - ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( A / 2 ) ) ) = ( ( ( A x. B ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) |
248 |
225 226 247
|
3eqtrd |
|- ( ph -> ( P x. ( A / 2 ) ) = ( ( ( A x. B ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) |
249 |
248
|
oveq2d |
|- ( ph -> ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( P x. ( A / 2 ) ) ) = ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( ( ( A x. B ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) ) |
250 |
|
mulcl |
|- ( ( 3 e. CC /\ ( ( ( A ^ 3 ) / 8 ) / 2 ) e. CC ) -> ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) e. CC ) |
251 |
33 135 250
|
sylancr |
|- ( ph -> ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) e. CC ) |
252 |
135 193 251
|
addsub12d |
|- ( ph -> ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( ( ( A x. B ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) = ( ( ( A x. B ) / 2 ) + ( ( ( ( A ^ 3 ) / 8 ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) ) |
253 |
193 251 135
|
subsub2d |
|- ( ph -> ( ( ( A x. B ) / 2 ) - ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) = ( ( ( A x. B ) / 2 ) + ( ( ( ( A ^ 3 ) / 8 ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) ) |
254 |
135
|
mulid2d |
|- ( ph -> ( 1 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) = ( ( ( A ^ 3 ) / 8 ) / 2 ) ) |
255 |
254
|
oveq2d |
|- ( ph -> ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( 1 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) = ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) |
256 |
|
3m1e2 |
|- ( 3 - 1 ) = 2 |
257 |
256
|
oveq1i |
|- ( ( 3 - 1 ) x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) = ( 2 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) |
258 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
259 |
236 258 135
|
subdird |
|- ( ph -> ( ( 3 - 1 ) x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) = ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( 1 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) |
260 |
134 95 98
|
divcan2d |
|- ( ph -> ( 2 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) = ( ( A ^ 3 ) / 8 ) ) |
261 |
257 259 260
|
3eqtr3a |
|- ( ph -> ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( 1 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) = ( ( A ^ 3 ) / 8 ) ) |
262 |
255 261
|
eqtr3d |
|- ( ph -> ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( ( ( A ^ 3 ) / 8 ) / 2 ) ) = ( ( A ^ 3 ) / 8 ) ) |
263 |
262
|
oveq2d |
|- ( ph -> ( ( ( A x. B ) / 2 ) - ( ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) - ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) = ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) |
264 |
252 253 263
|
3eqtr2d |
|- ( ph -> ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( ( ( A x. B ) / 2 ) - ( 3 x. ( ( ( A ^ 3 ) / 8 ) / 2 ) ) ) ) = ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) |
265 |
249 264
|
eqtrd |
|- ( ph -> ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( P x. ( A / 2 ) ) ) = ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) |
266 |
265
|
oveq1d |
|- ( ph -> ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) + ( P x. ( A / 2 ) ) ) x. X ) = ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) ) |
267 |
222 224 266
|
3eqtr2d |
|- ( ph -> ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) ) = ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) ) |
268 |
267
|
oveq1d |
|- ( ph -> ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( P x. ( 2 x. ( X x. ( A / 4 ) ) ) ) ) + ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) = ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) ) |
269 |
203 205 268
|
3eqtrd |
|- ( ph -> ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) = ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) ) |
270 |
9
|
oveq2d |
|- ( ph -> ( Q x. Y ) = ( Q x. ( X + ( A / 4 ) ) ) ) |
271 |
159 8 15
|
adddid |
|- ( ph -> ( Q x. ( X + ( A / 4 ) ) ) = ( ( Q x. X ) + ( Q x. ( A / 4 ) ) ) ) |
272 |
270 271
|
eqtrd |
|- ( ph -> ( Q x. Y ) = ( ( Q x. X ) + ( Q x. ( A / 4 ) ) ) ) |
273 |
272
|
oveq1d |
|- ( ph -> ( ( Q x. Y ) + R ) = ( ( ( Q x. X ) + ( Q x. ( A / 4 ) ) ) + R ) ) |
274 |
198 199 161
|
addassd |
|- ( ph -> ( ( ( Q x. X ) + ( Q x. ( A / 4 ) ) ) + R ) = ( ( Q x. X ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) |
275 |
273 274
|
eqtrd |
|- ( ph -> ( ( Q x. Y ) + R ) = ( ( Q x. X ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) |
276 |
269 275
|
oveq12d |
|- ( ph -> ( ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) ) + ( ( Q x. X ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) ) |
277 |
194 159
|
addcomd |
|- ( ph -> ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) + Q ) = ( Q + ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) ) |
278 |
6
|
oveq1d |
|- ( ph -> ( Q + ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) = ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) + ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) ) |
279 |
3 193
|
subcld |
|- ( ph -> ( C - ( ( A x. B ) / 2 ) ) e. CC ) |
280 |
279 134 193
|
ppncand |
|- ( ph -> ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) + ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A x. B ) / 2 ) ) ) |
281 |
3 193
|
npcand |
|- ( ph -> ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A x. B ) / 2 ) ) = C ) |
282 |
280 281
|
eqtrd |
|- ( ph -> ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) + ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) ) = C ) |
283 |
277 278 282
|
3eqtrd |
|- ( ph -> ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) + Q ) = C ) |
284 |
283
|
oveq1d |
|- ( ph -> ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) + Q ) x. X ) = ( C x. X ) ) |
285 |
194 159 8
|
adddird |
|- ( ph -> ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) + Q ) x. X ) = ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( Q x. X ) ) ) |
286 |
284 285
|
eqtr3d |
|- ( ph -> ( C x. X ) = ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( Q x. X ) ) ) |
287 |
1 2 3 4 5 6 7 8 9
|
quart1lem |
|- ( ph -> D = ( ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) |
288 |
286 287
|
oveq12d |
|- ( ph -> ( ( C x. X ) + D ) = ( ( ( ( ( ( A x. B ) / 2 ) - ( ( A ^ 3 ) / 8 ) ) x. X ) + ( Q x. X ) ) + ( ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( Q x. ( A / 4 ) ) + R ) ) ) ) |
289 |
201 276 288
|
3eqtr4d |
|- ( ph -> ( ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( C x. X ) + D ) ) |
290 |
289
|
oveq2d |
|- ( ph -> ( ( B x. ( X ^ 2 ) ) + ( ( ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) + ( P x. ( ( 2 x. ( X x. ( A / 4 ) ) ) + ( ( A / 4 ) ^ 2 ) ) ) ) + ( ( Q x. Y ) + R ) ) ) = ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) |
291 |
188 191 290
|
3eqtrd |
|- ( ph -> ( ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) = ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) |
292 |
291
|
oveq2d |
|- ( ph -> ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( ( ( ( ( 3 / 8 ) x. ( A ^ 2 ) ) x. ( X ^ 2 ) ) + ( ( ( ( ( A ^ 3 ) / 8 ) / 2 ) x. X ) + ( ( A ^ 4 ) / ; ; 2 5 6 ) ) ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) ) = ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) ) |
293 |
157 163 292
|
3eqtrrd |
|- ( ph -> ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = ( ( ( Y ^ 4 ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) ) |