MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dcubic1lem Structured version   Visualization version   GIF version

Theorem dcubic1lem 26196
Description: Lemma for dcubic1 26198 and dcubic2 26197: simplify the cubic equation under the substitution ๐‘‹ = ๐‘ˆ โˆ’ ๐‘€ / ๐‘ˆ. (Contributed by Mario Carneiro, 26-Apr-2015.)
Hypotheses
Ref Expression
dcubic.c (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
dcubic.d (๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚)
dcubic.x (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
dcubic.t (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
dcubic.3 (๐œ‘ โ†’ (๐‘‡โ†‘3) = (๐บ โˆ’ ๐‘))
dcubic.g (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
dcubic.2 (๐œ‘ โ†’ (๐บโ†‘2) = ((๐‘โ†‘2) + (๐‘€โ†‘3)))
dcubic.m (๐œ‘ โ†’ ๐‘€ = (๐‘ƒ / 3))
dcubic.n (๐œ‘ โ†’ ๐‘ = (๐‘„ / 2))
dcubic.0 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
dcubic2.u (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„‚)
dcubic2.z (๐œ‘ โ†’ ๐‘ˆ โ‰  0)
dcubic2.2 (๐œ‘ โ†’ ๐‘‹ = (๐‘ˆ โˆ’ (๐‘€ / ๐‘ˆ)))
Assertion
Ref Expression
dcubic1lem (๐œ‘ โ†’ (((๐‘‹โ†‘3) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = 0 โ†” (((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) = 0))

Proof of Theorem dcubic1lem
StepHypRef Expression
1 dcubic2.u . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„‚)
2 3nn0 12432 . . . . . . . . 9 3 โˆˆ โ„•0
3 expcl 13986 . . . . . . . . 9 ((๐‘ˆ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘ˆโ†‘3) โˆˆ โ„‚)
41, 2, 3sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ˆโ†‘3) โˆˆ โ„‚)
54sqvald 14049 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ˆโ†‘3)โ†‘2) = ((๐‘ˆโ†‘3) ยท (๐‘ˆโ†‘3)))
65oveq1d 7373 . . . . . 6 (๐œ‘ โ†’ (((๐‘ˆโ†‘3)โ†‘2) / (๐‘ˆโ†‘3)) = (((๐‘ˆโ†‘3) ยท (๐‘ˆโ†‘3)) / (๐‘ˆโ†‘3)))
7 dcubic2.z . . . . . . . 8 (๐œ‘ โ†’ ๐‘ˆ โ‰  0)
8 3z 12537 . . . . . . . . 9 3 โˆˆ โ„ค
98a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 3 โˆˆ โ„ค)
101, 7, 9expne0d 14058 . . . . . . 7 (๐œ‘ โ†’ (๐‘ˆโ†‘3) โ‰  0)
114, 4, 10divcan4d 11938 . . . . . 6 (๐œ‘ โ†’ (((๐‘ˆโ†‘3) ยท (๐‘ˆโ†‘3)) / (๐‘ˆโ†‘3)) = (๐‘ˆโ†‘3))
126, 11eqtr2d 2778 . . . . 5 (๐œ‘ โ†’ (๐‘ˆโ†‘3) = (((๐‘ˆโ†‘3)โ†‘2) / (๐‘ˆโ†‘3)))
13 dcubic.d . . . . . . . 8 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚)
14 dcubic.m . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ = (๐‘ƒ / 3))
15 dcubic.c . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
16 3cn 12235 . . . . . . . . . . . . 13 3 โˆˆ โ„‚
1716a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
18 3ne0 12260 . . . . . . . . . . . . 13 3 โ‰  0
1918a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 3 โ‰  0)
2015, 17, 19divcld 11932 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ƒ / 3) โˆˆ โ„‚)
2114, 20eqeltrd 2838 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
22 expcl 13986 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘€โ†‘3) โˆˆ โ„‚)
2321, 2, 22sylancl 587 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€โ†‘3) โˆˆ โ„‚)
2423, 4, 10divcld 11932 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘€โ†‘3) / (๐‘ˆโ†‘3)) โˆˆ โ„‚)
2513, 24negsubd 11519 . . . . . . 7 (๐œ‘ โ†’ (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) = (๐‘„ โˆ’ ((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
2613, 4, 10divcan4d 11938 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘„ ยท (๐‘ˆโ†‘3)) / (๐‘ˆโ†‘3)) = ๐‘„)
2726oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ (((๐‘„ ยท (๐‘ˆโ†‘3)) / (๐‘ˆโ†‘3)) โˆ’ ((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) = (๐‘„ โˆ’ ((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
2825, 27eqtr4d 2780 . . . . . 6 (๐œ‘ โ†’ (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) = (((๐‘„ ยท (๐‘ˆโ†‘3)) / (๐‘ˆโ†‘3)) โˆ’ ((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
29 dcubic.x . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
3015, 29mulcld 11176 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘‹) โˆˆ โ„‚)
3130negcld 11500 . . . . . . . 8 (๐œ‘ โ†’ -(๐‘ƒ ยท ๐‘‹) โˆˆ โ„‚)
3224negcld 11500 . . . . . . . 8 (๐œ‘ โ†’ -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)) โˆˆ โ„‚)
3331, 32, 30, 13add42d 11385 . . . . . . 7 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘‹) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = ((-(๐‘ƒ ยท ๐‘‹) + (๐‘ƒ ยท ๐‘‹)) + (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))))
3415, 29mulneg2d 11610 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ƒ ยท -๐‘‹) = -(๐‘ƒ ยท ๐‘‹))
35 dcubic2.2 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‹ = (๐‘ˆ โˆ’ (๐‘€ / ๐‘ˆ)))
3635negeqd 11396 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ -๐‘‹ = -(๐‘ˆ โˆ’ (๐‘€ / ๐‘ˆ)))
3721, 1, 7divcld 11932 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘€ / ๐‘ˆ) โˆˆ โ„‚)
381, 37negsubdid 11528 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ -(๐‘ˆ โˆ’ (๐‘€ / ๐‘ˆ)) = (-๐‘ˆ + (๐‘€ / ๐‘ˆ)))
3936, 38eqtrd 2777 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -๐‘‹ = (-๐‘ˆ + (๐‘€ / ๐‘ˆ)))
4039oveq2d 7374 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ƒ ยท -๐‘‹) = (๐‘ƒ ยท (-๐‘ˆ + (๐‘€ / ๐‘ˆ))))
4134, 40eqtr3d 2779 . . . . . . . . . . 11 (๐œ‘ โ†’ -(๐‘ƒ ยท ๐‘‹) = (๐‘ƒ ยท (-๐‘ˆ + (๐‘€ / ๐‘ˆ))))
421negcld 11500 . . . . . . . . . . . 12 (๐œ‘ โ†’ -๐‘ˆ โˆˆ โ„‚)
4315, 42, 37adddid 11180 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ƒ ยท (-๐‘ˆ + (๐‘€ / ๐‘ˆ))) = ((๐‘ƒ ยท -๐‘ˆ) + (๐‘ƒ ยท (๐‘€ / ๐‘ˆ))))
4415, 1mulneg2d 11610 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ƒ ยท -๐‘ˆ) = -(๐‘ƒ ยท ๐‘ˆ))
4544oveq1d 7373 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘ƒ ยท -๐‘ˆ) + (๐‘ƒ ยท (๐‘€ / ๐‘ˆ))) = (-(๐‘ƒ ยท ๐‘ˆ) + (๐‘ƒ ยท (๐‘€ / ๐‘ˆ))))
4641, 43, 453eqtrd 2781 . . . . . . . . . 10 (๐œ‘ โ†’ -(๐‘ƒ ยท ๐‘‹) = (-(๐‘ƒ ยท ๐‘ˆ) + (๐‘ƒ ยท (๐‘€ / ๐‘ˆ))))
4746oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ (-(๐‘ƒ ยท ๐‘‹) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) = ((-(๐‘ƒ ยท ๐‘ˆ) + (๐‘ƒ ยท (๐‘€ / ๐‘ˆ))) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
4815, 1mulcld 11176 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘ˆ) โˆˆ โ„‚)
4948negcld 11500 . . . . . . . . . 10 (๐œ‘ โ†’ -(๐‘ƒ ยท ๐‘ˆ) โˆˆ โ„‚)
5015, 37mulcld 11176 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) โˆˆ โ„‚)
5149, 50, 32addassd 11178 . . . . . . . . 9 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘ˆ) + (๐‘ƒ ยท (๐‘€ / ๐‘ˆ))) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) = (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))))
5247, 51eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ (-(๐‘ƒ ยท ๐‘‹) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) = (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))))
5352oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘‹) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = ((-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)))
5431, 30addcomd 11358 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘ƒ ยท ๐‘‹) + (๐‘ƒ ยท ๐‘‹)) = ((๐‘ƒ ยท ๐‘‹) + -(๐‘ƒ ยท ๐‘‹)))
5530negidd 11503 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ƒ ยท ๐‘‹) + -(๐‘ƒ ยท ๐‘‹)) = 0)
5654, 55eqtrd 2777 . . . . . . . . 9 (๐œ‘ โ†’ (-(๐‘ƒ ยท ๐‘‹) + (๐‘ƒ ยท ๐‘‹)) = 0)
5756oveq1d 7373 . . . . . . . 8 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘‹) + (๐‘ƒ ยท ๐‘‹)) + (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) = (0 + (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))))
5813, 32addcld 11175 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) โˆˆ โ„‚)
5958addid2d 11357 . . . . . . . 8 (๐œ‘ โ†’ (0 + (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) = (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
6057, 59eqtrd 2777 . . . . . . 7 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘‹) + (๐‘ƒ ยท ๐‘‹)) + (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) = (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
6133, 53, 603eqtr3d 2785 . . . . . 6 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = (๐‘„ + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
6213, 4mulcld 11176 . . . . . . 7 (๐œ‘ โ†’ (๐‘„ ยท (๐‘ˆโ†‘3)) โˆˆ โ„‚)
6362, 23, 4, 10divsubdird 11971 . . . . . 6 (๐œ‘ โ†’ (((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3)) / (๐‘ˆโ†‘3)) = (((๐‘„ ยท (๐‘ˆโ†‘3)) / (๐‘ˆโ†‘3)) โˆ’ ((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
6428, 61, 633eqtr4d 2787 . . . . 5 (๐œ‘ โ†’ ((-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = (((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3)) / (๐‘ˆโ†‘3)))
6512, 64oveq12d 7376 . . . 4 (๐œ‘ โ†’ ((๐‘ˆโ†‘3) + ((-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„))) = ((((๐‘ˆโ†‘3)โ†‘2) / (๐‘ˆโ†‘3)) + (((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3)) / (๐‘ˆโ†‘3))))
661, 37negsubd 11519 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ˆ + -(๐‘€ / ๐‘ˆ)) = (๐‘ˆ โˆ’ (๐‘€ / ๐‘ˆ)))
6735, 66eqtr4d 2780 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ = (๐‘ˆ + -(๐‘€ / ๐‘ˆ)))
6867oveq1d 7373 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‹โ†‘3) = ((๐‘ˆ + -(๐‘€ / ๐‘ˆ))โ†‘3))
6937negcld 11500 . . . . . . . . 9 (๐œ‘ โ†’ -(๐‘€ / ๐‘ˆ) โˆˆ โ„‚)
70 binom3 14128 . . . . . . . . 9 ((๐‘ˆ โˆˆ โ„‚ โˆง -(๐‘€ / ๐‘ˆ) โˆˆ โ„‚) โ†’ ((๐‘ˆ + -(๐‘€ / ๐‘ˆ))โ†‘3) = (((๐‘ˆโ†‘3) + (3 ยท ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ)))) + ((3 ยท (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2))) + (-(๐‘€ / ๐‘ˆ)โ†‘3))))
711, 69, 70syl2anc 585 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ˆ + -(๐‘€ / ๐‘ˆ))โ†‘3) = (((๐‘ˆโ†‘3) + (3 ยท ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ)))) + ((3 ยท (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2))) + (-(๐‘€ / ๐‘ˆ)โ†‘3))))
721sqcld 14050 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ˆโ†‘2) โˆˆ โ„‚)
7372, 37mulneg2d 11610 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ)) = -((๐‘ˆโ†‘2) ยท (๐‘€ / ๐‘ˆ)))
7472, 21, 1, 7div12d 11968 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘ˆโ†‘2) ยท (๐‘€ / ๐‘ˆ)) = (๐‘€ ยท ((๐‘ˆโ†‘2) / ๐‘ˆ)))
751sqvald 14049 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘ˆโ†‘2) = (๐‘ˆ ยท ๐‘ˆ))
7675oveq1d 7373 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ˆโ†‘2) / ๐‘ˆ) = ((๐‘ˆ ยท ๐‘ˆ) / ๐‘ˆ))
771, 1, 7divcan4d 11938 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ˆ ยท ๐‘ˆ) / ๐‘ˆ) = ๐‘ˆ)
7876, 77eqtrd 2777 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐‘ˆโ†‘2) / ๐‘ˆ) = ๐‘ˆ)
7978oveq2d 7374 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘€ ยท ((๐‘ˆโ†‘2) / ๐‘ˆ)) = (๐‘€ ยท ๐‘ˆ))
8074, 79eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐‘ˆโ†‘2) ยท (๐‘€ / ๐‘ˆ)) = (๐‘€ ยท ๐‘ˆ))
8180negeqd 11396 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -((๐‘ˆโ†‘2) ยท (๐‘€ / ๐‘ˆ)) = -(๐‘€ ยท ๐‘ˆ))
8273, 81eqtrd 2777 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ)) = -(๐‘€ ยท ๐‘ˆ))
8382oveq2d 7374 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 ยท ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ))) = (3 ยท -(๐‘€ ยท ๐‘ˆ)))
8421, 1mulcld 11176 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘€ ยท ๐‘ˆ) โˆˆ โ„‚)
8517, 84mulneg2d 11610 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 ยท -(๐‘€ ยท ๐‘ˆ)) = -(3 ยท (๐‘€ ยท ๐‘ˆ)))
8617, 21, 1mulassd 11179 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3 ยท ๐‘€) ยท ๐‘ˆ) = (3 ยท (๐‘€ ยท ๐‘ˆ)))
8714oveq2d 7374 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (3 ยท ๐‘€) = (3 ยท (๐‘ƒ / 3)))
8815, 17, 19divcan2d 11934 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (3 ยท (๐‘ƒ / 3)) = ๐‘ƒ)
8987, 88eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3 ยท ๐‘€) = ๐‘ƒ)
9089oveq1d 7373 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3 ยท ๐‘€) ยท ๐‘ˆ) = (๐‘ƒ ยท ๐‘ˆ))
9186, 90eqtr3d 2779 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (๐‘€ ยท ๐‘ˆ)) = (๐‘ƒ ยท ๐‘ˆ))
9291negeqd 11396 . . . . . . . . . . 11 (๐œ‘ โ†’ -(3 ยท (๐‘€ ยท ๐‘ˆ)) = -(๐‘ƒ ยท ๐‘ˆ))
9383, 85, 923eqtrd 2781 . . . . . . . . . 10 (๐œ‘ โ†’ (3 ยท ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ))) = -(๐‘ƒ ยท ๐‘ˆ))
9493oveq2d 7374 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ˆโ†‘3) + (3 ยท ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ)))) = ((๐‘ˆโ†‘3) + -(๐‘ƒ ยท ๐‘ˆ)))
95 sqneg 14022 . . . . . . . . . . . . . . . 16 ((๐‘€ / ๐‘ˆ) โˆˆ โ„‚ โ†’ (-(๐‘€ / ๐‘ˆ)โ†‘2) = ((๐‘€ / ๐‘ˆ)โ†‘2))
9637, 95syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (-(๐‘€ / ๐‘ˆ)โ†‘2) = ((๐‘€ / ๐‘ˆ)โ†‘2))
9737sqvald 14049 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘€ / ๐‘ˆ)โ†‘2) = ((๐‘€ / ๐‘ˆ) ยท (๐‘€ / ๐‘ˆ)))
9896, 97eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (-(๐‘€ / ๐‘ˆ)โ†‘2) = ((๐‘€ / ๐‘ˆ) ยท (๐‘€ / ๐‘ˆ)))
9998oveq2d 7374 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2)) = (๐‘ˆ ยท ((๐‘€ / ๐‘ˆ) ยท (๐‘€ / ๐‘ˆ))))
1001, 37, 37mulassd 11179 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ˆ ยท (๐‘€ / ๐‘ˆ)) ยท (๐‘€ / ๐‘ˆ)) = (๐‘ˆ ยท ((๐‘€ / ๐‘ˆ) ยท (๐‘€ / ๐‘ˆ))))
10121, 1, 7divcan2d 11934 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ˆ ยท (๐‘€ / ๐‘ˆ)) = ๐‘€)
102101oveq1d 7373 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ˆ ยท (๐‘€ / ๐‘ˆ)) ยท (๐‘€ / ๐‘ˆ)) = (๐‘€ ยท (๐‘€ / ๐‘ˆ)))
10399, 100, 1023eqtr2d 2783 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2)) = (๐‘€ ยท (๐‘€ / ๐‘ˆ)))
104103oveq2d 7374 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 ยท (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2))) = (3 ยท (๐‘€ ยท (๐‘€ / ๐‘ˆ))))
10517, 21, 37mulassd 11179 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3 ยท ๐‘€) ยท (๐‘€ / ๐‘ˆ)) = (3 ยท (๐‘€ ยท (๐‘€ / ๐‘ˆ))))
10689oveq1d 7373 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3 ยท ๐‘€) ยท (๐‘€ / ๐‘ˆ)) = (๐‘ƒ ยท (๐‘€ / ๐‘ˆ)))
107104, 105, 1063eqtr2d 2783 . . . . . . . . . 10 (๐œ‘ โ†’ (3 ยท (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2))) = (๐‘ƒ ยท (๐‘€ / ๐‘ˆ)))
108 3nn 12233 . . . . . . . . . . . . 13 3 โˆˆ โ„•
109108a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 3 โˆˆ โ„•)
110 n2dvds3 16254 . . . . . . . . . . . . 13 ยฌ 2 โˆฅ 3
111110a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ ยฌ 2 โˆฅ 3)
112 oexpneg 16228 . . . . . . . . . . . 12 (((๐‘€ / ๐‘ˆ) โˆˆ โ„‚ โˆง 3 โˆˆ โ„• โˆง ยฌ 2 โˆฅ 3) โ†’ (-(๐‘€ / ๐‘ˆ)โ†‘3) = -((๐‘€ / ๐‘ˆ)โ†‘3))
11337, 109, 111, 112syl3anc 1372 . . . . . . . . . . 11 (๐œ‘ โ†’ (-(๐‘€ / ๐‘ˆ)โ†‘3) = -((๐‘€ / ๐‘ˆ)โ†‘3))
1142a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
11521, 1, 7, 114expdivd 14066 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ / ๐‘ˆ)โ†‘3) = ((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))
116115negeqd 11396 . . . . . . . . . . 11 (๐œ‘ โ†’ -((๐‘€ / ๐‘ˆ)โ†‘3) = -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))
117113, 116eqtrd 2777 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘€ / ๐‘ˆ)โ†‘3) = -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))
118107, 117oveq12d 7376 . . . . . . . . 9 (๐œ‘ โ†’ ((3 ยท (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2))) + (-(๐‘€ / ๐‘ˆ)โ†‘3)) = ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))
11994, 118oveq12d 7376 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ˆโ†‘3) + (3 ยท ((๐‘ˆโ†‘2) ยท -(๐‘€ / ๐‘ˆ)))) + ((3 ยท (๐‘ˆ ยท (-(๐‘€ / ๐‘ˆ)โ†‘2))) + (-(๐‘€ / ๐‘ˆ)โ†‘3))) = (((๐‘ˆโ†‘3) + -(๐‘ƒ ยท ๐‘ˆ)) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))))
12068, 71, 1193eqtrd 2781 . . . . . . 7 (๐œ‘ โ†’ (๐‘‹โ†‘3) = (((๐‘ˆโ†‘3) + -(๐‘ƒ ยท ๐‘ˆ)) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))))
12150, 32addcld 11175 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))) โˆˆ โ„‚)
1224, 49, 121addassd 11178 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ˆโ†‘3) + -(๐‘ƒ ยท ๐‘ˆ)) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) = ((๐‘ˆโ†‘3) + (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))))
123120, 122eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ (๐‘‹โ†‘3) = ((๐‘ˆโ†‘3) + (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))))
124123oveq1d 7373 . . . . 5 (๐œ‘ โ†’ ((๐‘‹โ†‘3) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = (((๐‘ˆโ†‘3) + (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)))
12549, 121addcld 11175 . . . . . 6 (๐œ‘ โ†’ (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) โˆˆ โ„‚)
12630, 13addcld 11175 . . . . . 6 (๐œ‘ โ†’ ((๐‘ƒ ยท ๐‘‹) + ๐‘„) โˆˆ โ„‚)
1274, 125, 126addassd 11178 . . . . 5 (๐œ‘ โ†’ (((๐‘ˆโ†‘3) + (-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3))))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = ((๐‘ˆโ†‘3) + ((-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„))))
128124, 127eqtrd 2777 . . . 4 (๐œ‘ โ†’ ((๐‘‹โ†‘3) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = ((๐‘ˆโ†‘3) + ((-(๐‘ƒ ยท ๐‘ˆ) + ((๐‘ƒ ยท (๐‘€ / ๐‘ˆ)) + -((๐‘€โ†‘3) / (๐‘ˆโ†‘3)))) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„))))
1294sqcld 14050 . . . . 5 (๐œ‘ โ†’ ((๐‘ˆโ†‘3)โ†‘2) โˆˆ โ„‚)
13062, 23subcld 11513 . . . . 5 (๐œ‘ โ†’ ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3)) โˆˆ โ„‚)
131129, 130, 4, 10divdird 11970 . . . 4 (๐œ‘ โ†’ ((((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) / (๐‘ˆโ†‘3)) = ((((๐‘ˆโ†‘3)โ†‘2) / (๐‘ˆโ†‘3)) + (((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3)) / (๐‘ˆโ†‘3))))
13265, 128, 1313eqtr4d 2787 . . 3 (๐œ‘ โ†’ ((๐‘‹โ†‘3) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = ((((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) / (๐‘ˆโ†‘3)))
133132eqeq1d 2739 . 2 (๐œ‘ โ†’ (((๐‘‹โ†‘3) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = 0 โ†” ((((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) / (๐‘ˆโ†‘3)) = 0))
134129, 130addcld 11175 . . 3 (๐œ‘ โ†’ (((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) โˆˆ โ„‚)
135134, 4, 10diveq0ad 11942 . 2 (๐œ‘ โ†’ (((((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) / (๐‘ˆโ†‘3)) = 0 โ†” (((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) = 0))
136133, 135bitrd 279 1 (๐œ‘ โ†’ (((๐‘‹โ†‘3) + ((๐‘ƒ ยท ๐‘‹) + ๐‘„)) = 0 โ†” (((๐‘ˆโ†‘3)โ†‘2) + ((๐‘„ ยท (๐‘ˆโ†‘3)) โˆ’ (๐‘€โ†‘3))) = 0))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944   class class class wbr 5106  (class class class)co 7358  โ„‚cc 11050  0cc0 11052   + caddc 11055   ยท cmul 11057   โˆ’ cmin 11386  -cneg 11387   / cdiv 11813  โ„•cn 12154  2c2 12209  3c3 12210  โ„•0cn0 12414  โ„คcz 12500  โ†‘cexp 13968   โˆฅ cdvds 16137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-n0 12415  df-z 12501  df-uz 12765  df-rp 12917  df-seq 13908  df-exp 13969  df-dvds 16138
This theorem is referenced by:  dcubic2  26197  dcubic1  26198
  Copyright terms: Public domain W3C validator