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