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 eqtrid ( ( 𝑃 ↑ 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 eqtrid ( 𝜑 → ( 𝑃 ↑ 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 eqtrid ( 𝜑 → ( ( 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 ) ) ) ) )