Proof of Theorem dcubic1lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dcubic2.u | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 2 |  | 3nn0 12544 | . . . . . . . . 9
⊢ 3 ∈
ℕ0 | 
| 3 |  | expcl 14120 | . . . . . . . . 9
⊢ ((𝑈 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑈↑3) ∈ ℂ) | 
| 4 | 1, 2, 3 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → (𝑈↑3) ∈ ℂ) | 
| 5 | 4 | sqvald 14183 | . . . . . . 7
⊢ (𝜑 → ((𝑈↑3)↑2) = ((𝑈↑3) · (𝑈↑3))) | 
| 6 | 5 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((𝑈↑3)↑2) / (𝑈↑3)) = (((𝑈↑3) · (𝑈↑3)) / (𝑈↑3))) | 
| 7 |  | dcubic2.z | . . . . . . . 8
⊢ (𝜑 → 𝑈 ≠ 0) | 
| 8 |  | 3z 12650 | . . . . . . . . 9
⊢ 3 ∈
ℤ | 
| 9 | 8 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 3 ∈
ℤ) | 
| 10 | 1, 7, 9 | expne0d 14192 | . . . . . . 7
⊢ (𝜑 → (𝑈↑3) ≠ 0) | 
| 11 | 4, 4, 10 | divcan4d 12049 | . . . . . 6
⊢ (𝜑 → (((𝑈↑3) · (𝑈↑3)) / (𝑈↑3)) = (𝑈↑3)) | 
| 12 | 6, 11 | eqtr2d 2778 | . . . . 5
⊢ (𝜑 → (𝑈↑3) = (((𝑈↑3)↑2) / (𝑈↑3))) | 
| 13 |  | dcubic.d | . . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℂ) | 
| 14 |  | dcubic.m | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 = (𝑃 / 3)) | 
| 15 |  | dcubic.c | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 16 |  | 3cn 12347 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℂ | 
| 17 | 16 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ∈
ℂ) | 
| 18 |  | 3ne0 12372 | . . . . . . . . . . . . 13
⊢ 3 ≠
0 | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ≠ 0) | 
| 20 | 15, 17, 19 | divcld 12043 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃 / 3) ∈ ℂ) | 
| 21 | 14, 20 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 22 |  | expcl 14120 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑀↑3) ∈ ℂ) | 
| 23 | 21, 2, 22 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝑀↑3) ∈ ℂ) | 
| 24 | 23, 4, 10 | divcld 12043 | . . . . . . . 8
⊢ (𝜑 → ((𝑀↑3) / (𝑈↑3)) ∈ ℂ) | 
| 25 | 13, 24 | negsubd 11626 | . . . . . . 7
⊢ (𝜑 → (𝑄 + -((𝑀↑3) / (𝑈↑3))) = (𝑄 − ((𝑀↑3) / (𝑈↑3)))) | 
| 26 | 13, 4, 10 | divcan4d 12049 | . . . . . . . 8
⊢ (𝜑 → ((𝑄 · (𝑈↑3)) / (𝑈↑3)) = 𝑄) | 
| 27 | 26 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (((𝑄 · (𝑈↑3)) / (𝑈↑3)) − ((𝑀↑3) / (𝑈↑3))) = (𝑄 − ((𝑀↑3) / (𝑈↑3)))) | 
| 28 | 25, 27 | eqtr4d 2780 | . . . . . 6
⊢ (𝜑 → (𝑄 + -((𝑀↑3) / (𝑈↑3))) = (((𝑄 · (𝑈↑3)) / (𝑈↑3)) − ((𝑀↑3) / (𝑈↑3)))) | 
| 29 |  | dcubic.x | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 30 | 15, 29 | mulcld 11281 | . . . . . . . . 9
⊢ (𝜑 → (𝑃 · 𝑋) ∈ ℂ) | 
| 31 | 30 | negcld 11607 | . . . . . . . 8
⊢ (𝜑 → -(𝑃 · 𝑋) ∈ ℂ) | 
| 32 | 24 | negcld 11607 | . . . . . . . 8
⊢ (𝜑 → -((𝑀↑3) / (𝑈↑3)) ∈ ℂ) | 
| 33 | 31, 32, 30, 13 | add42d 11491 | . . . . . . 7
⊢ (𝜑 → ((-(𝑃 · 𝑋) + -((𝑀↑3) / (𝑈↑3))) + ((𝑃 · 𝑋) + 𝑄)) = ((-(𝑃 · 𝑋) + (𝑃 · 𝑋)) + (𝑄 + -((𝑀↑3) / (𝑈↑3))))) | 
| 34 | 15, 29 | mulneg2d 11717 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 · -𝑋) = -(𝑃 · 𝑋)) | 
| 35 |  | dcubic2.2 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 = (𝑈 − (𝑀 / 𝑈))) | 
| 36 | 35 | negeqd 11502 | . . . . . . . . . . . . . 14
⊢ (𝜑 → -𝑋 = -(𝑈 − (𝑀 / 𝑈))) | 
| 37 | 21, 1, 7 | divcld 12043 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 / 𝑈) ∈ ℂ) | 
| 38 | 1, 37 | negsubdid 11635 | . . . . . . . . . . . . . 14
⊢ (𝜑 → -(𝑈 − (𝑀 / 𝑈)) = (-𝑈 + (𝑀 / 𝑈))) | 
| 39 | 36, 38 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝜑 → -𝑋 = (-𝑈 + (𝑀 / 𝑈))) | 
| 40 | 39 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 · -𝑋) = (𝑃 · (-𝑈 + (𝑀 / 𝑈)))) | 
| 41 | 34, 40 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ (𝜑 → -(𝑃 · 𝑋) = (𝑃 · (-𝑈 + (𝑀 / 𝑈)))) | 
| 42 | 1 | negcld 11607 | . . . . . . . . . . . 12
⊢ (𝜑 → -𝑈 ∈ ℂ) | 
| 43 | 15, 42, 37 | adddid 11285 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃 · (-𝑈 + (𝑀 / 𝑈))) = ((𝑃 · -𝑈) + (𝑃 · (𝑀 / 𝑈)))) | 
| 44 | 15, 1 | mulneg2d 11717 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 · -𝑈) = -(𝑃 · 𝑈)) | 
| 45 | 44 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 · -𝑈) + (𝑃 · (𝑀 / 𝑈))) = (-(𝑃 · 𝑈) + (𝑃 · (𝑀 / 𝑈)))) | 
| 46 | 41, 43, 45 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (𝜑 → -(𝑃 · 𝑋) = (-(𝑃 · 𝑈) + (𝑃 · (𝑀 / 𝑈)))) | 
| 47 | 46 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → (-(𝑃 · 𝑋) + -((𝑀↑3) / (𝑈↑3))) = ((-(𝑃 · 𝑈) + (𝑃 · (𝑀 / 𝑈))) + -((𝑀↑3) / (𝑈↑3)))) | 
| 48 | 15, 1 | mulcld 11281 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃 · 𝑈) ∈ ℂ) | 
| 49 | 48 | negcld 11607 | . . . . . . . . . 10
⊢ (𝜑 → -(𝑃 · 𝑈) ∈ ℂ) | 
| 50 | 15, 37 | mulcld 11281 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃 · (𝑀 / 𝑈)) ∈ ℂ) | 
| 51 | 49, 50, 32 | addassd 11283 | . . . . . . . . 9
⊢ (𝜑 → ((-(𝑃 · 𝑈) + (𝑃 · (𝑀 / 𝑈))) + -((𝑀↑3) / (𝑈↑3))) = (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))))) | 
| 52 | 47, 51 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 → (-(𝑃 · 𝑋) + -((𝑀↑3) / (𝑈↑3))) = (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))))) | 
| 53 | 52 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((-(𝑃 · 𝑋) + -((𝑀↑3) / (𝑈↑3))) + ((𝑃 · 𝑋) + 𝑄)) = ((-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) + ((𝑃 · 𝑋) + 𝑄))) | 
| 54 | 31, 30 | addcomd 11463 | . . . . . . . . . 10
⊢ (𝜑 → (-(𝑃 · 𝑋) + (𝑃 · 𝑋)) = ((𝑃 · 𝑋) + -(𝑃 · 𝑋))) | 
| 55 | 30 | negidd 11610 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑃 · 𝑋) + -(𝑃 · 𝑋)) = 0) | 
| 56 | 54, 55 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → (-(𝑃 · 𝑋) + (𝑃 · 𝑋)) = 0) | 
| 57 | 56 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → ((-(𝑃 · 𝑋) + (𝑃 · 𝑋)) + (𝑄 + -((𝑀↑3) / (𝑈↑3)))) = (0 + (𝑄 + -((𝑀↑3) / (𝑈↑3))))) | 
| 58 | 13, 32 | addcld 11280 | . . . . . . . . 9
⊢ (𝜑 → (𝑄 + -((𝑀↑3) / (𝑈↑3))) ∈ ℂ) | 
| 59 | 58 | addlidd 11462 | . . . . . . . 8
⊢ (𝜑 → (0 + (𝑄 + -((𝑀↑3) / (𝑈↑3)))) = (𝑄 + -((𝑀↑3) / (𝑈↑3)))) | 
| 60 | 57, 59 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → ((-(𝑃 · 𝑋) + (𝑃 · 𝑋)) + (𝑄 + -((𝑀↑3) / (𝑈↑3)))) = (𝑄 + -((𝑀↑3) / (𝑈↑3)))) | 
| 61 | 33, 53, 60 | 3eqtr3d 2785 | . . . . . 6
⊢ (𝜑 → ((-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) + ((𝑃 · 𝑋) + 𝑄)) = (𝑄 + -((𝑀↑3) / (𝑈↑3)))) | 
| 62 | 13, 4 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝑄 · (𝑈↑3)) ∈ ℂ) | 
| 63 | 62, 23, 4, 10 | divsubdird 12082 | . . . . . 6
⊢ (𝜑 → (((𝑄 · (𝑈↑3)) − (𝑀↑3)) / (𝑈↑3)) = (((𝑄 · (𝑈↑3)) / (𝑈↑3)) − ((𝑀↑3) / (𝑈↑3)))) | 
| 64 | 28, 61, 63 | 3eqtr4d 2787 | . . . . 5
⊢ (𝜑 → ((-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) + ((𝑃 · 𝑋) + 𝑄)) = (((𝑄 · (𝑈↑3)) − (𝑀↑3)) / (𝑈↑3))) | 
| 65 | 12, 64 | oveq12d 7449 | . . . 4
⊢ (𝜑 → ((𝑈↑3) + ((-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) + ((𝑃 · 𝑋) + 𝑄))) = ((((𝑈↑3)↑2) / (𝑈↑3)) + (((𝑄 · (𝑈↑3)) − (𝑀↑3)) / (𝑈↑3)))) | 
| 66 | 1, 37 | negsubd 11626 | . . . . . . . . . 10
⊢ (𝜑 → (𝑈 + -(𝑀 / 𝑈)) = (𝑈 − (𝑀 / 𝑈))) | 
| 67 | 35, 66 | eqtr4d 2780 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 = (𝑈 + -(𝑀 / 𝑈))) | 
| 68 | 67 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → (𝑋↑3) = ((𝑈 + -(𝑀 / 𝑈))↑3)) | 
| 69 | 37 | negcld 11607 | . . . . . . . . 9
⊢ (𝜑 → -(𝑀 / 𝑈) ∈ ℂ) | 
| 70 |  | binom3 14263 | . . . . . . . . 9
⊢ ((𝑈 ∈ ℂ ∧ -(𝑀 / 𝑈) ∈ ℂ) → ((𝑈 + -(𝑀 / 𝑈))↑3) = (((𝑈↑3) + (3 · ((𝑈↑2) · -(𝑀 / 𝑈)))) + ((3 · (𝑈 · (-(𝑀 / 𝑈)↑2))) + (-(𝑀 / 𝑈)↑3)))) | 
| 71 | 1, 69, 70 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ((𝑈 + -(𝑀 / 𝑈))↑3) = (((𝑈↑3) + (3 · ((𝑈↑2) · -(𝑀 / 𝑈)))) + ((3 · (𝑈 · (-(𝑀 / 𝑈)↑2))) + (-(𝑀 / 𝑈)↑3)))) | 
| 72 | 1 | sqcld 14184 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈↑2) ∈ ℂ) | 
| 73 | 72, 37 | mulneg2d 11717 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈↑2) · -(𝑀 / 𝑈)) = -((𝑈↑2) · (𝑀 / 𝑈))) | 
| 74 | 72, 21, 1, 7 | div12d 12079 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑈↑2) · (𝑀 / 𝑈)) = (𝑀 · ((𝑈↑2) / 𝑈))) | 
| 75 | 1 | sqvald 14183 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈↑2) = (𝑈 · 𝑈)) | 
| 76 | 75 | oveq1d 7446 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑈↑2) / 𝑈) = ((𝑈 · 𝑈) / 𝑈)) | 
| 77 | 1, 1, 7 | divcan4d 12049 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑈 · 𝑈) / 𝑈) = 𝑈) | 
| 78 | 76, 77 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑈↑2) / 𝑈) = 𝑈) | 
| 79 | 78 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 · ((𝑈↑2) / 𝑈)) = (𝑀 · 𝑈)) | 
| 80 | 74, 79 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑈↑2) · (𝑀 / 𝑈)) = (𝑀 · 𝑈)) | 
| 81 | 80 | negeqd 11502 | . . . . . . . . . . . . 13
⊢ (𝜑 → -((𝑈↑2) · (𝑀 / 𝑈)) = -(𝑀 · 𝑈)) | 
| 82 | 73, 81 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈↑2) · -(𝑀 / 𝑈)) = -(𝑀 · 𝑈)) | 
| 83 | 82 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (3 · ((𝑈↑2) · -(𝑀 / 𝑈))) = (3 · -(𝑀 · 𝑈))) | 
| 84 | 21, 1 | mulcld 11281 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 · 𝑈) ∈ ℂ) | 
| 85 | 17, 84 | mulneg2d 11717 | . . . . . . . . . . 11
⊢ (𝜑 → (3 · -(𝑀 · 𝑈)) = -(3 · (𝑀 · 𝑈))) | 
| 86 | 17, 21, 1 | mulassd 11284 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((3 · 𝑀) · 𝑈) = (3 · (𝑀 · 𝑈))) | 
| 87 | 14 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (3 · 𝑀) = (3 · (𝑃 / 3))) | 
| 88 | 15, 17, 19 | divcan2d 12045 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (3 · (𝑃 / 3)) = 𝑃) | 
| 89 | 87, 88 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (3 · 𝑀) = 𝑃) | 
| 90 | 89 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((3 · 𝑀) · 𝑈) = (𝑃 · 𝑈)) | 
| 91 | 86, 90 | eqtr3d 2779 | . . . . . . . . . . . 12
⊢ (𝜑 → (3 · (𝑀 · 𝑈)) = (𝑃 · 𝑈)) | 
| 92 | 91 | negeqd 11502 | . . . . . . . . . . 11
⊢ (𝜑 → -(3 · (𝑀 · 𝑈)) = -(𝑃 · 𝑈)) | 
| 93 | 83, 85, 92 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (𝜑 → (3 · ((𝑈↑2) · -(𝑀 / 𝑈))) = -(𝑃 · 𝑈)) | 
| 94 | 93 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((𝑈↑3) + (3 · ((𝑈↑2) · -(𝑀 / 𝑈)))) = ((𝑈↑3) + -(𝑃 · 𝑈))) | 
| 95 |  | sqneg 14156 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 / 𝑈) ∈ ℂ → (-(𝑀 / 𝑈)↑2) = ((𝑀 / 𝑈)↑2)) | 
| 96 | 37, 95 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (-(𝑀 / 𝑈)↑2) = ((𝑀 / 𝑈)↑2)) | 
| 97 | 37 | sqvald 14183 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 / 𝑈)↑2) = ((𝑀 / 𝑈) · (𝑀 / 𝑈))) | 
| 98 | 96, 97 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (-(𝑀 / 𝑈)↑2) = ((𝑀 / 𝑈) · (𝑀 / 𝑈))) | 
| 99 | 98 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 · (-(𝑀 / 𝑈)↑2)) = (𝑈 · ((𝑀 / 𝑈) · (𝑀 / 𝑈)))) | 
| 100 | 1, 37, 37 | mulassd 11284 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 · (𝑀 / 𝑈)) · (𝑀 / 𝑈)) = (𝑈 · ((𝑀 / 𝑈) · (𝑀 / 𝑈)))) | 
| 101 | 21, 1, 7 | divcan2d 12045 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 · (𝑀 / 𝑈)) = 𝑀) | 
| 102 | 101 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 · (𝑀 / 𝑈)) · (𝑀 / 𝑈)) = (𝑀 · (𝑀 / 𝑈))) | 
| 103 | 99, 100, 102 | 3eqtr2d 2783 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 · (-(𝑀 / 𝑈)↑2)) = (𝑀 · (𝑀 / 𝑈))) | 
| 104 | 103 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (3 · (𝑈 · (-(𝑀 / 𝑈)↑2))) = (3 · (𝑀 · (𝑀 / 𝑈)))) | 
| 105 | 17, 21, 37 | mulassd 11284 | . . . . . . . . . . 11
⊢ (𝜑 → ((3 · 𝑀) · (𝑀 / 𝑈)) = (3 · (𝑀 · (𝑀 / 𝑈)))) | 
| 106 | 89 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝜑 → ((3 · 𝑀) · (𝑀 / 𝑈)) = (𝑃 · (𝑀 / 𝑈))) | 
| 107 | 104, 105,
106 | 3eqtr2d 2783 | . . . . . . . . . 10
⊢ (𝜑 → (3 · (𝑈 · (-(𝑀 / 𝑈)↑2))) = (𝑃 · (𝑀 / 𝑈))) | 
| 108 |  | 3nn 12345 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℕ | 
| 109 | 108 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ∈
ℕ) | 
| 110 |  | n2dvds3 16408 | . . . . . . . . . . . . 13
⊢  ¬ 2
∥ 3 | 
| 111 | 110 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ 2 ∥
3) | 
| 112 |  | oexpneg 16382 | . . . . . . . . . . . 12
⊢ (((𝑀 / 𝑈) ∈ ℂ ∧ 3 ∈ ℕ
∧ ¬ 2 ∥ 3) → (-(𝑀 / 𝑈)↑3) = -((𝑀 / 𝑈)↑3)) | 
| 113 | 37, 109, 111, 112 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (𝜑 → (-(𝑀 / 𝑈)↑3) = -((𝑀 / 𝑈)↑3)) | 
| 114 | 2 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 3 ∈
ℕ0) | 
| 115 | 21, 1, 7, 114 | expdivd 14200 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑀 / 𝑈)↑3) = ((𝑀↑3) / (𝑈↑3))) | 
| 116 | 115 | negeqd 11502 | . . . . . . . . . . 11
⊢ (𝜑 → -((𝑀 / 𝑈)↑3) = -((𝑀↑3) / (𝑈↑3))) | 
| 117 | 113, 116 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝜑 → (-(𝑀 / 𝑈)↑3) = -((𝑀↑3) / (𝑈↑3))) | 
| 118 | 107, 117 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝜑 → ((3 · (𝑈 · (-(𝑀 / 𝑈)↑2))) + (-(𝑀 / 𝑈)↑3)) = ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) | 
| 119 | 94, 118 | oveq12d 7449 | . . . . . . . 8
⊢ (𝜑 → (((𝑈↑3) + (3 · ((𝑈↑2) · -(𝑀 / 𝑈)))) + ((3 · (𝑈 · (-(𝑀 / 𝑈)↑2))) + (-(𝑀 / 𝑈)↑3))) = (((𝑈↑3) + -(𝑃 · 𝑈)) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))))) | 
| 120 | 68, 71, 119 | 3eqtrd 2781 | . . . . . . 7
⊢ (𝜑 → (𝑋↑3) = (((𝑈↑3) + -(𝑃 · 𝑈)) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))))) | 
| 121 | 50, 32 | addcld 11280 | . . . . . . . 8
⊢ (𝜑 → ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))) ∈ ℂ) | 
| 122 | 4, 49, 121 | addassd 11283 | . . . . . . 7
⊢ (𝜑 → (((𝑈↑3) + -(𝑃 · 𝑈)) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) = ((𝑈↑3) + (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))))) | 
| 123 | 120, 122 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → (𝑋↑3) = ((𝑈↑3) + (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))))) | 
| 124 | 123 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (((𝑈↑3) + (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))))) + ((𝑃 · 𝑋) + 𝑄))) | 
| 125 | 49, 121 | addcld 11280 | . . . . . 6
⊢ (𝜑 → (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) ∈ ℂ) | 
| 126 | 30, 13 | addcld 11280 | . . . . . 6
⊢ (𝜑 → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ) | 
| 127 | 4, 125, 126 | addassd 11283 | . . . . 5
⊢ (𝜑 → (((𝑈↑3) + (-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3))))) + ((𝑃 · 𝑋) + 𝑄)) = ((𝑈↑3) + ((-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) + ((𝑃 · 𝑋) + 𝑄)))) | 
| 128 | 124, 127 | eqtrd 2777 | . . . 4
⊢ (𝜑 → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = ((𝑈↑3) + ((-(𝑃 · 𝑈) + ((𝑃 · (𝑀 / 𝑈)) + -((𝑀↑3) / (𝑈↑3)))) + ((𝑃 · 𝑋) + 𝑄)))) | 
| 129 | 4 | sqcld 14184 | . . . . 5
⊢ (𝜑 → ((𝑈↑3)↑2) ∈
ℂ) | 
| 130 | 62, 23 | subcld 11620 | . . . . 5
⊢ (𝜑 → ((𝑄 · (𝑈↑3)) − (𝑀↑3)) ∈ ℂ) | 
| 131 | 129, 130,
4, 10 | divdird 12081 | . . . 4
⊢ (𝜑 → ((((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) / (𝑈↑3)) = ((((𝑈↑3)↑2) / (𝑈↑3)) + (((𝑄 · (𝑈↑3)) − (𝑀↑3)) / (𝑈↑3)))) | 
| 132 | 65, 128, 131 | 3eqtr4d 2787 | . . 3
⊢ (𝜑 → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = ((((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) / (𝑈↑3))) | 
| 133 | 132 | eqeq1d 2739 | . 2
⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ((((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) / (𝑈↑3)) = 0)) | 
| 134 | 129, 130 | addcld 11280 | . . 3
⊢ (𝜑 → (((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) ∈ ℂ) | 
| 135 | 134, 4, 10 | diveq0ad 12053 | . 2
⊢ (𝜑 → (((((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) / (𝑈↑3)) = 0 ↔ (((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) = 0)) | 
| 136 | 133, 135 | bitrd 279 | 1
⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ (((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) = 0)) |