Metamath Proof Explorer

Theorem quartlem1

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

Ref Expression
Hypotheses quartlem1.p ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
quartlem1.q ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
quartlem1.r ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
quartlem1.u ⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) )
quartlem1.v ⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
Assertion quartlem1 ( 𝜑 → ( 𝑈 = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ∧ 𝑉 = ( ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) + ( 2 7 · - ( 𝑄 ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quartlem1.p ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
2 quartlem1.q ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
3 quartlem1.r ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
4 quartlem1.u ⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) )
5 quartlem1.v ⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
6 2cn ⊢ 2 ∈ ℂ
7 sqmul ⊢ ( ( 2 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( ( 2 · 𝑃 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑃 ↑ 2 ) ) )
8 6 1 7 sylancr ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑃 ↑ 2 ) ) )
9 sq2 ⊢ ( 2 ↑ 2 ) = 4
10 9 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( 𝑃 ↑ 2 ) ) = ( 4 · ( 𝑃 ↑ 2 ) )
11 8 10 eqtrdi ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) ↑ 2 ) = ( 4 · ( 𝑃 ↑ 2 ) ) )
12 11 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) = ( ( 4 · ( 𝑃 ↑ 2 ) ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) )
13 4cn ⊢ 4 ∈ ℂ
14 13 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
15 3cn ⊢ 3 ∈ ℂ
16 15 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
17 1 sqcld ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℂ )
18 14 16 17 subdird ⊢ ( 𝜑 → ( ( 4 − 3 ) · ( 𝑃 ↑ 2 ) ) = ( ( 4 · ( 𝑃 ↑ 2 ) ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) )
19 12 18 eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) = ( ( 4 − 3 ) · ( 𝑃 ↑ 2 ) ) )
20 ax-1cn ⊢ 1 ∈ ℂ
21 3p1e4 ⊢ ( 3 + 1 ) = 4
22 13 15 20 21 subaddrii ⊢ ( 4 − 3 ) = 1
23 22 oveq1i ⊢ ( ( 4 − 3 ) · ( 𝑃 ↑ 2 ) ) = ( 1 · ( 𝑃 ↑ 2 ) )
24 mulid2 ⊢ ( ( 𝑃 ↑ 2 ) ∈ ℂ → ( 1 · ( 𝑃 ↑ 2 ) ) = ( 𝑃 ↑ 2 ) )
25 23 24 syl5eq ⊢ ( ( 𝑃 ↑ 2 ) ∈ ℂ → ( ( 4 − 3 ) · ( 𝑃 ↑ 2 ) ) = ( 𝑃 ↑ 2 ) )
26 17 25 syl ⊢ ( 𝜑 → ( ( 4 − 3 ) · ( 𝑃 ↑ 2 ) ) = ( 𝑃 ↑ 2 ) )
27 19 26 eqtr2d ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) )
28 27 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) = ( ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) + ( 1 2 · 𝑅 ) ) )
29 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( 2 · 𝑃 ) ∈ ℂ )
30 6 1 29 sylancr ⊢ ( 𝜑 → ( 2 · 𝑃 ) ∈ ℂ )
31 30 sqcld ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) ↑ 2 ) ∈ ℂ )
32 mulcl ⊢ ( ( 3 ∈ ℂ ∧ ( 𝑃 ↑ 2 ) ∈ ℂ ) → ( 3 · ( 𝑃 ↑ 2 ) ) ∈ ℂ )
33 15 17 32 sylancr ⊢ ( 𝜑 → ( 3 · ( 𝑃 ↑ 2 ) ) ∈ ℂ )
34 1nn0 ⊢ 1 ∈ ℕ0
35 2nn ⊢ 2 ∈ ℕ
36 34 35 decnncl ⊢ 1 2 ∈ ℕ
37 36 nncni ⊢ 1 2 ∈ ℂ
38 mulcl ⊢ ( ( 1 2 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 1 2 · 𝑅 ) ∈ ℂ )
39 37 3 38 sylancr ⊢ ( 𝜑 → ( 1 2 · 𝑅 ) ∈ ℂ )
40 31 33 39 subsubd ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 1 2 · 𝑅 ) ) ) = ( ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( 𝑃 ↑ 2 ) ) ) + ( 1 2 · 𝑅 ) ) )
41 28 40 eqtr4d ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 1 2 · 𝑅 ) ) ) )
42 mulcl ⊢ ( ( 4 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 4 · 𝑅 ) ∈ ℂ )
43 13 3 42 sylancr ⊢ ( 𝜑 → ( 4 · 𝑅 ) ∈ ℂ )
44 16 17 43 subdid ⊢ ( 𝜑 → ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) = ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 3 · ( 4 · 𝑅 ) ) ) )
45 4t3e12 ⊢ ( 4 · 3 ) = 1 2
46 13 15 45 mulcomli ⊢ ( 3 · 4 ) = 1 2
47 46 oveq1i ⊢ ( ( 3 · 4 ) · 𝑅 ) = ( 1 2 · 𝑅 )
48 16 14 3 mulassd ⊢ ( 𝜑 → ( ( 3 · 4 ) · 𝑅 ) = ( 3 · ( 4 · 𝑅 ) ) )
49 47 48 eqtr3id ⊢ ( 𝜑 → ( 1 2 · 𝑅 ) = ( 3 · ( 4 · 𝑅 ) ) )
50 49 oveq2d ⊢ ( 𝜑 → ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 1 2 · 𝑅 ) ) = ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 3 · ( 4 · 𝑅 ) ) ) )
51 44 50 eqtr4d ⊢ ( 𝜑 → ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) = ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 1 2 · 𝑅 ) ) )
52 51 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( ( 3 · ( 𝑃 ↑ 2 ) ) − ( 1 2 · 𝑅 ) ) ) )
53 41 4 52 3eqtr4d ⊢ ( 𝜑 → 𝑈 = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) )
54 6 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
55 3nn0 ⊢ 3 ∈ ℕ0
56 55 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
57 54 1 56 mulexpd ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) ↑ 3 ) = ( ( 2 ↑ 3 ) · ( 𝑃 ↑ 3 ) ) )
58 cu2 ⊢ ( 2 ↑ 3 ) = 8
59 58 oveq1i ⊢ ( ( 2 ↑ 3 ) · ( 𝑃 ↑ 3 ) ) = ( 8 · ( 𝑃 ↑ 3 ) )
60 57 59 eqtrdi ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) ↑ 3 ) = ( 8 · ( 𝑃 ↑ 3 ) ) )
61 60 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) = ( 2 · ( 8 · ( 𝑃 ↑ 3 ) ) ) )
62 8cn ⊢ 8 ∈ ℂ
63 62 a1i ⊢ ( 𝜑 → 8 ∈ ℂ )
64 expcl ⊢ ( ( 𝑃 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑃 ↑ 3 ) ∈ ℂ )
65 1 55 64 sylancl ⊢ ( 𝜑 → ( 𝑃 ↑ 3 ) ∈ ℂ )
66 54 63 65 mul12d ⊢ ( 𝜑 → ( 2 · ( 8 · ( 𝑃 ↑ 3 ) ) ) = ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) )
67 61 66 eqtrd ⊢ ( 𝜑 → ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) = ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) )
68 9cn ⊢ 9 ∈ ℂ
69 68 a1i ⊢ ( 𝜑 → 9 ∈ ℂ )
70 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑃 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
71 6 65 70 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
72 1 3 mulcld ⊢ ( 𝜑 → ( 𝑃 · 𝑅 ) ∈ ℂ )
73 mulcl ⊢ ( ( 8 ∈ ℂ ∧ ( 𝑃 · 𝑅 ) ∈ ℂ ) → ( 8 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
74 62 72 73 sylancr ⊢ ( 𝜑 → ( 8 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
75 69 71 74 subdid ⊢ ( 𝜑 → ( 9 · ( ( 2 · ( 𝑃 ↑ 3 ) ) − ( 8 · ( 𝑃 · 𝑅 ) ) ) ) = ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 9 · ( 8 · ( 𝑃 · 𝑅 ) ) ) ) )
76 30 17 43 subdid ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) = ( ( ( 2 · 𝑃 ) · ( 𝑃 ↑ 2 ) ) − ( ( 2 · 𝑃 ) · ( 4 · 𝑅 ) ) ) )
77 54 1 17 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) · ( 𝑃 ↑ 2 ) ) = ( 2 · ( 𝑃 · ( 𝑃 ↑ 2 ) ) ) )
78 1 17 mulcomd ⊢ ( 𝜑 → ( 𝑃 · ( 𝑃 ↑ 2 ) ) = ( ( 𝑃 ↑ 2 ) · 𝑃 ) )
79 df-3 ⊢ 3 = ( 2 + 1 )
80 79 oveq2i ⊢ ( 𝑃 ↑ 3 ) = ( 𝑃 ↑ ( 2 + 1 ) )
81 2nn0 ⊢ 2 ∈ ℕ0
82 expp1 ⊢ ( ( 𝑃 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝑃 ↑ ( 2 + 1 ) ) = ( ( 𝑃 ↑ 2 ) · 𝑃 ) )
83 1 81 82 sylancl ⊢ ( 𝜑 → ( 𝑃 ↑ ( 2 + 1 ) ) = ( ( 𝑃 ↑ 2 ) · 𝑃 ) )
84 80 83 syl5eq ⊢ ( 𝜑 → ( 𝑃 ↑ 3 ) = ( ( 𝑃 ↑ 2 ) · 𝑃 ) )
85 78 84 eqtr4d ⊢ ( 𝜑 → ( 𝑃 · ( 𝑃 ↑ 2 ) ) = ( 𝑃 ↑ 3 ) )
86 85 oveq2d ⊢ ( 𝜑 → ( 2 · ( 𝑃 · ( 𝑃 ↑ 2 ) ) ) = ( 2 · ( 𝑃 ↑ 3 ) ) )
87 77 86 eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) · ( 𝑃 ↑ 2 ) ) = ( 2 · ( 𝑃 ↑ 3 ) ) )
88 54 1 14 3 mul4d ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) · ( 4 · 𝑅 ) ) = ( ( 2 · 4 ) · ( 𝑃 · 𝑅 ) ) )
89 4t2e8 ⊢ ( 4 · 2 ) = 8
90 13 6 89 mulcomli ⊢ ( 2 · 4 ) = 8
91 90 oveq1i ⊢ ( ( 2 · 4 ) · ( 𝑃 · 𝑅 ) ) = ( 8 · ( 𝑃 · 𝑅 ) )
92 88 91 eqtrdi ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) · ( 4 · 𝑅 ) ) = ( 8 · ( 𝑃 · 𝑅 ) ) )
93 87 92 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) · ( 𝑃 ↑ 2 ) ) − ( ( 2 · 𝑃 ) · ( 4 · 𝑅 ) ) ) = ( ( 2 · ( 𝑃 ↑ 3 ) ) − ( 8 · ( 𝑃 · 𝑅 ) ) ) )
94 76 93 eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) = ( ( 2 · ( 𝑃 ↑ 3 ) ) − ( 8 · ( 𝑃 · 𝑅 ) ) ) )
95 94 oveq2d ⊢ ( 𝜑 → ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) = ( 9 · ( ( 2 · ( 𝑃 ↑ 3 ) ) − ( 8 · ( 𝑃 · 𝑅 ) ) ) ) )
96 9t8e72 ⊢ ( 9 · 8 ) = 7 2
97 96 oveq1i ⊢ ( ( 9 · 8 ) · ( 𝑃 · 𝑅 ) ) = ( 7 2 · ( 𝑃 · 𝑅 ) )
98 69 63 72 mulassd ⊢ ( 𝜑 → ( ( 9 · 8 ) · ( 𝑃 · 𝑅 ) ) = ( 9 · ( 8 · ( 𝑃 · 𝑅 ) ) ) )
99 97 98 eqtr3id ⊢ ( 𝜑 → ( 7 2 · ( 𝑃 · 𝑅 ) ) = ( 9 · ( 8 · ( 𝑃 · 𝑅 ) ) ) )
100 99 oveq2d ⊢ ( 𝜑 → ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 7 2 · ( 𝑃 · 𝑅 ) ) ) = ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 9 · ( 8 · ( 𝑃 · 𝑅 ) ) ) ) )
101 75 95 100 3eqtr4d ⊢ ( 𝜑 → ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) = ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
102 67 101 oveq12d ⊢ ( 𝜑 → ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) = ( ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 7 2 · ( 𝑃 · 𝑅 ) ) ) ) )
103 mulcl ⊢ ( ( 8 ∈ ℂ ∧ ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ ) → ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ∈ ℂ )
104 62 71 103 sylancr ⊢ ( 𝜑 → ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ∈ ℂ )
105 mulcl ⊢ ( ( 9 ∈ ℂ ∧ ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ ) → ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ∈ ℂ )
106 68 71 105 sylancr ⊢ ( 𝜑 → ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ∈ ℂ )
107 7nn0 ⊢ 7 ∈ ℕ0
108 107 35 decnncl ⊢ 7 2 ∈ ℕ
109 108 nncni ⊢ 7 2 ∈ ℂ
110 mulcl ⊢ ( ( 7 2 ∈ ℂ ∧ ( 𝑃 · 𝑅 ) ∈ ℂ ) → ( 7 2 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
111 109 72 110 sylancr ⊢ ( 𝜑 → ( 7 2 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
112 104 106 111 subsubd ⊢ ( 𝜑 → ( ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 7 2 · ( 𝑃 · 𝑅 ) ) ) ) = ( ( ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
113 106 104 negsubdi2d ⊢ ( 𝜑 → - ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) = ( ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) )
114 69 63 71 subdird ⊢ ( 𝜑 → ( ( 9 − 8 ) · ( 2 · ( 𝑃 ↑ 3 ) ) ) = ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) )
115 8p1e9 ⊢ ( 8 + 1 ) = 9
116 68 62 20 115 subaddrii ⊢ ( 9 − 8 ) = 1
117 116 oveq1i ⊢ ( ( 9 − 8 ) · ( 2 · ( 𝑃 ↑ 3 ) ) ) = ( 1 · ( 2 · ( 𝑃 ↑ 3 ) ) )
118 71 mulid2d ⊢ ( 𝜑 → ( 1 · ( 2 · ( 𝑃 ↑ 3 ) ) ) = ( 2 · ( 𝑃 ↑ 3 ) ) )
119 117 118 syl5eq ⊢ ( 𝜑 → ( ( 9 − 8 ) · ( 2 · ( 𝑃 ↑ 3 ) ) ) = ( 2 · ( 𝑃 ↑ 3 ) ) )
120 114 119 eqtr3d ⊢ ( 𝜑 → ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) = ( 2 · ( 𝑃 ↑ 3 ) ) )
121 120 negeqd ⊢ ( 𝜑 → - ( ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) = - ( 2 · ( 𝑃 ↑ 3 ) ) )
122 113 121 eqtr3d ⊢ ( 𝜑 → ( ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) = - ( 2 · ( 𝑃 ↑ 3 ) ) )
123 122 oveq1d ⊢ ( 𝜑 → ( ( ( 8 · ( 2 · ( 𝑃 ↑ 3 ) ) ) − ( 9 · ( 2 · ( 𝑃 ↑ 3 ) ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) = ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
124 102 112 123 3eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) = ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
125 7nn ⊢ 7 ∈ ℕ
126 81 125 decnncl ⊢ 2 7 ∈ ℕ
127 126 nncni ⊢ 2 7 ∈ ℂ
128 2 sqcld ⊢ ( 𝜑 → ( 𝑄 ↑ 2 ) ∈ ℂ )
129 mulneg2 ⊢ ( ( 2 7 ∈ ℂ ∧ ( 𝑄 ↑ 2 ) ∈ ℂ ) → ( 2 7 · - ( 𝑄 ↑ 2 ) ) = - ( 2 7 · ( 𝑄 ↑ 2 ) ) )
130 127 128 129 sylancr ⊢ ( 𝜑 → ( 2 7 · - ( 𝑄 ↑ 2 ) ) = - ( 2 7 · ( 𝑄 ↑ 2 ) ) )
131 124 130 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) + ( 2 7 · - ( 𝑄 ↑ 2 ) ) ) = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) + - ( 2 7 · ( 𝑄 ↑ 2 ) ) ) )
132 71 negcld ⊢ ( 𝜑 → - ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
133 mulcl ⊢ ( ( 2 7 ∈ ℂ ∧ ( 𝑄 ↑ 2 ) ∈ ℂ ) → ( 2 7 · ( 𝑄 ↑ 2 ) ) ∈ ℂ )
134 127 128 133 sylancr ⊢ ( 𝜑 → ( 2 7 · ( 𝑄 ↑ 2 ) ) ∈ ℂ )
135 132 111 134 addsubd ⊢ ( 𝜑 → ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
136 132 111 addcld ⊢ ( 𝜑 → ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) ∈ ℂ )
137 136 134 negsubd ⊢ ( 𝜑 → ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) + - ( 2 7 · ( 𝑄 ↑ 2 ) ) ) = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) )
138 135 137 5 3eqtr4d ⊢ ( 𝜑 → ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) + - ( 2 7 · ( 𝑄 ↑ 2 ) ) ) = 𝑉 )
139 131 138 eqtr2d ⊢ ( 𝜑 → 𝑉 = ( ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) + ( 2 7 · - ( 𝑄 ↑ 2 ) ) ) )
140 53 139 jca ⊢ ( 𝜑 → ( 𝑈 = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ∧ 𝑉 = ( ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) + ( 2 7 · - ( 𝑄 ↑ 2 ) ) ) ) )