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 \in ℚ \leftrightarrow \exists a \in ℚ \exists b \in ℚ \exists c \in ℚ A = a^{3} + b^{3} + c^{3}$

Proof

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

Metamath Proof Explorer

Theorem 3cubes

Proof