Metamath Proof Explorer

Theorem quart1

Description: Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quart1.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
quart1.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
quart1.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
quart1.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
quart1.p ⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
quart1.q ⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
quart1.r ⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 1 6 ) − ( ( 3 / 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
quart1.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
quart1.y ⊢ ( 𝜑 → 𝑌 = ( 𝑋 + ( 𝐴 / 4 ) ) )
Assertion quart1 ( 𝜑 → ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) = ( ( ( 𝑌 ↑ 4 ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) )

Proof

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