Theorem 3cubeslem3

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

	Ref	Expression
Hypothesis	3cubeslem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
Assertion	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 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3cubeslem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
2	1	3cubeslem3l	⊢ ( 𝜑 → ( 𝐴 · ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ↑ 3 ) ) = ( ( ( 𝐴 ↑ 7 ) · ( 3 ↑ 9 ) ) + ( ( ( 𝐴 ↑ 6 ) · ( 3 ↑ 9 ) ) + ( ( ( 𝐴 ↑ 5 ) · ( ( 3 ↑ 8 ) + ( 3 ↑ 8 ) ) ) + ( ( ( 𝐴 ↑ 4 ) · ( ( ( 3 ↑ 7 ) · 2 ) + ( 3 ↑ 6 ) ) ) + ( ( ( 𝐴 ↑ 3 ) · ( ( 3 ↑ 6 ) + ( 3 ↑ 6 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 3 ↑ 5 ) ) + ( 𝐴 · ( 3 ↑ 3 ) ) ) ) ) ) ) ) )
3	1	3cubeslem3r	⊢ ( 𝜑 → ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) ↑ 3 ) + ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) ↑ 3 ) ) + ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) ↑ 3 ) ) = ( ( ( 𝐴 ↑ 7 ) · ( 3 ↑ 9 ) ) + ( ( ( 𝐴 ↑ 6 ) · ( 3 ↑ 9 ) ) + ( ( ( 𝐴 ↑ 5 ) · ( ( 3 ↑ 8 ) + ( 3 ↑ 8 ) ) ) + ( ( ( 𝐴 ↑ 4 ) · ( ( ( 3 ↑ 7 ) · 2 ) + ( 3 ↑ 6 ) ) ) + ( ( ( 𝐴 ↑ 3 ) · ( ( 3 ↑ 6 ) + ( 3 ↑ 6 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 3 ↑ 5 ) ) + ( 𝐴 · ( 3 ↑ 3 ) ) ) ) ) ) ) ) )
4	2 3	eqtr4d	⊢ ( 𝜑 → ( 𝐴 · ( ( ( ( ( 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 ) ) )