Theorem 3cubeslem3

Description: Lemma for 3cubes . (Contributed by Igor Ieskov, 22-Jan-2024)

	Ref	Expression
Hypothesis	3cubeslem1.a	$$⊢\phi \to A\in \mathbb{Q}$$
Assertion	3cubeslem3	$$⊢\phi \to A{\left(3^3{A}^2+3^{2}A+3\right)}^3={\left(3^3{A}^3-1\right)}^3+{\left(\left(-3^3{A}^3\right)+3^{2}A+1\right)}^3+{\left(3^3{A}^2+3^{2}A\right)}^3$$

Proof

Step	Hyp	Ref	Expression
1		3cubeslem1.a	$$⊢\phi \to A\in \mathbb{Q}$$
2	1	3cubeslem3l	$$⊢\phi \to A{\left(3^3{A}^2+3^{2}A+3\right)}^3=A^7{3}^9+A^6{3}^9+\left(A^5\left(3^8+3^8\right)+A^4\left(3^7\cdot 2+3^6\right)+\left(A^3\left(3^6+3^6\right)+A^2{3}^5+A{3}^3\right)\right)$$
3	1	3cubeslem3r	$$⊢\phi \to {\left(3^3{A}^3-1\right)}^3+{\left(\left(-3^3{A}^3\right)+3^{2}A+1\right)}^3+{\left(3^3{A}^2+3^{2}A\right)}^3=A^7{3}^9+A^6{3}^9+\left(A^5\left(3^8+3^8\right)+A^4\left(3^7\cdot 2+3^6\right)+\left(A^3\left(3^6+3^6\right)+A^2{3}^5+A{3}^3\right)\right)$$
4	2 3	eqtr4d	$$⊢\phi \to A{\left(3^3{A}^2+3^{2}A+3\right)}^3={\left(3^3{A}^3-1\right)}^3+{\left(\left(-3^3{A}^3\right)+3^{2}A+1\right)}^3+{\left(3^3{A}^2+3^{2}A\right)}^3$$