Proof of Theorem 3cubes
Step | Hyp | Ref
| Expression |
1 | | 3nn 11797 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (¬
(3↑3) ∈ ℕ → 3 ∈ ℕ) |
3 | | 3nn0 11996 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (¬
(3↑3) ∈ ℕ → 3 ∈ ℕ0) |
5 | 2, 4 | nnexpcld 13700 |
. . . . . . . 8
⊢ (¬
(3↑3) ∈ ℕ → (3↑3) ∈ ℕ) |
6 | 5 | pm2.18i 131 |
. . . . . . 7
⊢
(3↑3) ∈ ℕ |
7 | | nnq 12446 |
. . . . . . 7
⊢
((3↑3) ∈ ℕ → (3↑3) ∈
ℚ) |
8 | 6, 7 | mp1i 13 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
(3↑3) ∈ ℚ) |
9 | | qexpcl 13539 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℚ) |
10 | 3, 9 | mpan2 691 |
. . . . . 6
⊢ (𝐴 ∈ ℚ → (𝐴↑3) ∈
ℚ) |
11 | | qmulcl 12451 |
. . . . . 6
⊢
(((3↑3) ∈ ℚ ∧ (𝐴↑3) ∈ ℚ) → ((3↑3)
· (𝐴↑3)) ∈
ℚ) |
12 | 8, 10, 11 | syl2anc 587 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
((3↑3) · (𝐴↑3)) ∈ ℚ) |
13 | | 1nn 11729 |
. . . . . 6
⊢ 1 ∈
ℕ |
14 | | nnq 12446 |
. . . . . 6
⊢ (1 ∈
ℕ → 1 ∈ ℚ) |
15 | 13, 14 | ax-mp 5 |
. . . . 5
⊢ 1 ∈
ℚ |
16 | | qsubcl 12452 |
. . . . 5
⊢
((((3↑3) · (𝐴↑3)) ∈ ℚ ∧ 1 ∈
ℚ) → (((3↑3) · (𝐴↑3)) − 1) ∈
ℚ) |
17 | 12, 15, 16 | sylancl 589 |
. . . 4
⊢ (𝐴 ∈ ℚ →
(((3↑3) · (𝐴↑3)) − 1) ∈
ℚ) |
18 | | qsqcl 13589 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈
ℚ) |
19 | | qmulcl 12451 |
. . . . . . 7
⊢
(((3↑3) ∈ ℚ ∧ (𝐴↑2) ∈ ℚ) → ((3↑3)
· (𝐴↑2)) ∈
ℚ) |
20 | 8, 18, 19 | syl2anc 587 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
((3↑3) · (𝐴↑2)) ∈ ℚ) |
21 | | nnq 12446 |
. . . . . . . . 9
⊢ (3 ∈
ℕ → 3 ∈ ℚ) |
22 | 1, 21 | ax-mp 5 |
. . . . . . . 8
⊢ 3 ∈
ℚ |
23 | | qsqcl 13589 |
. . . . . . . 8
⊢ (3 ∈
ℚ → (3↑2) ∈ ℚ) |
24 | 22, 23 | mp1i 13 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ →
(3↑2) ∈ ℚ) |
25 | | qmulcl 12451 |
. . . . . . 7
⊢
(((3↑2) ∈ ℚ ∧ 𝐴 ∈ ℚ) → ((3↑2) ·
𝐴) ∈
ℚ) |
26 | 24, 25 | mpancom 688 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
((3↑2) · 𝐴)
∈ ℚ) |
27 | | qaddcl 12449 |
. . . . . 6
⊢
((((3↑3) · (𝐴↑2)) ∈ ℚ ∧ ((3↑2)
· 𝐴) ∈ ℚ)
→ (((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) ∈
ℚ) |
28 | 20, 26, 27 | syl2anc 587 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
(((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) ∈
ℚ) |
29 | | qaddcl 12449 |
. . . . 5
⊢
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) ∈ ℚ ∧ 3 ∈
ℚ) → ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) ∈
ℚ) |
30 | 28, 22, 29 | sylancl 589 |
. . . 4
⊢ (𝐴 ∈ ℚ →
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) ∈
ℚ) |
31 | | id 22 |
. . . . . 6
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℚ) |
32 | 31 | 3cubeslem2 40101 |
. . . . 5
⊢ (𝐴 ∈ ℚ → ¬
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0) |
33 | 32 | neqned 2941 |
. . . 4
⊢ (𝐴 ∈ ℚ →
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) ≠ 0) |
34 | | qdivcl 12454 |
. . . 4
⊢
(((((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 1372 |
. . 3
⊢ (𝐴 ∈ ℚ →
((((3↑3) · (𝐴↑3)) − 1) / ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)) ∈ ℚ) |
36 | | qnegcl 12450 |
. . . . . . 7
⊢
(((3↑3) · (𝐴↑3)) ∈ ℚ → -((3↑3)
· (𝐴↑3)) ∈
ℚ) |
37 | 12, 36 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
-((3↑3) · (𝐴↑3)) ∈ ℚ) |
38 | | qaddcl 12449 |
. . . . . 6
⊢
((-((3↑3) · (𝐴↑3)) ∈ ℚ ∧ ((3↑2)
· 𝐴) ∈ ℚ)
→ (-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) ∈
ℚ) |
39 | 37, 26, 38 | syl2anc 587 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
(-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) ∈
ℚ) |
40 | | qaddcl 12449 |
. . . . 5
⊢
(((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) ∈ ℚ ∧ 1 ∈
ℚ) → ((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) ∈
ℚ) |
41 | 39, 15, 40 | sylancl 589 |
. . . 4
⊢ (𝐴 ∈ ℚ →
((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) ∈
ℚ) |
42 | | qdivcl 12454 |
. . . 4
⊢
((((-((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 1372 |
. . 3
⊢ (𝐴 ∈ ℚ →
(((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) / ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3)) ∈
ℚ) |
44 | | qdivcl 12454 |
. . . 4
⊢
(((((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 1372 |
. . 3
⊢ (𝐴 ∈ ℚ →
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) / ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3)) ∈
ℚ) |
46 | 31 | 3cubeslem4 40105 |
. . 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))) |
47 | | oveq1 7179 |
. . . . . . 7
⊢ (𝑎 = ((((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 7187 |
. . . . . 6
⊢ (𝑎 = ((((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 7187 |
. . . . 5
⊢ (𝑎 = ((((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 2749 |
. . . 4
⊢ (𝑎 = ((((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 7179 |
. . . . . . 7
⊢ (𝑏 = (((-((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 7188 |
. . . . . 6
⊢ (𝑏 = (((-((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 7187 |
. . . . 5
⊢ (𝑏 = (((-((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 2749 |
. . . 4
⊢ (𝑏 = (((-((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 7179 |
. . . . . 6
⊢ (𝑐 = ((((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 7188 |
. . . . 5
⊢ (𝑐 = ((((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 2749 |
. . . 4
⊢ (𝑐 = ((((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 3540 |
. . 3
⊢
(((((((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 1374 |
. 2
⊢ (𝐴 ∈ ℚ →
∃𝑎 ∈ ℚ
∃𝑏 ∈ ℚ
∃𝑐 ∈ ℚ
𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3))) |
60 | | 3anass 1096 |
. . . . 5
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ) ↔ (𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈
ℚ))) |
61 | | qexpcl 13539 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℚ ∧ 3 ∈
ℕ0) → (𝑎↑3) ∈ ℚ) |
62 | 3, 61 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℚ → (𝑎↑3) ∈
ℚ) |
63 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → 𝑏 ∈
ℚ) |
64 | | qexpcl 13539 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℚ ∧ 3 ∈
ℕ0) → (𝑏↑3) ∈ ℚ) |
65 | 63, 3, 64 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝑏↑3) ∈
ℚ) |
66 | | qaddcl 12449 |
. . . . . . . . 9
⊢ (((𝑎↑3) ∈ ℚ ∧
(𝑏↑3) ∈ ℚ)
→ ((𝑎↑3) + (𝑏↑3)) ∈
ℚ) |
67 | 62, 65, 66 | syl2an2r 685 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → ((𝑎↑3) + (𝑏↑3)) ∈ ℚ) |
68 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → 𝑐 ∈
ℚ) |
69 | | qexpcl 13539 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ℚ ∧ 3 ∈
ℕ0) → (𝑐↑3) ∈ ℚ) |
70 | 68, 3, 69 | sylancl 589 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝑐↑3) ∈
ℚ) |
71 | | qaddcl 12449 |
. . . . . . . 8
⊢ ((((𝑎↑3) + (𝑏↑3)) ∈ ℚ ∧ (𝑐↑3) ∈ ℚ) →
(((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) ∈ ℚ) |
72 | 67, 70, 71 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) →
(((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) ∈ ℚ) |
73 | | eleq1a 2828 |
. . . . . . 7
⊢ ((((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) ∈ ℚ → (𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) → 𝐴 ∈ ℚ)) |
74 | 72, 73 | syl 17 |
. . . . . 6
⊢ ((𝑎 ∈ ℚ ∧ (𝑏 ∈ ℚ ∧ 𝑐 ∈ ℚ)) → (𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) → 𝐴 ∈ ℚ)) |
75 | 74 | a1i 11 |
. . . . 5
⊢ (⊤
→ ((𝑎 ∈ ℚ
∧ (𝑏 ∈ ℚ
∧ 𝑐 ∈ ℚ))
→ (𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) → 𝐴 ∈ ℚ))) |
76 | 60, 75 | syl5bi 245 |
. . . 4
⊢ (⊤
→ ((𝑎 ∈ ℚ
∧ 𝑏 ∈ ℚ
∧ 𝑐 ∈ ℚ)
→ (𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) → 𝐴 ∈ ℚ))) |
77 | 76 | rexlimdv3d 40099 |
. . 3
⊢ (⊤
→ (∃𝑎 ∈
ℚ ∃𝑏 ∈
ℚ ∃𝑐 ∈
ℚ 𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) → 𝐴 ∈ ℚ)) |
78 | 77 | mptru 1549 |
. 2
⊢
(∃𝑎 ∈
ℚ ∃𝑏 ∈
ℚ ∃𝑐 ∈
ℚ 𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)) → 𝐴 ∈ ℚ) |
79 | 59, 78 | impbii 212 |
1
⊢ (𝐴 ∈ ℚ ↔
∃𝑎 ∈ ℚ
∃𝑏 ∈ ℚ
∃𝑐 ∈ ℚ
𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3))) |