Proof of Theorem 3cubeslem4
Step | Hyp | Ref
| Expression |
1 | | 3re 12053 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 3 ∈ ℝ) |
3 | | 3nn0 12251 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 3 ∈ ℕ0) |
5 | 2, 4 | reexpcld 13881 |
. . . . . . . . . . 11
⊢ (⊤
→ (3↑3) ∈ ℝ) |
6 | 5 | mptru 1546 |
. . . . . . . . . 10
⊢
(3↑3) ∈ ℝ |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (3↑3) ∈
ℝ) |
8 | | 3cubeslem1.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℚ) |
9 | | qre 12693 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
10 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℚ → 3 ∈
ℕ0) |
11 | 9, 10 | reexpcld 13881 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → (𝐴↑3) ∈
ℝ) |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑3) ∈ ℝ) |
13 | 7, 12 | remulcld 11005 |
. . . . . . . 8
⊢ (𝜑 → ((3↑3) ·
(𝐴↑3)) ∈
ℝ) |
14 | | 1red 10976 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
15 | 13, 14 | resubcld 11403 |
. . . . . . 7
⊢ (𝜑 → (((3↑3) ·
(𝐴↑3)) − 1)
∈ ℝ) |
16 | 15 | recnd 11003 |
. . . . . 6
⊢ (𝜑 → (((3↑3) ·
(𝐴↑3)) − 1)
∈ ℂ) |
17 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 3 ∈
ℕ0) |
18 | 16, 17 | expcld 13864 |
. . . . 5
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑3)) −
1)↑3) ∈ ℂ) |
19 | 13 | renegcld 11402 |
. . . . . . . . 9
⊢ (𝜑 → -((3↑3) ·
(𝐴↑3)) ∈
ℝ) |
20 | 19 | recnd 11003 |
. . . . . . . 8
⊢ (𝜑 → -((3↑3) ·
(𝐴↑3)) ∈
ℂ) |
21 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 3 ∈
ℝ) |
22 | 21 | recnd 11003 |
. . . . . . . . . 10
⊢ (𝜑 → 3 ∈
ℂ) |
23 | 22 | sqcld 13862 |
. . . . . . . . 9
⊢ (𝜑 → (3↑2) ∈
ℂ) |
24 | | qcn 12703 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
25 | 8, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
26 | 23, 25 | mulcld 10995 |
. . . . . . . 8
⊢ (𝜑 → ((3↑2) · 𝐴) ∈
ℂ) |
27 | 20, 26 | addcld 10994 |
. . . . . . 7
⊢ (𝜑 → (-((3↑3) ·
(𝐴↑3)) + ((3↑2)
· 𝐴)) ∈
ℂ) |
28 | | 1cnd 10970 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
29 | 27, 28 | addcld 10994 |
. . . . . 6
⊢ (𝜑 → ((-((3↑3) ·
(𝐴↑3)) + ((3↑2)
· 𝐴)) + 1) ∈
ℂ) |
30 | 29, 17 | expcld 13864 |
. . . . 5
⊢ (𝜑 → (((-((3↑3) ·
(𝐴↑3)) + ((3↑2)
· 𝐴)) + 1)↑3)
∈ ℂ) |
31 | 7 | recnd 11003 |
. . . . . . . . 9
⊢ (𝜑 → (3↑3) ∈
ℂ) |
32 | 25 | sqcld 13862 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
33 | 31, 32 | mulcld 10995 |
. . . . . . . 8
⊢ (𝜑 → ((3↑3) ·
(𝐴↑2)) ∈
ℂ) |
34 | 33, 26 | addcld 10994 |
. . . . . . 7
⊢ (𝜑 → (((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) ∈
ℂ) |
35 | 34, 22 | addcld 10994 |
. . . . . 6
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) ∈
ℂ) |
36 | 35, 17 | expcld 13864 |
. . . . 5
⊢ (𝜑 → (((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3)↑3)
∈ ℂ) |
37 | 8 | 3cubeslem2 40507 |
. . . . . . 7
⊢ (𝜑 → ¬ ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3) = 0) |
38 | 37 | neqned 2950 |
. . . . . 6
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) ≠
0) |
39 | | 3z 12353 |
. . . . . . 7
⊢ 3 ∈
ℤ |
40 | 39 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 3 ∈
ℤ) |
41 | 35, 38, 40 | expne0d 13870 |
. . . . 5
⊢ (𝜑 → (((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3)↑3)
≠ 0) |
42 | 18, 30, 36, 41 | divdird 11789 |
. . . 4
⊢ (𝜑 → ((((((3↑3) ·
(𝐴↑3)) −
1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) =
((((((3↑3) · (𝐴↑3)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3)))) |
43 | 42 | oveq1d 7290 |
. . 3
⊢ (𝜑 → (((((((3↑3) ·
(𝐴↑3)) −
1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) = (((((((3↑3) · (𝐴↑3)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3)))) |
44 | 18, 30 | addcld 10994 |
. . . 4
⊢ (𝜑 → (((((3↑3) ·
(𝐴↑3)) −
1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) ∈
ℂ) |
45 | 34, 17 | expcld 13864 |
. . . 4
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴))↑3) ∈
ℂ) |
46 | 44, 45, 36, 41 | divdird 11789 |
. . 3
⊢ (𝜑 → (((((((3↑3) ·
(𝐴↑3)) −
1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴))↑3)) / (((((3↑3) · (𝐴↑2)) + ((3↑2) ·
𝐴)) + 3)↑3)) =
(((((((3↑3) · (𝐴↑3)) − 1)↑3) +
(((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3)))) |
47 | 16, 35, 38, 17 | expdivd 13878 |
. . . . . 6
⊢ (𝜑 → (((((3↑3) ·
(𝐴↑3)) − 1) /
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3) =
(((((3↑3) · (𝐴↑3)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) +
3)↑3))) |
48 | 47 | oveq1d 7290 |
. . . . 5
⊢ (𝜑 → ((((((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)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) / ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) +
3))↑3))) |
49 | 48 | oveq1d 7290 |
. . . 4
⊢ (𝜑 → (((((((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)) − 1)↑3) /
(((((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))) |
50 | 29, 35, 38, 17 | expdivd 13878 |
. . . . . 6
⊢ (𝜑 → ((((-((3↑3) ·
(𝐴↑3)) + ((3↑2)
· 𝐴)) + 1) /
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3) =
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) |
51 | 50 | oveq2d 7291 |
. . . . 5
⊢ (𝜑 → ((((((3↑3) ·
(𝐴↑3)) −
1)↑3) / (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) / ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3))↑3))
= ((((((3↑3) · (𝐴↑3)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3)))) |
52 | 51 | oveq1d 7290 |
. . . 4
⊢ (𝜑 → (((((((3↑3) ·
(𝐴↑3)) −
1)↑3) / (((((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)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) / ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) +
3))↑3))) |
53 | 34, 35, 38, 17 | expdivd 13878 |
. . . . 5
⊢ (𝜑 → (((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) /
((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3) =
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) |
54 | 53 | oveq2d 7291 |
. . . 4
⊢ (𝜑 → (((((((3↑3) ·
(𝐴↑3)) −
1)↑3) / (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) / ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3))↑3))
= (((((((3↑3) · (𝐴↑3)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3)))) |
55 | 49, 52, 54 | 3eqtrd 2782 |
. . 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)) − 1)↑3) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) +
((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3))) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3) / (((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3)↑3)))) |
56 | 43, 46, 55 | 3eqtr4rd 2789 |
. 2
⊢ (𝜑 → (((((((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)) − 1)↑3) +
(((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴))↑3)) / (((((3↑3) · (𝐴↑2)) + ((3↑2) ·
𝐴)) +
3)↑3))) |
57 | 8 | 3cubeslem3 40510 |
. . 3
⊢ (𝜑 → (𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) ·
𝐴)) + 3)↑3)) =
((((((3↑3) · (𝐴↑3)) − 1)↑3) +
(((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴))↑3))) |
58 | 57 | oveq1d 7290 |
. 2
⊢ (𝜑 → ((𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) ·
𝐴)) + 3)↑3)) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) =
(((((((3↑3) · (𝐴↑3)) − 1)↑3) +
(((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴))↑3)) / (((((3↑3) · (𝐴↑2)) + ((3↑2) ·
𝐴)) +
3)↑3))) |
59 | 25, 36, 41 | divcan4d 11757 |
. 2
⊢ (𝜑 → ((𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) ·
𝐴)) + 3)↑3)) /
(((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) = 𝐴) |
60 | 56, 58, 59 | 3eqtr2rd 2785 |
1
⊢ (𝜑 → 𝐴 = (((((((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))) |