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 biimtrid 
 |-  ( 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 ) ) )