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 26899

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 7446	. . . . . 6 ⊢ (𝜑 → (𝑌↑4) = ((𝑋 + (𝐴 / 4))↑4))
3		quart1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
4		quart1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		4cn 12351	. . . . . . . . 9 ⊢ 4 ∈ ℂ
6	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ ℂ)
7		4ne0 12374	. . . . . . . . 9 ⊢ 4 ≠ 0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 4 ≠ 0)
9	4, 6, 8	divcld 12043	. . . . . . 7 ⊢ (𝜑 → (𝐴 / 4) ∈ ℂ)
10		binom4 26893	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
11	3, 9, 10	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑4) = (((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) + ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)))))
12		3nn0 12544	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
13		expcl 14120	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
14	3, 12, 13	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
15	6, 14, 9	mul12d 11470	. . . . . . . . 9 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = ((𝑋↑3) · (4 · (𝐴 / 4))))
16	4, 6, 8	divcan2d 12045	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝐴 / 4)) = 𝐴)
17	16	oveq2d 7447	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · (4 · (𝐴 / 4))) = ((𝑋↑3) · 𝐴))
18	14, 4	mulcomd 11282	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑3) · 𝐴) = (𝐴 · (𝑋↑3)))
19	15, 17, 18	3eqtrd 2781	. . . . . . . 8 ⊢ (𝜑 → (4 · ((𝑋↑3) · (𝐴 / 4))) = (𝐴 · (𝑋↑3)))
20	19	oveq2d 7447	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑4) + (4 · ((𝑋↑3) · (𝐴 / 4)))) = ((𝑋↑4) + (𝐴 · (𝑋↑3))))
21		6nn 12355	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
22	21	nncni 12276	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
24	9	sqcld 14184	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑2) ∈ ℂ)
25	3	sqcld 14184	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
26	23, 24, 25	mulassd 11284	. . . . . . . . 9 ⊢ (𝜑 → ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
27		3cn 12347	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
28		2cn 12341	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
29		3t2e6 12432	. . . . . . . . . . . . . . . 16 ⊢ (3 · 2) = 6
30	27, 28, 29	mulcomli 11270	. . . . . . . . . . . . . . 15 ⊢ (2 · 3) = 6
31		8cn 12363	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℂ
32		8t2e16 12848	. . . . . . . . . . . . . . . 16 ⊢ (8 · 2) = ;16
33	31, 28, 32	mulcomli 11270	. . . . . . . . . . . . . . 15 ⊢ (2 · 8) = ;16
34	30, 33	oveq12i 7443	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (6 / ;16)
35		8nn 12361	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℕ
36	35	nnne0i 12306	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
37	31, 36	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ ℂ ∧ 8 ≠ 0)
38		2cnne0 12476	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
39		divcan5 11969	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · 8)) = (3 / 8))
40	27, 37, 38, 39	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ ((2 · 3) / (2 · 8)) = (3 / 8)
41	34, 40	eqtr3i 2767	. . . . . . . . . . . . 13 ⊢ (6 / ;16) = (3 / 8)
42	41	oveq2i 7442	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) · (6 / ;16)) = ((𝐴↑2) · (3 / 8))
43	4	sqcld 14184	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
44		1nn0 12542	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
45	44, 21	decnncl 12753	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℕ
46	45	nncni 12276	. . . . . . . . . . . . . 14 ⊢ ;16 ∈ ℂ
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ∈ ℂ)
48	45	nnne0i 12306	. . . . . . . . . . . . . 14 ⊢ ;16 ≠ 0
49	48	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ;16 ≠ 0)
50	43, 23, 47, 49	div12d 12079	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴↑2) · (6 / ;16)) = (6 · ((𝐴↑2) / ;16)))
51	42, 50	eqtr3id 2791	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑2) · (3 / 8)) = (6 · ((𝐴↑2) / ;16)))
52	27, 31, 36	divcli 12009	. . . . . . . . . . . 12 ⊢ (3 / 8) ∈ ℂ
53		mulcom 11241	. . . . . . . . . . . 12 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
54	52, 43, 53	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = ((𝐴↑2) · (3 / 8)))
55	4, 6, 8	sqdivd 14199	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2)))
56	5	sqvali 14219	. . . . . . . . . . . . . . 15 ⊢ (4↑2) = (4 · 4)
57		4t4e16 12832	. . . . . . . . . . . . . . 15 ⊢ (4 · 4) = ;16
58	56, 57	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ (4↑2) = ;16
59	58	oveq2i 7442	. . . . . . . . . . . . 13 ⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16)
60	55, 59	eqtrdi 2793	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16))
61	60	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝜑 → (6 · ((𝐴 / 4)↑2)) = (6 · ((𝐴↑2) / ;16)))
62	51, 54, 61	3eqtr4d 2787	. . . . . . . . . 10 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) = (6 · ((𝐴 / 4)↑2)))
63	62	oveq1d 7446	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) = ((6 · ((𝐴 / 4)↑2)) · (𝑋↑2)))
64	25, 24	mulcomd 11282	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋↑2) · ((𝐴 / 4)↑2)) = (((𝐴 / 4)↑2) · (𝑋↑2)))
65	64	oveq2d 7447	. . . . . . . . 9 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (6 · (((𝐴 / 4)↑2) · (𝑋↑2))))
66	26, 63, 65	3eqtr4rd 2788	. . . . . . . 8 ⊢ (𝜑 → (6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) = (((3 / 8) · (𝐴↑2)) · (𝑋↑2)))
67		expcl 14120	. . . . . . . . . . . 12 ⊢ (((𝐴 / 4) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 / 4)↑3) ∈ ℂ)
68	9, 12, 67	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / 4)↑3) ∈ ℂ)
69	6, 3, 68	mul12d 11470	. . . . . . . . . 10 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = (𝑋 · (4 · ((𝐴 / 4)↑3))))
70	6, 68	mulcld 11281	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) ∈ ℂ)
71	3, 70	mulcomd 11282	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 · (4 · ((𝐴 / 4)↑3))) = ((4 · ((𝐴 / 4)↑3)) · 𝑋))
72		df-3 12330	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
73	72	oveq2i 7442	. . . . . . . . . . . . . . . 16 ⊢ (4↑3) = (4↑(2 + 1))
74		2nn0 12543	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
75		expp1 14109	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℕ₀) → (4↑(2 + 1)) = ((4↑2) · 4))
76	5, 74, 75	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (4↑(2 + 1)) = ((4↑2) · 4)
77	58	oveq1i 7441	. . . . . . . . . . . . . . . 16 ⊢ ((4↑2) · 4) = (;16 · 4)
78	73, 76, 77	3eqtri 2769	. . . . . . . . . . . . . . 15 ⊢ (4↑3) = (;16 · 4)
79	78	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑3) / (4↑3)) = ((𝐴↑3) / (;16 · 4))
80	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ ℕ₀)
81	4, 6, 8, 80	expdivd 14200	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 / 4)↑3) = ((𝐴↑3) / (4↑3)))
82		expcl 14120	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
83	4, 12, 82	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴↑3) ∈ ℂ)
84	83, 47, 6, 49, 8	divdiv1d 12074	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴↑3) / ;16) / 4) = ((𝐴↑3) / (;16 · 4)))
85	79, 81, 84	3eqtr4a 2803	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑3) = (((𝐴↑3) / ;16) / 4))
86	85	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (4 · (((𝐴↑3) / ;16) / 4)))
87	32	oveq2i 7442	. . . . . . . . . . . . 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 12370	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
92	91	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
93	83, 88, 89, 90, 92	divdiv1d 12074	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = ((𝐴↑3) / (8 · 2)))
94	83, 47, 49	divcld 12043	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴↑3) / ;16) ∈ ℂ)
95	94, 6, 8	divcan2d 12045	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 · (((𝐴↑3) / ;16) / 4)) = ((𝐴↑3) / ;16))
96	87, 93, 95	3eqtr4a 2803	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) = (4 · (((𝐴↑3) / ;16) / 4)))
97	86, 96	eqtr4d 2780	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · ((𝐴 / 4)↑3)) = (((𝐴↑3) / 8) / 2))
98	97	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · ((𝐴 / 4)↑3)) · 𝑋) = ((((𝐴↑3) / 8) / 2) · 𝑋))
99	69, 71, 98	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝜑 → (4 · (𝑋 · ((𝐴 / 4)↑3))) = ((((𝐴↑3) / 8) / 2) · 𝑋))
100		4nn0 12545	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
101	100	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℕ₀)
102	4, 6, 8, 101	expdivd 14200	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / (4↑4)))
103		expmul 14148	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) → (2↑(2 · 4)) = ((2↑2)↑4))
104	28, 74, 100, 103	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = ((2↑2)↑4)
105		4t2e8 12434	. . . . . . . . . . . . . . . 16 ⊢ (4 · 2) = 8
106	5, 28, 105	mulcomli 11270	. . . . . . . . . . . . . . 15 ⊢ (2 · 4) = 8
107	106	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ (2↑(2 · 4)) = (2↑8)
108	104, 107	eqtr3i 2767	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (2↑8)
109		sq2 14236	. . . . . . . . . . . . . 14 ⊢ (2↑2) = 4
110	109	oveq1i 7441	. . . . . . . . . . . . 13 ⊢ ((2↑2)↑4) = (4↑4)
111	108, 110	eqtr3i 2767	. . . . . . . . . . . 12 ⊢ (2↑8) = (4↑4)
112		2exp8 17126	. . . . . . . . . . . 12 ⊢ (2↑8) = ;;256
113	111, 112	eqtr3i 2767	. . . . . . . . . . 11 ⊢ (4↑4) = ;;256
114	113	oveq2i 7442	. . . . . . . . . 10 ⊢ ((𝐴↑4) / (4↑4)) = ((𝐴↑4) / ;;256)
115	102, 114	eqtrdi 2793	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 / 4)↑4) = ((𝐴↑4) / ;;256))
116	99, 115	oveq12d 7449	. . . . . . . 8 ⊢ (𝜑 → ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4)) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))
117	66, 116	oveq12d 7449	. . . . . . 7 ⊢ (𝜑 → ((6 · ((𝑋↑2) · ((𝐴 / 4)↑2))) + ((4 · (𝑋 · ((𝐴 / 4)↑3))) + ((𝐴 / 4)↑4))) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))))
118	20, 117	oveq12d 7449	. . . . . 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 2781	. . . . 5 ⊢ (𝜑 → (𝑌↑4) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))))
120	119	oveq1d 7446	. . . 4 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)))) + (𝑃 · (𝑌↑2))))
121		expcl 14120	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝑋↑4) ∈ ℂ)
122	3, 100, 121	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑋↑4) ∈ ℂ)
123	4, 14	mulcld 11281	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑3)) ∈ ℂ)
124	122, 123	addcld 11280	. . . . 5 ⊢ (𝜑 → ((𝑋↑4) + (𝐴 · (𝑋↑3))) ∈ ℂ)
125		mulcl 11239	. . . . . . . 8 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
126	52, 43, 125	sylancr 587	. . . . . . 7 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
127	126, 25	mulcld 11281	. . . . . 6 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝑋↑2)) ∈ ℂ)
128	83, 88, 90	divcld 12043	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑3) / 8) ∈ ℂ)
129	128	halfcld 12511	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑3) / 8) / 2) ∈ ℂ)
130	129, 3	mulcld 11281	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) · 𝑋) ∈ ℂ)
131		expcl 14120	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
132	4, 100, 131	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝐴↑4) ∈ ℂ)
133		5nn0 12546	. . . . . . . . . . . 12 ⊢ 5 ∈ ℕ₀
134	74, 133	deccl 12748	. . . . . . . . . . 11 ⊢ ;25 ∈ ℕ₀
135	134, 21	decnncl 12753	. . . . . . . . . 10 ⊢ ;;256 ∈ ℕ
136	135	nncni 12276	. . . . . . . . 9 ⊢ ;;256 ∈ ℂ
137	136	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ∈ ℂ)
138	135	nnne0i 12306	. . . . . . . . 9 ⊢ ;;256 ≠ 0
139	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ;;256 ≠ 0)
140	132, 137, 139	divcld 12043	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑4) / ;;256) ∈ ℂ)
141	130, 140	addcld 11280	. . . . . 6 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) ∈ ℂ)
142	127, 141	addcld 11280	. . . . 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 26897	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
150	149	simp1d 1143	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℂ)
151	3, 9	addcld 11280	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝐴 / 4)) ∈ ℂ)
152	1, 151	eqeltrd 2841	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ℂ)
153	152	sqcld 14184	. . . . . 6 ⊢ (𝜑 → (𝑌↑2) ∈ ℂ)
154	150, 153	mulcld 11281	. . . . 5 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) ∈ ℂ)
155	124, 142, 154	addassd 11283	. . . 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 2777	. . 3 ⊢ (𝜑 → ((𝑌↑4) + (𝑃 · (𝑌↑2))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))))
157	156	oveq1d 7446	. 2 ⊢ (𝜑 → (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2)))) + ((𝑄 · 𝑌) + 𝑅)))
158	142, 154	addcld 11280	. . 3 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) ∈ ℂ)
159	149	simp2d 1144	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℂ)
160	159, 152	mulcld 11281	. . . 4 ⊢ (𝜑 → (𝑄 · 𝑌) ∈ ℂ)
161	149	simp3d 1145	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ℂ)
162	160, 161	addcld 11280	. . 3 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) ∈ ℂ)
163	124, 158, 162	addassd 11283	. 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 7446	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌↑2) = ((𝑋 + (𝐴 / 4))↑2))
165		binom2 14256	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ (𝐴 / 4) ∈ ℂ) → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
166	3, 9, 165	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 + (𝐴 / 4))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)))
167	3, 9	mulcld 11281	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐴 / 4)) ∈ ℂ)
168		mulcl 11239	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ (𝑋 · (𝐴 / 4)) ∈ ℂ) → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
169	28, 167, 168	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) ∈ ℂ)
170	25, 169, 24	addassd 11283	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐴 / 4)))) + ((𝐴 / 4)↑2)) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
171	164, 166, 170	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝜑 → (𝑌↑2) = ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))
172	171	oveq2d 7447	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
173	169, 24	addcld 11280	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)) ∈ ℂ)
174	150, 25, 173	adddid 11285	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝑋↑2) + ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
175	172, 174	eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑌↑2)) = ((𝑃 · (𝑋↑2)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))))
176	175	oveq2d 7447	. . . . . 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 11281	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (𝑋↑2)) ∈ ℂ)
178	150, 173	mulcld 11281	. . . . . . 7 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) ∈ ℂ)
179	127, 141, 177, 178	add4d 11490	. . . . . 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 11286	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))))
181	146	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))))
182	126, 143	pncan3d 11623	. . . . . . . . . 10 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + (𝐵 − ((3 / 8) · (𝐴↑2)))) = 𝐵)
183	181, 182	eqtrd 2777	. . . . . . . . 9 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) + 𝑃) = 𝐵)
184	183	oveq1d 7446	. . . . . . . 8 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) + 𝑃) · (𝑋↑2)) = (𝐵 · (𝑋↑2)))
185	180, 184	eqtr3d 2779	. . . . . . 7 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (𝑃 · (𝑋↑2))) = (𝐵 · (𝑋↑2)))
186	185	oveq1d 7446	. . . . . 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 2781	. . . . 5 ⊢ (𝜑 → (((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) = ((𝐵 · (𝑋↑2)) + ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))))))
188	187	oveq1d 7446	. . . 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 11281	. . . . 5 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
190	141, 178	addcld 11280	. . . . 5 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) ∈ ℂ)
191	189, 190, 162	addassd 11283	. . . 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 11281	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
193	192	halfcld 12511	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ)
194	193, 128	subcld 11620	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) ∈ ℂ)
195	194, 3	mulcld 11281	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) ∈ ℂ)
196	150, 24	mulcld 11281	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈ ℂ)
197	140, 196	addcld 11280	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) ∈ ℂ)
198	159, 3	mulcld 11281	. . . . . . 7 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
199	159, 9	mulcld 11281	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) ∈ ℂ)
200	199, 161	addcld 11280	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) ∈ ℂ)
201	195, 197, 198, 200	add4d 11490	. . . . . 6 ⊢ (𝜑 → ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
202	150, 169, 24	adddid 11285	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2))) = ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2))))
203	202	oveq2d 7447	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + ((𝑃 · (2 · (𝑋 · (𝐴 / 4)))) + (𝑃 · ((𝐴 / 4)↑2)))))
204	150, 169	mulcld 11281	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) ∈ ℂ)
205	130, 140, 204, 196	add4d 11490	. . . . . . . 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 12074	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / (2 · 2)))
207		2t2e4 12430	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 2) = 4
208	207	oveq2i 7442	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (2 · 2)) = (𝐴 / 4)
209	206, 208	eqtrdi 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴 / 2) / 2) = (𝐴 / 4))
210	209	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (2 · (𝐴 / 4)))
211	4	halfcld 12511	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ)
212	211, 89, 92	divcan2d 12045	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · ((𝐴 / 2) / 2)) = (𝐴 / 2))
213	210, 212	eqtr3d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝐴 / 4)) = (𝐴 / 2))
214	213	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = (𝑋 · (𝐴 / 2)))
215	3, 211	mulcomd 11282	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 · (𝐴 / 2)) = ((𝐴 / 2) · 𝑋))
216	214, 215	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (2 · (𝐴 / 4))) = ((𝐴 / 2) · 𝑋))
217	216	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (𝑋 · (2 · (𝐴 / 4)))) = (𝑃 · ((𝐴 / 2) · 𝑋)))
218	89, 3, 9	mul12d 11470	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑋 · (𝐴 / 4))) = (𝑋 · (2 · (𝐴 / 4))))
219	218	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = (𝑃 · (𝑋 · (2 · (𝐴 / 4)))))
220	150, 211, 3	mulassd 11284	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃 · (𝐴 / 2)) · 𝑋) = (𝑃 · ((𝐴 / 2) · 𝑋)))
221	217, 219, 220	3eqtr4d 2787	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (2 · (𝑋 · (𝐴 / 4)))) = ((𝑃 · (𝐴 / 2)) · 𝑋))
222	221	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
223	150, 211	mulcld 11281	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) ∈ ℂ)
224	129, 223, 3	adddird 11286	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝑃 · (𝐴 / 2)) · 𝑋)))
225	146	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)))
226	143, 126, 211	subdird 11720	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · (𝐴 / 2)) = ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))))
227	143, 4, 89, 92	divassd 12078	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = (𝐵 · (𝐴 / 2)))
228	143, 4	mulcomd 11282	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 · 𝐴) = (𝐴 · 𝐵))
229	228	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐴) / 2) = ((𝐴 · 𝐵) / 2))
230	227, 229	eqtr3d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 · (𝐴 / 2)) = ((𝐴 · 𝐵) / 2))
231	72	oveq2i 7442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
232		expp1 14109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
233	4, 74, 232	sylancl 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
234	231, 233	eqtrid 2789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴↑3) = ((𝐴↑2) · 𝐴))
235	234	oveq2d 7447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 / 8) · (𝐴↑3)) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
236	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 3 ∈ ℂ)
237	236, 83, 88, 90	div23d 12080	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = ((3 / 8) · (𝐴↑3)))
238	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (3 / 8) ∈ ℂ)
239	238, 43, 4	mulassd 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 / 8) · ((𝐴↑2) · 𝐴)))
240	235, 237, 239	3eqtr4rd 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = ((3 · (𝐴↑3)) / 8))
241	236, 83, 88, 90	divassd 12078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐴↑3)) / 8) = (3 · ((𝐴↑3) / 8)))
242	240, 241	eqtrd 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · 𝐴) = (3 · ((𝐴↑3) / 8)))
243	242	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = ((3 · ((𝐴↑3) / 8)) / 2))
244	126, 4, 89, 92	divassd 12078	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · 𝐴) / 2) = (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)))
245	236, 128, 89, 92	divassd 12078	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · ((𝐴↑3) / 8)) / 2) = (3 · (((𝐴↑3) / 8) / 2)))
246	243, 244, 245	3eqtr3d 2785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴 / 2)) = (3 · (((𝐴↑3) / 8) / 2)))
247	230, 246	oveq12d 7449	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 · (𝐴 / 2)) − (((3 / 8) · (𝐴↑2)) · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
248	225, 226, 247	3eqtrd 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · (𝐴 / 2)) = (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2))))
249	248	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
250		mulcl 11239	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ (((𝐴↑3) / 8) / 2) ∈ ℂ) → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
251	27, 129, 250	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (((𝐴↑3) / 8) / 2)) ∈ ℂ)
252	129, 193, 251	addsub12d 11643	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
253	193, 251, 129	subsub2d 11649	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) + ((((𝐴↑3) / 8) / 2) − (3 · (((𝐴↑3) / 8) / 2)))))
254	129	mullidd 11279	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (((𝐴↑3) / 8) / 2)) = (((𝐴↑3) / 8) / 2))
255	254	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)))
256		3m1e2 12394	. . . . . . . . . . . . . . . . 17 ⊢ (3 − 1) = 2
257	256	oveq1i 7441	. . . . . . . . . . . . . . . 16 ⊢ ((3 − 1) · (((𝐴↑3) / 8) / 2)) = (2 · (((𝐴↑3) / 8) / 2))
258		1cnd 11256	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
259	236, 258, 129	subdird 11720	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 − 1) · (((𝐴↑3) / 8) / 2)) = ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))))
260	128, 89, 92	divcan2d 12045	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
261	257, 259, 260	3eqtr3a 2801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (1 · (((𝐴↑3) / 8) / 2))) = ((𝐴↑3) / 8))
262	255, 261	eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2)) = ((𝐴↑3) / 8))
263	262	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) − ((3 · (((𝐴↑3) / 8) / 2)) − (((𝐴↑3) / 8) / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
264	252, 253, 263	3eqtr2d 2783	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (((𝐴 · 𝐵) / 2) − (3 · (((𝐴↑3) / 8) / 2)))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
265	249, 264	eqtrd 2777	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) = (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)))
266	265	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) + (𝑃 · (𝐴 / 2))) · 𝑋) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
267	222, 224, 266	3eqtr2d 2783	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) = ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋))
268	267	oveq1d 7446	. . . . . . . 8 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + (𝑃 · (2 · (𝑋 · (𝐴 / 4))))) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
269	203, 205, 268	3eqtrd 2781	. . . . . . 7 ⊢ (𝜑 → ((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
270	1	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · 𝑌) = (𝑄 · (𝑋 + (𝐴 / 4))))
271	159, 3, 9	adddid 11285	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 · (𝑋 + (𝐴 / 4))) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
272	270, 271	eqtrd 2777	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 · 𝑌) = ((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))))
273	272	oveq1d 7446	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅))
274	198, 199, 161	addassd 11283	. . . . . . . 8 ⊢ (𝜑 → (((𝑄 · 𝑋) + (𝑄 · (𝐴 / 4))) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
275	273, 274	eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → ((𝑄 · 𝑌) + 𝑅) = ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
276	269, 275	oveq12d 7449	. . . . . 6 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑋) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
277	194, 159	addcomd 11463	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
278	147	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))))
279	144, 193	subcld 11620	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ)
280	279, 128, 193	ppncand 11660	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)))
281	144, 193	npcand 11624	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴 · 𝐵) / 2)) = 𝐶)
282	280, 281	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) + (((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8))) = 𝐶)
283	277, 278, 282	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) = 𝐶)
284	283	oveq1d 7446	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (𝐶 · 𝑋))
285	194, 159, 3	adddird 11286	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) + 𝑄) · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
286	284, 285	eqtr3d 2779	. . . . . . 7 ⊢ (𝜑 → (𝐶 · 𝑋) = (((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)))
287	4, 143, 144, 145, 146, 147, 148, 3, 1	quart1lem 26898	. . . . . . 7 ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
288	286, 287	oveq12d 7449	. . . . . 6 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) = ((((((𝐴 · 𝐵) / 2) − ((𝐴↑3) / 8)) · 𝑋) + (𝑄 · 𝑋)) + ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))))
289	201, 276, 288	3eqtr4d 2787	. . . . 5 ⊢ (𝜑 → (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐶 · 𝑋) + 𝐷))
290	289	oveq2d 7447	. . . 4 ⊢ (𝜑 → ((𝐵 · (𝑋↑2)) + (((((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256)) + (𝑃 · ((2 · (𝑋 · (𝐴 / 4))) + ((𝐴 / 4)↑2)))) + ((𝑄 · 𝑌) + 𝑅))) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
291	188, 191, 290	3eqtrd 2781	. . 3 ⊢ (𝜑 → ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)) = ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷)))
292	291	oveq2d 7447	. 2 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((((((3 / 8) · (𝐴↑2)) · (𝑋↑2)) + (((((𝐴↑3) / 8) / 2) · 𝑋) + ((𝐴↑4) / ;;256))) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅))) = (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))))
293	157, 163, 292	3eqtrrd 2782	1 ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 (class class class)co 7431 ℂcc 11153 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 − cmin 11492 / cdiv 11920 2c2 12321 3c3 12322 4c4 12323 5c5 12324 6c6 12325 8c8 12327 ℕ₀cn0 12526 cdc 12733 ↑cexp 14102

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-seq 14043 df-exp 14103

This theorem is referenced by: quart 26904

W3C validator