Metamath Proof Explorer

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 mulid2d ⊢ ( 𝜑 → ( 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 mulid2d ⊢ ( 𝜑 → ( 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 ) ) + 𝑅 ) ) )