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 ( 𝜑𝐴 ∈ ℚ )
Assertion 3cubeslem4 ( 𝜑𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) )

Proof

Step Hyp Ref Expression
1 3cubeslem1.a ( 𝜑𝐴 ∈ ℚ )
2 3re 3 ∈ ℝ
3 2 a1i ( ⊤ → 3 ∈ ℝ )
4 3nn0 3 ∈ ℕ0
5 4 a1i ( ⊤ → 3 ∈ ℕ0 )
6 3 5 reexpcld ( ⊤ → ( 3 ↑ 3 ) ∈ ℝ )
7 6 mptru ( 3 ↑ 3 ) ∈ ℝ
8 7 a1i ( 𝜑 → ( 3 ↑ 3 ) ∈ ℝ )
9 qre ( 𝐴 ∈ ℚ → 𝐴 ∈ ℝ )
10 4 a1i ( 𝐴 ∈ ℚ → 3 ∈ ℕ0 )
11 9 10 reexpcld ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 3 ) ∈ ℝ )
12 1 11 syl ( 𝜑 → ( 𝐴 ↑ 3 ) ∈ ℝ )
13 8 12 remulcld ( 𝜑 → ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℝ )
14 1red ( 𝜑 → 1 ∈ ℝ )
15 13 14 resubcld ( 𝜑 → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ∈ ℝ )
16 15 recnd ( 𝜑 → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ∈ ℂ )
17 4 a1i ( 𝜑 → 3 ∈ ℕ0 )
18 16 17 expcld ( 𝜑 → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) ∈ ℂ )
19 13 renegcld ( 𝜑 → - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℝ )
20 19 recnd ( 𝜑 → - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) ∈ ℂ )
21 2 a1i ( 𝜑 → 3 ∈ ℝ )
22 21 recnd ( 𝜑 → 3 ∈ ℂ )
23 22 sqcld ( 𝜑 → ( 3 ↑ 2 ) ∈ ℂ )
24 qcn ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
25 1 24 syl ( 𝜑𝐴 ∈ ℂ )
26 23 25 mulcld ( 𝜑 → ( ( 3 ↑ 2 ) · 𝐴 ) ∈ ℂ )
27 20 26 addcld ( 𝜑 → ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℂ )
28 1cnd ( 𝜑 → 1 ∈ ℂ )
29 27 28 addcld ( 𝜑 → ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ∈ ℂ )
30 29 17 expcld ( 𝜑 → ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ∈ ℂ )
31 8 recnd ( 𝜑 → ( 3 ↑ 3 ) ∈ ℂ )
32 25 sqcld ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
33 31 32 mulcld ( 𝜑 → ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
34 33 26 addcld ( 𝜑 → ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ∈ ℂ )
35 34 22 addcld ( 𝜑 → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ∈ ℂ )
36 35 17 expcld ( 𝜑 → ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ∈ ℂ )
37 1 3cubeslem2 ( 𝜑 → ¬ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) = 0 )
38 37 neqned ( 𝜑 → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ≠ 0 )
39 3z 3 ∈ ℤ
40 39 a1i ( 𝜑 → 3 ∈ ℤ )
41 35 38 40 expne0d ( 𝜑 → ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ≠ 0 )
42 18 30 36 41 divdird ( 𝜑 → ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) = ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) )
43 42 oveq1d ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) )
44 18 30 addcld ( 𝜑 → ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) ∈ ℂ )
45 34 17 expcld ( 𝜑 → ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) ∈ ℂ )
46 44 45 36 41 divdird ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) + ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) )
47 16 35 38 17 expdivd ( 𝜑 → ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) = ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) )
48 47 oveq1d ( 𝜑 → ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) )
49 48 oveq1d ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) )
50 29 35 38 17 expdivd ( 𝜑 → ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) = ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) )
51 50 oveq2d ( 𝜑 → ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) )
52 51 oveq1d ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) )
53 34 35 38 17 expdivd ( 𝜑 → ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) = ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) )
54 53 oveq2d ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) )
55 49 52 54 3eqtrd ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) ) )
56 43 46 55 3eqtr4rd ( 𝜑 → ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) + ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) )
57 1 3cubeslem3 ( 𝜑 → ( 𝐴 · ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) = ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) + ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) ) )
58 57 oveq1d ( 𝜑 → ( ( 𝐴 · ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) + ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) )
59 25 36 41 divcan4d ( 𝜑 → ( ( 𝐴 · ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) / ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) = 𝐴 )
60 56 58 59 3eqtr2rd ( 𝜑𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) )