Metamath Proof Explorer

Theorem quartlem1

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

Ref Expression
Hypotheses quartlem1.p 
|- ( ph -> P e. CC )
quartlem1.q 
|- ( ph -> Q e. CC )
quartlem1.r 
|- ( ph -> R e. CC )
quartlem1.u 
|- ( ph -> U = ( ( P ^ 2 ) + ( ; 1 2 x. R ) ) )
quartlem1.v 
|- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) + ( ; 7 2 x. ( P x. R ) ) ) )
Assertion quartlem1 
|- ( ph -> ( U = ( ( ( 2 x. P ) ^ 2 ) - ( 3 x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) /\ V = ( ( ( 2 x. ( ( 2 x. P ) ^ 3 ) ) - ( 9 x. ( ( 2 x. P ) x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) ) + ( ; 2 7 x. -u ( Q ^ 2 ) ) ) ) )

Proof

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