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