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 26999

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 7427	. . . . . 6 ⊢ (𝜑 → (𝑌↑4) = ((𝑋 + (𝐴 / 4))↑4))
3		quart1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
4		quart1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		4cn 12327	. . . . . . . . 9 ⊢ 4 ∈ ℂ
6	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
7		4ne0 12353	. . . . . . . . 9 ⊢ 4 ≠ 0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ≠ 0)
9	4, 6, 8	divcld 11992	. . . . . . 7 ⊢ (𝜑 → (𝐴 / 4) ∈ ℂ)
10		binom4 26993	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
11	3, 9, 10	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
12		3nn0 12523	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
13		expcl 14117	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
14	3, 12, 13	sylancl 597	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
15	6, 14, 9	mul12d 11420	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = ((𝑋↑3) · (4 · (𝐴 / 4))))
16	4, 6, 8	divcan2d 11994	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝐴 / 4)) = 𝐴)
17	16	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · (4 · (𝐴 / 4))) = ((𝑋↑3) · 𝐴))
18	14, 4	mulcomd 11231	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · 𝐴) = (𝐴 · (𝑋↑3)))
19	15, 17, 18	3eqtrd 2802	. . . . . . . 8 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = (𝐴 · (𝑋↑3)))
20	19	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) = ((𝑋↑4) + (𝐴 · (𝑋↑3))))
21		6nn 12331	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
22	21	nncni 12244	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
24	9	sqcld 14182	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑2) ∈ ℂ)
25	3	sqcld 14182	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
26	23, 24, 25	mulassd 11233	. . . . . . . . 9 ⊢ (𝜑 → ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
27		2t3e6 12408	. . . . . . . . . . . . . . 15 ⊢ (2 · 3) = 6
28		8cn 12339	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℂ
29		2cn 12317	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
30		8t2e16 12832	. . . . . . . . . . . . . . . 16 ⊢ (8 · 2) = ;16
31	28, 29, 30	mulcomli 11219	. . . . . . . . . . . . . . 15 ⊢ (2 · 8) = ;16
32	27, 31	oveq12i 7424	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (6 / ;16)
33		3cn 12323	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
34		8nn 12337	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℕ
35	34	nnne0i 12277	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
36	28, 35	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℂ ∧ 8 ≠ 0)
37		2cnne0 12454	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
38		divcan5 11918	. . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . 13 ⊢ (6 / ;16) = (3 / 8)
41	40	oveq2i 7423	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) · (6 / ;16)) = ((𝐴↑2) · (3 / 8))
42	4	sqcld 14182	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
43		1nn0 12521	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
44	43, 21	decnncl 12736	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℕ
45	44	nncni 12244	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℂ
46	45	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ∈ ℂ)
47	44	nnne0i 12277	. . . . . . . . . . . . . 14 ⊢ ;16 ≠ 0
48	47	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ≠ 0)
49	42, 23, 46, 48	div12d 12028	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴↑2) · (6 / ;16)) = (6 · ((𝐴↑2) / ;16)))
50	41, 49	eqtr3id 2812	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑2) · (3 / 8)) = (6 · ((𝐴↑2) / ;16)))
51	33, 28, 35	divcli 11958	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
52		mulcom 11187	. . . . . . . . . . . 12 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
53	51, 42, 52	sylancr 598	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
54	4, 6, 8	sqdivd 14197	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2)))
55	5	sqvali 14218	. . . . . . . . . . . . . . 15 ⊢ (4↑2) = (4 · 4)
56		4t4e16 12816	. . . . . . . . . . . . . . 15 ⊢ (4 · 4) = ;16
57	55, 56	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ (4↑2) = ;16
58	57	oveq2i 7423	. . . . . . . . . . . . 13 ⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16)
59	54, 58	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16))
60	59	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (6 · ((𝐴 / 4)↑2)) = (6 · ((𝐴↑2) / ;16)))
61	50, 53, 60	3eqtr4d 2808	. . . . . . . . . 10 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = (6 · ((𝐴 / 4)↑2)))
62	61	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) = ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)))
63	25, 24	mulcomd 11231	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋↑2) · ((𝐴 / 4)↑2)) = (((𝐴 / 4)↑2) · (𝑋↑2)))
64	63	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
65	26, 62, 64	3eqtr4rd 2809	. . . . . . . 8 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (((3 / 8) · (𝐴↑2)) · (𝑋↑2)))
66		expcl 14117	. . . . . . . . . . . 12 ⊢ (((𝐴 / 4) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 / 4)↑3) ∈ ℂ)
67	9, 12, 66	sylancl 597	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / 4)↑3) ∈ ℂ)
68	6, 3, 67	mul12d 11420	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = (𝑋 · (4 · ((𝐴 / 4)↑3))))
69	6, 67	mulcld 11230	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) ∈ ℂ)
70	3, 69	mulcomd 11231	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 · (4 · ((𝐴 / 4)↑3))) = ((4 · ((𝐴 / 4)↑3)) · 𝑋))
71		df-3 12305	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
72	71	oveq2i 7423	. . . . . . . . . . . . . . . 16 ⊢ (4↑3) = (4↑(2 + 1))
73		2nn0 12522	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
74		expp1 14106	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℕ₀) → (4↑(2 + 1)) = ((4↑2) · 4))
75	5, 73, 74	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ (4↑(2 + 1)) = ((4↑2) · 4)
76	57	oveq1i 7422	. . . . . . . . . . . . . . . 16 ⊢ ((4↑2) · 4) = (;16 · 4)
77	72, 75, 76	3eqtri 2790	. . . . . . . . . . . . . . 15 ⊢ (4↑3) = (;16 · 4)
78	77	oveq2i 7423	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑3) / (4↑3)) = ((𝐴↑3) / (;16 · 4))
79	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ ℕ₀)
80	4, 6, 8, 79	expdivd 14198	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 / 4)↑3) = ((𝐴↑3) / (4↑3)))
81		expcl 14117	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
82	4, 12, 81	sylancl 597	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴↑3) ∈ ℂ)
83	82, 46, 6, 48, 8	divdiv1d 12023	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴↑3) / ;16) / 4) = ((𝐴↑3) / (;16 · 4)))
84	78, 80, 83	3eqtr4a 2824	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑3) = (((𝐴↑3) / ;16) / 4))
85	84	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (4 · (((𝐴↑3) / ;16) / 4)))
86	30	oveq2i 7423	. . . . . . . . . . . . 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 12348	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
91	90	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
92	82, 87, 88, 89, 91	divdiv1d 12023	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = ((𝐴↑3) / (8 · 2)))
93	82, 46, 48	divcld 11992	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴↑3) / ;16) ∈ ℂ)
94	93, 6, 8	divcan2d 11994	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · (((𝐴↑3) / ;16) / 4)) = ((𝐴↑3) / ;16))
95	86, 92, 94	3eqtr4a 2824	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = (4 · (((𝐴↑3) / ;16) / 4)))
96	85, 95	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (((𝐴↑3) / 8) / 2))
97	96	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · ((𝐴 / 4)↑3)) · 𝑋) = ((((𝐴↑3) / 8) / 2) · 𝑋))
98	68, 70, 97	3eqtrd 2802	. . . . . . . . 9 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = ((((𝐴↑3) / 8) / 2) · 𝑋))
99		4nn0 12524	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
100	99	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℕ₀)
101	4, 6, 8, 100	expdivd 14198	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / (4↑4)))
102		expmul 14145	. . . . . . . . . . . . . . 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		4t2e8 12410	. . . . . . . . . . . . . . . 16 ⊢ (4 · 2) = 8
105	5, 29, 104	mulcomli 11219	. . . . . . . . . . . . . . 15 ⊢ (2 · 4) = 8
106	105	oveq2i 7423	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = (2↑8)
107	103, 106	eqtr3i 2788	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (2↑8)
108		sq2 14235	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
109	108	oveq1i 7422	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (4↑4)
110	107, 109	eqtr3i 2788	. . . . . . . . . . . 12 ⊢ (2↑8) = (4↑4)
111		2exp8 17149	. . . . . . . . . . . 12 ⊢ (2↑8) = ;;256
112	110, 111	eqtr3i 2788	. . . . . . . . . . 11 ⊢ (4↑4) = ;;256
113	112	oveq2i 7423	. . . . . . . . . 10 ⊢ ((𝐴↑4) / (4↑4)) = ((𝐴↑4) / ;;256)
114	101, 113	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / ;;256))
115	98, 114	oveq12d 7430	. . . . . . . 8 ⊢ (𝜑 → ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))
116	65, 115	oveq12d 7430	. . . . . . 7 ⊢ (𝜑 → ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4))) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))))
117	20, 116	oveq12d 7430	. . . . . 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)))))
118	2, 11, 117	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → (𝑌↑4) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))))
119	118	oveq1d 7427	. . . 4 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))) + (𝑃 · (𝑌↑2))))
120		expcl 14117	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝑋↑4) ∈ ℂ)
121	3, 99, 120	sylancl 597	. . . . . 6 ⊢ (𝜑 → (𝑋↑4) ∈ ℂ)
122	4, 14	mulcld 11230	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑3)) ∈ ℂ)
123	121, 122	addcld 11229	. . . . 5 ⊢ (𝜑 → ((𝑋↑4) + (𝐴 · (𝑋↑3))) ∈ ℂ)
124		mulcl 11185	. . . . . . . 8 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
125	51, 42, 124	sylancr 598	. . . . . . 7 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
126	125, 25	mulcld 11230	. . . . . 6 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) ∈ ℂ)
127	82, 87, 89	divcld 11992	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑3) / 8) ∈ ℂ)
128	127	halfcld 12490	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) ∈ ℂ)
129	128, 3	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) · 𝑋) ∈ ℂ)
130		expcl 14117	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
131	4, 99, 130	sylancl 597	. . . . . . . 8 ⊢ (𝜑 → (𝐴↑4) ∈ ℂ)
132		5nn0 12525	. . . . . . . . . . . 12 ⊢ 5 ∈ ℕ₀
133	73, 132	deccl 12727	. . . . . . . . . . 11 ⊢ ;25 ∈ ℕ₀
134	133, 21	decnncl 12736	. . . . . . . . . 10 ⊢ ;;256 ∈ ℕ
135	134	nncni 12244	. . . . . . . . 9 ⊢ ;;256 ∈ ℂ
136	135	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ∈ ℂ)
137	134	nnne0i 12277	. . . . . . . . 9 ⊢ ;;256 ≠ 0
138	137	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ≠ 0)
139	131, 136, 138	divcld 11992	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑4) / ;;256) ∈ ℂ)
140	129, 139	addcld 11229	. . . . . 6 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) ∈ ℂ)
141	126, 140	addcld 11229	. . . . 5 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) ∈ ℂ)
142		quart1.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℂ)
143		quart1.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
144		quart1.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
145		quart1.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))
146		quart1.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))
147		quart1.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
148	4, 142, 143, 144, 145, 146, 147	quart1cl 26997	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
149	148	simp1d 1160	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℂ)
150	3, 9	addcld 11229	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝐴 / 4)) ∈ ℂ)
151	1, 150	eqeltrd 2863	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
152	151	sqcld 14182	. . . . . 6 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
153	149, 152	mulcld 11230	. . . . 5 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) ∈ ℂ)
154	123, 141, 153	addassd 11232	. . . 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)))))
155	119, 154	eqtrd 2798	. . 3 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))))
156	155	oveq1d 7427	. 2 ⊢ (𝜑 → (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))) + ((𝑄 · 𝑌) + 𝑅)))
157	141, 153	addcld 11229	. . 3 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) ∈ ℂ)
158	148	simp2d 1161	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℂ)
159	158, 151	mulcld 11230	. . . 4 ⊢ (𝜑 → (𝑄 · 𝑌) ∈ ℂ)
160	148	simp3d 1162	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ℂ)
161	159, 160	addcld 11229	. . 3 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) ∈ ℂ)
162	123, 157, 161	addassd 11232	. 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))) + ((𝑄 · 𝑌) + 𝑅))))
163	1	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌↑2) = ((𝑋 + (𝐴 / 4))↑2))
164		binom2 14255	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
165	3, 9, 164	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
166	3, 9	mulcld 11230	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐴 / 4)) ∈ ℂ)
167		mulcl 11185	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ (𝑋 · (𝐴 / 4)) ∈ ℂ) → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
168	29, 166, 167	sylancr 598	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
169	25, 168, 24	addassd 11232	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
170	163, 165, 169	3eqtrd 2802	. . . . . . . . 9 ⊢ (𝜑 → (𝑌↑2) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
171	170	oveq2d 7428	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
172	168, 24	addcld 11229	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)) ∈ ℂ)
173	149, 25, 172	adddid 11234	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
174	171, 173	eqtrd 2798	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
175	174	oveq2d 7428	. . . . . 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))))))
176	149, 25	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑋↑2)) ∈ ℂ)
177	149, 172	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) ∈ ℂ)
178	126, 140, 176, 177	add4d 11440	. . . . . 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))))))
179	125, 149, 25	adddird 11235	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))))
180	145	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))))
181	125, 142	pncan3d 11573	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))) = 𝐵)
182	180, 181	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = 𝐵)
183	182	oveq1d 7427	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = (𝐵 · (𝑋↑2)))
184	179, 183	eqtr3d 2800	. . . . . . 7 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) = (𝐵 · (𝑋↑2)))
185	184	oveq1d 7427	. . . . . 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))))))
186	175, 178, 185	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) = ((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
187	186	oveq1d 7427	. . . 4 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = (((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) + ((𝑄 · 𝑌) + 𝑅)))
188	142, 25	mulcld 11230	. . . . 5 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
189	140, 177	addcld 11229	. . . . 5 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) ∈ ℂ)
190	188, 189, 161	addassd 11232	. . . 4 ⊢ (𝜑 → (((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))))
191	4, 142	mulcld 11230	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
192	191	halfcld 12490	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ)
193	192, 127	subcld 11570	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) ∈ ℂ)
194	193, 3	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) ∈ ℂ)
195	149, 24	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈ ℂ)
196	139, 195	addcld 11229	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) ∈ ℂ)
197	158, 3	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
198	158, 9	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) ∈ ℂ)
199	198, 160	addcld 11229	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) ∈ ℂ)
200	194, 196, 197, 199	add4d 11440	. . . . . 6 ⊢ (𝜑 → ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
201	149, 168, 24	adddid 11234	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) = ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2))))
202	201	oveq2d 7428	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))))
203	149, 168	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) ∈ ℂ)
204	129, 139, 203, 195	add4d 11440	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
205	4, 88, 88, 91, 91	divdiv1d 12023	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / (2 · 2)))
206		2t2e4 12405	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
207	206	oveq2i 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (2 · 2)) = (𝐴 / 4)
208	205, 207	eqtrdi 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / 4))
209	208	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (2 · (𝐴 / 4)))
210	4	halfcld 12490	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)
211	210, 88, 91	divcan2d 11994	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (𝐴 / 2))
212	209, 211	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝐴 / 4)) = (𝐴 / 2))
213	212	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = (𝑋 · (𝐴 / 2)))
214	3, 210	mulcomd 11231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (𝐴 / 2)) = ((𝐴 / 2) · 𝑋))
215	213, 214	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = ((𝐴 / 2) · 𝑋))
216	215	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (𝑋 · (2 · (𝐴 / 4)))) = (𝑃 · ((𝐴 / 2) · 𝑋)))
217	88, 3, 9	mul12d 11420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) = (𝑋 · (2 · (𝐴 / 4))))
218	217	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = (𝑃 · (𝑋 · (2 · (𝐴 / 4)))))
219	149, 210, 3	mulassd 11233	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃 · (𝐴 / 2)) · 𝑋) = (𝑃 · ((𝐴 / 2) · 𝑋)))
220	216, 218, 219	3eqtr4d 2808	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = ((𝑃 · (𝐴 / 2)) · 𝑋))
221	220	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
222	149, 210	mulcld 11230	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) ∈ ℂ)
223	128, 222, 3	adddird 11235	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
224	145	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)))
225	142, 125, 210	subdird 11672	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)) = ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))))
226	142, 4, 88, 91	divassd 12027	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = (𝐵 · (𝐴 / 2)))
227	142, 4	mulcomd 11231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 · 𝐴) = (𝐴 · 𝐵))
228	227	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = ((𝐴 · 𝐵) / 2))
229	226, 228	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 · (𝐴 / 2)) = ((𝐴 · 𝐵) / 2))
230	71	oveq2i 7423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
231		expp1 14106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
232	4, 73, 231	sylancl 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
233	230, 232	eqtrid 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴↑3) = ((𝐴↑2) · 𝐴))
234	233	oveq2d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 / 8) · (𝐴↑3)) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
235	33	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 3 ∈ ℂ)
236	235, 82, 87, 89	div23d 12029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = ((3 / 8) · (𝐴↑3)))
237	51	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (3 / 8) ∈ ℂ)
238	237, 42, 4	mulassd 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
239	234, 236, 238	3eqtr4rd 2809	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 · (𝐴↑3)) / 8))
240	235, 82, 87, 89	divassd 12027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = (3 · ((𝐴↑3) / 8)))
241	239, 240	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = (3 · ((𝐴↑3) / 8)))
242	241	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = ((3 · ((𝐴↑3) / 8)) / 2))
243	125, 4, 88, 91	divassd 12027	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)))
244	235, 127, 88, 91	divassd 12027	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · ((𝐴↑3) / 8)) / 2) = (3 · (((𝐴↑3) / 8) / 2)))
245	242, 243, 244	3eqtr3d 2806	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)) = (3 · (((𝐴↑3) / 8) / 2)))
246	229, 245	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
247	224, 225, 246	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
248	247	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
249		mulcl 11185	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (((𝐴↑3) / 8) / 2) ∈ ℂ) → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
250	33, 128, 249	sylancr 598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
251	128, 192, 250	addsub12d 11593	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
252	192, 250, 128	subsub2d 11599	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
253	128	mullidd 11228	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (((𝐴↑3) / 8) / 2)) = (((𝐴↑3) / 8) / 2))
254	253	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)))
255		3m1e2 12369	. . . . . . . . . . . . . . . . 17 ⊢ (3 − 1) = 2
256	255	oveq1i 7422	. . . . . . . . . . . . . . . 16 ⊢ ((3 − 1) · (((𝐴↑3) / 8) / 2)) = (2 · (((𝐴↑3) / 8) / 2))
257		1cnd 11203	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
258	235, 257, 128	subdird 11672	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 − 1) · (((𝐴↑3) / 8) / 2)) = ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))))
259	127, 88, 91	divcan2d 11994	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
260	256, 258, 259	3eqtr3a 2822	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((𝐴↑3) / 8))
261	254, 260	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
262	261	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
263	251, 252, 262	3eqtr2d 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
264	248, 263	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
265	264	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
266	221, 223, 265	3eqtr2d 2804	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
267	266	oveq1d 7427	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
268	202, 204, 267	3eqtrd 2802	. . . . . . 7 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
269	1	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · 𝑌) = (𝑄 · (𝑋 + (𝐴 / 4))))
270	158, 3, 9	adddid 11234	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · (𝑋 + (𝐴 / 4))) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
271	269, 270	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 · 𝑌) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
272	271	oveq1d 7427	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅))
273	197, 198, 160	addassd 11232	. . . . . . . 8 ⊢ (𝜑 → (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
274	272, 273	eqtrd 2798	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
275	268, 274	oveq12d 7430	. . . . . 6 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
276	193, 158	addcomd 11413	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
277	146	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
278	143, 192	subcld 11570	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ)
279	278, 127, 192	ppncand 11610	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)))
280	143, 192	npcand 11574	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)) = 𝐶)
281	279, 280	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = 𝐶)
282	276, 277, 281	3eqtrd 2802	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = 𝐶)
283	282	oveq1d 7427	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (𝐶 · 𝑋))
284	193, 158, 3	adddird 11235	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
285	283, 284	eqtr3d 2800	. . . . . . 7 ⊢ (𝜑 → (𝐶 · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
286	4, 142, 143, 144, 145, 146, 147, 3, 1	quart1lem 26998	. . . . . . 7 ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
287	285, 286	oveq12d 7430	. . . . . 6 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
288	200, 275, 287	3eqtr4d 2808	. . . . 5 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐶 · 𝑋) + 𝐷))
289	288	oveq2d 7428	. . . 4 ⊢ (𝜑 → ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
290	187, 190, 289	3eqtrd 2802	. . 3 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
291	290	oveq2d 7428	. 2 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))))
292	156, 162, 291	3eqtrrd 2803	1 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 (class class class)co 7412 ℂcc 11099 0cc0 11101 1c1 11102 + caddc 11104 · cmul 11106 − cmin 11442 / cdiv 11872 2c2 12296 3c3 12297 4c4 12298 5c5 12299 6c6 12300 8c8 12302 ℕ₀cn0 12505 cdc 12712 ↑cexp 14099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-5 12307 df-6 12308 df-7 12309 df-8 12310 df-9 12311 df-n0 12506 df-z 12593 df-dec 12713 df-uz 12864 df-seq 14040 df-exp 14100

This theorem is referenced by: quart 27004

W3C validator