Metamath Proof Explorer

Theorem 3cubeslem4

Description: Lemma for 3cubes . This is Ryley's explicit formula for decomposing a rational A into a sum of three rational cubes. (Contributed by Igor Ieskov, 22-Jan-2024)

Ref Expression
Hypothesis 3cubeslem1.a 
|- ( ph -> A e. QQ )
Assertion 3cubeslem4 
|- ( ph -> A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )

Proof

Step Hyp Ref Expression
1 3cubeslem1.a 
 |-  ( ph -> A e. QQ )
2 3re 
 |-  3 e. RR
3 2 a1i 
 |-  ( T. -> 3 e. RR )
4 3nn0 
 |-  3 e. NN0
5 4 a1i 
 |-  ( T. -> 3 e. NN0 )
6 3 5 reexpcld 
 |-  ( T. -> ( 3 ^ 3 ) e. RR )
7 6 mptru 
 |-  ( 3 ^ 3 ) e. RR
8 7 a1i 
 |-  ( ph -> ( 3 ^ 3 ) e. RR )
9 qre 
 |-  ( A e. QQ -> A e. RR )
10 4 a1i 
 |-  ( A e. QQ -> 3 e. NN0 )
11 9 10 reexpcld 
 |-  ( A e. QQ -> ( A ^ 3 ) e. RR )
12 1 11 syl 
 |-  ( ph -> ( A ^ 3 ) e. RR )
13 8 12 remulcld 
 |-  ( ph -> ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. RR )
14 1red 
 |-  ( ph -> 1 e. RR )
15 13 14 resubcld 
 |-  ( ph -> ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) e. RR )
16 15 recnd 
 |-  ( ph -> ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) e. CC )
17 4 a1i 
 |-  ( ph -> 3 e. NN0 )
18 16 17 expcld 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) e. CC )
19 13 renegcld 
 |-  ( ph -> -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. RR )
20 19 recnd 
 |-  ( ph -> -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. CC )
21 2 a1i 
 |-  ( ph -> 3 e. RR )
22 21 recnd 
 |-  ( ph -> 3 e. CC )
23 22 sqcld 
 |-  ( ph -> ( 3 ^ 2 ) e. CC )
24 qcn 
 |-  ( A e. QQ -> A e. CC )
25 1 24 syl 
 |-  ( ph -> A e. CC )
26 23 25 mulcld 
 |-  ( ph -> ( ( 3 ^ 2 ) x. A ) e. CC )
27 20 26 addcld 
 |-  ( ph -> ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. CC )
28 1cnd 
 |-  ( ph -> 1 e. CC )
29 27 28 addcld 
 |-  ( ph -> ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) e. CC )
30 29 17 expcld 
 |-  ( ph -> ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) e. CC )
31 8 recnd 
 |-  ( ph -> ( 3 ^ 3 ) e. CC )
32 25 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
33 31 32 mulcld 
 |-  ( ph -> ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) e. CC )
34 33 26 addcld 
 |-  ( ph -> ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. CC )
35 34 22 addcld 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) e. CC )
36 35 17 expcld 
 |-  ( ph -> ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) e. CC )
37 1 3cubeslem2 
 |-  ( ph -> -. ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = 0 )
38 37 neqned 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) =/= 0 )
39 3z 
 |-  3 e. ZZ
40 39 a1i 
 |-  ( ph -> 3 e. ZZ )
41 35 38 40 expne0d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) =/= 0 )
42 18 30 36 41 divdird 
 |-  ( ph -> ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) )
43 42 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) )
44 18 30 addcld 
 |-  ( ph -> ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) e. CC )
45 34 17 expcld 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) e. CC )
46 44 45 36 41 divdird 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) )
47 16 35 38 17 expdivd 
 |-  ( ph -> ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) = ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) )
48 47 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )
49 48 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )
50 29 35 38 17 expdivd 
 |-  ( ph -> ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) = ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) )
51 50 oveq2d 
 |-  ( ph -> ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) )
52 51 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )
53 34 35 38 17 expdivd 
 |-  ( ph -> ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) = ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) )
54 53 oveq2d 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) )
55 49 52 54 3eqtrd 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) ) )
56 43 46 55 3eqtr4rd 
 |-  ( ph -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) )
57 1 3cubeslem3 
 |-  ( ph -> ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) )
58 57 oveq1d 
 |-  ( ph -> ( ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) )
59 25 36 41 divcan4d 
 |-  ( ph -> ( ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) / ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = A )
60 56 58 59 3eqtr2rd 
 |-  ( ph -> A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )