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 4t2e8 ⊢ ( 4 · 2 ) = 8
111 11 35 110 mulcomli ⊢ ( 2 · 4 ) = 8
112 111 oveq2i ⊢ ( 2 ↑ ( 2 · 4 ) ) = ( 2 ↑ 8 )
113 109 112 eqtr3i ⊢ ( ( 2 ↑ 2 ) ↑ 4 ) = ( 2 ↑ 8 )
114 sq2 ⊢ ( 2 ↑ 2 ) = 4
115 114 oveq1i ⊢ ( ( 2 ↑ 2 ) ↑ 4 ) = ( 4 ↑ 4 )
116 113 115 eqtr3i ⊢ ( 2 ↑ 8 ) = ( 4 ↑ 4 )
117 2exp8 ⊢ ( 2 ↑ 8 ) = 2 5 6
118 116 117 eqtr3i ⊢ ( 4 ↑ 4 ) = 2 5 6
119 118 oveq2i ⊢ ( ( 𝐴 ↑ 4 ) / ( 4 ↑ 4 ) ) = ( ( 𝐴 ↑ 4 ) / 2 5 6 )
120 107 119 eqtrdi ⊢ ( 𝜑 → ( ( 𝐴 / 4 ) ↑ 4 ) = ( ( 𝐴 ↑ 4 ) / 2 5 6 ) )
121 104 120 oveq12d ⊢ ( 𝜑 → ( ( 4 · ( 𝑋 · ( ( 𝐴 / 4 ) ↑ 3 ) ) ) + ( ( 𝐴 / 4 ) ↑ 4 ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) )
122 71 121 oveq12d ⊢ ( 𝜑 → ( ( 6 · ( ( 𝑋 ↑ 2 ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 4 · ( 𝑋 · ( ( 𝐴 / 4 ) ↑ 3 ) ) ) + ( ( 𝐴 / 4 ) ↑ 4 ) ) ) = ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) )
123 26 122 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 ) ) ) ) )
124 10 17 123 3eqtrd ⊢ ( 𝜑 → ( 𝑌 ↑ 4 ) = ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) ) )
125 124 oveq1d ⊢ ( 𝜑 → ( ( 𝑌 ↑ 4 ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) = ( ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) )
126 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝑋 ↑ 4 ) ∈ ℂ )
127 8 105 126 sylancl ⊢ ( 𝜑 → ( 𝑋 ↑ 4 ) ∈ ℂ )
128 1 20 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 ↑ 3 ) ) ∈ ℂ )
129 127 128 addcld ⊢ ( 𝜑 → ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) ∈ ℂ )
130 mulcl ⊢ ( ( ( 3 / 8 ) ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
131 57 48 130 sylancr ⊢ ( 𝜑 → ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
132 131 31 mulcld ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
133 88 93 95 divcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 3 ) / 8 ) ∈ ℂ )
134 133 halfcld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ∈ ℂ )
135 134 8 mulcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) ∈ ℂ )
136 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝐴 ↑ 4 ) ∈ ℂ )
137 1 105 136 sylancl ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℂ )
138 5nn0 ⊢ 5 ∈ ℕ0
139 79 138 deccl ⊢ 2 5 ∈ ℕ0
140 139 27 decnncl ⊢ 2 5 6 ∈ ℕ
141 140 nncni ⊢ 2 5 6 ∈ ℂ
142 141 a1i ⊢ ( 𝜑 → 2 5 6 ∈ ℂ )
143 140 nnne0i ⊢ 2 5 6 ≠ 0
144 143 a1i ⊢ ( 𝜑 → 2 5 6 ≠ 0 )
145 137 142 144 divcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ∈ ℂ )
146 135 145 addcld ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ∈ ℂ )
147 132 146 addcld ⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) ∈ ℂ )
148 1 2 3 4 5 6 7 quart1cl ⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
149 148 simp1d ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
150 8 15 addcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝐴 / 4 ) ) ∈ ℂ )
151 9 150 eqeltrd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
152 151 sqcld ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℂ )
153 149 152 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( 𝑌 ↑ 2 ) ) ∈ ℂ )
154 129 147 153 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 ) ) ) ) )
155 125 154 eqtrd ⊢ ( 𝜑 → ( ( 𝑌 ↑ 4 ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) ) )
156 155 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 4 ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) = ( ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) )
157 147 153 addcld ⊢ ( 𝜑 → ( ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) ∈ ℂ )
158 148 simp2d ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
159 158 151 mulcld ⊢ ( 𝜑 → ( 𝑄 · 𝑌 ) ∈ ℂ )
160 148 simp3d ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
161 159 160 addcld ⊢ ( 𝜑 → ( ( 𝑄 · 𝑌 ) + 𝑅 ) ∈ ℂ )
162 129 157 161 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 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) ) )
163 9 oveq1d ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) = ( ( 𝑋 + ( 𝐴 / 4 ) ) ↑ 2 ) )
164 binom2 ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝐴 / 4 ) ∈ ℂ ) → ( ( 𝑋 + ( 𝐴 / 4 ) ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) )
165 8 15 164 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐴 / 4 ) ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) )
166 8 15 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( 𝐴 / 4 ) ) ∈ ℂ )
167 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑋 · ( 𝐴 / 4 ) ) ∈ ℂ ) → ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ∈ ℂ )
168 35 166 167 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ∈ ℂ )
169 31 168 30 addassd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
170 163 165 169 3eqtrd ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) = ( ( 𝑋 ↑ 2 ) + ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
171 170 oveq2d ⊢ ( 𝜑 → ( 𝑃 · ( 𝑌 ↑ 2 ) ) = ( 𝑃 · ( ( 𝑋 ↑ 2 ) + ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
172 168 30 addcld ⊢ ( 𝜑 → ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ∈ ℂ )
173 149 31 172 adddid ⊢ ( 𝜑 → ( 𝑃 · ( ( 𝑋 ↑ 2 ) + ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) = ( ( 𝑃 · ( 𝑋 ↑ 2 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
174 171 173 eqtrd ⊢ ( 𝜑 → ( 𝑃 · ( 𝑌 ↑ 2 ) ) = ( ( 𝑃 · ( 𝑋 ↑ 2 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
175 174 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 ) ) ) ) ) )
176 149 31 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
177 149 172 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ∈ ℂ )
178 132 146 176 177 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 ) ) ) ) ) )
179 131 149 31 adddird ⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) + 𝑃 ) · ( 𝑋 ↑ 2 ) ) = ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( 𝑃 · ( 𝑋 ↑ 2 ) ) ) )
180 5 oveq2d ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) + 𝑃 ) = ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) + ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) ) )
181 131 2 pncan3d ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) + ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) ) = 𝐵 )
182 180 181 eqtrd ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) + 𝑃 ) = 𝐵 )
183 182 oveq1d ⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) + 𝑃 ) · ( 𝑋 ↑ 2 ) ) = ( 𝐵 · ( 𝑋 ↑ 2 ) ) )
184 179 183 eqtr3d ⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( 𝑃 · ( 𝑋 ↑ 2 ) ) ) = ( 𝐵 · ( 𝑋 ↑ 2 ) ) )
185 184 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 ) ) ) ) ) )
186 175 178 185 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 ) ) ) ) ) )
187 186 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 ) ) ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) )
188 2 31 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
189 146 177 addcld ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) ∈ ℂ )
190 188 189 161 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 ) ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) ) )
191 1 2 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
192 191 halfcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) / 2 ) ∈ ℂ )
193 192 133 subcld ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) ∈ ℂ )
194 193 8 mulcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) ∈ ℂ )
195 149 30 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ∈ ℂ )
196 145 195 addcld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ∈ ℂ )
197 158 8 mulcld ⊢ ( 𝜑 → ( 𝑄 · 𝑋 ) ∈ ℂ )
198 158 15 mulcld ⊢ ( 𝜑 → ( 𝑄 · ( 𝐴 / 4 ) ) ∈ ℂ )
199 198 160 addcld ⊢ ( 𝜑 → ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ∈ ℂ )
200 194 196 197 199 add4d ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) + ( ( 𝑄 · 𝑋 ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) ) = ( ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( 𝑄 · 𝑋 ) ) + ( ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) ) )
201 149 168 30 adddid ⊢ ( 𝜑 → ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) = ( ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
202 201 oveq2d ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
203 149 168 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) ∈ ℂ )
204 135 145 203 195 add4d ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) ) + ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
205 1 94 94 97 97 divdiv1d ⊢ ( 𝜑 → ( ( 𝐴 / 2 ) / 2 ) = ( 𝐴 / ( 2 · 2 ) ) )
206 2t2e4 ⊢ ( 2 · 2 ) = 4
207 206 oveq2i ⊢ ( 𝐴 / ( 2 · 2 ) ) = ( 𝐴 / 4 )
208 205 207 eqtrdi ⊢ ( 𝜑 → ( ( 𝐴 / 2 ) / 2 ) = ( 𝐴 / 4 ) )
209 208 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 / 2 ) / 2 ) ) = ( 2 · ( 𝐴 / 4 ) ) )
210 1 halfcld ⊢ ( 𝜑 → ( 𝐴 / 2 ) ∈ ℂ )
211 210 94 97 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 / 2 ) / 2 ) ) = ( 𝐴 / 2 ) )
212 209 211 eqtr3d ⊢ ( 𝜑 → ( 2 · ( 𝐴 / 4 ) ) = ( 𝐴 / 2 ) )
213 212 oveq2d ⊢ ( 𝜑 → ( 𝑋 · ( 2 · ( 𝐴 / 4 ) ) ) = ( 𝑋 · ( 𝐴 / 2 ) ) )
214 8 210 mulcomd ⊢ ( 𝜑 → ( 𝑋 · ( 𝐴 / 2 ) ) = ( ( 𝐴 / 2 ) · 𝑋 ) )
215 213 214 eqtrd ⊢ ( 𝜑 → ( 𝑋 · ( 2 · ( 𝐴 / 4 ) ) ) = ( ( 𝐴 / 2 ) · 𝑋 ) )
216 215 oveq2d ⊢ ( 𝜑 → ( 𝑃 · ( 𝑋 · ( 2 · ( 𝐴 / 4 ) ) ) ) = ( 𝑃 · ( ( 𝐴 / 2 ) · 𝑋 ) ) )
217 94 8 15 mul12d ⊢ ( 𝜑 → ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) = ( 𝑋 · ( 2 · ( 𝐴 / 4 ) ) ) )
218 217 oveq2d ⊢ ( 𝜑 → ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) = ( 𝑃 · ( 𝑋 · ( 2 · ( 𝐴 / 4 ) ) ) ) )
219 149 210 8 mulassd ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝐴 / 2 ) ) · 𝑋 ) = ( 𝑃 · ( ( 𝐴 / 2 ) · 𝑋 ) ) )
220 216 218 219 3eqtr4d ⊢ ( 𝜑 → ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) = ( ( 𝑃 · ( 𝐴 / 2 ) ) · 𝑋 ) )
221 220 oveq2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝑃 · ( 𝐴 / 2 ) ) · 𝑋 ) ) )
222 149 210 mulcld ⊢ ( 𝜑 → ( 𝑃 · ( 𝐴 / 2 ) ) ∈ ℂ )
223 134 222 8 adddird ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( 𝑃 · ( 𝐴 / 2 ) ) ) · 𝑋 ) = ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝑃 · ( 𝐴 / 2 ) ) · 𝑋 ) ) )
224 5 oveq1d ⊢ ( 𝜑 → ( 𝑃 · ( 𝐴 / 2 ) ) = ( ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) · ( 𝐴 / 2 ) ) )
225 2 131 210 subdird ⊢ ( 𝜑 → ( ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) · ( 𝐴 / 2 ) ) = ( ( 𝐵 · ( 𝐴 / 2 ) ) − ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 / 2 ) ) ) )
226 2 1 94 97 divassd ⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) / 2 ) = ( 𝐵 · ( 𝐴 / 2 ) ) )
227 2 1 mulcomd ⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
228 227 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) / 2 ) = ( ( 𝐴 · 𝐵 ) / 2 ) )
229 226 228 eqtr3d ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 / 2 ) ) = ( ( 𝐴 · 𝐵 ) / 2 ) )
230 77 oveq2i ⊢ ( 𝐴 ↑ 3 ) = ( 𝐴 ↑ ( 2 + 1 ) )
231 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝐴 ↑ ( 2 + 1 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
232 1 79 231 sylancl ⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 + 1 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
233 230 232 eqtrid ⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
234 233 oveq2d ⊢ ( 𝜑 → ( ( 3 / 8 ) · ( 𝐴 ↑ 3 ) ) = ( ( 3 / 8 ) · ( ( 𝐴 ↑ 2 ) · 𝐴 ) ) )
235 39 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
236 235 88 93 95 div23d ⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 3 ) ) / 8 ) = ( ( 3 / 8 ) · ( 𝐴 ↑ 3 ) ) )
237 57 a1i ⊢ ( 𝜑 → ( 3 / 8 ) ∈ ℂ )
238 237 48 1 mulassd ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · 𝐴 ) = ( ( 3 / 8 ) · ( ( 𝐴 ↑ 2 ) · 𝐴 ) ) )
239 234 236 238 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · 𝐴 ) = ( ( 3 · ( 𝐴 ↑ 3 ) ) / 8 ) )
240 235 88 93 95 divassd ⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 3 ) ) / 8 ) = ( 3 · ( ( 𝐴 ↑ 3 ) / 8 ) ) )
241 239 240 eqtrd ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · 𝐴 ) = ( 3 · ( ( 𝐴 ↑ 3 ) / 8 ) ) )
242 241 oveq1d ⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · 𝐴 ) / 2 ) = ( ( 3 · ( ( 𝐴 ↑ 3 ) / 8 ) ) / 2 ) )
243 131 1 94 97 divassd ⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · 𝐴 ) / 2 ) = ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 / 2 ) ) )
244 235 133 94 97 divassd ⊢ ( 𝜑 → ( ( 3 · ( ( 𝐴 ↑ 3 ) / 8 ) ) / 2 ) = ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) )
245 242 243 244 3eqtr3d ⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 / 2 ) ) = ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) )
246 229 245 oveq12d ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 / 2 ) ) − ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 / 2 ) ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) )
247 224 225 246 3eqtrd ⊢ ( 𝜑 → ( 𝑃 · ( 𝐴 / 2 ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) )
248 247 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( 𝑃 · ( 𝐴 / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) ) )
249 mulcl ⊢ ( ( 3 ∈ ℂ ∧ ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ∈ ℂ ) → ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ∈ ℂ )
250 39 134 249 sylancr ⊢ ( 𝜑 → ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ∈ ℂ )
251 134 192 250 addsub12d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) + ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) ) )
252 192 250 134 subsub2d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) + ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) ) )
253 134 mullidd ⊢ ( 𝜑 → ( 1 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) = ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) )
254 253 oveq2d ⊢ ( 𝜑 → ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( 1 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) = ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) )
255 3m1e2 ⊢ ( 3 − 1 ) = 2
256 255 oveq1i ⊢ ( ( 3 − 1 ) · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) = ( 2 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) )
257 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
258 235 257 134 subdird ⊢ ( 𝜑 → ( ( 3 − 1 ) · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) = ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( 1 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) )
259 133 94 97 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) = ( ( 𝐴 ↑ 3 ) / 8 ) )
260 256 258 259 3eqtr3a ⊢ ( 𝜑 → ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( 1 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) = ( ( 𝐴 ↑ 3 ) / 8 ) )
261 254 260 eqtr3d ⊢ ( 𝜑 → ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) = ( ( 𝐴 ↑ 3 ) / 8 ) )
262 261 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) − ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) )
263 251 252 262 3eqtr2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( 3 · ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) ) ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) )
264 248 263 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( 𝑃 · ( 𝐴 / 2 ) ) ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) )
265 264 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) + ( 𝑃 · ( 𝐴 / 2 ) ) ) · 𝑋 ) = ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) )
266 221 223 265 3eqtr2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) ) = ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) )
267 266 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( 𝑃 · ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) ) ) + ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) = ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
268 202 204 267 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) = ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
269 9 oveq2d ⊢ ( 𝜑 → ( 𝑄 · 𝑌 ) = ( 𝑄 · ( 𝑋 + ( 𝐴 / 4 ) ) ) )
270 158 8 15 adddid ⊢ ( 𝜑 → ( 𝑄 · ( 𝑋 + ( 𝐴 / 4 ) ) ) = ( ( 𝑄 · 𝑋 ) + ( 𝑄 · ( 𝐴 / 4 ) ) ) )
271 269 270 eqtrd ⊢ ( 𝜑 → ( 𝑄 · 𝑌 ) = ( ( 𝑄 · 𝑋 ) + ( 𝑄 · ( 𝐴 / 4 ) ) ) )
272 271 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 · 𝑌 ) + 𝑅 ) = ( ( ( 𝑄 · 𝑋 ) + ( 𝑄 · ( 𝐴 / 4 ) ) ) + 𝑅 ) )
273 197 198 160 addassd ⊢ ( 𝜑 → ( ( ( 𝑄 · 𝑋 ) + ( 𝑄 · ( 𝐴 / 4 ) ) ) + 𝑅 ) = ( ( 𝑄 · 𝑋 ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) )
274 272 273 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 · 𝑌 ) + 𝑅 ) = ( ( 𝑄 · 𝑋 ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) )
275 268 274 oveq12d ⊢ ( 𝜑 → ( ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) = ( ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) + ( ( 𝑄 · 𝑋 ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) ) )
276 193 158 addcomd ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) + 𝑄 ) = ( 𝑄 + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) ) )
277 6 oveq1d ⊢ ( 𝜑 → ( 𝑄 + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) ) = ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) ) )
278 3 192 subcld ⊢ ( 𝜑 → ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) ∈ ℂ )
279 278 133 192 ppncand ⊢ ( 𝜑 → ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) ) = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 · 𝐵 ) / 2 ) ) )
280 3 192 npcand ⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 · 𝐵 ) / 2 ) ) = 𝐶 )
281 279 280 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) + ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) ) = 𝐶 )
282 276 277 281 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) + 𝑄 ) = 𝐶 )
283 282 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) + 𝑄 ) · 𝑋 ) = ( 𝐶 · 𝑋 ) )
284 193 158 8 adddird ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) + 𝑄 ) · 𝑋 ) = ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( 𝑄 · 𝑋 ) ) )
285 283 284 eqtr3d ⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) = ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( 𝑄 · 𝑋 ) ) )
286 1 2 3 4 5 6 7 8 9 quart1lem ⊢ ( 𝜑 → 𝐷 = ( ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) )
287 285 286 oveq12d ⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) + 𝐷 ) = ( ( ( ( ( ( 𝐴 · 𝐵 ) / 2 ) − ( ( 𝐴 ↑ 3 ) / 8 ) ) · 𝑋 ) + ( 𝑄 · 𝑋 ) ) + ( ( ( ( 𝐴 ↑ 4 ) / 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) ) )
288 200 275 287 3eqtr4d ⊢ ( 𝜑 → ( ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
289 288 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) + ( 𝑃 · ( ( 2 · ( 𝑋 · ( 𝐴 / 4 ) ) ) + ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) ) = ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
290 187 190 289 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) = ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
291 290 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( ( ( 𝐴 ↑ 3 ) / 8 ) / 2 ) · 𝑋 ) + ( ( 𝐴 ↑ 4 ) / 2 5 6 ) ) ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) ) = ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) )
292 156 162 291 3eqtrrd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) = ( ( ( 𝑌 ↑ 4 ) + ( 𝑃 · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) )