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 25911

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 7270	. . . . . 6 ⊢ (𝜑 → (𝑌↑4) = ((𝑋 + (𝐴 / 4))↑4))
3		quart1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
4		quart1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		4cn 11988	. . . . . . . . 9 ⊢ 4 ∈ ℂ
6	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
7		4ne0 12011	. . . . . . . . 9 ⊢ 4 ≠ 0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ≠ 0)
9	4, 6, 8	divcld 11681	. . . . . . 7 ⊢ (𝜑 → (𝐴 / 4) ∈ ℂ)
10		binom4 25905	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
11	3, 9, 10	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
12		3nn0 12181	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
13		expcl 13728	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
14	3, 12, 13	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
15	6, 14, 9	mul12d 11114	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = ((𝑋↑3) · (4 · (𝐴 / 4))))
16	4, 6, 8	divcan2d 11683	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝐴 / 4)) = 𝐴)
17	16	oveq2d 7271	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · (4 · (𝐴 / 4))) = ((𝑋↑3) · 𝐴))
18	14, 4	mulcomd 10927	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · 𝐴) = (𝐴 · (𝑋↑3)))
19	15, 17, 18	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = (𝐴 · (𝑋↑3)))
20	19	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) = ((𝑋↑4) + (𝐴 · (𝑋↑3))))
21		6nn 11992	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
22	21	nncni 11913	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
24	9	sqcld 13790	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑2) ∈ ℂ)
25	3	sqcld 13790	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
26	23, 24, 25	mulassd 10929	. . . . . . . . 9 ⊢ (𝜑 → ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
27		3cn 11984	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
28		2cn 11978	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
29		3t2e6 12069	. . . . . . . . . . . . . . . 16 ⊢ (3 · 2) = 6
30	27, 28, 29	mulcomli 10915	. . . . . . . . . . . . . . 15 ⊢ (2 · 3) = 6
31		8cn 12000	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℂ
32		8t2e16 12481	. . . . . . . . . . . . . . . 16 ⊢ (8 · 2) = ;16
33	31, 28, 32	mulcomli 10915	. . . . . . . . . . . . . . 15 ⊢ (2 · 8) = ;16
34	30, 33	oveq12i 7267	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (6 / ;16)
35		8nn 11998	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℕ
36	35	nnne0i 11943	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
37	31, 36	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℂ ∧ 8 ≠ 0)
38		2cnne0 12113	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
39		divcan5 11607	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 8)) = (3 / 8))
40	27, 37, 38, 39	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (3 / 8)
41	34, 40	eqtr3i 2768	. . . . . . . . . . . . 13 ⊢ (6 / ;16) = (3 / 8)
42	41	oveq2i 7266	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) · (6 / ;16)) = ((𝐴↑2) · (3 / 8))
43	4	sqcld 13790	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
44		1nn0 12179	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
45	44, 21	decnncl 12386	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℕ
46	45	nncni 11913	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℂ
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ∈ ℂ)
48	45	nnne0i 11943	. . . . . . . . . . . . . 14 ⊢ ;16 ≠ 0
49	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ≠ 0)
50	43, 23, 47, 49	div12d 11717	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴↑2) · (6 / ;16)) = (6 · ((𝐴↑2) / ;16)))
51	42, 50	eqtr3id 2793	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑2) · (3 / 8)) = (6 · ((𝐴↑2) / ;16)))
52	27, 31, 36	divcli 11647	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
53		mulcom 10888	. . . . . . . . . . . 12 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
54	52, 43, 53	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
55	4, 6, 8	sqdivd 13805	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2)))
56	5	sqvali 13825	. . . . . . . . . . . . . . 15 ⊢ (4↑2) = (4 · 4)
57		4t4e16 12465	. . . . . . . . . . . . . . 15 ⊢ (4 · 4) = ;16
58	56, 57	eqtri 2766	. . . . . . . . . . . . . 14 ⊢ (4↑2) = ;16
59	58	oveq2i 7266	. . . . . . . . . . . . 13 ⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16)
60	55, 59	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16))
61	60	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → (6 · ((𝐴 / 4)↑2)) = (6 · ((𝐴↑2) / ;16)))
62	51, 54, 61	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = (6 · ((𝐴 / 4)↑2)))
63	62	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) = ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)))
64	25, 24	mulcomd 10927	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋↑2) · ((𝐴 / 4)↑2)) = (((𝐴 / 4)↑2) · (𝑋↑2)))
65	64	oveq2d 7271	. . . . . . . . 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 13728	. . . . . . . . . . . 12 ⊢ (((𝐴 / 4) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 / 4)↑3) ∈ ℂ)
68	9, 12, 67	sylancl 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / 4)↑3) ∈ ℂ)
69	6, 3, 68	mul12d 11114	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = (𝑋 · (4 · ((𝐴 / 4)↑3))))
70	6, 68	mulcld 10926	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) ∈ ℂ)
71	3, 70	mulcomd 10927	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 · (4 · ((𝐴 / 4)↑3))) = ((4 · ((𝐴 / 4)↑3)) · 𝑋))
72		df-3 11967	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
73	72	oveq2i 7266	. . . . . . . . . . . . . . . 16 ⊢ (4↑3) = (4↑(2 + 1))
74		2nn0 12180	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
75		expp1 13717	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℕ₀) → (4↑(2 + 1)) = ((4↑2) · 4))
76	5, 74, 75	mp2an 688	. . . . . . . . . . . . . . . 16 ⊢ (4↑(2 + 1)) = ((4↑2) · 4)
77	58	oveq1i 7265	. . . . . . . . . . . . . . . 16 ⊢ ((4↑2) · 4) = (;16 · 4)
78	73, 76, 77	3eqtri 2770	. . . . . . . . . . . . . . 15 ⊢ (4↑3) = (;16 · 4)
79	78	oveq2i 7266	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑3) / (4↑3)) = ((𝐴↑3) / (;16 · 4))
80	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ ℕ₀)
81	4, 6, 8, 80	expdivd 13806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 / 4)↑3) = ((𝐴↑3) / (4↑3)))
82		expcl 13728	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
83	4, 12, 82	sylancl 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴↑3) ∈ ℂ)
84	83, 47, 6, 49, 8	divdiv1d 11712	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴↑3) / ;16) / 4) = ((𝐴↑3) / (;16 · 4)))
85	79, 81, 84	3eqtr4a 2805	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑3) = (((𝐴↑3) / ;16) / 4))
86	85	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (4 · (((𝐴↑3) / ;16) / 4)))
87	32	oveq2i 7266	. . . . . . . . . . . . 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 12007	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
92	91	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
93	83, 88, 89, 90, 92	divdiv1d 11712	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = ((𝐴↑3) / (8 · 2)))
94	83, 47, 49	divcld 11681	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴↑3) / ;16) ∈ ℂ)
95	94, 6, 8	divcan2d 11683	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · (((𝐴↑3) / ;16) / 4)) = ((𝐴↑3) / ;16))
96	87, 93, 95	3eqtr4a 2805	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = (4 · (((𝐴↑3) / ;16) / 4)))
97	86, 96	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (((𝐴↑3) / 8) / 2))
98	97	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · ((𝐴 / 4)↑3)) · 𝑋) = ((((𝐴↑3) / 8) / 2) · 𝑋))
99	69, 71, 98	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = ((((𝐴↑3) / 8) / 2) · 𝑋))
100		4nn0 12182	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℕ₀)
102	4, 6, 8, 101	expdivd 13806	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / (4↑4)))
103		expmul 13756	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) → (2↑(2 · 4)) = ((2↑2)↑4))
104	28, 74, 100, 103	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = ((2↑2)↑4)
105		4t2e8 12071	. . . . . . . . . . . . . . . 16 ⊢ (4 · 2) = 8
106	5, 28, 105	mulcomli 10915	. . . . . . . . . . . . . . 15 ⊢ (2 · 4) = 8
107	106	oveq2i 7266	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = (2↑8)
108	104, 107	eqtr3i 2768	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (2↑8)
109		sq2 13842	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
110	109	oveq1i 7265	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (4↑4)
111	108, 110	eqtr3i 2768	. . . . . . . . . . . 12 ⊢ (2↑8) = (4↑4)
112		2exp8 16718	. . . . . . . . . . . 12 ⊢ (2↑8) = ;;256
113	111, 112	eqtr3i 2768	. . . . . . . . . . 11 ⊢ (4↑4) = ;;256
114	113	oveq2i 7266	. . . . . . . . . 10 ⊢ ((𝐴↑4) / (4↑4)) = ((𝐴↑4) / ;;256)
115	102, 114	eqtrdi 2795	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / ;;256))
116	99, 115	oveq12d 7273	. . . . . . . 8 ⊢ (𝜑 → ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))
117	66, 116	oveq12d 7273	. . . . . . 7 ⊢ (𝜑 → ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4))) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))))
118	20, 117	oveq12d 7273	. . . . . 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 7270	. . . 4 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))) + (𝑃 · (𝑌↑2))))
121		expcl 13728	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝑋↑4) ∈ ℂ)
122	3, 100, 121	sylancl 585	. . . . . 6 ⊢ (𝜑 → (𝑋↑4) ∈ ℂ)
123	4, 14	mulcld 10926	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑3)) ∈ ℂ)
124	122, 123	addcld 10925	. . . . 5 ⊢ (𝜑 → ((𝑋↑4) + (𝐴 · (𝑋↑3))) ∈ ℂ)
125		mulcl 10886	. . . . . . . 8 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
126	52, 43, 125	sylancr 586	. . . . . . 7 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
127	126, 25	mulcld 10926	. . . . . 6 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) ∈ ℂ)
128	83, 88, 90	divcld 11681	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑3) / 8) ∈ ℂ)
129	128	halfcld 12148	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) ∈ ℂ)
130	129, 3	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) · 𝑋) ∈ ℂ)
131		expcl 13728	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
132	4, 100, 131	sylancl 585	. . . . . . . 8 ⊢ (𝜑 → (𝐴↑4) ∈ ℂ)
133		5nn0 12183	. . . . . . . . . . . 12 ⊢ 5 ∈ ℕ₀
134	74, 133	deccl 12381	. . . . . . . . . . 11 ⊢ ;25 ∈ ℕ₀
135	134, 21	decnncl 12386	. . . . . . . . . 10 ⊢ ;;256 ∈ ℕ
136	135	nncni 11913	. . . . . . . . 9 ⊢ ;;256 ∈ ℂ
137	136	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ∈ ℂ)
138	135	nnne0i 11943	. . . . . . . . 9 ⊢ ;;256 ≠ 0
139	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ≠ 0)
140	132, 137, 139	divcld 11681	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑4) / ;;256) ∈ ℂ)
141	130, 140	addcld 10925	. . . . . 6 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) ∈ ℂ)
142	127, 141	addcld 10925	. . . . 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 25909	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
150	149	simp1d 1140	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℂ)
151	3, 9	addcld 10925	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝐴 / 4)) ∈ ℂ)
152	1, 151	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
153	152	sqcld 13790	. . . . . 6 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
154	150, 153	mulcld 10926	. . . . 5 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) ∈ ℂ)
155	124, 142, 154	addassd 10928	. . . 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 7270	. 2 ⊢ (𝜑 → (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))) + ((𝑄 · 𝑌) + 𝑅)))
158	142, 154	addcld 10925	. . 3 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) ∈ ℂ)
159	149	simp2d 1141	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℂ)
160	159, 152	mulcld 10926	. . . 4 ⊢ (𝜑 → (𝑄 · 𝑌) ∈ ℂ)
161	149	simp3d 1142	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ℂ)
162	160, 161	addcld 10925	. . 3 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) ∈ ℂ)
163	124, 158, 162	addassd 10928	. 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 7270	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌↑2) = ((𝑋 + (𝐴 / 4))↑2))
165		binom2 13861	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
166	3, 9, 165	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
167	3, 9	mulcld 10926	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐴 / 4)) ∈ ℂ)
168		mulcl 10886	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ (𝑋 · (𝐴 / 4)) ∈ ℂ) → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
169	28, 167, 168	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
170	25, 169, 24	addassd 10928	. . . . . . . . . 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 7271	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
173	169, 24	addcld 10925	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)) ∈ ℂ)
174	150, 25, 173	adddid 10930	. . . . . . . 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 7271	. . . . . 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 10926	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑋↑2)) ∈ ℂ)
178	150, 173	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) ∈ ℂ)
179	127, 141, 177, 178	add4d 11133	. . . . . 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 10931	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))))
181	146	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))))
182	126, 143	pncan3d 11265	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))) = 𝐵)
183	181, 182	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = 𝐵)
184	183	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = (𝐵 · (𝑋↑2)))
185	180, 184	eqtr3d 2780	. . . . . . 7 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) = (𝐵 · (𝑋↑2)))
186	185	oveq1d 7270	. . . . . 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 7270	. . . 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 10926	. . . . 5 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
190	141, 178	addcld 10925	. . . . 5 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) ∈ ℂ)
191	189, 190, 162	addassd 10928	. . . 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 10926	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
193	192	halfcld 12148	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ)
194	193, 128	subcld 11262	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) ∈ ℂ)
195	194, 3	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) ∈ ℂ)
196	150, 24	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈ ℂ)
197	140, 196	addcld 10925	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) ∈ ℂ)
198	159, 3	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
199	159, 9	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) ∈ ℂ)
200	199, 161	addcld 10925	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) ∈ ℂ)
201	195, 197, 198, 200	add4d 11133	. . . . . 6 ⊢ (𝜑 → ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
202	150, 169, 24	adddid 10930	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) = ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2))))
203	202	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))))
204	150, 169	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) ∈ ℂ)
205	130, 140, 204, 196	add4d 11133	. . . . . . . 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 11712	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / (2 · 2)))
207		2t2e4 12067	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
208	207	oveq2i 7266	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (2 · 2)) = (𝐴 / 4)
209	206, 208	eqtrdi 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / 4))
210	209	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (2 · (𝐴 / 4)))
211	4	halfcld 12148	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)
212	211, 89, 92	divcan2d 11683	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (𝐴 / 2))
213	210, 212	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝐴 / 4)) = (𝐴 / 2))
214	213	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = (𝑋 · (𝐴 / 2)))
215	3, 211	mulcomd 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (𝐴 / 2)) = ((𝐴 / 2) · 𝑋))
216	214, 215	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = ((𝐴 / 2) · 𝑋))
217	216	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (𝑋 · (2 · (𝐴 / 4)))) = (𝑃 · ((𝐴 / 2) · 𝑋)))
218	89, 3, 9	mul12d 11114	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) = (𝑋 · (2 · (𝐴 / 4))))
219	218	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = (𝑃 · (𝑋 · (2 · (𝐴 / 4)))))
220	150, 211, 3	mulassd 10929	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃 · (𝐴 / 2)) · 𝑋) = (𝑃 · ((𝐴 / 2) · 𝑋)))
221	217, 219, 220	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = ((𝑃 · (𝐴 / 2)) · 𝑋))
222	221	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
223	150, 211	mulcld 10926	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) ∈ ℂ)
224	129, 223, 3	adddird 10931	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
225	146	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)))
226	143, 126, 211	subdird 11362	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)) = ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))))
227	143, 4, 89, 92	divassd 11716	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = (𝐵 · (𝐴 / 2)))
228	143, 4	mulcomd 10927	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 · 𝐴) = (𝐴 · 𝐵))
229	228	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = ((𝐴 · 𝐵) / 2))
230	227, 229	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 · (𝐴 / 2)) = ((𝐴 · 𝐵) / 2))
231	72	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
232		expp1 13717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
233	4, 74, 232	sylancl 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
234	231, 233	syl5eq 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴↑3) = ((𝐴↑2) · 𝐴))
235	234	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 / 8) · (𝐴↑3)) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
236	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 3 ∈ ℂ)
237	236, 83, 88, 90	div23d 11718	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = ((3 / 8) · (𝐴↑3)))
238	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (3 / 8) ∈ ℂ)
239	238, 43, 4	mulassd 10929	. . . . . . . . . . . . . . . . . . 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 11716	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = (3 · ((𝐴↑3) / 8)))
242	240, 241	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = (3 · ((𝐴↑3) / 8)))
243	242	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = ((3 · ((𝐴↑3) / 8)) / 2))
244	126, 4, 89, 92	divassd 11716	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)))
245	236, 128, 89, 92	divassd 11716	. . . . . . . . . . . . . . . 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 7273	. . . . . . . . . . . . . 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 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
250		mulcl 10886	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (((𝐴↑3) / 8) / 2) ∈ ℂ) → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
251	27, 129, 250	sylancr 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
252	129, 193, 251	addsub12d 11285	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
253	193, 251, 129	subsub2d 11291	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
254	129	mulid2d 10924	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (((𝐴↑3) / 8) / 2)) = (((𝐴↑3) / 8) / 2))
255	254	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)))
256		3m1e2 12031	. . . . . . . . . . . . . . . . 17 ⊢ (3 − 1) = 2
257	256	oveq1i 7265	. . . . . . . . . . . . . . . 16 ⊢ ((3 − 1) · (((𝐴↑3) / 8) / 2)) = (2 · (((𝐴↑3) / 8) / 2))
258		1cnd 10901	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
259	236, 258, 129	subdird 11362	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 − 1) · (((𝐴↑3) / 8) / 2)) = ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))))
260	128, 89, 92	divcan2d 11683	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
261	257, 259, 260	3eqtr3a 2803	. . . . . . . . . . . . . . 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 7271	. . . . . . . . . . . . 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 7270	. . . . . . . . . 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 7270	. . . . . . . 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 7271	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · 𝑌) = (𝑄 · (𝑋 + (𝐴 / 4))))
271	159, 3, 9	adddid 10930	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · (𝑋 + (𝐴 / 4))) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
272	270, 271	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 · 𝑌) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
273	272	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅))
274	198, 199, 161	addassd 10928	. . . . . . . 8 ⊢ (𝜑 → (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
275	273, 274	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
276	269, 275	oveq12d 7273	. . . . . 6 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
277	194, 159	addcomd 11107	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
278	147	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
279	144, 193	subcld 11262	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ)
280	279, 128, 193	ppncand 11302	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)))
281	144, 193	npcand 11266	. . . . . . . . . . 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 7270	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (𝐶 · 𝑋))
285	194, 159, 3	adddird 10931	. . . . . . . 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 25910	. . . . . . 7 ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
288	286, 287	oveq12d 7273	. . . . . 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 7271	. . . 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 7271	. 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 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 (class class class)co 7255 ℂcc 10800 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 − cmin 11135 / cdiv 11562 2c2 11958 3c3 11959 4c4 11960 5c5 11961 6c6 11962 8c8 11964 ℕ₀cn0 12163 cdc 12366 ↑cexp 13710

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-seq 13650 df-exp 13711

This theorem is referenced by: quart 25916

W3C validator