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 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 eqtrid ⊢ ( 𝜑 → ( 𝐴 ↑ 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 mullidd ⊢ ( 𝜑 → ( 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 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) )