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∈ℚ↔∃a∈ℚ∃b∈ℚ∃c∈ℚA=a3+b3+c3

Proof

Step Hyp Ref Expression
1 3nn ⊢3∈ℕ
2 1 a1i ⊢¬33∈ℕ→3∈ℕ
3 3nn0 ⊢3∈ℕ0
4 3 a1i ⊢¬33∈ℕ→3∈ℕ0
5 2 4 nnexpcld ⊢¬33∈ℕ→33∈ℕ
6 5 pm2.18i ⊢33∈ℕ
7 nnq ⊢33∈ℕ→33∈ℚ
8 6 7 mp1i ⊢A∈ℚ→33∈ℚ
9 qexpcl ⊢A∈ℚ∧3∈ℕ0→A3∈ℚ
10 3 9 mpan2 ⊢A∈ℚ→A3∈ℚ
11 qmulcl ⊢33∈ℚ∧A3∈ℚ→33⁢A3∈ℚ
12 8 10 11 syl2anc ⊢A∈ℚ→33⁢A3∈ℚ
13 1nn ⊢1∈ℕ
14 nnq ⊢1∈ℕ→1∈ℚ
15 13 14 ax-mp ⊢1∈ℚ
16 qsubcl ⊢33⁢A3∈ℚ∧1∈ℚ→33⁢A3−1∈ℚ
17 12 15 16 sylancl ⊢A∈ℚ→33⁢A3−1∈ℚ
18 qsqcl ⊢A∈ℚ→A2∈ℚ
19 qmulcl ⊢33∈ℚ∧A2∈ℚ→33⁢A2∈ℚ
20 8 18 19 syl2anc ⊢A∈ℚ→33⁢A2∈ℚ
21 nnq ⊢3∈ℕ→3∈ℚ
22 1 21 ax-mp ⊢3∈ℚ
23 qsqcl ⊢3∈ℚ→32∈ℚ
24 22 23 mp1i ⊢A∈ℚ→32∈ℚ
25 qmulcl ⊢32∈ℚ∧A∈ℚ→32⁢A∈ℚ
26 24 25 mpancom ⊢A∈ℚ→32⁢A∈ℚ
27 qaddcl ⊢33⁢A2∈ℚ∧32⁢A∈ℚ→33⁢A2+32⁢A∈ℚ
28 20 26 27 syl2anc ⊢A∈ℚ→33⁢A2+32⁢A∈ℚ
29 qaddcl ⊢33⁢A2+32⁢A∈ℚ∧3∈ℚ→33⁢A2+32⁢A+3∈ℚ
30 28 22 29 sylancl ⊢A∈ℚ→33⁢A2+32⁢A+3∈ℚ
31 id ⊢A∈ℚ→A∈ℚ
32 31 3cubeslem2 ⊢A∈ℚ→¬33⁢A2+32⁢A+3=0
33 32 neqned ⊢A∈ℚ→33⁢A2+32⁢A+3≠0
34 qdivcl ⊢33⁢A3−1∈ℚ∧33⁢A2+32⁢A+3∈ℚ∧33⁢A2+32⁢A+3≠0→33⁢A3−133⁢A2+32⁢A+3∈ℚ
35 17 30 33 34 syl3anc ⊢A∈ℚ→33⁢A3−133⁢A2+32⁢A+3∈ℚ
36 qnegcl ⊢33⁢A3∈ℚ→−33⁢A3∈ℚ
37 12 36 syl ⊢A∈ℚ→−33⁢A3∈ℚ
38 qaddcl ⊢−33⁢A3∈ℚ∧32⁢A∈ℚ→-33⁢A3+32⁢A∈ℚ
39 37 26 38 syl2anc ⊢A∈ℚ→-33⁢A3+32⁢A∈ℚ
40 qaddcl ⊢-33⁢A3+32⁢A∈ℚ∧1∈ℚ→−33⁢A3+32⁢A+1∈ℚ
41 39 15 40 sylancl ⊢A∈ℚ→−33⁢A3+32⁢A+1∈ℚ
42 qdivcl ⊢−33⁢A3+32⁢A+1∈ℚ∧33⁢A2+32⁢A+3∈ℚ∧33⁢A2+32⁢A+3≠0→−33⁢A3+32⁢A+133⁢A2+32⁢A+3∈ℚ
43 41 30 33 42 syl3anc ⊢A∈ℚ→−33⁢A3+32⁢A+133⁢A2+32⁢A+3∈ℚ
44 qdivcl ⊢33⁢A2+32⁢A∈ℚ∧33⁢A2+32⁢A+3∈ℚ∧33⁢A2+32⁢A+3≠0→33⁢A2+32⁢A33⁢A2+32⁢A+3∈ℚ
45 28 30 33 44 syl3anc ⊢A∈ℚ→33⁢A2+32⁢A33⁢A2+32⁢A+3∈ℚ
46 31 3cubeslem4 ⊢A∈ℚ→A=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+33⁢A2+32⁢A33⁢A2+32⁢A+33
47 oveq1 ⊢a=33⁢A3−133⁢A2+32⁢A+3→a3=33⁢A3−133⁢A2+32⁢A+33
48 47 oveq1d ⊢a=33⁢A3−133⁢A2+32⁢A+3→a3+b3=33⁢A3−133⁢A2+32⁢A+33+b3
49 48 oveq1d ⊢a=33⁢A3−133⁢A2+32⁢A+3→a3+b3+c3=33⁢A3−133⁢A2+32⁢A+33+b3+c3
50 49 eqeq2d ⊢a=33⁢A3−133⁢A2+32⁢A+3→A=a3+b3+c3↔A=33⁢A3−133⁢A2+32⁢A+33+b3+c3
51 oveq1 ⊢b=−33⁢A3+32⁢A+133⁢A2+32⁢A+3→b3=−33⁢A3+32⁢A+133⁢A2+32⁢A+33
52 51 oveq2d ⊢b=−33⁢A3+32⁢A+133⁢A2+32⁢A+3→33⁢A3−133⁢A2+32⁢A+33+b3=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33
53 52 oveq1d ⊢b=−33⁢A3+32⁢A+133⁢A2+32⁢A+3→33⁢A3−133⁢A2+32⁢A+33+b3+c3=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+c3
54 53 eqeq2d ⊢b=−33⁢A3+32⁢A+133⁢A2+32⁢A+3→A=33⁢A3−133⁢A2+32⁢A+33+b3+c3↔A=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+c3
55 oveq1 ⊢c=33⁢A2+32⁢A33⁢A2+32⁢A+3→c3=33⁢A2+32⁢A33⁢A2+32⁢A+33
56 55 oveq2d ⊢c=33⁢A2+32⁢A33⁢A2+32⁢A+3→33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+c3=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+33⁢A2+32⁢A33⁢A2+32⁢A+33
57 56 eqeq2d ⊢c=33⁢A2+32⁢A33⁢A2+32⁢A+3→A=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+c3↔A=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+33⁢A2+32⁢A33⁢A2+32⁢A+33
58 50 54 57 rspc3ev ⊢33⁢A3−133⁢A2+32⁢A+3∈ℚ∧−33⁢A3+32⁢A+133⁢A2+32⁢A+3∈ℚ∧33⁢A2+32⁢A33⁢A2+32⁢A+3∈ℚ∧A=33⁢A3−133⁢A2+32⁢A+33+−33⁢A3+32⁢A+133⁢A2+32⁢A+33+33⁢A2+32⁢A33⁢A2+32⁢A+33→∃a∈ℚ∃b∈ℚ∃c∈ℚA=a3+b3+c3
59 35 43 45 46 58 syl31anc ⊢A∈ℚ→∃a∈ℚ∃b∈ℚ∃c∈ℚA=a3+b3+c3
60 3anass ⊢a∈ℚ∧b∈ℚ∧c∈ℚ↔a∈ℚ∧b∈ℚ∧c∈ℚ
61 qexpcl ⊢a∈ℚ∧3∈ℕ0→a3∈ℚ
62 3 61 mpan2 ⊢a∈ℚ→a3∈ℚ
63 simprl ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→b∈ℚ
64 qexpcl ⊢b∈ℚ∧3∈ℕ0→b3∈ℚ
65 63 3 64 sylancl ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→b3∈ℚ
66 qaddcl ⊢a3∈ℚ∧b3∈ℚ→a3+b3∈ℚ
67 62 65 66 syl2an2r ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→a3+b3∈ℚ
68 simprr ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→c∈ℚ
69 qexpcl ⊢c∈ℚ∧3∈ℕ0→c3∈ℚ
70 68 3 69 sylancl ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→c3∈ℚ
71 qaddcl ⊢a3+b3∈ℚ∧c3∈ℚ→a3+b3+c3∈ℚ
72 67 70 71 syl2anc ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→a3+b3+c3∈ℚ
73 eleq1a ⊢a3+b3+c3∈ℚ→A=a3+b3+c3→A∈ℚ
74 72 73 syl ⊢a∈ℚ∧b∈ℚ∧c∈ℚ→A=a3+b3+c3→A∈ℚ
75 74 a1i ⊢⊤→a∈ℚ∧b∈ℚ∧c∈ℚ→A=a3+b3+c3→A∈ℚ
76 60 75 biimtrid ⊢⊤→a∈ℚ∧b∈ℚ∧c∈ℚ→A=a3+b3+c3→A∈ℚ
77 76 rexlimdv3d ⊢⊤→∃a∈ℚ∃b∈ℚ∃c∈ℚA=a3+b3+c3→A∈ℚ
78 77 mptru ⊢∃a∈ℚ∃b∈ℚ∃c∈ℚA=a3+b3+c3→A∈ℚ
79 59 78 impbii ⊢A∈ℚ↔∃a∈ℚ∃b∈ℚ∃c∈ℚA=a3+b3+c3