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