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 ) ) ) + ( ( 𝑄 · 𝑌 ) + 𝑅 ) ) )