Theorem quart1lem

Description: Lemma for quart1 . (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	quart1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	quart1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	quart1.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	quart1.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	quart1.p	⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
	quart1.q	⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
	quart1.r	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
	quart1.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	quart1.y	⊢ ( 𝜑 → 𝑌 = ( 𝑋 + ( 𝐴 / 4 ) ) )
Assertion	quart1lem	⊢ ( 𝜑 → 𝐷 = ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		quart1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		quart1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		quart1.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		quart1.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		quart1.p	⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
6		quart1.q	⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
7		quart1.r	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
8		quart1.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
9		quart1.y	⊢ ( 𝜑 → 𝑌 = ( 𝑋 + ( 𝐴 / 4 ) ) )
10	1 2	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
11	10	halfcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) / 2 ) ∈ ℂ )
12	3 11	subcld	⊢ ( 𝜑 → ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) ∈ ℂ )
13		3nn0	⊢ 3 ∈ ℕ0
14		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
15	1 13 14	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) ∈ ℂ )
16		8cn	⊢ 8 ∈ ℂ
17	16	a1i	⊢ ( 𝜑 → 8 ∈ ℂ )
18		8nn	⊢ 8 ∈ ℕ
19	18	nnne0i	⊢ 8 ≠ 0
20	19	a1i	⊢ ( 𝜑 → 8 ≠ 0 )
21	15 17 20	divcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 3 ) / 8 ) ∈ ℂ )
22		4cn	⊢ 4 ∈ ℂ
23	22	a1i	⊢ ( 𝜑 → 4 ∈ ℂ )
24		4ne0	⊢ 4 ≠ 0
25	24	a1i	⊢ ( 𝜑 → 4 ≠ 0 )
26	1 23 25	divcld	⊢ ( 𝜑 → ( 𝐴 / 4 ) ∈ ℂ )
27	12 21 26	adddird	⊢ ( 𝜑 → ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) · ( 𝐴 / 4 ) ) = ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) · ( 𝐴 / 4 ) ) + ( ( ( 𝐴 ↑ 3 ) / 8 ) · ( 𝐴 / 4 ) ) ) )
28	6	oveq1d	⊢ ( 𝜑 → ( 𝑄 · ( 𝐴 / 4 ) ) = ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) · ( 𝐴 / 4 ) ) )
29	3 1 23 25	divassd	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) / 4 ) = ( 𝐶 · ( 𝐴 / 4 ) ) )
30	1	sqvald	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
31	30	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐵 ) = ( ( 𝐴 · 𝐴 ) · 𝐵 ) )
32	1 1 2	mul32d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐴 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) · 𝐴 ) )
33	31 32	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) · 𝐴 ) )
34	33	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) = ( ( ( 𝐴 · 𝐵 ) · 𝐴 ) / 8 ) )
35		2cn	⊢ 2 ∈ ℂ
36		4t2e8	⊢ ( 4 · 2 ) = 8
37	22 35 36	mulcomli	⊢ ( 2 · 4 ) = 8
38	37	oveq2i	⊢ ( ( ( 𝐴 · 𝐵 ) · 𝐴 ) / ( 2 · 4 ) ) = ( ( ( 𝐴 · 𝐵 ) · 𝐴 ) / 8 )
39	34 38	eqtr4di	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) = ( ( ( 𝐴 · 𝐵 ) · 𝐴 ) / ( 2 · 4 ) ) )
40	35	a1i	⊢ ( 𝜑 → 2 ∈ ℂ )
41		2ne0	⊢ 2 ≠ 0
42	41	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
43	10 40 1 23 42 25	divmuldivd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) / 2 ) · ( 𝐴 / 4 ) ) = ( ( ( 𝐴 · 𝐵 ) · 𝐴 ) / ( 2 · 4 ) ) )
44	39 43	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) = ( ( ( 𝐴 · 𝐵 ) / 2 ) · ( 𝐴 / 4 ) ) )
45	29 44	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) = ( ( 𝐶 · ( 𝐴 / 4 ) ) − ( ( ( 𝐴 · 𝐵 ) / 2 ) · ( 𝐴 / 4 ) ) ) )
46	3 11 26	subdird	⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) · ( 𝐴 / 4 ) ) = ( ( 𝐶 · ( 𝐴 / 4 ) ) − ( ( ( 𝐴 · 𝐵 ) / 2 ) · ( 𝐴 / 4 ) ) ) )
47	45 46	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) · ( 𝐴 / 4 ) ) )
48		df-4	⊢ 4 = ( 3 + 1 )
49	48	oveq2i	⊢ ( 𝐴 ↑ 4 ) = ( 𝐴 ↑ ( 3 + 1 ) )
50		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ ( 3 + 1 ) ) = ( ( 𝐴 ↑ 3 ) · 𝐴 ) )
51	1 13 50	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ ( 3 + 1 ) ) = ( ( 𝐴 ↑ 3 ) · 𝐴 ) )
52	49 51	eqtrid	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 3 ) · 𝐴 ) )
53	52	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) / 8 ) = ( ( ( 𝐴 ↑ 3 ) · 𝐴 ) / 8 ) )
54	15 1 17 20	div23d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 3 ) · 𝐴 ) / 8 ) = ( ( ( 𝐴 ↑ 3 ) / 8 ) · 𝐴 ) )
55	53 54	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) / 8 ) = ( ( ( 𝐴 ↑ 3 ) / 8 ) · 𝐴 ) )
56	55	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) = ( ( ( ( 𝐴 ↑ 3 ) / 8 ) · 𝐴 ) / 4 ) )
57	21 1 23 25	divassd	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) / 8 ) · 𝐴 ) / 4 ) = ( ( ( 𝐴 ↑ 3 ) / 8 ) · ( 𝐴 / 4 ) ) )
58	56 57	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) = ( ( ( 𝐴 ↑ 3 ) / 8 ) · ( 𝐴 / 4 ) ) )
59	47 58	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝐶 · 𝐴 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) = ( ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) · ( 𝐴 / 4 ) ) + ( ( ( 𝐴 ↑ 3 ) / 8 ) · ( 𝐴 / 4 ) ) ) )
60	27 28 59	3eqtr4d	⊢ ( 𝜑 → ( 𝑄 · ( 𝐴 / 4 ) ) = ( ( ( ( 𝐶 · 𝐴 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) )
61	3 1	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ ℂ )
62	61 23 25	divcld	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) / 4 ) ∈ ℂ )
63	1	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
64	63 2	mulcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐵 ) ∈ ℂ )
65	64 17 20	divcld	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ∈ ℂ )
66		4nn0	⊢ 4 ∈ ℕ0
67		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝐴 ↑ 4 ) ∈ ℂ )
68	1 66 67	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℂ )
69	68 17 20	divcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) / 8 ) ∈ ℂ )
70	69 23 25	divcld	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ∈ ℂ )
71	62 65 70	subadd23d	⊢ ( 𝜑 → ( ( ( ( 𝐶 · 𝐴 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) = ( ( ( 𝐶 · 𝐴 ) / 4 ) + ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) ) )
72	70 65	subcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) ∈ ℂ )
73	62 72	addcomd	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) / 4 ) + ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) ) = ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( 𝐶 · 𝐴 ) / 4 ) ) )
74	60 71 73	3eqtrd	⊢ ( 𝜑 → ( 𝑄 · ( 𝐴 / 4 ) ) = ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( 𝐶 · 𝐴 ) / 4 ) ) )
75		1nn0	⊢ 1 ∈ ℕ0
76		6nn	⊢ 6 ∈ ℕ
77	75 76	decnncl	⊢ ; 1 6 ∈ ℕ
78	77	nncni	⊢ ; 1 6 ∈ ℂ
79	78	a1i	⊢ ( 𝜑 → ; 1 6 ∈ ℂ )
80	77	nnne0i	⊢ ; 1 6 ≠ 0
81	80	a1i	⊢ ( 𝜑 → ; 1 6 ≠ 0 )
82	64 79 81	divcld	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ∈ ℂ )
83		3cn	⊢ 3 ∈ ℂ
84		2nn0	⊢ 2 ∈ ℕ0
85		5nn0	⊢ 5 ∈ ℕ0
86	84 85	deccl	⊢ ; 2 5 ∈ ℕ0
87	86 76	decnncl	⊢ ; ; 2 5 6 ∈ ℕ
88	87	nncni	⊢ ; ; 2 5 6 ∈ ℂ
89	87	nnne0i	⊢ ; ; 2 5 6 ≠ 0
90	83 88 89	divcli	⊢ ( 3 / ; ; 2 5 6 ) ∈ ℂ
91		mulcl	⊢ ( ( ( 3 / ; ; 2 5 6 ) ∈ ℂ ∧ ( 𝐴 ↑ 4 ) ∈ ℂ ) → ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ∈ ℂ )
92	90 68 91	sylancr	⊢ ( 𝜑 → ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ∈ ℂ )
93	82 92	subcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ∈ ℂ )
94	4 93 62	addsubd	⊢ ( 𝜑 → ( ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) − ( ( 𝐶 · 𝐴 ) / 4 ) ) = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
95	7 94	eqtr4d	⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) − ( ( 𝐶 · 𝐴 ) / 4 ) ) )
96	74 95	oveq12d	⊢ ( 𝜑 → ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) = ( ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) − ( ( 𝐶 · 𝐴 ) / 4 ) ) ) )
97	4 93	addcld	⊢ ( 𝜑 → ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ∈ ℂ )
98	72 62 97	ppncand	⊢ ( 𝜑 → ( ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) − ( ( 𝐶 · 𝐴 ) / 4 ) ) ) = ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ) )
99	72 4 93	add12d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ) = ( 𝐷 + ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ) )
100	65 92	addcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ∈ ℂ )
101	70 82	addcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) ∈ ℂ )
102	100 101	negsubdi2d	⊢ ( 𝜑 → - ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) − ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) ) = ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) − ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
103	70 82	addcomd	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) )
104	103	oveq2d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) − ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) − ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) )
105	65 92 82 70	addsub4d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) − ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) + ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) )
106	83	a1i	⊢ ( 𝜑 → 3 ∈ ℂ )
107	88	a1i	⊢ ( 𝜑 → ; ; 2 5 6 ∈ ℂ )
108	89	a1i	⊢ ( 𝜑 → ; ; 2 5 6 ≠ 0 )
109	106 68 107 108	divassd	⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 4 ) ) / ; ; 2 5 6 ) = ( 3 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) )
110	106 68 107 108	div23d	⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 4 ) ) / ; ; 2 5 6 ) = ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) )
111		1p2e3	⊢ ( 1 + 2 ) = 3
112	111	oveq1i	⊢ ( ( 1 + 2 ) · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) = ( 3 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) )
113		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
114	68 107 108	divcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ∈ ℂ )
115	113 40 114	adddird	⊢ ( 𝜑 → ( ( 1 + 2 ) · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) = ( ( 1 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
116	112 115	eqtr3id	⊢ ( 𝜑 → ( 3 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) = ( ( 1 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
117	114	mullidd	⊢ ( 𝜑 → ( 1 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) = ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) )
118	117	oveq1d	⊢ ( 𝜑 → ( ( 1 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
119	116 118	eqtrd	⊢ ( 𝜑 → ( 3 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
120	109 110 119	3eqtr3d	⊢ ( 𝜑 → ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
121	48	oveq1i	⊢ ( 4 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( ( 3 + 1 ) · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) )
122	70 23 25	divcld	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ∈ ℂ )
123	106 113 122	adddird	⊢ ( 𝜑 → ( ( 3 + 1 ) · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 1 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) )
124	121 123	eqtrid	⊢ ( 𝜑 → ( 4 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 1 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) )
125	70 23 25	divcan2d	⊢ ( 𝜑 → ( 4 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) )
126	122	mullidd	⊢ ( 𝜑 → ( 1 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) )
127	69 23 23 25 25	divdiv1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) = ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 · 4 ) ) )
128		4t4e16	⊢ ( 4 · 4 ) = ; 1 6
129	128	oveq2i	⊢ ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 · 4 ) ) = ( ( ( 𝐴 ↑ 4 ) / 8 ) / ; 1 6 )
130	127 129	eqtrdi	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) = ( ( ( 𝐴 ↑ 4 ) / 8 ) / ; 1 6 ) )
131	68 17 79 20 81	divdiv1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 8 ) / ; 1 6 ) = ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) )
132	16 78	mulcli	⊢ ( 8 · ; 1 6 ) ∈ ℂ
133	132	a1i	⊢ ( 𝜑 → ( 8 · ; 1 6 ) ∈ ℂ )
134	16 78 19 80	mulne0i	⊢ ( 8 · ; 1 6 ) ≠ 0
135	134	a1i	⊢ ( 𝜑 → ( 8 · ; 1 6 ) ≠ 0 )
136	68 133 135	divcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) ∈ ℂ )
137	136 40 42	divcan2d	⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) / 2 ) ) = ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) )
138	68 133 40 135 42	divdiv1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) / 2 ) = ( ( 𝐴 ↑ 4 ) / ( ( 8 · ; 1 6 ) · 2 ) ) )
139	16 78 35	mul32i	⊢ ( ( 8 · ; 1 6 ) · 2 ) = ( ( 8 · 2 ) · ; 1 6 )
140		2exp4	⊢ ( 2 ↑ 4 ) = ; 1 6
141		8t2e16	⊢ ( 8 · 2 ) = ; 1 6
142	140 141	eqtr4i	⊢ ( 2 ↑ 4 ) = ( 8 · 2 )
143	142 140	oveq12i	⊢ ( ( 2 ↑ 4 ) · ( 2 ↑ 4 ) ) = ( ( 8 · 2 ) · ; 1 6 )
144		4p4e8	⊢ ( 4 + 4 ) = 8
145	144	oveq2i	⊢ ( 2 ↑ ( 4 + 4 ) ) = ( 2 ↑ 8 )
146		expadd	⊢ ( ( 2 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) → ( 2 ↑ ( 4 + 4 ) ) = ( ( 2 ↑ 4 ) · ( 2 ↑ 4 ) ) )
147	35 66 66 146	mp3an	⊢ ( 2 ↑ ( 4 + 4 ) ) = ( ( 2 ↑ 4 ) · ( 2 ↑ 4 ) )
148		2exp8	⊢ ( 2 ↑ 8 ) = ; ; 2 5 6
149	145 147 148	3eqtr3i	⊢ ( ( 2 ↑ 4 ) · ( 2 ↑ 4 ) ) = ; ; 2 5 6
150	139 143 149	3eqtr2i	⊢ ( ( 8 · ; 1 6 ) · 2 ) = ; ; 2 5 6
151	150	oveq2i	⊢ ( ( 𝐴 ↑ 4 ) / ( ( 8 · ; 1 6 ) · 2 ) ) = ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 )
152	138 151	eqtrdi	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) / 2 ) = ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) )
153	152	oveq2d	⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 ↑ 4 ) / ( 8 · ; 1 6 ) ) / 2 ) ) = ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) )
154	131 137 153	3eqtr2d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 8 ) / ; 1 6 ) = ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) )
155	126 130 154	3eqtrd	⊢ ( 𝜑 → ( 1 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) )
156	155	oveq2d	⊢ ( 𝜑 → ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 1 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) = ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
157	124 125 156	3eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) = ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) )
158	120 157	oveq12d	⊢ ( 𝜑 → ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) = ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) − ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) ) )
159		mulcl	⊢ ( ( 3 ∈ ℂ ∧ ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ∈ ℂ ) → ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ∈ ℂ )
160	83 122 159	sylancr	⊢ ( 𝜑 → ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ∈ ℂ )
161		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ∈ ℂ ) → ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ∈ ℂ )
162	35 114 161	sylancr	⊢ ( 𝜑 → ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ∈ ℂ )
163	114 160 162	pnpcan2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) − ( ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) + ( 2 · ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) )
164	158 163	eqtrd	⊢ ( 𝜑 → ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) )
165	164	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) ) )
166	82 114 160	addsub12d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) ) )
167	165 166	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) ) )
168	64 17 40 20 42	divdiv1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) / 2 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ( 8 · 2 ) ) )
169	141	oveq2i	⊢ ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ( 8 · 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 )
170	168 169	eqtrdi	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) / 2 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) )
171	170	oveq2d	⊢ ( 𝜑 → ( 2 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) / 2 ) ) = ( 2 · ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) )
172	65 40 42	divcan2d	⊢ ( 𝜑 → ( 2 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) / 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) )
173	82	2timesd	⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) )
174	171 172 173	3eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) )
175	82 82 174	mvrladdd	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) )
176	175	oveq1d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) + ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) + ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) )
177	5	oveq1d	⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) )
178	83 16 19	divcli	⊢ ( 3 / 8 ) ∈ ℂ
179		mulcl	⊢ ( ( ( 3 / 8 ) ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
180	178 63 179	sylancr	⊢ ( 𝜑 → ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
181	26	sqcld	⊢ ( 𝜑 → ( ( 𝐴 / 4 ) ↑ 2 ) ∈ ℂ )
182	2 180 181	subdird	⊢ ( 𝜑 → ( ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( ( 𝐵 · ( ( 𝐴 / 4 ) ↑ 2 ) ) − ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
183	1 23 25	sqdivd	⊢ ( 𝜑 → ( ( 𝐴 / 4 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 4 ↑ 2 ) ) )
184	22	sqvali	⊢ ( 4 ↑ 2 ) = ( 4 · 4 )
185	184 128	eqtri	⊢ ( 4 ↑ 2 ) = ; 1 6
186	185	oveq2i	⊢ ( ( 𝐴 ↑ 2 ) / ( 4 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) / ; 1 6 )
187	183 186	eqtrdi	⊢ ( 𝜑 → ( ( 𝐴 / 4 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ; 1 6 ) )
188	187	oveq2d	⊢ ( 𝜑 → ( 𝐵 · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( 𝐵 · ( ( 𝐴 ↑ 2 ) / ; 1 6 ) ) )
189	2 63 79 81	divassd	⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 ↑ 2 ) ) / ; 1 6 ) = ( 𝐵 · ( ( 𝐴 ↑ 2 ) / ; 1 6 ) ) )
190	2 63	mulcomd	⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐵 ) )
191	190	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 ↑ 2 ) ) / ; 1 6 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) )
192	188 189 191	3eqtr2d	⊢ ( 𝜑 → ( 𝐵 · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) )
193	178	a1i	⊢ ( 𝜑 → ( 3 / 8 ) ∈ ℂ )
194	193 63 63	mulassd	⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) = ( ( 3 / 8 ) · ( ( 𝐴 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
195	106 68 17 20	div23d	⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 4 ) ) / 8 ) = ( ( 3 / 8 ) · ( 𝐴 ↑ 4 ) ) )
196		2p2e4	⊢ ( 2 + 2 ) = 4
197	196	oveq2i	⊢ ( 𝐴 ↑ ( 2 + 2 ) ) = ( 𝐴 ↑ 4 )
198	84	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
199	1 198 198	expaddd	⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 + 2 ) ) = ( ( 𝐴 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
200	197 199	eqtr3id	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
201	200	oveq2d	⊢ ( 𝜑 → ( ( 3 / 8 ) · ( 𝐴 ↑ 4 ) ) = ( ( 3 / 8 ) · ( ( 𝐴 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
202	195 201	eqtrd	⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 4 ) ) / 8 ) = ( ( 3 / 8 ) · ( ( 𝐴 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
203	106 68 17 20	divassd	⊢ ( 𝜑 → ( ( 3 · ( 𝐴 ↑ 4 ) ) / 8 ) = ( 3 · ( ( 𝐴 ↑ 4 ) / 8 ) ) )
204	194 202 203	3eqtr2d	⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) = ( 3 · ( ( 𝐴 ↑ 4 ) / 8 ) ) )
205	204	oveq1d	⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) / ( 4 ↑ 2 ) ) = ( ( 3 · ( ( 𝐴 ↑ 4 ) / 8 ) ) / ( 4 ↑ 2 ) ) )
206	185 79	eqeltrid	⊢ ( 𝜑 → ( 4 ↑ 2 ) ∈ ℂ )
207	185 80	eqnetri	⊢ ( 4 ↑ 2 ) ≠ 0
208	207	a1i	⊢ ( 𝜑 → ( 4 ↑ 2 ) ≠ 0 )
209	180 63 206 208	divassd	⊢ ( 𝜑 → ( ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) / ( 4 ↑ 2 ) ) = ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 ↑ 2 ) / ( 4 ↑ 2 ) ) ) )
210	106 69 206 208	divassd	⊢ ( 𝜑 → ( ( 3 · ( ( 𝐴 ↑ 4 ) / 8 ) ) / ( 4 ↑ 2 ) ) = ( 3 · ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 ↑ 2 ) ) ) )
211	205 209 210	3eqtr3d	⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 ↑ 2 ) / ( 4 ↑ 2 ) ) ) = ( 3 · ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 ↑ 2 ) ) ) )
212	183	oveq2d	⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 ↑ 2 ) / ( 4 ↑ 2 ) ) ) )
213	185	oveq2i	⊢ ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 4 ) / 8 ) / ; 1 6 )
214	130 213	eqtr4di	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) = ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 ↑ 2 ) ) )
215	214	oveq2d	⊢ ( 𝜑 → ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) = ( 3 · ( ( ( 𝐴 ↑ 4 ) / 8 ) / ( 4 ↑ 2 ) ) ) )
216	211 212 215	3eqtr4d	⊢ ( 𝜑 → ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) )
217	192 216	oveq12d	⊢ ( 𝜑 → ( ( 𝐵 · ( ( 𝐴 / 4 ) ↑ 2 ) ) − ( ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) )
218	177 182 217	3eqtrd	⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) )
219	218	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( 3 · ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) / 4 ) ) ) ) )
220	167 176 219	3eqtr4d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) + ( ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) − ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
221	104 105 220	3eqtrd	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) − ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) ) = ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
222	221	negeqd	⊢ ( 𝜑 → - ( ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) − ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) ) = - ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
223	70 82 65 92	addsub4d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) ) − ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) + ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) = ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
224	102 222 223	3eqtr3rd	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) = - ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) )
225	224	oveq2d	⊢ ( 𝜑 → ( 𝐷 + ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ) = ( 𝐷 + - ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
226	2 180	subcld	⊢ ( 𝜑 → ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
227	5 226	eqeltrd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
228	227 181	mulcld	⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ∈ ℂ )
229	114 228	addcld	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ∈ ℂ )
230	4 229	negsubd	⊢ ( 𝜑 → ( 𝐷 + - ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) = ( 𝐷 − ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
231	99 225 230	3eqtrd	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 4 ) / 8 ) / 4 ) − ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 8 ) ) + ( 𝐷 + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ) = ( 𝐷 − ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
232	96 98 231	3eqtrd	⊢ ( 𝜑 → ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) = ( 𝐷 − ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) )
233	232	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) = ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( 𝐷 − ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) ) )
234	229 4	pncan3d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( 𝐷 − ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) ) ) = 𝐷 )
235	233 234	eqtr2d	⊢ ( 𝜑 → 𝐷 = ( ( ( ( 𝐴 ↑ 4 ) / ; ; 2 5 6 ) + ( 𝑃 · ( ( 𝐴 / 4 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝐴 / 4 ) ) + 𝑅 ) ) )