quart1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > quart1		Structured version Visualization version GIF version

Theorem quart1 26006

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

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

**Assertion**
Ref	Expression
quart1	⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))

**Proof of Theorem quart1**
Step	Hyp	Ref	Expression
1		quart1.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4)))
2	1	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → (𝑌↑4) = ((𝑋 + (𝐴 / 4))↑4))
3		quart1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
4		quart1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		4cn 12058	. . . . . . . . 9 ⊢ 4 ∈ ℂ
6	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
7		4ne0 12081	. . . . . . . . 9 ⊢ 4 ≠ 0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ≠ 0)
9	4, 6, 8	divcld 11751	. . . . . . 7 ⊢ (𝜑 → (𝐴 / 4) ∈ ℂ)
10		binom4 26000	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
11	3, 9, 10	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
12		3nn0 12251	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
13		expcl 13800	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
14	3, 12, 13	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
15	6, 14, 9	mul12d 11184	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = ((𝑋↑3) · (4 · (𝐴 / 4))))
16	4, 6, 8	divcan2d 11753	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝐴 / 4)) = 𝐴)
17	16	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · (4 · (𝐴 / 4))) = ((𝑋↑3) · 𝐴))
18	14, 4	mulcomd 10996	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · 𝐴) = (𝐴 · (𝑋↑3)))
19	15, 17, 18	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = (𝐴 · (𝑋↑3)))
20	19	oveq2d 7291	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) = ((𝑋↑4) + (𝐴 · (𝑋↑3))))
21		6nn 12062	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
22	21	nncni 11983	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
24	9	sqcld 13862	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑2) ∈ ℂ)
25	3	sqcld 13862	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
26	23, 24, 25	mulassd 10998	. . . . . . . . 9 ⊢ (𝜑 → ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
27		3cn 12054	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
28		2cn 12048	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
29		3t2e6 12139	. . . . . . . . . . . . . . . 16 ⊢ (3 · 2) = 6
30	27, 28, 29	mulcomli 10984	. . . . . . . . . . . . . . 15 ⊢ (2 · 3) = 6
31		8cn 12070	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℂ
32		8t2e16 12552	. . . . . . . . . . . . . . . 16 ⊢ (8 · 2) = ;16
33	31, 28, 32	mulcomli 10984	. . . . . . . . . . . . . . 15 ⊢ (2 · 8) = ;16
34	30, 33	oveq12i 7287	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (6 / ;16)
35		8nn 12068	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℕ
36	35	nnne0i 12013	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
37	31, 36	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℂ ∧ 8 ≠ 0)
38		2cnne0 12183	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
39		divcan5 11677	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 8)) = (3 / 8))
40	27, 37, 38, 39	mp3an 1460	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (3 / 8)
41	34, 40	eqtr3i 2768	. . . . . . . . . . . . 13 ⊢ (6 / ;16) = (3 / 8)
42	41	oveq2i 7286	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) · (6 / ;16)) = ((𝐴↑2) · (3 / 8))
43	4	sqcld 13862	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
44		1nn0 12249	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
45	44, 21	decnncl 12457	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℕ
46	45	nncni 11983	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℂ
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ∈ ℂ)
48	45	nnne0i 12013	. . . . . . . . . . . . . 14 ⊢ ;16 ≠ 0
49	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ≠ 0)
50	43, 23, 47, 49	div12d 11787	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴↑2) · (6 / ;16)) = (6 · ((𝐴↑2) / ;16)))
51	42, 50	eqtr3id 2792	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑2) · (3 / 8)) = (6 · ((𝐴↑2) / ;16)))
52	27, 31, 36	divcli 11717	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
53		mulcom 10957	. . . . . . . . . . . 12 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
54	52, 43, 53	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
55	4, 6, 8	sqdivd 13877	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2)))
56	5	sqvali 13897	. . . . . . . . . . . . . . 15 ⊢ (4↑2) = (4 · 4)
57		4t4e16 12536	. . . . . . . . . . . . . . 15 ⊢ (4 · 4) = ;16
58	56, 57	eqtri 2766	. . . . . . . . . . . . . 14 ⊢ (4↑2) = ;16
59	58	oveq2i 7286	. . . . . . . . . . . . 13 ⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16)
60	55, 59	eqtrdi 2794	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16))
61	60	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝜑 → (6 · ((𝐴 / 4)↑2)) = (6 · ((𝐴↑2) / ;16)))
62	51, 54, 61	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = (6 · ((𝐴 / 4)↑2)))
63	62	oveq1d 7290	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) = ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)))
64	25, 24	mulcomd 10996	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋↑2) · ((𝐴 / 4)↑2)) = (((𝐴 / 4)↑2) · (𝑋↑2)))
65	64	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
66	26, 63, 65	3eqtr4rd 2789	. . . . . . . 8 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (((3 / 8) · (𝐴↑2)) · (𝑋↑2)))
67		expcl 13800	. . . . . . . . . . . 12 ⊢ (((𝐴 / 4) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 / 4)↑3) ∈ ℂ)
68	9, 12, 67	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / 4)↑3) ∈ ℂ)
69	6, 3, 68	mul12d 11184	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = (𝑋 · (4 · ((𝐴 / 4)↑3))))
70	6, 68	mulcld 10995	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) ∈ ℂ)
71	3, 70	mulcomd 10996	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 · (4 · ((𝐴 / 4)↑3))) = ((4 · ((𝐴 / 4)↑3)) · 𝑋))
72		df-3 12037	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
73	72	oveq2i 7286	. . . . . . . . . . . . . . . 16 ⊢ (4↑3) = (4↑(2 + 1))
74		2nn0 12250	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
75		expp1 13789	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℕ₀) → (4↑(2 + 1)) = ((4↑2) · 4))
76	5, 74, 75	mp2an 689	. . . . . . . . . . . . . . . 16 ⊢ (4↑(2 + 1)) = ((4↑2) · 4)
77	58	oveq1i 7285	. . . . . . . . . . . . . . . 16 ⊢ ((4↑2) · 4) = (;16 · 4)
78	73, 76, 77	3eqtri 2770	. . . . . . . . . . . . . . 15 ⊢ (4↑3) = (;16 · 4)
79	78	oveq2i 7286	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑3) / (4↑3)) = ((𝐴↑3) / (;16 · 4))
80	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ ℕ₀)
81	4, 6, 8, 80	expdivd 13878	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 / 4)↑3) = ((𝐴↑3) / (4↑3)))
82		expcl 13800	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
83	4, 12, 82	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴↑3) ∈ ℂ)
84	83, 47, 6, 49, 8	divdiv1d 11782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴↑3) / ;16) / 4) = ((𝐴↑3) / (;16 · 4)))
85	79, 81, 84	3eqtr4a 2804	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑3) = (((𝐴↑3) / ;16) / 4))
86	85	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (4 · (((𝐴↑3) / ;16) / 4)))
87	32	oveq2i 7286	. . . . . . . . . . . . 13 ⊢ ((𝐴↑3) / (8 · 2)) = ((𝐴↑3) / ;16)
88	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 8 ∈ ℂ)
89	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℂ)
90	36	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 8 ≠ 0)
91		2ne0 12077	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
92	91	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
93	83, 88, 89, 90, 92	divdiv1d 11782	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = ((𝐴↑3) / (8 · 2)))
94	83, 47, 49	divcld 11751	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴↑3) / ;16) ∈ ℂ)
95	94, 6, 8	divcan2d 11753	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · (((𝐴↑3) / ;16) / 4)) = ((𝐴↑3) / ;16))
96	87, 93, 95	3eqtr4a 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = (4 · (((𝐴↑3) / ;16) / 4)))
97	86, 96	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (((𝐴↑3) / 8) / 2))
98	97	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · ((𝐴 / 4)↑3)) · 𝑋) = ((((𝐴↑3) / 8) / 2) · 𝑋))
99	69, 71, 98	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = ((((𝐴↑3) / 8) / 2) · 𝑋))
100		4nn0 12252	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℕ₀)
102	4, 6, 8, 101	expdivd 13878	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / (4↑4)))
103		expmul 13828	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) → (2↑(2 · 4)) = ((2↑2)↑4))
104	28, 74, 100, 103	mp3an 1460	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = ((2↑2)↑4)
105		4t2e8 12141	. . . . . . . . . . . . . . . 16 ⊢ (4 · 2) = 8
106	5, 28, 105	mulcomli 10984	. . . . . . . . . . . . . . 15 ⊢ (2 · 4) = 8
107	106	oveq2i 7286	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = (2↑8)
108	104, 107	eqtr3i 2768	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (2↑8)
109		sq2 13914	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
110	109	oveq1i 7285	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (4↑4)
111	108, 110	eqtr3i 2768	. . . . . . . . . . . 12 ⊢ (2↑8) = (4↑4)
112		2exp8 16790	. . . . . . . . . . . 12 ⊢ (2↑8) = ;;256
113	111, 112	eqtr3i 2768	. . . . . . . . . . 11 ⊢ (4↑4) = ;;256
114	113	oveq2i 7286	. . . . . . . . . 10 ⊢ ((𝐴↑4) / (4↑4)) = ((𝐴↑4) / ;;256)
115	102, 114	eqtrdi 2794	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / ;;256))
116	99, 115	oveq12d 7293	. . . . . . . 8 ⊢ (𝜑 → ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))
117	66, 116	oveq12d 7293	. . . . . . 7 ⊢ (𝜑 → ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4))) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))))
118	20, 117	oveq12d 7293	. . . . . 6 ⊢ (𝜑 → (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))))
119	2, 11, 118	3eqtrd 2782	. . . . 5 ⊢ (𝜑 → (𝑌↑4) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))))
120	119	oveq1d 7290	. . . 4 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))) + (𝑃 · (𝑌↑2))))
121		expcl 13800	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝑋↑4) ∈ ℂ)
122	3, 100, 121	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑋↑4) ∈ ℂ)
123	4, 14	mulcld 10995	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑3)) ∈ ℂ)
124	122, 123	addcld 10994	. . . . 5 ⊢ (𝜑 → ((𝑋↑4) + (𝐴 · (𝑋↑3))) ∈ ℂ)
125		mulcl 10955	. . . . . . . 8 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
126	52, 43, 125	sylancr 587	. . . . . . 7 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
127	126, 25	mulcld 10995	. . . . . 6 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) ∈ ℂ)
128	83, 88, 90	divcld 11751	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑3) / 8) ∈ ℂ)
129	128	halfcld 12218	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) ∈ ℂ)
130	129, 3	mulcld 10995	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) · 𝑋) ∈ ℂ)
131		expcl 13800	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
132	4, 100, 131	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝐴↑4) ∈ ℂ)
133		5nn0 12253	. . . . . . . . . . . 12 ⊢ 5 ∈ ℕ₀
134	74, 133	deccl 12452	. . . . . . . . . . 11 ⊢ ;25 ∈ ℕ₀
135	134, 21	decnncl 12457	. . . . . . . . . 10 ⊢ ;;256 ∈ ℕ
136	135	nncni 11983	. . . . . . . . 9 ⊢ ;;256 ∈ ℂ
137	136	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ∈ ℂ)
138	135	nnne0i 12013	. . . . . . . . 9 ⊢ ;;256 ≠ 0
139	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ≠ 0)
140	132, 137, 139	divcld 11751	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑4) / ;;256) ∈ ℂ)
141	130, 140	addcld 10994	. . . . . 6 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) ∈ ℂ)
142	127, 141	addcld 10994	. . . . 5 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) ∈ ℂ)
143		quart1.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℂ)
144		quart1.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
145		quart1.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
146		quart1.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))
147		quart1.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))
148		quart1.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
149	4, 143, 144, 145, 146, 147, 148	quart1cl 26004	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
150	149	simp1d 1141	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℂ)
151	3, 9	addcld 10994	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝐴 / 4)) ∈ ℂ)
152	1, 151	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
153	152	sqcld 13862	. . . . . 6 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
154	150, 153	mulcld 10995	. . . . 5 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) ∈ ℂ)
155	124, 142, 154	addassd 10997	. . . 4 ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))) + (𝑃 · (𝑌↑2))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))))
156	120, 155	eqtrd 2778	. . 3 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))))
157	156	oveq1d 7290	. 2 ⊢ (𝜑 → (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))) + ((𝑄 · 𝑌) + 𝑅)))
158	142, 154	addcld 10994	. . 3 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) ∈ ℂ)
159	149	simp2d 1142	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℂ)
160	159, 152	mulcld 10995	. . . 4 ⊢ (𝜑 → (𝑄 · 𝑌) ∈ ℂ)
161	149	simp3d 1143	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ℂ)
162	160, 161	addcld 10994	. . 3 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) ∈ ℂ)
163	124, 158, 162	addassd 10997	. 2 ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅))))
164	1	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌↑2) = ((𝑋 + (𝐴 / 4))↑2))
165		binom2 13933	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
166	3, 9, 165	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
167	3, 9	mulcld 10995	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐴 / 4)) ∈ ℂ)
168		mulcl 10955	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ (𝑋 · (𝐴 / 4)) ∈ ℂ) → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
169	28, 167, 168	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
170	25, 169, 24	addassd 10997	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
171	164, 166, 170	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝜑 → (𝑌↑2) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
172	171	oveq2d 7291	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
173	169, 24	addcld 10994	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)) ∈ ℂ)
174	150, 25, 173	adddid 10999	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
175	172, 174	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
176	175	oveq2d 7291	. . . . . 6 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) = (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
177	150, 25	mulcld 10995	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑋↑2)) ∈ ℂ)
178	150, 173	mulcld 10995	. . . . . . 7 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) ∈ ℂ)
179	127, 141, 177, 178	add4d 11203	. . . . . 6 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) = (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
180	126, 150, 25	adddird 11000	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))))
181	146	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))))
182	126, 143	pncan3d 11335	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))) = 𝐵)
183	181, 182	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = 𝐵)
184	183	oveq1d 7290	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = (𝐵 · (𝑋↑2)))
185	180, 184	eqtr3d 2780	. . . . . . 7 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) = (𝐵 · (𝑋↑2)))
186	185	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) = ((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
187	176, 179, 186	3eqtrd 2782	. . . . 5 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) = ((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
188	187	oveq1d 7290	. . . 4 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = (((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) + ((𝑄 · 𝑌) + 𝑅)))
189	143, 25	mulcld 10995	. . . . 5 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
190	141, 178	addcld 10994	. . . . 5 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) ∈ ℂ)
191	189, 190, 162	addassd 10997	. . . 4 ⊢ (𝜑 → (((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))))
192	4, 143	mulcld 10995	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
193	192	halfcld 12218	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ)
194	193, 128	subcld 11332	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) ∈ ℂ)
195	194, 3	mulcld 10995	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) ∈ ℂ)
196	150, 24	mulcld 10995	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈ ℂ)
197	140, 196	addcld 10994	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) ∈ ℂ)
198	159, 3	mulcld 10995	. . . . . . 7 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
199	159, 9	mulcld 10995	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) ∈ ℂ)
200	199, 161	addcld 10994	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) ∈ ℂ)
201	195, 197, 198, 200	add4d 11203	. . . . . 6 ⊢ (𝜑 → ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
202	150, 169, 24	adddid 10999	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) = ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2))))
203	202	oveq2d 7291	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))))
204	150, 169	mulcld 10995	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) ∈ ℂ)
205	130, 140, 204, 196	add4d 11203	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
206	4, 89, 89, 92, 92	divdiv1d 11782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / (2 · 2)))
207		2t2e4 12137	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
208	207	oveq2i 7286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (2 · 2)) = (𝐴 / 4)
209	206, 208	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / 4))
210	209	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (2 · (𝐴 / 4)))
211	4	halfcld 12218	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)
212	211, 89, 92	divcan2d 11753	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (𝐴 / 2))
213	210, 212	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝐴 / 4)) = (𝐴 / 2))
214	213	oveq2d 7291	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = (𝑋 · (𝐴 / 2)))
215	3, 211	mulcomd 10996	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (𝐴 / 2)) = ((𝐴 / 2) · 𝑋))
216	214, 215	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = ((𝐴 / 2) · 𝑋))
217	216	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (𝑋 · (2 · (𝐴 / 4)))) = (𝑃 · ((𝐴 / 2) · 𝑋)))
218	89, 3, 9	mul12d 11184	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) = (𝑋 · (2 · (𝐴 / 4))))
219	218	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = (𝑃 · (𝑋 · (2 · (𝐴 / 4)))))
220	150, 211, 3	mulassd 10998	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃 · (𝐴 / 2)) · 𝑋) = (𝑃 · ((𝐴 / 2) · 𝑋)))
221	217, 219, 220	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = ((𝑃 · (𝐴 / 2)) · 𝑋))
222	221	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
223	150, 211	mulcld 10995	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) ∈ ℂ)
224	129, 223, 3	adddird 11000	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
225	146	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)))
226	143, 126, 211	subdird 11432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)) = ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))))
227	143, 4, 89, 92	divassd 11786	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = (𝐵 · (𝐴 / 2)))
228	143, 4	mulcomd 10996	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 · 𝐴) = (𝐴 · 𝐵))
229	228	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = ((𝐴 · 𝐵) / 2))
230	227, 229	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 · (𝐴 / 2)) = ((𝐴 · 𝐵) / 2))
231	72	oveq2i 7286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
232		expp1 13789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
233	4, 74, 232	sylancl 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
234	231, 233	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴↑3) = ((𝐴↑2) · 𝐴))
235	234	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 / 8) · (𝐴↑3)) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
236	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 3 ∈ ℂ)
237	236, 83, 88, 90	div23d 11788	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = ((3 / 8) · (𝐴↑3)))
238	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (3 / 8) ∈ ℂ)
239	238, 43, 4	mulassd 10998	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
240	235, 237, 239	3eqtr4rd 2789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 · (𝐴↑3)) / 8))
241	236, 83, 88, 90	divassd 11786	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = (3 · ((𝐴↑3) / 8)))
242	240, 241	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = (3 · ((𝐴↑3) / 8)))
243	242	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = ((3 · ((𝐴↑3) / 8)) / 2))
244	126, 4, 89, 92	divassd 11786	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)))
245	236, 128, 89, 92	divassd 11786	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · ((𝐴↑3) / 8)) / 2) = (3 · (((𝐴↑3) / 8) / 2)))
246	243, 244, 245	3eqtr3d 2786	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)) = (3 · (((𝐴↑3) / 8) / 2)))
247	230, 246	oveq12d 7293	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
248	225, 226, 247	3eqtrd 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
249	248	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
250		mulcl 10955	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (((𝐴↑3) / 8) / 2) ∈ ℂ) → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
251	27, 129, 250	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
252	129, 193, 251	addsub12d 11355	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
253	193, 251, 129	subsub2d 11361	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
254	129	mulid2d 10993	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (((𝐴↑3) / 8) / 2)) = (((𝐴↑3) / 8) / 2))
255	254	oveq2d 7291	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)))
256		3m1e2 12101	. . . . . . . . . . . . . . . . 17 ⊢ (3 − 1) = 2
257	256	oveq1i 7285	. . . . . . . . . . . . . . . 16 ⊢ ((3 − 1) · (((𝐴↑3) / 8) / 2)) = (2 · (((𝐴↑3) / 8) / 2))
258		1cnd 10970	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
259	236, 258, 129	subdird 11432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 − 1) · (((𝐴↑3) / 8) / 2)) = ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))))
260	128, 89, 92	divcan2d 11753	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
261	257, 259, 260	3eqtr3a 2802	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((𝐴↑3) / 8))
262	255, 261	eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
263	262	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
264	252, 253, 263	3eqtr2d 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
265	249, 264	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
266	265	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
267	222, 224, 266	3eqtr2d 2784	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
268	267	oveq1d 7290	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
269	203, 205, 268	3eqtrd 2782	. . . . . . 7 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
270	1	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · 𝑌) = (𝑄 · (𝑋 + (𝐴 / 4))))
271	159, 3, 9	adddid 10999	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · (𝑋 + (𝐴 / 4))) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
272	270, 271	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 · 𝑌) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
273	272	oveq1d 7290	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅))
274	198, 199, 161	addassd 10997	. . . . . . . 8 ⊢ (𝜑 → (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
275	273, 274	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
276	269, 275	oveq12d 7293	. . . . . 6 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
277	194, 159	addcomd 11177	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
278	147	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
279	144, 193	subcld 11332	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ)
280	279, 128, 193	ppncand 11372	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)))
281	144, 193	npcand 11336	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)) = 𝐶)
282	280, 281	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = 𝐶)
283	277, 278, 282	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = 𝐶)
284	283	oveq1d 7290	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (𝐶 · 𝑋))
285	194, 159, 3	adddird 11000	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
286	284, 285	eqtr3d 2780	. . . . . . 7 ⊢ (𝜑 → (𝐶 · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
287	4, 143, 144, 145, 146, 147, 148, 3, 1	quart1lem 26005	. . . . . . 7 ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
288	286, 287	oveq12d 7293	. . . . . 6 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
289	201, 276, 288	3eqtr4d 2788	. . . . 5 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐶 · 𝑋) + 𝐷))
290	289	oveq2d 7291	. . . 4 ⊢ (𝜑 → ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
291	188, 191, 290	3eqtrd 2782	. . 3 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
292	291	oveq2d 7291	. 2 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))))
293	157, 163, 292	3eqtrrd 2783	1 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 (class class class)co 7275 ℂcc 10869 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 − cmin 11205 / cdiv 11632 2c2 12028 3c3 12029 4c4 12030 5c5 12031 6c6 12032 8c8 12034 ℕ₀cn0 12233 cdc 12437 ↑cexp 13782

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-seq 13722 df-exp 13783

This theorem is referenced by: quart 26011

W3C validator