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 ⊢φ→A∈ℚ
Assertion 3cubeslem4 ⊢φ→A=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+33⁢A2+32⁢A33⁢A2+32⁢A+33

Proof

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