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 syl5bi ( ⊤ → ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ ) → ( 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) ) )
77 76 rexlimdv3d ( ⊤ → ( ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ ) )
78 77 mptru ( ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) → 𝐴 ∈ ℚ )
79 59 78 impbii ( 𝐴 ∈ ℚ ↔ ∃ 𝑎 ∈ ℚ ∃ 𝑏 ∈ ℚ ∃ 𝑐 ∈ ℚ 𝐴 = ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) + ( 𝑐 ↑ 3 ) ) )