Metamath Proof Explorer

Theorem 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 โˆˆ โ„•0
5 4 a1i โŠข ( โŠค โ†’ 3 โˆˆ โ„•0 )
6 3 5 reexpcld โŠข ( โŠค โ†’ ( 3 โ†‘ 3 ) โˆˆ โ„ )
7 6 mptru โŠข ( 3 โ†‘ 3 ) โˆˆ โ„
8 7 a1i โŠข ( ๐œ‘ โ†’ ( 3 โ†‘ 3 ) โˆˆ โ„ )
9 qre โŠข ( ๐ด โˆˆ โ„š โ†’ ๐ด โˆˆ โ„ )
10 4 a1i โŠข ( ๐ด โˆˆ โ„š โ†’ 3 โˆˆ โ„•0 )
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 โˆˆ โ„•0 )
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 ) ) )