Metamath Proof Explorer

Theorem 3cubes

Description: Every rational number is a sum of three rational cubes. See S. Ryley, The Ladies' Diary 122 (1825), 35. (Contributed by Igor Ieskov, 22-Jan-2024)

Ref Expression
Assertion 3cubes ( ๐ด โˆˆ โ„š โ†” โˆƒ ๐‘Ž โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) )

Proof

Step Hyp Ref Expression
1 3nn โŠข 3 โˆˆ โ„•
2 1 a1i โŠข ( ยฌ ( 3 โ†‘ 3 ) โˆˆ โ„• โ†’ 3 โˆˆ โ„• )
3 3nn0 โŠข 3 โˆˆ โ„•0
4 3 a1i โŠข ( ยฌ ( 3 โ†‘ 3 ) โˆˆ โ„• โ†’ 3 โˆˆ โ„•0 )
5 2 4 nnexpcld โŠข ( ยฌ ( 3 โ†‘ 3 ) โˆˆ โ„• โ†’ ( 3 โ†‘ 3 ) โˆˆ โ„• )
6 5 pm2.18i โŠข ( 3 โ†‘ 3 ) โˆˆ โ„•
7 nnq โŠข ( ( 3 โ†‘ 3 ) โˆˆ โ„• โ†’ ( 3 โ†‘ 3 ) โˆˆ โ„š )
8 6 7 mp1i โŠข ( ๐ด โˆˆ โ„š โ†’ ( 3 โ†‘ 3 ) โˆˆ โ„š )
9 qexpcl โŠข ( ( ๐ด โˆˆ โ„š โˆง 3 โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ 3 ) โˆˆ โ„š )
10 3 9 mpan2 โŠข ( ๐ด โˆˆ โ„š โ†’ ( ๐ด โ†‘ 3 ) โˆˆ โ„š )
11 qmulcl โŠข ( ( ( 3 โ†‘ 3 ) โˆˆ โ„š โˆง ( ๐ด โ†‘ 3 ) โˆˆ โ„š ) โ†’ ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š )
12 8 10 11 syl2anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š )
13 1nn โŠข 1 โˆˆ โ„•
14 nnq โŠข ( 1 โˆˆ โ„• โ†’ 1 โˆˆ โ„š )
15 13 14 ax-mp โŠข 1 โˆˆ โ„š
16 qsubcl โŠข ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š โˆง 1 โˆˆ โ„š ) โ†’ ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) โˆˆ โ„š )
17 12 15 16 sylancl โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) โˆˆ โ„š )
18 qsqcl โŠข ( ๐ด โˆˆ โ„š โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„š )
19 qmulcl โŠข ( ( ( 3 โ†‘ 3 ) โˆˆ โ„š โˆง ( ๐ด โ†‘ 2 ) โˆˆ โ„š ) โ†’ ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) โˆˆ โ„š )
20 8 18 19 syl2anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) โˆˆ โ„š )
21 nnq โŠข ( 3 โˆˆ โ„• โ†’ 3 โˆˆ โ„š )
22 1 21 ax-mp โŠข 3 โˆˆ โ„š
23 qsqcl โŠข ( 3 โˆˆ โ„š โ†’ ( 3 โ†‘ 2 ) โˆˆ โ„š )
24 22 23 mp1i โŠข ( ๐ด โˆˆ โ„š โ†’ ( 3 โ†‘ 2 ) โˆˆ โ„š )
25 qmulcl โŠข ( ( ( 3 โ†‘ 2 ) โˆˆ โ„š โˆง ๐ด โˆˆ โ„š ) โ†’ ( ( 3 โ†‘ 2 ) ยท ๐ด ) โˆˆ โ„š )
26 24 25 mpancom โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( 3 โ†‘ 2 ) ยท ๐ด ) โˆˆ โ„š )
27 qaddcl โŠข ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) โˆˆ โ„š โˆง ( ( 3 โ†‘ 2 ) ยท ๐ด ) โˆˆ โ„š ) โ†’ ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š )
28 20 26 27 syl2anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š )
29 qaddcl โŠข ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š โˆง 3 โˆˆ โ„š ) โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โˆˆ โ„š )
30 28 22 29 sylancl โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โˆˆ โ„š )
31 id โŠข ( ๐ด โˆˆ โ„š โ†’ ๐ด โˆˆ โ„š )
32 31 3cubeslem2 โŠข ( ๐ด โˆˆ โ„š โ†’ ยฌ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) = 0 )
33 32 neqned โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โ‰  0 )
34 qdivcl โŠข ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โ‰  0 ) โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š )
35 17 30 33 34 syl3anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š )
36 qnegcl โŠข ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š โ†’ - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š )
37 12 36 syl โŠข ( ๐ด โˆˆ โ„š โ†’ - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š )
38 qaddcl โŠข ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆˆ โ„š โˆง ( ( 3 โ†‘ 2 ) ยท ๐ด ) โˆˆ โ„š ) โ†’ ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š )
39 37 26 38 syl2anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š )
40 qaddcl โŠข ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š โˆง 1 โˆˆ โ„š ) โ†’ ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) โˆˆ โ„š )
41 39 15 40 sylancl โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) โˆˆ โ„š )
42 qdivcl โŠข ( ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โ‰  0 ) โ†’ ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š )
43 41 30 33 42 syl3anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š )
44 qdivcl โŠข ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) โ‰  0 ) โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š )
45 28 30 33 44 syl3anc โŠข ( ๐ด โˆˆ โ„š โ†’ ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š )
46 31 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 ) ) )
47 oveq1 โŠข ( ๐‘Ž = ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ๐‘Ž โ†‘ 3 ) = ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 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 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) )
49 48 oveq1d โŠข ( ๐‘Ž = ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) = ( ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) )
50 49 eqeq2d โŠข ( ๐‘Ž = ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†” ๐ด = ( ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) ) )
51 oveq1 โŠข ( ๐‘ = ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ๐‘ โ†‘ 3 ) = ( ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) )
52 51 oveq2d โŠข ( ๐‘ = ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) = ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) ) )
53 52 oveq1d โŠข ( ๐‘ = ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) = ( ( ( ( ( ( ( 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 ) ) )
54 53 eqeq2d โŠข ( ๐‘ = ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ๐ด = ( ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†” ๐ด = ( ( ( ( ( ( ( 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 ) ) ) )
55 oveq1 โŠข ( ๐‘ = ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ๐‘ โ†‘ 3 ) = ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†‘ 3 ) )
56 55 oveq2d โŠข ( ๐‘ = ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ( ( ( ( ( ( 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 ) ยท ( ๐ด โ†‘ 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 ) ) )
57 56 eqeq2d โŠข ( ๐‘ = ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โ†’ ( ๐ด = ( ( ( ( ( ( ( 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 ) ยท ( ๐ด โ†‘ 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 ) ) ) )
58 50 54 57 rspc3ev โŠข ( ( ( ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) โˆ’ 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š โˆง ( ( ( - ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 3 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 1 ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š โˆง ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) / ( ( ( ( 3 โ†‘ 3 ) ยท ( ๐ด โ†‘ 2 ) ) + ( ( 3 โ†‘ 2 ) ยท ๐ด ) ) + 3 ) ) โˆˆ โ„š ) โˆง ๐ด = ( ( ( ( ( ( ( 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 ) ) )
59 35 43 45 46 58 syl31anc โŠข ( ๐ด โˆˆ โ„š โ†’ โˆƒ ๐‘Ž โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) )
60 3anass โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) โ†” ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) )
61 qexpcl โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง 3 โˆˆ โ„•0 ) โ†’ ( ๐‘Ž โ†‘ 3 ) โˆˆ โ„š )
62 3 61 mpan2 โŠข ( ๐‘Ž โˆˆ โ„š โ†’ ( ๐‘Ž โ†‘ 3 ) โˆˆ โ„š )
63 simprl โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ๐‘ โˆˆ โ„š )
64 qexpcl โŠข ( ( ๐‘ โˆˆ โ„š โˆง 3 โˆˆ โ„•0 ) โ†’ ( ๐‘ โ†‘ 3 ) โˆˆ โ„š )
65 63 3 64 sylancl โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ( ๐‘ โ†‘ 3 ) โˆˆ โ„š )
66 qaddcl โŠข ( ( ( ๐‘Ž โ†‘ 3 ) โˆˆ โ„š โˆง ( ๐‘ โ†‘ 3 ) โˆˆ โ„š ) โ†’ ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) โˆˆ โ„š )
67 62 65 66 syl2an2r โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) โˆˆ โ„š )
68 simprr โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ๐‘ โˆˆ โ„š )
69 qexpcl โŠข ( ( ๐‘ โˆˆ โ„š โˆง 3 โˆˆ โ„•0 ) โ†’ ( ๐‘ โ†‘ 3 ) โˆˆ โ„š )
70 68 3 69 sylancl โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ( ๐‘ โ†‘ 3 ) โˆˆ โ„š )
71 qaddcl โŠข ( ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) โˆˆ โ„š โˆง ( ๐‘ โ†‘ 3 ) โˆˆ โ„š ) โ†’ ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โˆˆ โ„š )
72 67 70 71 syl2anc โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โˆˆ โ„š )
73 eleq1a โŠข ( ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โˆˆ โ„š โ†’ ( ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†’ ๐ด โˆˆ โ„š ) )
74 72 73 syl โŠข ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ( ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†’ ๐ด โˆˆ โ„š ) )
75 74 a1i โŠข ( โŠค โ†’ ( ( ๐‘Ž โˆˆ โ„š โˆง ( ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) ) โ†’ ( ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†’ ๐ด โˆˆ โ„š ) ) )
76 60 75 biimtrid โŠข ( โŠค โ†’ ( ( ๐‘Ž โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š โˆง ๐‘ โˆˆ โ„š ) โ†’ ( ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†’ ๐ด โˆˆ โ„š ) ) )
77 76 rexlimdv3d โŠข ( โŠค โ†’ ( โˆƒ ๐‘Ž โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†’ ๐ด โˆˆ โ„š ) )
78 77 mptru โŠข ( โˆƒ ๐‘Ž โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) โ†’ ๐ด โˆˆ โ„š )
79 59 78 impbii โŠข ( ๐ด โˆˆ โ„š โ†” โˆƒ ๐‘Ž โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š โˆƒ ๐‘ โˆˆ โ„š ๐ด = ( ( ( ๐‘Ž โ†‘ 3 ) + ( ๐‘ โ†‘ 3 ) ) + ( ๐‘ โ†‘ 3 ) ) )