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
|- ( A e. QQ <-> E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) )

Proof

Step Hyp Ref Expression
1 3nn
 |-  3 e. NN
2 1 a1i
 |-  ( -. ( 3 ^ 3 ) e. NN -> 3 e. NN )
3 3nn0
 |-  3 e. NN0
4 3 a1i
 |-  ( -. ( 3 ^ 3 ) e. NN -> 3 e. NN0 )
5 2 4 nnexpcld
 |-  ( -. ( 3 ^ 3 ) e. NN -> ( 3 ^ 3 ) e. NN )
6 5 pm2.18i
 |-  ( 3 ^ 3 ) e. NN
7 nnq
 |-  ( ( 3 ^ 3 ) e. NN -> ( 3 ^ 3 ) e. QQ )
8 6 7 mp1i
 |-  ( A e. QQ -> ( 3 ^ 3 ) e. QQ )
9 qexpcl
 |-  ( ( A e. QQ /\ 3 e. NN0 ) -> ( A ^ 3 ) e. QQ )
10 3 9 mpan2
 |-  ( A e. QQ -> ( A ^ 3 ) e. QQ )
11 qmulcl
 |-  ( ( ( 3 ^ 3 ) e. QQ /\ ( A ^ 3 ) e. QQ ) -> ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ )
12 8 10 11 syl2anc
 |-  ( A e. QQ -> ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ )
13 1nn
 |-  1 e. NN
14 nnq
 |-  ( 1 e. NN -> 1 e. QQ )
15 13 14 ax-mp
 |-  1 e. QQ
16 qsubcl
 |-  ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ /\ 1 e. QQ ) -> ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) e. QQ )
17 12 15 16 sylancl
 |-  ( A e. QQ -> ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) e. QQ )
18 qsqcl
 |-  ( A e. QQ -> ( A ^ 2 ) e. QQ )
19 qmulcl
 |-  ( ( ( 3 ^ 3 ) e. QQ /\ ( A ^ 2 ) e. QQ ) -> ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) e. QQ )
20 8 18 19 syl2anc
 |-  ( A e. QQ -> ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) e. QQ )
21 nnq
 |-  ( 3 e. NN -> 3 e. QQ )
22 1 21 ax-mp
 |-  3 e. QQ
23 qsqcl
 |-  ( 3 e. QQ -> ( 3 ^ 2 ) e. QQ )
24 22 23 mp1i
 |-  ( A e. QQ -> ( 3 ^ 2 ) e. QQ )
25 qmulcl
 |-  ( ( ( 3 ^ 2 ) e. QQ /\ A e. QQ ) -> ( ( 3 ^ 2 ) x. A ) e. QQ )
26 24 25 mpancom
 |-  ( A e. QQ -> ( ( 3 ^ 2 ) x. A ) e. QQ )
27 qaddcl
 |-  ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) e. QQ /\ ( ( 3 ^ 2 ) x. A ) e. QQ ) -> ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ )
28 20 26 27 syl2anc
 |-  ( A e. QQ -> ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ )
29 qaddcl
 |-  ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ /\ 3 e. QQ ) -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) e. QQ )
30 28 22 29 sylancl
 |-  ( A e. QQ -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) e. QQ )
31 id
 |-  ( A e. QQ -> A e. QQ )
32 31 3cubeslem2
 |-  ( A e. QQ -> -. ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = 0 )
33 32 neqned
 |-  ( A e. QQ -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) =/= 0 )
34 qdivcl
 |-  ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) =/= 0 ) -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ )
35 17 30 33 34 syl3anc
 |-  ( A e. QQ -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ )
36 qnegcl
 |-  ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ -> -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ )
37 12 36 syl
 |-  ( A e. QQ -> -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ )
38 qaddcl
 |-  ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) e. QQ /\ ( ( 3 ^ 2 ) x. A ) e. QQ ) -> ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ )
39 37 26 38 syl2anc
 |-  ( A e. QQ -> ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ )
40 qaddcl
 |-  ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ /\ 1 e. QQ ) -> ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) e. QQ )
41 39 15 40 sylancl
 |-  ( A e. QQ -> ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) e. QQ )
42 qdivcl
 |-  ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) =/= 0 ) -> ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ )
43 41 30 33 42 syl3anc
 |-  ( A e. QQ -> ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ )
44 qdivcl
 |-  ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) =/= 0 ) -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ )
45 28 30 33 44 syl3anc
 |-  ( A e. QQ -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ )
46 31 3cubeslem4
 |-  ( A e. QQ -> A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )
47 oveq1
 |-  ( a = ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( a ^ 3 ) = ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) )
48 47 oveq1d
 |-  ( a = ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( ( a ^ 3 ) + ( b ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( b ^ 3 ) ) )
49 48 oveq1d
 |-  ( a = ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) )
50 49 eqeq2d
 |-  ( a = ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) <-> A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) ) )
51 oveq1
 |-  ( b = ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( b ^ 3 ) = ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) )
52 51 oveq2d
 |-  ( b = ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( b ^ 3 ) ) = ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )
53 52 oveq1d
 |-  ( b = ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( c ^ 3 ) ) )
54 53 eqeq2d
 |-  ( b = ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) <-> A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( c ^ 3 ) ) ) )
55 oveq1
 |-  ( c = ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( c ^ 3 ) = ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) )
56 55 oveq2d
 |-  ( c = ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( c ^ 3 ) ) = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) )
57 56 eqeq2d
 |-  ( c = ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) -> ( A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( c ^ 3 ) ) <-> A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) ) )
58 50 54 57 rspc3ev
 |-  ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ /\ ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ /\ ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) e. QQ ) /\ A = ( ( ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) - 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) + ( ( ( ( -u ( ( 3 ^ 3 ) x. ( A ^ 3 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 1 ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) + ( ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) / ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) ) ^ 3 ) ) ) -> E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) )
59 35 43 45 46 58 syl31anc
 |-  ( A e. QQ -> E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) )
60 3anass
 |-  ( ( a e. QQ /\ b e. QQ /\ c e. QQ ) <-> ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) )
61 qexpcl
 |-  ( ( a e. QQ /\ 3 e. NN0 ) -> ( a ^ 3 ) e. QQ )
62 3 61 mpan2
 |-  ( a e. QQ -> ( a ^ 3 ) e. QQ )
63 simprl
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> b e. QQ )
64 qexpcl
 |-  ( ( b e. QQ /\ 3 e. NN0 ) -> ( b ^ 3 ) e. QQ )
65 63 3 64 sylancl
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> ( b ^ 3 ) e. QQ )
66 qaddcl
 |-  ( ( ( a ^ 3 ) e. QQ /\ ( b ^ 3 ) e. QQ ) -> ( ( a ^ 3 ) + ( b ^ 3 ) ) e. QQ )
67 62 65 66 syl2an2r
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> ( ( a ^ 3 ) + ( b ^ 3 ) ) e. QQ )
68 simprr
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> c e. QQ )
69 qexpcl
 |-  ( ( c e. QQ /\ 3 e. NN0 ) -> ( c ^ 3 ) e. QQ )
70 68 3 69 sylancl
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> ( c ^ 3 ) e. QQ )
71 qaddcl
 |-  ( ( ( ( a ^ 3 ) + ( b ^ 3 ) ) e. QQ /\ ( c ^ 3 ) e. QQ ) -> ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) e. QQ )
72 67 70 71 syl2anc
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) e. QQ )
73 eleq1a
 |-  ( ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) e. QQ -> ( A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) -> A e. QQ ) )
74 72 73 syl
 |-  ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> ( A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) -> A e. QQ ) )
75 74 a1i
 |-  ( T. -> ( ( a e. QQ /\ ( b e. QQ /\ c e. QQ ) ) -> ( A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) -> A e. QQ ) ) )
76 60 75 syl5bi
 |-  ( T. -> ( ( a e. QQ /\ b e. QQ /\ c e. QQ ) -> ( A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) -> A e. QQ ) ) )
77 76 rexlimdv3d
 |-  ( T. -> ( E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) -> A e. QQ ) )
78 77 mptru
 |-  ( E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) -> A e. QQ )
79 59 78 impbii
 |-  ( A e. QQ <-> E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) )