Theorem quart1lem 27213

Description: Lemma for quart1 27214. (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
quart1lem	⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))

Proof of Theorem quart1lem

Step	Hyp	Ref	Expression
1		quart1.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
2		quart1.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		quart1.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4	2, 3	mulcld 11356	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
5	4	halfcld 12618	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · 𝐵) / 2) ∈ ℂ)
6	1, 5	subcld 11696	. . . . . . . 8 ⊢ (𝜑 → (𝐶 − ((𝐴 · 𝐵) / 2)) ∈ ℂ)
7		3nn0 12651	. . . . . . . . . 10 ⊢ 3 ∈ ℕ0
8		expcl 14249	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝐴↑3) ∈ ℂ)
9	2, 7, 8	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑3) ∈ ℂ)
10		8cn 12467	. . . . . . . . . 10 ⊢ 8 ∈ ℂ
11	10	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 8 ∈ ℂ)
12		8nn 12465	. . . . . . . . . . 11 ⊢ 8 ∈ ℕ
13	12	nnne0i 12405	. . . . . . . . . 10 ⊢ 8 ≠ 0
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 8 ≠ 0)
15	9, 11, 14	divcld 12120	. . . . . . . 8 ⊢ (𝜑 → ((𝐴↑3) / 8) ∈ ℂ)
16		4cn 12455	. . . . . . . . . 10 ⊢ 4 ∈ ℂ
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 4 ∈ ℂ)
18		4ne0 12481	. . . . . . . . . 10 ⊢ 4 ≠ 0
19	18	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 4 ≠ 0)
20	2, 17, 19	divcld 12120	. . . . . . . 8 ⊢ (𝜑 → (𝐴 / 4) ∈ ℂ)
21	6, 15, 20	adddird 11361	. . . . . . 7 ⊢ (𝜑 → (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) · (𝐴 / 4)) = (((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)) + (((𝐴↑3) / 8) · (𝐴 / 4))))
22		quart1.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))
23	22	oveq1d 7458	. . . . . . 7 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) = (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) · (𝐴 / 4)))
24	1, 2, 17, 19	divassd 12155	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 · 𝐴) / 4) = (𝐶 · (𝐴 / 4)))
25	2	sqvald 14313	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
26	25	oveq1d 7458	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐴) · 𝐵))
27	2, 2, 3	mul32d 11547	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐴) · 𝐵) = ((𝐴 · 𝐵) · 𝐴))
28	26, 27	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐵) · 𝐴))
29	28	oveq1d 7458	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = (((𝐴 · 𝐵) · 𝐴) / 8))
30		2t4e8 12539	. . . . . . . . . . . . 13 ⊢ (2 · 4) = 8
31	30	oveq2i 7454	. . . . . . . . . . . 12 ⊢ (((𝐴 · 𝐵) · 𝐴) / (2 · 4)) = (((𝐴 · 𝐵) · 𝐴) / 8)
32	29, 31	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = (((𝐴 · 𝐵) · 𝐴) / (2 · 4)))
33		2cn 12445	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
34	33	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
35		2ne0 12476	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 0)
37	4, 34, 2, 17, 36, 19	divmuldivd 12161	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴 · 𝐵) / 2) · (𝐴 / 4)) = (((𝐴 · 𝐵) · 𝐴) / (2 · 4)))
38	32, 37	eqtr4d 2801	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = (((𝐴 · 𝐵) / 2) · (𝐴 / 4)))
39	24, 38	oveq12d 7461	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) = ((𝐶 · (𝐴 / 4)) − (((𝐴 · 𝐵) / 2) · (𝐴 / 4))))
40	1, 5, 20	subdird 11800	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)) = ((𝐶 · (𝐴 / 4)) − (((𝐴 · 𝐵) / 2) · (𝐴 / 4))))
41	39, 40	eqtr4d 2801	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) = ((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)))
42		df-4 12434	. . . . . . . . . . . . . 14 ⊢ 4 = (3 + 1)
43	42	oveq2i 7454	. . . . . . . . . . . . 13 ⊢ (𝐴↑4) = (𝐴↑(3 + 1))
44		expp1 14238	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴))
45	2, 7, 44	sylancl 598	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴))
46	43, 45	eqtrid 2810	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑3) · 𝐴))
47	46	oveq1d 7458	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑4) / 8) = (((𝐴↑3) · 𝐴) / 8))
48	9, 2, 11, 14	div23d 12157	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴↑3) · 𝐴) / 8) = (((𝐴↑3) / 8) · 𝐴))
49	47, 48	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑4) / 8) = (((𝐴↑3) / 8) · 𝐴))
50	49	oveq1d 7458	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑4) / 8) / 4) = ((((𝐴↑3) / 8) · 𝐴) / 4))
51	15, 2, 17, 19	divassd 12155	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐴↑3) / 8) · 𝐴) / 4) = (((𝐴↑3) / 8) · (𝐴 / 4)))
52	50, 51	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑4) / 8) / 4) = (((𝐴↑3) / 8) · (𝐴 / 4)))
53	41, 52	oveq12d 7461	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (((𝐴↑4) / 8) / 4)) = (((𝐶 − ((𝐴 · 𝐵) / 2)) · (𝐴 / 4)) + (((𝐴↑3) / 8) · (𝐴 / 4))))
54	21, 23, 53	3eqtr4d 2808	. . . . . 6 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) = ((((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (((𝐴↑4) / 8) / 4)))
55	1, 2	mulcld 11356	. . . . . . . 8 ⊢ (𝜑 → (𝐶 · 𝐴) ∈ ℂ)
56	55, 17, 19	divcld 12120	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝐴) / 4) ∈ ℂ)
57	2	sqcld 14314	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
58	57, 3	mulcld 11356	. . . . . . . 8 ⊢ (𝜑 → ((𝐴↑2) · 𝐵) ∈ ℂ)
59	58, 11, 14	divcld 12120	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) ∈ ℂ)
60		4nn0 12652	. . . . . . . . . 10 ⊢ 4 ∈ ℕ0
61		expcl 14249	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ0) → (𝐴↑4) ∈ ℂ)
62	2, 60, 61	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑4) ∈ ℂ)
63	62, 11, 14	divcld 12120	. . . . . . . 8 ⊢ (𝜑 → ((𝐴↑4) / 8) ∈ ℂ)
64	63, 17, 19	divcld 12120	. . . . . . 7 ⊢ (𝜑 → (((𝐴↑4) / 8) / 4) ∈ ℂ)
65	56, 59, 64	subadd23d 11718	. . . . . 6 ⊢ (𝜑 → ((((𝐶 · 𝐴) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (((𝐴↑4) / 8) / 4)) = (((𝐶 · 𝐴) / 4) + ((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8))))
66	64, 59	subcld 11696	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) ∈ ℂ)
67	56, 66	addcomd 11539	. . . . . 6 ⊢ (𝜑 → (((𝐶 · 𝐴) / 4) + ((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8))) = (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4)))
68	54, 65, 67	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → (𝑄 · (𝐴 / 4)) = (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4)))
69		quart1.r	. . . . . 6 ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
70		quart1.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
71		1nn0 12649	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ0
72		6nn 12459	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
73	71, 72	decnncl 12865	. . . . . . . . . . 11 ⊢ ;16 ∈ ℕ
74	73	nncni 12372	. . . . . . . . . 10 ⊢ ;16 ∈ ℂ
75	74	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ;16 ∈ ℂ)
76	73	nnne0i 12405	. . . . . . . . . 10 ⊢ ;16 ≠ 0
77	76	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ;16 ≠ 0)
78	58, 75, 77	divcld 12120	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) · 𝐵) / ;16) ∈ ℂ)
79		3cn 12451	. . . . . . . . . 10 ⊢ 3 ∈ ℂ
80		2nn0 12650	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ0
81		5nn0 12653	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ0
82	80, 81	deccl 12856	. . . . . . . . . . . 12 ⊢ ;25 ∈ ℕ0
83	82, 72	decnncl 12865	. . . . . . . . . . 11 ⊢ ;;256 ∈ ℕ
84	83	nncni 12372	. . . . . . . . . 10 ⊢ ;;256 ∈ ℂ
85	83	nnne0i 12405	. . . . . . . . . 10 ⊢ ;;256 ≠ 0
86	79, 84, 85	divcli 12086	. . . . . . . . 9 ⊢ (3 / ;;256) ∈ ℂ
87		mulcl 11311	. . . . . . . . 9 ⊢ (((3 / ;;256) ∈ ℂ ∧ (𝐴↑4) ∈ ℂ) → ((3 / ;;256) · (𝐴↑4)) ∈ ℂ)
88	86, 62, 87	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → ((3 / ;;256) · (𝐴↑4)) ∈ ℂ)
89	78, 88	subcld 11696	. . . . . . 7 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))) ∈ ℂ)
90	70, 89, 56	addsubd 11717	. . . . . 6 ⊢ (𝜑 → ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))) − ((𝐶 · 𝐴) / 4)) = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
91	69, 90	eqtr4d 2801	. . . . 5 ⊢ (𝜑 → 𝑅 = ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))) − ((𝐶 · 𝐴) / 4)))
92	68, 91	oveq12d 7461	. . . 4 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) = ((((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4)) + ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))) − ((𝐶 · 𝐴) / 4))))
93	70, 89	addcld 11355	. . . . 5 ⊢ (𝜑 → (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))) ∈ ℂ)
94	66, 56, 93	ppncand 11736	. . . 4 ⊢ (𝜑 → ((((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((𝐶 · 𝐴) / 4)) + ((𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))) − ((𝐶 · 𝐴) / 4))) = (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))
95	66, 70, 89	add12d 11564	. . . . 5 ⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) = (𝐷 + (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))
96	59, 88	addcld 11355	. . . . . . . 8 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) ∈ ℂ)
97	64, 78	addcld 11355	. . . . . . . 8 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) ∈ ℂ)
98	96, 97	negsubdi2d 11712	. . . . . . 7 ⊢ (𝜑 → -(((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) − ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16))) = (((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) − ((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4)))))
99	64, 78	addcomd 11539	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / 8) / 4)))
100	99	oveq2d 7459	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) − ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16))) = (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) − ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / 8) / 4))))
101	59, 88, 78, 64	addsub4d 11743	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) − ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / 8) / 4))) = (((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) + (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4))))
102	79	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ∈ ℂ)
103	84	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ;;256 ∈ ℂ)
104	85	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ;;256 ≠ 0)
105	102, 62, 103, 104	divassd 12155	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (𝐴↑4)) / ;;256) = (3 · ((𝐴↑4) / ;;256)))
106	102, 62, 103, 104	div23d 12157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · (𝐴↑4)) / ;;256) = ((3 / ;;256) · (𝐴↑4)))
107		1p2e3 12512	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 2) = 3
108	107	oveq1i 7453	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + 2) · ((𝐴↑4) / ;;256)) = (3 · ((𝐴↑4) / ;;256))
109		1cnd 11329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
110	62, 103, 104	divcld 12120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴↑4) / ;;256) ∈ ℂ)
111	109, 34, 110	adddird 11361	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1 + 2) · ((𝐴↑4) / ;;256)) = ((1 · ((𝐴↑4) / ;;256)) + (2 · ((𝐴↑4) / ;;256))))
112	108, 111	eqtr3id 2812	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 · ((𝐴↑4) / ;;256)) = ((1 · ((𝐴↑4) / ;;256)) + (2 · ((𝐴↑4) / ;;256))))
113	110	mullidd 11354	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 · ((𝐴↑4) / ;;256)) = ((𝐴↑4) / ;;256))
114	113	oveq1d 7458	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 · ((𝐴↑4) / ;;256)) + (2 · ((𝐴↑4) / ;;256))) = (((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256))))
115	112, 114	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · ((𝐴↑4) / ;;256)) = (((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256))))
116	105, 106, 115	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((3 / ;;256) · (𝐴↑4)) = (((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256))))
117	42	oveq1i 7453	. . . . . . . . . . . . . . . 16 ⊢ (4 · ((((𝐴↑4) / 8) / 4) / 4)) = ((3 + 1) · ((((𝐴↑4) / 8) / 4) / 4))
118	64, 17, 19	divcld 12120	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) ∈ ℂ)
119	102, 109, 118	adddird 11361	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 + 1) · ((((𝐴↑4) / 8) / 4) / 4)) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (1 · ((((𝐴↑4) / 8) / 4) / 4))))
120	117, 119	eqtrid 2810	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · ((((𝐴↑4) / 8) / 4) / 4)) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (1 · ((((𝐴↑4) / 8) / 4) / 4))))
121	64, 17, 19	divcan2d 12122	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · ((((𝐴↑4) / 8) / 4) / 4)) = (((𝐴↑4) / 8) / 4))
122	118	mullidd 11354	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 · ((((𝐴↑4) / 8) / 4) / 4)) = ((((𝐴↑4) / 8) / 4) / 4))
123	63, 17, 17, 19, 19	divdiv1d 12151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) = (((𝐴↑4) / 8) / (4 · 4)))
124		4t4e16 12945	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 · 4) = ;16
125	124	oveq2i 7454	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴↑4) / 8) / (4 · 4)) = (((𝐴↑4) / 8) / ;16)
126	123, 125	eqtrdi 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) = (((𝐴↑4) / 8) / ;16))
127	62, 11, 75, 14, 77	divdiv1d 12151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐴↑4) / 8) / ;16) = ((𝐴↑4) / (8 · ;16)))
128	10, 74	mulcli 11343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (8 · ;16) ∈ ℂ
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (8 · ;16) ∈ ℂ)
130	10, 74, 13, 76	mulne0i 11986	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (8 · ;16) ≠ 0
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (8 · ;16) ≠ 0)
132	62, 129, 131	divcld 12120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐴↑4) / (8 · ;16)) ∈ ℂ)
133	132, 34, 36	divcan2d 12122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · (((𝐴↑4) / (8 · ;16)) / 2)) = ((𝐴↑4) / (8 · ;16)))
134	62, 129, 34, 131, 36	divdiv1d 12151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝐴↑4) / (8 · ;16)) / 2) = ((𝐴↑4) / ((8 · ;16) · 2)))
135	10, 74, 33	mul32i 11533	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((8 · ;16) · 2) = ((8 · 2) · ;16)
136		2exp4 17291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2↑4) = ;16
137		8t2e16 12961	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (8 · 2) = ;16
138	136, 137	eqtr4i 2789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2↑4) = (8 · 2)
139	138, 136	oveq12i 7455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2↑4) · (2↑4)) = ((8 · 2) · ;16)
140		4p4e8 12524	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 + 4) = 8
141	140	oveq2i 7454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2↑(4 + 4)) = (2↑8)
142		expadd 14274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 4 ∈ ℕ0) → (2↑(4 + 4)) = ((2↑4) · (2↑4)))
143	33, 60, 60, 142	mp3an 1491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2↑(4 + 4)) = ((2↑4) · (2↑4))
144		2exp8 17295	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2↑8) = ;;256
145	141, 143, 144	3eqtr3i 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2↑4) · (2↑4)) = ;;256
146	135, 139, 145	3eqtr2i 2792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((8 · ;16) · 2) = ;;256
147	146	oveq2i 7454	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴↑4) / ((8 · ;16) · 2)) = ((𝐴↑4) / ;;256)
148	134, 147	eqtrdi 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝐴↑4) / (8 · ;16)) / 2) = ((𝐴↑4) / ;;256))
149	148	oveq2d 7459	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · (((𝐴↑4) / (8 · ;16)) / 2)) = (2 · ((𝐴↑4) / ;;256)))
150	127, 133, 149	3eqtr2d 2804	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐴↑4) / 8) / ;16) = (2 · ((𝐴↑4) / ;;256)))
151	122, 126, 150	3eqtrd 2802	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · ((((𝐴↑4) / 8) / 4) / 4)) = (2 · ((𝐴↑4) / ;;256)))
152	151	oveq2d 7459	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (1 · ((((𝐴↑4) / 8) / 4) / 4))) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 · ((𝐴↑4) / ;;256))))
153	120, 121, 152	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴↑4) / 8) / 4) = ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 · ((𝐴↑4) / ;;256))))
154	116, 153	oveq12d 7461	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4)) = ((((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256))) − ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 · ((𝐴↑4) / ;;256)))))
155		mulcl 11311	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℂ ∧ ((((𝐴↑4) / 8) / 4) / 4) ∈ ℂ) → (3 · ((((𝐴↑4) / 8) / 4) / 4)) ∈ ℂ)
156	79, 118, 155	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((((𝐴↑4) / 8) / 4) / 4)) ∈ ℂ)
157		mulcl 11311	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ ((𝐴↑4) / ;;256) ∈ ℂ) → (2 · ((𝐴↑4) / ;;256)) ∈ ℂ)
158	33, 110, 157	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · ((𝐴↑4) / ;;256)) ∈ ℂ)
159	110, 156, 158	pnpcan2d 11734	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴↑4) / ;;256) + (2 · ((𝐴↑4) / ;;256))) − ((3 · ((((𝐴↑4) / 8) / 4) / 4)) + (2 · ((𝐴↑4) / ;;256)))) = (((𝐴↑4) / ;;256) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))
160	154, 159	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4)) = (((𝐴↑4) / ;;256) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))
161	160	oveq2d 7459	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) + (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4))) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / ;;256) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))))
162	78, 110, 156	addsub12d 11719	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑4) / ;;256) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))) = (((𝐴↑4) / ;;256) + ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))))
163	161, 162	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / ;16) + (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4))) = (((𝐴↑4) / ;;256) + ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))))
164	58, 11, 34, 14, 36	divdiv1d 12151	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) / 2) = (((𝐴↑2) · 𝐵) / (8 · 2)))
165	137	oveq2i 7454	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑2) · 𝐵) / (8 · 2)) = (((𝐴↑2) · 𝐵) / ;16)
166	164, 165	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) / 2) = (((𝐴↑2) · 𝐵) / ;16))
167	166	oveq2d 7459	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · ((((𝐴↑2) · 𝐵) / 8) / 2)) = (2 · (((𝐴↑2) · 𝐵) / ;16)))
168	59, 34, 36	divcan2d 12122	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · ((((𝐴↑2) · 𝐵) / 8) / 2)) = (((𝐴↑2) · 𝐵) / 8))
169	78	2timesd 12616	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (((𝐴↑2) · 𝐵) / ;16)) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑2) · 𝐵) / ;16)))
170	167, 168, 169	3eqtr3d 2806	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑2) · 𝐵) / 8) = ((((𝐴↑2) · 𝐵) / ;16) + (((𝐴↑2) · 𝐵) / ;16)))
171	78, 78, 170	mvrladdd 11755	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) = (((𝐴↑2) · 𝐵) / ;16))
172	171	oveq1d 7458	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) + (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4))) = ((((𝐴↑2) · 𝐵) / ;16) + (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4))))
173		quart1.p	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))
174	173	oveq1d 7458	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) = ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐴 / 4)↑2)))
175	79, 10, 13	divcli 12086	. . . . . . . . . . . . . 14 ⊢ (3 / 8) ∈ ℂ
176		mulcl 11311	. . . . . . . . . . . . . 14 ⊢ (((3 / 8) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
177	175, 57, 176	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 / 8) · (𝐴↑2)) ∈ ℂ)
178	20	sqcld 14314	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 / 4)↑2) ∈ ℂ)
179	3, 177, 178	subdird 11800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐴 / 4)↑2)) = ((𝐵 · ((𝐴 / 4)↑2)) − (((3 / 8) · (𝐴↑2)) · ((𝐴 / 4)↑2))))
180	2, 17, 19	sqdivd 14329	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / (4↑2)))
181	16	sqvali 14350	. . . . . . . . . . . . . . . . . 18 ⊢ (4↑2) = (4 · 4)
182	181, 124	eqtri 2786	. . . . . . . . . . . . . . . . 17 ⊢ (4↑2) = ;16
183	182	oveq2i 7454	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴↑2) / (4↑2)) = ((𝐴↑2) / ;16)
184	180, 183	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 / 4)↑2) = ((𝐴↑2) / ;16))
185	184	oveq2d 7459	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · ((𝐴 / 4)↑2)) = (𝐵 · ((𝐴↑2) / ;16)))
186	3, 57, 75, 77	divassd 12155	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 · (𝐴↑2)) / ;16) = (𝐵 · ((𝐴↑2) / ;16)))
187	3, 57	mulcomd 11357	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 · (𝐴↑2)) = ((𝐴↑2) · 𝐵))
188	187	oveq1d 7458	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 · (𝐴↑2)) / ;16) = (((𝐴↑2) · 𝐵) / ;16))
189	185, 186, 188	3eqtr2d 2804	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 · ((𝐴 / 4)↑2)) = (((𝐴↑2) · 𝐵) / ;16))
190	175	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (3 / 8) ∈ ℂ)
191	190, 57, 57	mulassd 11359	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴↑2)) = ((3 / 8) · ((𝐴↑2) · (𝐴↑2))))
192	102, 62, 11, 14	div23d 12157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐴↑4)) / 8) = ((3 / 8) · (𝐴↑4)))
193		2p2e4 12504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 2) = 4
194	193	oveq2i 7454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴↑(2 + 2)) = (𝐴↑4)
195	80	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℕ0)
196	2, 195, 195	expaddd 14318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴↑(2 + 2)) = ((𝐴↑2) · (𝐴↑2)))
197	194, 196	eqtr3id 2812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2) · (𝐴↑2)))
198	197	oveq2d 7459	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 / 8) · (𝐴↑4)) = ((3 / 8) · ((𝐴↑2) · (𝐴↑2))))
199	192, 198	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐴↑4)) / 8) = ((3 / 8) · ((𝐴↑2) · (𝐴↑2))))
200	102, 62, 11, 14	divassd 12155	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐴↑4)) / 8) = (3 · ((𝐴↑4) / 8)))
201	191, 199, 200	3eqtr2d 2804	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · (𝐴↑2)) = (3 · ((𝐴↑4) / 8)))
202	201	oveq1d 7458	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝐴↑2)) / (4↑2)) = ((3 · ((𝐴↑4) / 8)) / (4↑2)))
203	182, 75	eqeltrid 2868	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (4↑2) ∈ ℂ)
204	182, 76	eqnetri 3029	. . . . . . . . . . . . . . . . 17 ⊢ (4↑2) ≠ 0
205	204	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (4↑2) ≠ 0)
206	177, 57, 203, 205	divassd 12155	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((3 / 8) · (𝐴↑2)) · (𝐴↑2)) / (4↑2)) = (((3 / 8) · (𝐴↑2)) · ((𝐴↑2) / (4↑2))))
207	102, 63, 203, 205	divassd 12155	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((3 · ((𝐴↑4) / 8)) / (4↑2)) = (3 · (((𝐴↑4) / 8) / (4↑2))))
208	202, 206, 207	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · ((𝐴↑2) / (4↑2))) = (3 · (((𝐴↑4) / 8) / (4↑2))))
209	180	oveq2d 7459	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · ((𝐴 / 4)↑2)) = (((3 / 8) · (𝐴↑2)) · ((𝐴↑2) / (4↑2))))
210	182	oveq2i 7454	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴↑4) / 8) / (4↑2)) = (((𝐴↑4) / 8) / ;16)
211	126, 210	eqtr4di 2816	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐴↑4) / 8) / 4) / 4) = (((𝐴↑4) / 8) / (4↑2)))
212	211	oveq2d 7459	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((((𝐴↑4) / 8) / 4) / 4)) = (3 · (((𝐴↑4) / 8) / (4↑2))))
213	208, 209, 212	3eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((3 / 8) · (𝐴↑2)) · ((𝐴 / 4)↑2)) = (3 · ((((𝐴↑4) / 8) / 4) / 4)))
214	189, 213	oveq12d 7461	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · ((𝐴 / 4)↑2)) − (((3 / 8) · (𝐴↑2)) · ((𝐴 / 4)↑2))) = ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))
215	174, 179, 214	3eqtrd 2802	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) = ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4))))
216	215	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) = (((𝐴↑4) / ;;256) + ((((𝐴↑2) · 𝐵) / ;16) − (3 · ((((𝐴↑4) / 8) / 4) / 4)))))
217	163, 172, 216	3eqtr4d 2808	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) − (((𝐴↑2) · 𝐵) / ;16)) + (((3 / ;;256) · (𝐴↑4)) − (((𝐴↑4) / 8) / 4))) = (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))))
218	100, 101, 217	3eqtrd 2802	. . . . . . . 8 ⊢ (𝜑 → (((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) − ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16))) = (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))))
219	218	negeqd 11578	. . . . . . 7 ⊢ (𝜑 → -(((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4))) − ((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16))) = -(((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))))
220	64, 78, 59, 88	addsub4d 11743	. . . . . . 7 ⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) + (((𝐴↑2) · 𝐵) / ;16)) − ((((𝐴↑2) · 𝐵) / 8) + ((3 / ;;256) · (𝐴↑4)))) = (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
221	98, 219, 220	3eqtr3rd 2807	. . . . . 6 ⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))) = -(((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))))
222	221	oveq2d 7459	. . . . 5 ⊢ (𝜑 → (𝐷 + (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) = (𝐷 + -(((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
223	3, 177	subcld 11696	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − ((3 / 8) · (𝐴↑2))) ∈ ℂ)
224	173, 223	eqeltrd 2864	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
225	224, 178	mulcld 11356	. . . . . . 7 ⊢ (𝜑 → (𝑃 · ((𝐴 / 4)↑2)) ∈ ℂ)
226	110, 225	addcld 11355	. . . . . 6 ⊢ (𝜑 → (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) ∈ ℂ)
227	70, 226	negsubd 11702	. . . . 5 ⊢ (𝜑 → (𝐷 + -(((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))) = (𝐷 − (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
228	95, 222, 227	3eqtrd 2802	. . . 4 ⊢ (𝜑 → (((((𝐴↑4) / 8) / 4) − (((𝐴↑2) · 𝐵) / 8)) + (𝐷 + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) = (𝐷 − (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
229	92, 94, 228	3eqtrd 2802	. . 3 ⊢ (𝜑 → ((𝑄 · (𝐴 / 4)) + 𝑅) = (𝐷 − (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2)))))
230	229	oveq2d 7459	. 2 ⊢ (𝜑 → ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)) = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + (𝐷 − (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))))))
231	226, 70	pncan3d 11699	. 2 ⊢ (𝜑 → ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + (𝐷 − (((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))))) = 𝐷)
232	230, 231	eqtr2d 2799	1 ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  (class class class)co 7443  ℂcc 11225  0cc0 11227  1c1 11228   + caddc 11230   · cmul 11232   − cmin 11568   -cneg 11569   / cdiv 12000  2c2 12424  3c3 12425  4c4 12426  5c5 12427  6c6 12428  8c8 12430  ℕ₀cn0 12633  ;cdc 12841  ↑cexp 14231

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001  df-nn 12363  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438  df-9 12439  df-n0 12634  df-z 12721  df-dec 12842  df-uz 12993  df-seq 14172  df-exp 14232

This theorem is used by:  quart1  27214