Proof of Theorem 3cubeslem2
| Step | Hyp | Ref
| Expression |
| 1 | | 3re 12346 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
| 2 | 1 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 3 ∈
ℝ) |
| 3 | 2 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 3 ∈
ℂ) |
| 4 | 3 | mullidd 11279 |
. . . . . 6
⊢ (𝜑 → (1 · 3) =
3) |
| 5 | 4 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) · 3) + (1
· 3)) = (((((3↑2) · (𝐴↑2)) + (3 · 𝐴)) · 3) + 3)) |
| 6 | 3 | sqcld 14184 |
. . . . . . . 8
⊢ (𝜑 → (3↑2) ∈
ℂ) |
| 7 | | 3cubeslem1.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℚ) |
| 8 | | qre 12995 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 10 | 9 | resqcld 14165 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑2) ∈ ℝ) |
| 11 | 10 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
| 12 | 6, 11 | mulcld 11281 |
. . . . . . 7
⊢ (𝜑 → ((3↑2) ·
(𝐴↑2)) ∈
ℂ) |
| 13 | 9 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 14 | 3, 13 | mulcld 11281 |
. . . . . . 7
⊢ (𝜑 → (3 · 𝐴) ∈
ℂ) |
| 15 | 12, 14 | addcld 11280 |
. . . . . 6
⊢ (𝜑 → (((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) ∈
ℂ) |
| 16 | | 1cnd 11256 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
| 17 | 15, 16, 3 | adddird 11286 |
. . . . 5
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) · 3) =
(((((3↑2) · (𝐴↑2)) + (3 · 𝐴)) · 3) + (1 ·
3))) |
| 18 | 3, 13, 3 | mulassd 11284 |
. . . . . . . 8
⊢ (𝜑 → ((3 · 𝐴) · 3) = (3 ·
(𝐴 ·
3))) |
| 19 | 18 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) · 3) +
((3 · 𝐴) ·
3)) = ((((3↑2) · (𝐴↑2)) · 3) + (3 · (𝐴 · 3)))) |
| 20 | 19 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) · 3) +
((3 · 𝐴) ·
3)) + 3) = (((((3↑2) · (𝐴↑2)) · 3) + (3 · (𝐴 · 3))) +
3)) |
| 21 | 12, 14, 3 | adddird 11286 |
. . . . . . 7
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) · 3) =
((((3↑2) · (𝐴↑2)) · 3) + ((3 · 𝐴) · 3))) |
| 22 | 21 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) · 3) + 3) =
(((((3↑2) · (𝐴↑2)) · 3) + ((3 · 𝐴) · 3)) +
3)) |
| 23 | 3, 3, 13 | mulassd 11284 |
. . . . . . . . 9
⊢ (𝜑 → ((3 · 3) ·
𝐴) = (3 · (3
· 𝐴))) |
| 24 | 23 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) · 3) +
((3 · 3) · 𝐴)) = ((((3↑2) · (𝐴↑2)) · 3) + (3
· (3 · 𝐴)))) |
| 25 | 24 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) · 3) +
((3 · 3) · 𝐴)) + 3) = (((((3↑2) · (𝐴↑2)) · 3) + (3
· (3 · 𝐴))) +
3)) |
| 26 | 11, 3 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑2) · 3) = (3 · (𝐴↑2))) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → ((3↑2) ·
((𝐴↑2) · 3)) =
((3↑2) · (3 · (𝐴↑2)))) |
| 28 | 27 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((3↑2) ·
((𝐴↑2) · 3)) +
((3 · 3) · 𝐴)) = (((3↑2) · (3 ·
(𝐴↑2))) + ((3 ·
3) · 𝐴))) |
| 29 | 28 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((((3↑2) ·
((𝐴↑2) · 3)) +
((3 · 3) · 𝐴)) + 3) = ((((3↑2) · (3 ·
(𝐴↑2))) + ((3 ·
3) · 𝐴)) +
3)) |
| 30 | 6, 11, 3 | mulassd 11284 |
. . . . . . . . . 10
⊢ (𝜑 → (((3↑2) ·
(𝐴↑2)) · 3) =
((3↑2) · ((𝐴↑2) · 3))) |
| 31 | 30 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) · 3) +
((3 · 3) · 𝐴)) = (((3↑2) · ((𝐴↑2) · 3)) + ((3
· 3) · 𝐴))) |
| 32 | 31 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) · 3) +
((3 · 3) · 𝐴)) + 3) = ((((3↑2) · ((𝐴↑2) · 3)) + ((3
· 3) · 𝐴)) +
3)) |
| 33 | | df-3 12330 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
| 34 | 33 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 = (2 +
1)) |
| 35 | 34 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (3↑3) = (3↑(2 +
1))) |
| 36 | 35 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3↑3) ·
(𝐴↑2)) = ((3↑(2 +
1)) · (𝐴↑2))) |
| 37 | 36 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) = (((3↑(2
+ 1)) · (𝐴↑2))
+ ((3↑2) · 𝐴))) |
| 38 | 37 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
((((3↑(2 + 1)) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)) |
| 39 | | 2nn0 12543 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℕ0) |
| 41 | 3, 40 | expp1d 14187 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (3↑(2 + 1)) =
((3↑2) · 3)) |
| 42 | 41 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3↑(2 + 1)) ·
(𝐴↑2)) = (((3↑2)
· 3) · (𝐴↑2))) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((3↑(2 + 1))
· (𝐴↑2)) +
((3↑2) · 𝐴)) =
((((3↑2) · 3) · (𝐴↑2)) + ((3↑2) · 𝐴))) |
| 44 | 43 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((3↑(2 + 1))
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3) = (((((3↑2) · 3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)) |
| 45 | 38, 44 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
(((((3↑2) · 3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)) |
| 46 | 3 | sqvald 14183 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (3↑2) = (3 ·
3)) |
| 47 | 46 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((3↑2) · 𝐴) = ((3 · 3) ·
𝐴)) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((3↑2) · 3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) =
((((3↑2) · 3) · (𝐴↑2)) + ((3 · 3) · 𝐴))) |
| 49 | 48 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (((((3↑2) · 3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3) = (((((3↑2) · 3) · (𝐴↑2)) + ((3 · 3) · 𝐴)) + 3)) |
| 50 | 45, 49 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
(((((3↑2) · 3) · (𝐴↑2)) + ((3 · 3) · 𝐴)) + 3)) |
| 51 | 6, 3, 11 | mulassd 11284 |
. . . . . . . . . . 11
⊢ (𝜑 → (((3↑2) · 3)
· (𝐴↑2)) =
((3↑2) · (3 · (𝐴↑2)))) |
| 52 | 51 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((((3↑2) · 3)
· (𝐴↑2)) + ((3
· 3) · 𝐴)) =
(((3↑2) · (3 · (𝐴↑2))) + ((3 · 3) · 𝐴))) |
| 53 | 52 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((((3↑2) · 3)
· (𝐴↑2)) + ((3
· 3) · 𝐴)) +
3) = ((((3↑2) · (3 · (𝐴↑2))) + ((3 · 3) · 𝐴)) + 3)) |
| 54 | 50, 53 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
((((3↑2) · (3 · (𝐴↑2))) + ((3 · 3) · 𝐴)) + 3)) |
| 55 | 29, 32, 54 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
(((((3↑2) · (𝐴↑2)) · 3) + ((3 · 3)
· 𝐴)) +
3)) |
| 56 | 13, 3 | mulcomd 11282 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 3) = (3 · 𝐴)) |
| 57 | 56 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (3 · (𝐴 · 3)) = (3 · (3
· 𝐴))) |
| 58 | 57 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) · 3) +
(3 · (𝐴 ·
3))) = ((((3↑2) · (𝐴↑2)) · 3) + (3 · (3
· 𝐴)))) |
| 59 | 58 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) · 3) +
(3 · (𝐴 ·
3))) + 3) = (((((3↑2) · (𝐴↑2)) · 3) + (3 · (3
· 𝐴))) +
3)) |
| 60 | 25, 55, 59 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
(((((3↑2) · (𝐴↑2)) · 3) + (3 · (𝐴 · 3))) +
3)) |
| 61 | 20, 22, 60 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
(((((3↑2) · (𝐴↑2)) + (3 · 𝐴)) · 3) + 3)) |
| 62 | 5, 17, 61 | 3eqtr4rd 2788 |
. . . 4
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) =
(((((3↑2) · (𝐴↑2)) + (3 · 𝐴)) + 1) · 3)) |
| 63 | 14 | mulridd 11278 |
. . . . . . . . . 10
⊢ (𝜑 → ((3 · 𝐴) · 1) = (3 ·
𝐴)) |
| 64 | 63 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (2 · ((3 ·
𝐴) · 1)) = (2
· (3 · 𝐴))) |
| 65 | 64 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (((3 · 𝐴)↑2) + (2 · ((3
· 𝐴) · 1))) =
(((3 · 𝐴)↑2) +
(2 · (3 · 𝐴)))) |
| 66 | 65 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((((3 · 𝐴)↑2) + (2 · ((3
· 𝐴) · 1))) +
(1↑2)) = ((((3 · 𝐴)↑2) + (2 · (3 · 𝐴))) +
(1↑2))) |
| 67 | 66 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (2 · ((3
· 𝐴) · 1))) +
(1↑2)) − (3 · 𝐴)) = (((((3 · 𝐴)↑2) + (2 · (3 · 𝐴))) + (1↑2)) − (3
· 𝐴))) |
| 68 | 14, 16 | binom2d 14257 |
. . . . . . 7
⊢ (𝜑 → (((3 · 𝐴) + 1)↑2) = ((((3 ·
𝐴)↑2) + (2 ·
((3 · 𝐴) ·
1))) + (1↑2))) |
| 69 | 68 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((((3 · 𝐴) + 1)↑2) − (3
· 𝐴)) = (((((3
· 𝐴)↑2) + (2
· ((3 · 𝐴)
· 1))) + (1↑2)) − (3 · 𝐴))) |
| 70 | 14 | 2timesd 12509 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · (3 ·
𝐴)) = ((3 · 𝐴) + (3 · 𝐴))) |
| 71 | 70 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (((3 · 𝐴)↑2) + (2 · (3
· 𝐴))) = (((3
· 𝐴)↑2) + ((3
· 𝐴) + (3 ·
𝐴)))) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((((3 · 𝐴)↑2) + (2 · (3
· 𝐴))) + 1) = ((((3
· 𝐴)↑2) + ((3
· 𝐴) + (3 ·
𝐴))) + 1)) |
| 73 | 72 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (2 · (3
· 𝐴))) + 1) −
(3 · 𝐴)) = (((((3
· 𝐴)↑2) + ((3
· 𝐴) + (3 ·
𝐴))) + 1) − (3
· 𝐴))) |
| 74 | | sq1 14234 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
| 75 | 74 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1↑2) =
1) |
| 76 | 75 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → ((((3 · 𝐴)↑2) + (2 · (3
· 𝐴))) + (1↑2))
= ((((3 · 𝐴)↑2)
+ (2 · (3 · 𝐴))) + 1)) |
| 77 | 76 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (2 · (3
· 𝐴))) + (1↑2))
− (3 · 𝐴)) =
(((((3 · 𝐴)↑2)
+ (2 · (3 · 𝐴))) + 1) − (3 · 𝐴))) |
| 78 | 14, 16 | addcomd 11463 |
. . . . . . . . . . 11
⊢ (𝜑 → ((3 · 𝐴) + 1) = (1 + (3 · 𝐴))) |
| 79 | 78 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → ((((3 · 𝐴)↑2) + (3 · 𝐴)) + ((3 · 𝐴) + 1)) = ((((3 · 𝐴)↑2) + (3 · 𝐴)) + (1 + (3 · 𝐴)))) |
| 80 | 79 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (3 · 𝐴)) + ((3 · 𝐴) + 1)) − (3 ·
𝐴)) = (((((3 · 𝐴)↑2) + (3 · 𝐴)) + (1 + (3 · 𝐴))) − (3 · 𝐴))) |
| 81 | 3, 13 | sqmuld 14198 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3 · 𝐴)↑2) = ((3↑2) ·
(𝐴↑2))) |
| 82 | 81, 12 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((3 · 𝐴)↑2) ∈
ℂ) |
| 83 | 82, 14 | addcld 11280 |
. . . . . . . . . . 11
⊢ (𝜑 → (((3 · 𝐴)↑2) + (3 · 𝐴)) ∈
ℂ) |
| 84 | 83, 14, 16 | addassd 11283 |
. . . . . . . . . 10
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (3 · 𝐴)) + (3 · 𝐴)) + 1) = ((((3 · 𝐴)↑2) + (3 · 𝐴)) + ((3 · 𝐴) + 1))) |
| 85 | 84 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((((((3 · 𝐴)↑2) + (3 · 𝐴)) + (3 · 𝐴)) + 1) − (3 ·
𝐴)) = (((((3 · 𝐴)↑2) + (3 · 𝐴)) + ((3 · 𝐴) + 1)) − (3 ·
𝐴))) |
| 86 | 15, 16 | addcld 11280 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) ∈
ℂ) |
| 87 | 86, 14, 14 | addsubassd 11640 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) + (3 ·
𝐴)) − (3 ·
𝐴)) = (((((3↑2)
· (𝐴↑2)) + (3
· 𝐴)) + 1) + ((3
· 𝐴) − (3
· 𝐴)))) |
| 88 | 81 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((3 · 𝐴)↑2) + (3 · 𝐴)) = (((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴))) |
| 89 | 88 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((3 · 𝐴)↑2) + (3 · 𝐴)) + 1) = ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1)) |
| 90 | 89 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (3 · 𝐴)) + 1) + (3 · 𝐴)) = (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) + (3 ·
𝐴))) |
| 91 | 90 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((((3 · 𝐴)↑2) + (3 · 𝐴)) + 1) + (3 · 𝐴)) − (3 · 𝐴)) = ((((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) + (3 ·
𝐴)) − (3 ·
𝐴))) |
| 92 | 14 | subidd 11608 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3 · 𝐴) − (3 · 𝐴)) = 0) |
| 93 | 92 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) + ((3 ·
𝐴) − (3 ·
𝐴))) = (((((3↑2)
· (𝐴↑2)) + (3
· 𝐴)) + 1) +
0)) |
| 94 | 86 | addridd 11461 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) + 0) =
((((3↑2) · (𝐴↑2)) + (3 · 𝐴)) + 1)) |
| 95 | 93, 94 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = (((((3↑2)
· (𝐴↑2)) + (3
· 𝐴)) + 1) + ((3
· 𝐴) − (3
· 𝐴)))) |
| 96 | 87, 91, 95 | 3eqtr4rd 2788 |
. . . . . . . . . 10
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = ((((((3 ·
𝐴)↑2) + (3 ·
𝐴)) + 1) + (3 ·
𝐴)) − (3 ·
𝐴))) |
| 97 | 83, 16, 14 | addassd 11283 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (3 · 𝐴)) + 1) + (3 · 𝐴)) = ((((3 · 𝐴)↑2) + (3 · 𝐴)) + (1 + (3 · 𝐴)))) |
| 98 | 97 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((((((3 · 𝐴)↑2) + (3 · 𝐴)) + 1) + (3 · 𝐴)) − (3 · 𝐴)) = (((((3 · 𝐴)↑2) + (3 · 𝐴)) + (1 + (3 · 𝐴))) − (3 · 𝐴))) |
| 99 | 96, 98 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = (((((3 ·
𝐴)↑2) + (3 ·
𝐴)) + (1 + (3 ·
𝐴))) − (3 ·
𝐴))) |
| 100 | 80, 85, 99 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = ((((((3 ·
𝐴)↑2) + (3 ·
𝐴)) + (3 · 𝐴)) + 1) − (3 ·
𝐴))) |
| 101 | 82, 14, 14 | addassd 11283 |
. . . . . . . . . 10
⊢ (𝜑 → ((((3 · 𝐴)↑2) + (3 · 𝐴)) + (3 · 𝐴)) = (((3 · 𝐴)↑2) + ((3 · 𝐴) + (3 · 𝐴)))) |
| 102 | 101 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((((3 · 𝐴)↑2) + (3 · 𝐴)) + (3 · 𝐴)) + 1) = ((((3 · 𝐴)↑2) + ((3 · 𝐴) + (3 · 𝐴))) + 1)) |
| 103 | 102 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((((((3 · 𝐴)↑2) + (3 · 𝐴)) + (3 · 𝐴)) + 1) − (3 ·
𝐴)) = (((((3 · 𝐴)↑2) + ((3 · 𝐴) + (3 · 𝐴))) + 1) − (3 ·
𝐴))) |
| 104 | 100, 103 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = (((((3 ·
𝐴)↑2) + ((3 ·
𝐴) + (3 · 𝐴))) + 1) − (3 ·
𝐴))) |
| 105 | 73, 77, 104 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = (((((3 ·
𝐴)↑2) + (2 · (3
· 𝐴))) + (1↑2))
− (3 · 𝐴))) |
| 106 | 67, 69, 105 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝜑 → ((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) = ((((3 ·
𝐴) + 1)↑2) − (3
· 𝐴))) |
| 107 | 106 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (((((3↑2) ·
(𝐴↑2)) + (3 ·
𝐴)) + 1) · 3) =
(((((3 · 𝐴) +
1)↑2) − (3 · 𝐴)) · 3)) |
| 108 | 62, 107 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) = (((((3
· 𝐴) + 1)↑2)
− (3 · 𝐴))
· 3)) |
| 109 | 2, 9 | remulcld 11291 |
. . . . . . . 8
⊢ (𝜑 → (3 · 𝐴) ∈
ℝ) |
| 110 | | peano2re 11434 |
. . . . . . . 8
⊢ ((3
· 𝐴) ∈ ℝ
→ ((3 · 𝐴) + 1)
∈ ℝ) |
| 111 | 109, 110 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((3 · 𝐴) + 1) ∈
ℝ) |
| 112 | 111 | resqcld 14165 |
. . . . . 6
⊢ (𝜑 → (((3 · 𝐴) + 1)↑2) ∈
ℝ) |
| 113 | 112, 109 | resubcld 11691 |
. . . . 5
⊢ (𝜑 → ((((3 · 𝐴) + 1)↑2) − (3
· 𝐴)) ∈
ℝ) |
| 114 | 113 | recnd 11289 |
. . . 4
⊢ (𝜑 → ((((3 · 𝐴) + 1)↑2) − (3
· 𝐴)) ∈
ℂ) |
| 115 | | 3nn 12345 |
. . . . . . . 8
⊢ 3 ∈
ℕ |
| 116 | | nnq 13004 |
. . . . . . . 8
⊢ (3 ∈
ℕ → 3 ∈ ℚ) |
| 117 | 115, 116 | ax-mp 5 |
. . . . . . 7
⊢ 3 ∈
ℚ |
| 118 | | qmulcl 13009 |
. . . . . . 7
⊢ ((3
∈ ℚ ∧ 𝐴
∈ ℚ) → (3 · 𝐴) ∈ ℚ) |
| 119 | 117, 7, 118 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (3 · 𝐴) ∈
ℚ) |
| 120 | 119 | 3cubeslem1 42695 |
. . . . 5
⊢ (𝜑 → 0 < ((((3 ·
𝐴) + 1)↑2) − (3
· 𝐴))) |
| 121 | 120 | gt0ne0d 11827 |
. . . 4
⊢ (𝜑 → ((((3 · 𝐴) + 1)↑2) − (3
· 𝐴)) ≠
0) |
| 122 | | 3ne0 12372 |
. . . . 5
⊢ 3 ≠
0 |
| 123 | 122 | a1i 11 |
. . . 4
⊢ (𝜑 → 3 ≠ 0) |
| 124 | 114, 3, 121, 123 | mulne0d 11915 |
. . 3
⊢ (𝜑 → (((((3 · 𝐴) + 1)↑2) − (3
· 𝐴)) · 3)
≠ 0) |
| 125 | 108, 124 | eqnetrd 3008 |
. 2
⊢ (𝜑 → ((((3↑3) ·
(𝐴↑2)) + ((3↑2)
· 𝐴)) + 3) ≠
0) |
| 126 | 125 | neneqd 2945 |
1
⊢ (𝜑 → ¬ ((((3↑3)
· (𝐴↑2)) +
((3↑2) · 𝐴)) +
3) = 0) |