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	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
	Assertion	3cubeslem4	⊢ ( 𝜑 → 𝐴 = ( ( ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) − 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) + ( ( ( ( - ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 3 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 1 ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) + ( ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) / ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) ) ↑ 3 ) ) )

Proof

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

Metamath Proof Explorer

Theorem 3cubeslem4

Proof