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