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 27101

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 7432	. . . . . 6 ⊢ (𝜑 → (𝑌↑4) = ((𝑋 + (𝐴 / 4))↑4))
3		quart1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
4		quart1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		4cn 12354	. . . . . . . . 9 ⊢ 4 ∈ ℂ
6	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
7		4ne0 12380	. . . . . . . . 9 ⊢ 4 ≠ 0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ≠ 0)
9	4, 6, 8	divcld 12019	. . . . . . 7 ⊢ (𝜑 → (𝐴 / 4) ∈ ℂ)
10		binom4 27095	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
11	3, 9, 10	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
12		3nn0 12550	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
13		expcl 14147	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
14	3, 12, 13	sylancl 598	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
15	6, 14, 9	mul12d 11447	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = ((𝑋↑3) · (4 · (𝐴 / 4))))
16	4, 6, 8	divcan2d 12021	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝐴 / 4)) = 𝐴)
17	16	oveq2d 7433	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · (4 · (𝐴 / 4))) = ((𝑋↑3) · 𝐴))
18	14, 4	mulcomd 11258	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · 𝐴) = (𝐴 · (𝑋↑3)))
19	15, 17, 18	3eqtrd 2801	. . . . . . . 8 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = (𝐴 · (𝑋↑3)))
20	19	oveq2d 7433	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) = ((𝑋↑4) + (𝐴 · (𝑋↑3))))
21		6nn 12358	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
22	21	nncni 12271	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
24	9	sqcld 14212	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑2) ∈ ℂ)
25	3	sqcld 14212	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
26	23, 24, 25	mulassd 11260	. . . . . . . . 9 ⊢ (𝜑 → ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
27		2t3e6 12435	. . . . . . . . . . . . . . 15 ⊢ (2 · 3) = 6
28		8cn 12366	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℂ
29		2cn 12344	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
30		8t2e16 12860	. . . . . . . . . . . . . . . 16 ⊢ (8 · 2) = ;16
31	28, 29, 30	mulcomli 11246	. . . . . . . . . . . . . . 15 ⊢ (2 · 8) = ;16
32	27, 31	oveq12i 7429	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (6 / ;16)
33		3cn 12350	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
34		8nn 12364	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℕ
35	34	nnne0i 12304	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
36	28, 35	pm3.2i 476	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℂ ∧ 8 ≠ 0)
37		2cnne0 12481	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
38		divcan5 11945	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 8)) = (3 / 8))
39	33, 36, 37, 38	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (3 / 8)
40	32, 39	eqtr3i 2787	. . . . . . . . . . . . 13 ⊢ (6 / ;16) = (3 / 8)
41	40	oveq2i 7428	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) · (6 / ;16)) = ((𝐴↑2) · (3 / 8))
42	4	sqcld 14212	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
43		1nn0 12548	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
44	43, 21	decnncl 12764	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℕ
45	44	nncni 12271	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℂ
46	45	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ∈ ℂ)
47	44	nnne0i 12304	. . . . . . . . . . . . . 14 ⊢ ;16 ≠ 0
48	47	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ≠ 0)
49	42, 23, 46, 48	div12d 12055	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴↑2) · (6 / ;16)) = (6 · ((𝐴↑2) / ;16)))
50	41, 49	eqtr3id 2811	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑2) · (3 / 8)) = (6 · ((𝐴↑2) / ;16)))
51	33, 28, 35	divcli 11985	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
52		mulcom 11214	. . . . . . . . . . . 12 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
53	51, 42, 52	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
54	4, 6, 8	sqdivd 14227	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2)))
55	5	sqvali 14248	. . . . . . . . . . . . . . 15 ⊢ (4↑2) = (4 · 4)
56		4t4e16 12844	. . . . . . . . . . . . . . 15 ⊢ (4 · 4) = ;16
57	55, 56	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ (4↑2) = ;16
58	57	oveq2i 7428	. . . . . . . . . . . . 13 ⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16)
59	54, 58	eqtrdi 2813	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16))
60	59	oveq2d 7433	. . . . . . . . . . 11 ⊢ (𝜑 → (6 · ((𝐴 / 4)↑2)) = (6 · ((𝐴↑2) / ;16)))
61	50, 53, 60	3eqtr4d 2807	. . . . . . . . . 10 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = (6 · ((𝐴 / 4)↑2)))
62	61	oveq1d 7432	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) = ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)))
63	25, 24	mulcomd 11258	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋↑2) · ((𝐴 / 4)↑2)) = (((𝐴 / 4)↑2) · (𝑋↑2)))
64	63	oveq2d 7433	. . . . . . . . 9 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
65	26, 62, 64	3eqtr4rd 2808	. . . . . . . 8 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (((3 / 8) · (𝐴↑2)) · (𝑋↑2)))
66		expcl 14147	. . . . . . . . . . . 12 ⊢ (((𝐴 / 4) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 / 4)↑3) ∈ ℂ)
67	9, 12, 66	sylancl 598	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / 4)↑3) ∈ ℂ)
68	6, 3, 67	mul12d 11447	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = (𝑋 · (4 · ((𝐴 / 4)↑3))))
69	6, 67	mulcld 11257	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) ∈ ℂ)
70	3, 69	mulcomd 11258	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 · (4 · ((𝐴 / 4)↑3))) = ((4 · ((𝐴 / 4)↑3)) · 𝑋))
71		df-3 12332	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
72	71	oveq2i 7428	. . . . . . . . . . . . . . . 16 ⊢ (4↑3) = (4↑(2 + 1))
73		2nn0 12549	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
74		expp1 14136	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℕ₀) → (4↑(2 + 1)) = ((4↑2) · 4))
75	5, 73, 74	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (4↑(2 + 1)) = ((4↑2) · 4)
76	57	oveq1i 7427	. . . . . . . . . . . . . . . 16 ⊢ ((4↑2) · 4) = (;16 · 4)
77	72, 75, 76	3eqtri 2789	. . . . . . . . . . . . . . 15 ⊢ (4↑3) = (;16 · 4)
78	77	oveq2i 7428	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑3) / (4↑3)) = ((𝐴↑3) / (;16 · 4))
79	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ ℕ₀)
80	4, 6, 8, 79	expdivd 14228	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 / 4)↑3) = ((𝐴↑3) / (4↑3)))
81		expcl 14147	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
82	4, 12, 81	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴↑3) ∈ ℂ)
83	82, 46, 6, 48, 8	divdiv1d 12050	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴↑3) / ;16) / 4) = ((𝐴↑3) / (;16 · 4)))
84	78, 80, 83	3eqtr4a 2823	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑3) = (((𝐴↑3) / ;16) / 4))
85	84	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (4 · (((𝐴↑3) / ;16) / 4)))
86	30	oveq2i 7428	. . . . . . . . . . . . 13 ⊢ ((𝐴↑3) / (8 · 2)) = ((𝐴↑3) / ;16)
87	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 8 ∈ ℂ)
88	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℂ)
89	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 8 ≠ 0)
90		2ne0 12375	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
91	90	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
92	82, 87, 88, 89, 91	divdiv1d 12050	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = ((𝐴↑3) / (8 · 2)))
93	82, 46, 48	divcld 12019	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴↑3) / ;16) ∈ ℂ)
94	93, 6, 8	divcan2d 12021	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · (((𝐴↑3) / ;16) / 4)) = ((𝐴↑3) / ;16))
95	86, 92, 94	3eqtr4a 2823	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = (4 · (((𝐴↑3) / ;16) / 4)))
96	85, 95	eqtr4d 2800	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (((𝐴↑3) / 8) / 2))
97	96	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · ((𝐴 / 4)↑3)) · 𝑋) = ((((𝐴↑3) / 8) / 2) · 𝑋))
98	68, 70, 97	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = ((((𝐴↑3) / 8) / 2) · 𝑋))
99		4nn0 12551	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
100	99	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℕ₀)
101	4, 6, 8, 100	expdivd 14228	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / (4↑4)))
102		expmul 14175	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) → (2↑(2 · 4)) = ((2↑2)↑4))
103	29, 73, 99, 102	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = ((2↑2)↑4)
104		2t4e8 12438	. . . . . . . . . . . . . . 15 ⊢ (2 · 4) = 8
105	104	oveq2i 7428	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = (2↑8)
106	103, 105	eqtr3i 2787	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (2↑8)
107		sq2 14265	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
108	107	oveq1i 7427	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (4↑4)
109	106, 108	eqtr3i 2787	. . . . . . . . . . . 12 ⊢ (2↑8) = (4↑4)
110		2exp8 17186	. . . . . . . . . . . 12 ⊢ (2↑8) = ;;256
111	109, 110	eqtr3i 2787	. . . . . . . . . . 11 ⊢ (4↑4) = ;;256
112	111	oveq2i 7428	. . . . . . . . . 10 ⊢ ((𝐴↑4) / (4↑4)) = ((𝐴↑4) / ;;256)
113	101, 112	eqtrdi 2813	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / ;;256))
114	98, 113	oveq12d 7435	. . . . . . . 8 ⊢ (𝜑 → ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))
115	65, 114	oveq12d 7435	. . . . . . 7 ⊢ (𝜑 → ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4))) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))))
116	20, 115	oveq12d 7435	. . . . . 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)))))
117	2, 11, 116	3eqtrd 2801	. . . . 5 ⊢ (𝜑 → (𝑌↑4) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))))
118	117	oveq1d 7432	. . . 4 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))) + (𝑃 · (𝑌↑2))))
119		expcl 14147	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝑋↑4) ∈ ℂ)
120	3, 99, 119	sylancl 598	. . . . . 6 ⊢ (𝜑 → (𝑋↑4) ∈ ℂ)
121	4, 14	mulcld 11257	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑3)) ∈ ℂ)
122	120, 121	addcld 11256	. . . . 5 ⊢ (𝜑 → ((𝑋↑4) + (𝐴 · (𝑋↑3))) ∈ ℂ)
123		mulcl 11212	. . . . . . . 8 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
124	51, 42, 123	sylancr 599	. . . . . . 7 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
125	124, 25	mulcld 11257	. . . . . 6 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) ∈ ℂ)
126	82, 87, 89	divcld 12019	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑3) / 8) ∈ ℂ)
127	126	halfcld 12517	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) ∈ ℂ)
128	127, 3	mulcld 11257	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) · 𝑋) ∈ ℂ)
129		expcl 14147	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
130	4, 99, 129	sylancl 598	. . . . . . . 8 ⊢ (𝜑 → (𝐴↑4) ∈ ℂ)
131		5nn0 12552	. . . . . . . . . . . 12 ⊢ 5 ∈ ℕ₀
132	73, 131	deccl 12755	. . . . . . . . . . 11 ⊢ ;25 ∈ ℕ₀
133	132, 21	decnncl 12764	. . . . . . . . . 10 ⊢ ;;256 ∈ ℕ
134	133	nncni 12271	. . . . . . . . 9 ⊢ ;;256 ∈ ℂ
135	134	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ∈ ℂ)
136	133	nnne0i 12304	. . . . . . . . 9 ⊢ ;;256 ≠ 0
137	136	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ≠ 0)
138	130, 135, 137	divcld 12019	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑4) / ;;256) ∈ ℂ)
139	128, 138	addcld 11256	. . . . . 6 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) ∈ ℂ)
140	125, 139	addcld 11256	. . . . 5 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) ∈ ℂ)
141		quart1.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℂ)
142		quart1.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
143		quart1.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
144		quart1.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))
145		quart1.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))
146		quart1.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
147	4, 141, 142, 143, 144, 145, 146	quart1cl 27099	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
148	147	simp1d 1160	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℂ)
149	3, 9	addcld 11256	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝐴 / 4)) ∈ ℂ)
150	1, 149	eqeltrd 2862	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
151	150	sqcld 14212	. . . . . 6 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
152	148, 151	mulcld 11257	. . . . 5 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) ∈ ℂ)
153	122, 140, 152	addassd 11259	. . . 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)))))
154	118, 153	eqtrd 2797	. . 3 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))))
155	154	oveq1d 7432	. 2 ⊢ (𝜑 → (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))) + ((𝑄 · 𝑌) + 𝑅)))
156	140, 152	addcld 11256	. . 3 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) ∈ ℂ)
157	147	simp2d 1161	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℂ)
158	157, 150	mulcld 11257	. . . 4 ⊢ (𝜑 → (𝑄 · 𝑌) ∈ ℂ)
159	147	simp3d 1162	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ℂ)
160	158, 159	addcld 11256	. . 3 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) ∈ ℂ)
161	122, 156, 160	addassd 11259	. 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))) + ((𝑄 · 𝑌) + 𝑅))))
162	1	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌↑2) = ((𝑋 + (𝐴 / 4))↑2))
163		binom2 14285	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
164	3, 9, 163	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
165	3, 9	mulcld 11257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐴 / 4)) ∈ ℂ)
166		mulcl 11212	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ (𝑋 · (𝐴 / 4)) ∈ ℂ) → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
167	29, 165, 166	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
168	25, 167, 24	addassd 11259	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
169	162, 164, 168	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝜑 → (𝑌↑2) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
170	169	oveq2d 7433	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
171	167, 24	addcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)) ∈ ℂ)
172	148, 25, 171	adddid 11261	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
173	170, 172	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
174	173	oveq2d 7433	. . . . . 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))))))
175	148, 25	mulcld 11257	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑋↑2)) ∈ ℂ)
176	148, 171	mulcld 11257	. . . . . . 7 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) ∈ ℂ)
177	125, 139, 175, 176	add4d 11467	. . . . . 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))))))
178	124, 148, 25	adddird 11262	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))))
179	144	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))))
180	124, 141	pncan3d 11600	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))) = 𝐵)
181	179, 180	eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = 𝐵)
182	181	oveq1d 7432	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = (𝐵 · (𝑋↑2)))
183	178, 182	eqtr3d 2799	. . . . . . 7 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) = (𝐵 · (𝑋↑2)))
184	183	oveq1d 7432	. . . . . 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))))))
185	174, 177, 184	3eqtrd 2801	. . . . 5 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) = ((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
186	185	oveq1d 7432	. . . 4 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = (((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) + ((𝑄 · 𝑌) + 𝑅)))
187	141, 25	mulcld 11257	. . . . 5 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
188	139, 176	addcld 11256	. . . . 5 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) ∈ ℂ)
189	187, 188, 160	addassd 11259	. . . 4 ⊢ (𝜑 → (((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))))
190	4, 141	mulcld 11257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
191	190	halfcld 12517	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ)
192	191, 126	subcld 11597	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) ∈ ℂ)
193	192, 3	mulcld 11257	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) ∈ ℂ)
194	148, 24	mulcld 11257	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈ ℂ)
195	138, 194	addcld 11256	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) ∈ ℂ)
196	157, 3	mulcld 11257	. . . . . . 7 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
197	157, 9	mulcld 11257	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) ∈ ℂ)
198	197, 159	addcld 11256	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) ∈ ℂ)
199	193, 195, 196, 198	add4d 11467	. . . . . 6 ⊢ (𝜑 → ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
200	148, 167, 24	adddid 11261	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) = ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2))))
201	200	oveq2d 7433	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))))
202	148, 167	mulcld 11257	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) ∈ ℂ)
203	128, 138, 202, 194	add4d 11467	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
204	4, 88, 88, 91, 91	divdiv1d 12050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / (2 · 2)))
205		2t2e4 12432	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
206	205	oveq2i 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (2 · 2)) = (𝐴 / 4)
207	204, 206	eqtrdi 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / 4))
208	207	oveq2d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (2 · (𝐴 / 4)))
209	4	halfcld 12517	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)
210	209, 88, 91	divcan2d 12021	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (𝐴 / 2))
211	208, 210	eqtr3d 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝐴 / 4)) = (𝐴 / 2))
212	211	oveq2d 7433	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = (𝑋 · (𝐴 / 2)))
213	3, 209	mulcomd 11258	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (𝐴 / 2)) = ((𝐴 / 2) · 𝑋))
214	212, 213	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = ((𝐴 / 2) · 𝑋))
215	214	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (𝑋 · (2 · (𝐴 / 4)))) = (𝑃 · ((𝐴 / 2) · 𝑋)))
216	88, 3, 9	mul12d 11447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) = (𝑋 · (2 · (𝐴 / 4))))
217	216	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = (𝑃 · (𝑋 · (2 · (𝐴 / 4)))))
218	148, 209, 3	mulassd 11260	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃 · (𝐴 / 2)) · 𝑋) = (𝑃 · ((𝐴 / 2) · 𝑋)))
219	215, 217, 218	3eqtr4d 2807	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = ((𝑃 · (𝐴 / 2)) · 𝑋))
220	219	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
221	148, 209	mulcld 11257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) ∈ ℂ)
222	127, 221, 3	adddird 11262	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
223	144	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)))
224	141, 124, 209	subdird 11699	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)) = ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))))
225	141, 4, 88, 91	divassd 12054	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = (𝐵 · (𝐴 / 2)))
226	141, 4	mulcomd 11258	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 · 𝐴) = (𝐴 · 𝐵))
227	226	oveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = ((𝐴 · 𝐵) / 2))
228	225, 227	eqtr3d 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 · (𝐴 / 2)) = ((𝐴 · 𝐵) / 2))
229	71	oveq2i 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
230		expp1 14136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
231	4, 73, 230	sylancl 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
232	229, 231	eqtrid 2809	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴↑3) = ((𝐴↑2) · 𝐴))
233	232	oveq2d 7433	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 / 8) · (𝐴↑3)) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
234	33	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 3 ∈ ℂ)
235	234, 82, 87, 89	div23d 12056	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = ((3 / 8) · (𝐴↑3)))
236	51	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (3 / 8) ∈ ℂ)
237	236, 42, 4	mulassd 11260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
238	233, 235, 237	3eqtr4rd 2808	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 · (𝐴↑3)) / 8))
239	234, 82, 87, 89	divassd 12054	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = (3 · ((𝐴↑3) / 8)))
240	238, 239	eqtrd 2797	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = (3 · ((𝐴↑3) / 8)))
241	240	oveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = ((3 · ((𝐴↑3) / 8)) / 2))
242	124, 4, 88, 91	divassd 12054	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)))
243	234, 126, 88, 91	divassd 12054	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · ((𝐴↑3) / 8)) / 2) = (3 · (((𝐴↑3) / 8) / 2)))
244	241, 242, 243	3eqtr3d 2805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)) = (3 · (((𝐴↑3) / 8) / 2)))
245	228, 244	oveq12d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
246	223, 224, 245	3eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
247	246	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
248		mulcl 11212	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (((𝐴↑3) / 8) / 2) ∈ ℂ) → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
249	33, 127, 248	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
250	127, 191, 249	addsub12d 11620	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
251	191, 249, 127	subsub2d 11626	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
252	127	mullidd 11255	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (((𝐴↑3) / 8) / 2)) = (((𝐴↑3) / 8) / 2))
253	252	oveq2d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)))
254		3m1e2 12396	. . . . . . . . . . . . . . . . 17 ⊢ (3 − 1) = 2
255	254	oveq1i 7427	. . . . . . . . . . . . . . . 16 ⊢ ((3 − 1) · (((𝐴↑3) / 8) / 2)) = (2 · (((𝐴↑3) / 8) / 2))
256		1cnd 11230	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
257	234, 256, 127	subdird 11699	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 − 1) · (((𝐴↑3) / 8) / 2)) = ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))))
258	126, 88, 91	divcan2d 12021	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
259	255, 257, 258	3eqtr3a 2821	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((𝐴↑3) / 8))
260	253, 259	eqtr3d 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
261	260	oveq2d 7433	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
262	250, 251, 261	3eqtr2d 2803	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
263	247, 262	eqtrd 2797	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
264	263	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
265	220, 222, 264	3eqtr2d 2803	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
266	265	oveq1d 7432	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
267	201, 203, 266	3eqtrd 2801	. . . . . . 7 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
268	1	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · 𝑌) = (𝑄 · (𝑋 + (𝐴 / 4))))
269	157, 3, 9	adddid 11261	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · (𝑋 + (𝐴 / 4))) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
270	268, 269	eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 · 𝑌) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
271	270	oveq1d 7432	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅))
272	196, 197, 159	addassd 11259	. . . . . . . 8 ⊢ (𝜑 → (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
273	271, 272	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
274	267, 273	oveq12d 7435	. . . . . 6 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
275	192, 157	addcomd 11440	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
276	145	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
277	142, 191	subcld 11597	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ)
278	277, 126, 191	ppncand 11637	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)))
279	142, 191	npcand 11601	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)) = 𝐶)
280	278, 279	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = 𝐶)
281	275, 276, 280	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = 𝐶)
282	281	oveq1d 7432	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (𝐶 · 𝑋))
283	192, 157, 3	adddird 11262	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
284	282, 283	eqtr3d 2799	. . . . . . 7 ⊢ (𝜑 → (𝐶 · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
285	4, 141, 142, 143, 144, 145, 146, 3, 1	quart1lem 27100	. . . . . . 7 ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
286	284, 285	oveq12d 7435	. . . . . 6 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
287	199, 274, 286	3eqtr4d 2807	. . . . 5 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐶 · 𝑋) + 𝐷))
288	287	oveq2d 7433	. . . 4 ⊢ (𝜑 → ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
289	186, 189, 288	3eqtrd 2801	. . 3 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
290	289	oveq2d 7433	. 2 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))))
291	155, 161, 290	3eqtrrd 2802	1 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 (class class class)co 7417 ℂcc 11126 0cc0 11128 1c1 11129 + caddc 11131 · cmul 11133 − cmin 11469 / cdiv 11899 2c2 12323 3c3 12324 4c4 12325 5c5 12326 6c6 12327 8c8 12329 ℕ₀cn0 12532 cdc 12740 ↑cexp 14129

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-er 8700 df-en 8957 df-dom 8958 df-sdom 8959 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-seq 14070 df-exp 14130

This theorem is used by: quart 27106

W3C validator