Theorem 3cubeslem3

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

	Ref	Expression
Hypothesis	3cubeslem1.a	|- ( ph -> A e. QQ )
Assertion	3cubeslem3	|- ( ph -> ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3cubeslem1.a	|- ( ph -> A e. QQ )
2	1	3cubeslem3l	|- ( ph -> ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( A ^ 7 ) x. ( 3 ^ 9 ) ) + ( ( ( A ^ 6 ) x. ( 3 ^ 9 ) ) + ( ( ( A ^ 5 ) x. ( ( 3 ^ 8 ) + ( 3 ^ 8 ) ) ) + ( ( ( A ^ 4 ) x. ( ( ( 3 ^ 7 ) x. 2 ) + ( 3 ^ 6 ) ) ) + ( ( ( A ^ 3 ) x. ( ( 3 ^ 6 ) + ( 3 ^ 6 ) ) ) + ( ( ( A ^ 2 ) x. ( 3 ^ 5 ) ) + ( A x. ( 3 ^ 3 ) ) ) ) ) ) ) ) )
3	1	3cubeslem3r	|- ( ph -> ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) = ( ( ( A ^ 7 ) x. ( 3 ^ 9 ) ) + ( ( ( A ^ 6 ) x. ( 3 ^ 9 ) ) + ( ( ( A ^ 5 ) x. ( ( 3 ^ 8 ) + ( 3 ^ 8 ) ) ) + ( ( ( A ^ 4 ) x. ( ( ( 3 ^ 7 ) x. 2 ) + ( 3 ^ 6 ) ) ) + ( ( ( A ^ 3 ) x. ( ( 3 ^ 6 ) + ( 3 ^ 6 ) ) ) + ( ( ( A ^ 2 ) x. ( 3 ^ 5 ) ) + ( A x. ( 3 ^ 3 ) ) ) ) ) ) ) ) )
4	2 3	eqtr4d	|- ( ph -> ( A x. ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) ^ 3 ) + ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) ^ 3 ) ) + ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) ^ 3 ) ) )