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	$⊢ φ \to A \in ℚ$
	Assertion	3cubeslem4	$⊢ φ \to A = {(\frac{3^{3} A^{3} - 1}{3^{3} A^{2} + 3^{2} A + 3})}^{3} + {(\frac{(- 3^{3} A^{3}) + 3^{2} A + 1}{3^{3} A^{2} + 3^{2} A + 3})}^{3} + {(\frac{3^{3} A^{2} + 3^{2} A}{3^{3} A^{2} + 3^{2} A + 3})}^{3}$

Proof

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

Metamath Proof Explorer

Theorem 3cubeslem4

Proof