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

Theorem cubic2 26214
Description: The solution to the general cubic equation, for arbitrary choices ๐บ and ๐‘‡ of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
cubic2.a (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
cubic2.z (๐œ‘ โ†’ ๐ด โ‰  0)
cubic2.b (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
cubic2.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
cubic2.d (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
cubic2.x (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
cubic2.t (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
cubic2.3 (๐œ‘ โ†’ (๐‘‡โ†‘3) = ((๐‘ + ๐บ) / 2))
cubic2.g (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
cubic2.2 (๐œ‘ โ†’ (๐บโ†‘2) = ((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))))
cubic2.m (๐œ‘ โ†’ ๐‘€ = ((๐ตโ†‘2) โˆ’ (3 ยท (๐ด ยท ๐ถ))))
cubic2.n (๐œ‘ โ†’ ๐‘ = (((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) + (27 ยท ((๐ดโ†‘2) ยท ๐ท))))
cubic2.0 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
Assertion
Ref Expression
cubic2 (๐œ‘ โ†’ ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))))
Distinct variable groups:   ๐ด,๐‘Ÿ   ๐ต,๐‘Ÿ   ๐‘€,๐‘Ÿ   ๐‘,๐‘Ÿ   ๐œ‘,๐‘Ÿ   ๐‘‡,๐‘Ÿ   ๐‘‹,๐‘Ÿ
Allowed substitution hints:   ๐ถ(๐‘Ÿ)   ๐ท(๐‘Ÿ)   ๐บ(๐‘Ÿ)

Proof of Theorem cubic2
StepHypRef Expression
1 cubic2.a . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
2 cubic2.x . . . . . . . 8 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
3 3nn0 12438 . . . . . . . 8 3 โˆˆ โ„•0
4 expcl 13992 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
52, 3, 4sylancl 587 . . . . . . 7 (๐œ‘ โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
61, 5mulcld 11182 . . . . . 6 (๐œ‘ โ†’ (๐ด ยท (๐‘‹โ†‘3)) โˆˆ โ„‚)
7 cubic2.b . . . . . . 7 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
82sqcld 14056 . . . . . . 7 (๐œ‘ โ†’ (๐‘‹โ†‘2) โˆˆ โ„‚)
97, 8mulcld 11182 . . . . . 6 (๐œ‘ โ†’ (๐ต ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
106, 9addcld 11181 . . . . 5 (๐œ‘ โ†’ ((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) โˆˆ โ„‚)
11 cubic2.c . . . . . . 7 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
1211, 2mulcld 11182 . . . . . 6 (๐œ‘ โ†’ (๐ถ ยท ๐‘‹) โˆˆ โ„‚)
13 cubic2.d . . . . . 6 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
1412, 13addcld 11181 . . . . 5 (๐œ‘ โ†’ ((๐ถ ยท ๐‘‹) + ๐ท) โˆˆ โ„‚)
1510, 14addcld 11181 . . . 4 (๐œ‘ โ†’ (((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) โˆˆ โ„‚)
16 cubic2.z . . . 4 (๐œ‘ โ†’ ๐ด โ‰  0)
1715, 1, 16diveq0ad 11948 . . 3 (๐œ‘ โ†’ (((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) / ๐ด) = 0 โ†” (((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0))
1810, 14, 1, 16divdird 11976 . . . . 5 (๐œ‘ โ†’ ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) / ๐ด) = ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) / ๐ด) + (((๐ถ ยท ๐‘‹) + ๐ท) / ๐ด)))
196, 9, 1, 16divdird 11976 . . . . . . 7 (๐œ‘ โ†’ (((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) / ๐ด) = (((๐ด ยท (๐‘‹โ†‘3)) / ๐ด) + ((๐ต ยท (๐‘‹โ†‘2)) / ๐ด)))
205, 1, 16divcan3d 11943 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด ยท (๐‘‹โ†‘3)) / ๐ด) = (๐‘‹โ†‘3))
217, 8, 1, 16div23d 11975 . . . . . . . 8 (๐œ‘ โ†’ ((๐ต ยท (๐‘‹โ†‘2)) / ๐ด) = ((๐ต / ๐ด) ยท (๐‘‹โ†‘2)))
2220, 21oveq12d 7380 . . . . . . 7 (๐œ‘ โ†’ (((๐ด ยท (๐‘‹โ†‘3)) / ๐ด) + ((๐ต ยท (๐‘‹โ†‘2)) / ๐ด)) = ((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))))
2319, 22eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ (((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) / ๐ด) = ((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))))
2412, 13, 1, 16divdird 11976 . . . . . . 7 (๐œ‘ โ†’ (((๐ถ ยท ๐‘‹) + ๐ท) / ๐ด) = (((๐ถ ยท ๐‘‹) / ๐ด) + (๐ท / ๐ด)))
2511, 2, 1, 16div23d 11975 . . . . . . . 8 (๐œ‘ โ†’ ((๐ถ ยท ๐‘‹) / ๐ด) = ((๐ถ / ๐ด) ยท ๐‘‹))
2625oveq1d 7377 . . . . . . 7 (๐œ‘ โ†’ (((๐ถ ยท ๐‘‹) / ๐ด) + (๐ท / ๐ด)) = (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด)))
2724, 26eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ (((๐ถ ยท ๐‘‹) + ๐ท) / ๐ด) = (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด)))
2823, 27oveq12d 7380 . . . . 5 (๐œ‘ โ†’ ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) / ๐ด) + (((๐ถ ยท ๐‘‹) + ๐ท) / ๐ด)) = (((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))) + (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด))))
2918, 28eqtrd 2777 . . . 4 (๐œ‘ โ†’ ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) / ๐ด) = (((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))) + (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด))))
3029eqeq1d 2739 . . 3 (๐œ‘ โ†’ (((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) / ๐ด) = 0 โ†” (((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))) + (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด))) = 0))
3117, 30bitr3d 281 . 2 (๐œ‘ โ†’ ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” (((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))) + (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด))) = 0))
327, 1, 16divcld 11938 . . 3 (๐œ‘ โ†’ (๐ต / ๐ด) โˆˆ โ„‚)
3311, 1, 16divcld 11938 . . 3 (๐œ‘ โ†’ (๐ถ / ๐ด) โˆˆ โ„‚)
3413, 1, 16divcld 11938 . . 3 (๐œ‘ โ†’ (๐ท / ๐ด) โˆˆ โ„‚)
35 cubic2.t . . . 4 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
3635, 1, 16divcld 11938 . . 3 (๐œ‘ โ†’ (๐‘‡ / ๐ด) โˆˆ โ„‚)
373a1i 11 . . . . 5 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
3835, 1, 16, 37expdivd 14072 . . . 4 (๐œ‘ โ†’ ((๐‘‡ / ๐ด)โ†‘3) = ((๐‘‡โ†‘3) / (๐ดโ†‘3)))
39 cubic2.3 . . . . 5 (๐œ‘ โ†’ (๐‘‡โ†‘3) = ((๐‘ + ๐บ) / 2))
4039oveq1d 7377 . . . 4 (๐œ‘ โ†’ ((๐‘‡โ†‘3) / (๐ดโ†‘3)) = (((๐‘ + ๐บ) / 2) / (๐ดโ†‘3)))
41 cubic2.n . . . . . . . 8 (๐œ‘ โ†’ ๐‘ = (((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) + (27 ยท ((๐ดโ†‘2) ยท ๐ท))))
42 2cn 12235 . . . . . . . . . . 11 2 โˆˆ โ„‚
43 expcl 13992 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐ตโ†‘3) โˆˆ โ„‚)
447, 3, 43sylancl 587 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ตโ†‘3) โˆˆ โ„‚)
45 mulcl 11142 . . . . . . . . . . 11 ((2 โˆˆ โ„‚ โˆง (๐ตโ†‘3) โˆˆ โ„‚) โ†’ (2 ยท (๐ตโ†‘3)) โˆˆ โ„‚)
4642, 44, 45sylancr 588 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท (๐ตโ†‘3)) โˆˆ โ„‚)
47 9cn 12260 . . . . . . . . . . . 12 9 โˆˆ โ„‚
48 mulcl 11142 . . . . . . . . . . . 12 ((9 โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (9 ยท ๐ด) โˆˆ โ„‚)
4947, 1, 48sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ (9 ยท ๐ด) โˆˆ โ„‚)
507, 11mulcld 11182 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ต ยท ๐ถ) โˆˆ โ„‚)
5149, 50mulcld 11182 . . . . . . . . . 10 (๐œ‘ โ†’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) โˆˆ โ„‚)
5246, 51subcld 11519 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) โˆˆ โ„‚)
53 2nn0 12437 . . . . . . . . . . . 12 2 โˆˆ โ„•0
54 7nn 12252 . . . . . . . . . . . 12 7 โˆˆ โ„•
5553, 54decnncl 12645 . . . . . . . . . . 11 27 โˆˆ โ„•
5655nncni 12170 . . . . . . . . . 10 27 โˆˆ โ„‚
571sqcld 14056 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
5857, 13mulcld 11182 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ดโ†‘2) ยท ๐ท) โˆˆ โ„‚)
59 mulcl 11142 . . . . . . . . . 10 ((27 โˆˆ โ„‚ โˆง ((๐ดโ†‘2) ยท ๐ท) โˆˆ โ„‚) โ†’ (27 ยท ((๐ดโ†‘2) ยท ๐ท)) โˆˆ โ„‚)
6056, 58, 59sylancr 588 . . . . . . . . 9 (๐œ‘ โ†’ (27 ยท ((๐ดโ†‘2) ยท ๐ท)) โˆˆ โ„‚)
6152, 60addcld 11181 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) + (27 ยท ((๐ดโ†‘2) ยท ๐ท))) โˆˆ โ„‚)
6241, 61eqeltrd 2838 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
63 cubic2.g . . . . . . 7 (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
6462, 63addcld 11181 . . . . . 6 (๐œ‘ โ†’ (๐‘ + ๐บ) โˆˆ โ„‚)
65 2cnd 12238 . . . . . 6 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
66 expcl 13992 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐ดโ†‘3) โˆˆ โ„‚)
671, 3, 66sylancl 587 . . . . . 6 (๐œ‘ โ†’ (๐ดโ†‘3) โˆˆ โ„‚)
68 2ne0 12264 . . . . . . 7 2 โ‰  0
6968a1i 11 . . . . . 6 (๐œ‘ โ†’ 2 โ‰  0)
70 3z 12543 . . . . . . . 8 3 โˆˆ โ„ค
7170a1i 11 . . . . . . 7 (๐œ‘ โ†’ 3 โˆˆ โ„ค)
721, 16, 71expne0d 14064 . . . . . 6 (๐œ‘ โ†’ (๐ดโ†‘3) โ‰  0)
7364, 65, 67, 69, 72divdiv32d 11963 . . . . 5 (๐œ‘ โ†’ (((๐‘ + ๐บ) / 2) / (๐ดโ†‘3)) = (((๐‘ + ๐บ) / (๐ดโ†‘3)) / 2))
7462, 63, 67, 72divdird 11976 . . . . . 6 (๐œ‘ โ†’ ((๐‘ + ๐บ) / (๐ดโ†‘3)) = ((๐‘ / (๐ดโ†‘3)) + (๐บ / (๐ดโ†‘3))))
7574oveq1d 7377 . . . . 5 (๐œ‘ โ†’ (((๐‘ + ๐บ) / (๐ดโ†‘3)) / 2) = (((๐‘ / (๐ดโ†‘3)) + (๐บ / (๐ดโ†‘3))) / 2))
7673, 75eqtrd 2777 . . . 4 (๐œ‘ โ†’ (((๐‘ + ๐บ) / 2) / (๐ดโ†‘3)) = (((๐‘ / (๐ดโ†‘3)) + (๐บ / (๐ดโ†‘3))) / 2))
7738, 40, 763eqtrd 2781 . . 3 (๐œ‘ โ†’ ((๐‘‡ / ๐ด)โ†‘3) = (((๐‘ / (๐ดโ†‘3)) + (๐บ / (๐ดโ†‘3))) / 2))
7863, 67, 72divcld 11938 . . 3 (๐œ‘ โ†’ (๐บ / (๐ดโ†‘3)) โˆˆ โ„‚)
7963, 67, 72sqdivd 14071 . . . 4 (๐œ‘ โ†’ ((๐บ / (๐ดโ†‘3))โ†‘2) = ((๐บโ†‘2) / ((๐ดโ†‘3)โ†‘2)))
80 cubic2.2 . . . . 5 (๐œ‘ โ†’ (๐บโ†‘2) = ((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))))
8180oveq1d 7377 . . . 4 (๐œ‘ โ†’ ((๐บโ†‘2) / ((๐ดโ†‘3)โ†‘2)) = (((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))) / ((๐ดโ†‘3)โ†‘2)))
8262sqcld 14056 . . . . . 6 (๐œ‘ โ†’ (๐‘โ†‘2) โˆˆ โ„‚)
83 4cn 12245 . . . . . . 7 4 โˆˆ โ„‚
84 cubic2.m . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ = ((๐ตโ†‘2) โˆ’ (3 ยท (๐ด ยท ๐ถ))))
857sqcld 14056 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
86 3cn 12241 . . . . . . . . . . 11 3 โˆˆ โ„‚
871, 11mulcld 11182 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด ยท ๐ถ) โˆˆ โ„‚)
88 mulcl 11142 . . . . . . . . . . 11 ((3 โˆˆ โ„‚ โˆง (๐ด ยท ๐ถ) โˆˆ โ„‚) โ†’ (3 ยท (๐ด ยท ๐ถ)) โˆˆ โ„‚)
8986, 87, 88sylancr 588 . . . . . . . . . 10 (๐œ‘ โ†’ (3 ยท (๐ด ยท ๐ถ)) โˆˆ โ„‚)
9085, 89subcld 11519 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ตโ†‘2) โˆ’ (3 ยท (๐ด ยท ๐ถ))) โˆˆ โ„‚)
9184, 90eqeltrd 2838 . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
92 expcl 13992 . . . . . . . 8 ((๐‘€ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘€โ†‘3) โˆˆ โ„‚)
9391, 3, 92sylancl 587 . . . . . . 7 (๐œ‘ โ†’ (๐‘€โ†‘3) โˆˆ โ„‚)
94 mulcl 11142 . . . . . . 7 ((4 โˆˆ โ„‚ โˆง (๐‘€โ†‘3) โˆˆ โ„‚) โ†’ (4 ยท (๐‘€โ†‘3)) โˆˆ โ„‚)
9583, 93, 94sylancr 588 . . . . . 6 (๐œ‘ โ†’ (4 ยท (๐‘€โ†‘3)) โˆˆ โ„‚)
9667sqcld 14056 . . . . . 6 (๐œ‘ โ†’ ((๐ดโ†‘3)โ†‘2) โˆˆ โ„‚)
97 sqne0 14035 . . . . . . . 8 ((๐ดโ†‘3) โˆˆ โ„‚ โ†’ (((๐ดโ†‘3)โ†‘2) โ‰  0 โ†” (๐ดโ†‘3) โ‰  0))
9867, 97syl 17 . . . . . . 7 (๐œ‘ โ†’ (((๐ดโ†‘3)โ†‘2) โ‰  0 โ†” (๐ดโ†‘3) โ‰  0))
9972, 98mpbird 257 . . . . . 6 (๐œ‘ โ†’ ((๐ดโ†‘3)โ†‘2) โ‰  0)
10082, 95, 96, 99divsubdird 11977 . . . . 5 (๐œ‘ โ†’ (((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))) / ((๐ดโ†‘3)โ†‘2)) = (((๐‘โ†‘2) / ((๐ดโ†‘3)โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / ((๐ดโ†‘3)โ†‘2))))
10162, 67, 72sqdivd 14071 . . . . . 6 (๐œ‘ โ†’ ((๐‘ / (๐ดโ†‘3))โ†‘2) = ((๐‘โ†‘2) / ((๐ดโ†‘3)โ†‘2)))
102 2z 12542 . . . . . . . . . . . 12 2 โˆˆ โ„ค
103102a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
1041, 16, 103expne0d 14064 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ดโ†‘2) โ‰  0)
10591, 57, 104, 37expdivd 14072 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€ / (๐ดโ†‘2))โ†‘3) = ((๐‘€โ†‘3) / ((๐ดโ†‘2)โ†‘3)))
10642, 86mulcomi 11170 . . . . . . . . . . . 12 (2 ยท 3) = (3 ยท 2)
107106oveq2i 7373 . . . . . . . . . . 11 (๐ดโ†‘(2 ยท 3)) = (๐ดโ†‘(3 ยท 2))
10853a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆˆ โ„•0)
1091, 37, 108expmuld 14061 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ดโ†‘(2 ยท 3)) = ((๐ดโ†‘2)โ†‘3))
1101, 108, 37expmuld 14061 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ดโ†‘(3 ยท 2)) = ((๐ดโ†‘3)โ†‘2))
111107, 109, 1103eqtr3a 2801 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ดโ†‘2)โ†‘3) = ((๐ดโ†‘3)โ†‘2))
112111oveq2d 7378 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€โ†‘3) / ((๐ดโ†‘2)โ†‘3)) = ((๐‘€โ†‘3) / ((๐ดโ†‘3)โ†‘2)))
113105, 112eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘€ / (๐ดโ†‘2))โ†‘3) = ((๐‘€โ†‘3) / ((๐ดโ†‘3)โ†‘2)))
114113oveq2d 7378 . . . . . . 7 (๐œ‘ โ†’ (4 ยท ((๐‘€ / (๐ดโ†‘2))โ†‘3)) = (4 ยท ((๐‘€โ†‘3) / ((๐ดโ†‘3)โ†‘2))))
11583a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 4 โˆˆ โ„‚)
116115, 93, 96, 99divassd 11973 . . . . . . 7 (๐œ‘ โ†’ ((4 ยท (๐‘€โ†‘3)) / ((๐ดโ†‘3)โ†‘2)) = (4 ยท ((๐‘€โ†‘3) / ((๐ดโ†‘3)โ†‘2))))
117114, 116eqtr4d 2780 . . . . . 6 (๐œ‘ โ†’ (4 ยท ((๐‘€ / (๐ดโ†‘2))โ†‘3)) = ((4 ยท (๐‘€โ†‘3)) / ((๐ดโ†‘3)โ†‘2)))
118101, 117oveq12d 7380 . . . . 5 (๐œ‘ โ†’ (((๐‘ / (๐ดโ†‘3))โ†‘2) โˆ’ (4 ยท ((๐‘€ / (๐ดโ†‘2))โ†‘3))) = (((๐‘โ†‘2) / ((๐ดโ†‘3)โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / ((๐ดโ†‘3)โ†‘2))))
119100, 118eqtr4d 2780 . . . 4 (๐œ‘ โ†’ (((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))) / ((๐ดโ†‘3)โ†‘2)) = (((๐‘ / (๐ดโ†‘3))โ†‘2) โˆ’ (4 ยท ((๐‘€ / (๐ดโ†‘2))โ†‘3))))
12079, 81, 1193eqtrd 2781 . . 3 (๐œ‘ โ†’ ((๐บ / (๐ดโ†‘3))โ†‘2) = (((๐‘ / (๐ดโ†‘3))โ†‘2) โˆ’ (4 ยท ((๐‘€ / (๐ดโ†‘2))โ†‘3))))
12185, 89, 57, 104divsubdird 11977 . . . 4 (๐œ‘ โ†’ (((๐ตโ†‘2) โˆ’ (3 ยท (๐ด ยท ๐ถ))) / (๐ดโ†‘2)) = (((๐ตโ†‘2) / (๐ดโ†‘2)) โˆ’ ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ†‘2))))
12284oveq1d 7377 . . . 4 (๐œ‘ โ†’ (๐‘€ / (๐ดโ†‘2)) = (((๐ตโ†‘2) โˆ’ (3 ยท (๐ด ยท ๐ถ))) / (๐ดโ†‘2)))
1237, 1, 16sqdivd 14071 . . . . 5 (๐œ‘ โ†’ ((๐ต / ๐ด)โ†‘2) = ((๐ตโ†‘2) / (๐ดโ†‘2)))
1241sqvald 14055 . . . . . . . . 9 (๐œ‘ โ†’ (๐ดโ†‘2) = (๐ด ยท ๐ด))
125124oveq2d 7378 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด ยท ๐ถ) / (๐ดโ†‘2)) = ((๐ด ยท ๐ถ) / (๐ด ยท ๐ด)))
12611, 1, 1, 16, 16divcan5d 11964 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด ยท ๐ถ) / (๐ด ยท ๐ด)) = (๐ถ / ๐ด))
127125, 126eqtr2d 2778 . . . . . . 7 (๐œ‘ โ†’ (๐ถ / ๐ด) = ((๐ด ยท ๐ถ) / (๐ดโ†‘2)))
128127oveq2d 7378 . . . . . 6 (๐œ‘ โ†’ (3 ยท (๐ถ / ๐ด)) = (3 ยท ((๐ด ยท ๐ถ) / (๐ดโ†‘2))))
12986a1i 11 . . . . . . 7 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
130129, 87, 57, 104divassd 11973 . . . . . 6 (๐œ‘ โ†’ ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ†‘2)) = (3 ยท ((๐ด ยท ๐ถ) / (๐ดโ†‘2))))
131128, 130eqtr4d 2780 . . . . 5 (๐œ‘ โ†’ (3 ยท (๐ถ / ๐ด)) = ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ†‘2)))
132123, 131oveq12d 7380 . . . 4 (๐œ‘ โ†’ (((๐ต / ๐ด)โ†‘2) โˆ’ (3 ยท (๐ถ / ๐ด))) = (((๐ตโ†‘2) / (๐ดโ†‘2)) โˆ’ ((3 ยท (๐ด ยท ๐ถ)) / (๐ดโ†‘2))))
133121, 122, 1323eqtr4d 2787 . . 3 (๐œ‘ โ†’ (๐‘€ / (๐ดโ†‘2)) = (((๐ต / ๐ด)โ†‘2) โˆ’ (3 ยท (๐ถ / ๐ด))))
13452, 60, 67, 72divdird 11976 . . . 4 (๐œ‘ โ†’ ((((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) + (27 ยท ((๐ดโ†‘2) ยท ๐ท))) / (๐ดโ†‘3)) = ((((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ†‘3)) + ((27 ยท ((๐ดโ†‘2) ยท ๐ท)) / (๐ดโ†‘3))))
13541oveq1d 7377 . . . 4 (๐œ‘ โ†’ (๐‘ / (๐ดโ†‘3)) = ((((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) + (27 ยท ((๐ดโ†‘2) ยท ๐ท))) / (๐ดโ†‘3)))
1367, 1, 16, 37expdivd 14072 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ต / ๐ด)โ†‘3) = ((๐ตโ†‘3) / (๐ดโ†‘3)))
137136oveq2d 7378 . . . . . . . 8 (๐œ‘ โ†’ (2 ยท ((๐ต / ๐ด)โ†‘3)) = (2 ยท ((๐ตโ†‘3) / (๐ดโ†‘3))))
13865, 44, 67, 72divassd 11973 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท (๐ตโ†‘3)) / (๐ดโ†‘3)) = (2 ยท ((๐ตโ†‘3) / (๐ดโ†‘3))))
139137, 138eqtr4d 2780 . . . . . . 7 (๐œ‘ โ†’ (2 ยท ((๐ต / ๐ด)โ†‘3)) = ((2 ยท (๐ตโ†‘3)) / (๐ดโ†‘3)))
14047a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ 9 โˆˆ โ„‚)
1411, 50mulcld 11182 . . . . . . . . 9 (๐œ‘ โ†’ (๐ด ยท (๐ต ยท ๐ถ)) โˆˆ โ„‚)
142140, 141, 67, 72divassd 11973 . . . . . . . 8 (๐œ‘ โ†’ ((9 ยท (๐ด ยท (๐ต ยท ๐ถ))) / (๐ดโ†‘3)) = (9 ยท ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3))))
143140, 1, 50mulassd 11185 . . . . . . . . 9 (๐œ‘ โ†’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) = (9 ยท (๐ด ยท (๐ต ยท ๐ถ))))
144143oveq1d 7377 . . . . . . . 8 (๐œ‘ โ†’ (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3)) = ((9 ยท (๐ด ยท (๐ต ยท ๐ถ))) / (๐ดโ†‘3)))
14550, 57, 1, 104, 16divcan5d 11964 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ด ยท (๐ดโ†‘2))) = ((๐ต ยท ๐ถ) / (๐ดโ†‘2)))
146 df-3 12224 . . . . . . . . . . . . . 14 3 = (2 + 1)
147146oveq2i 7373 . . . . . . . . . . . . 13 (๐ดโ†‘3) = (๐ดโ†‘(2 + 1))
148 expp1 13981 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (๐ดโ†‘(2 + 1)) = ((๐ดโ†‘2) ยท ๐ด))
1491, 53, 148sylancl 587 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ดโ†‘(2 + 1)) = ((๐ดโ†‘2) ยท ๐ด))
150147, 149eqtrid 2789 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ดโ†‘3) = ((๐ดโ†‘2) ยท ๐ด))
15157, 1mulcomd 11183 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ดโ†‘2) ยท ๐ด) = (๐ด ยท (๐ดโ†‘2)))
152150, 151eqtrd 2777 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ดโ†‘3) = (๐ด ยท (๐ดโ†‘2)))
153152oveq2d 7378 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3)) = ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ด ยท (๐ดโ†‘2))))
1547, 1, 11, 1, 16, 16divmuldivd 11979 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ต / ๐ด) ยท (๐ถ / ๐ด)) = ((๐ต ยท ๐ถ) / (๐ด ยท ๐ด)))
155124oveq2d 7378 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ต ยท ๐ถ) / (๐ดโ†‘2)) = ((๐ต ยท ๐ถ) / (๐ด ยท ๐ด)))
156154, 155eqtr4d 2780 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต / ๐ด) ยท (๐ถ / ๐ด)) = ((๐ต ยท ๐ถ) / (๐ดโ†‘2)))
157145, 153, 1563eqtr4rd 2788 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ต / ๐ด) ยท (๐ถ / ๐ด)) = ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3)))
158157oveq2d 7378 . . . . . . . 8 (๐œ‘ โ†’ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด))) = (9 ยท ((๐ด ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3))))
159142, 144, 1583eqtr4rd 2788 . . . . . . 7 (๐œ‘ โ†’ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด))) = (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3)))
160139, 159oveq12d 7380 . . . . . 6 (๐œ‘ โ†’ ((2 ยท ((๐ต / ๐ด)โ†‘3)) โˆ’ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) = (((2 ยท (๐ตโ†‘3)) / (๐ดโ†‘3)) โˆ’ (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3))))
16146, 51, 67, 72divsubdird 11977 . . . . . 6 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ†‘3)) = (((2 ยท (๐ตโ†‘3)) / (๐ดโ†‘3)) โˆ’ (((9 ยท ๐ด) ยท (๐ต ยท ๐ถ)) / (๐ดโ†‘3))))
162160, 161eqtr4d 2780 . . . . 5 (๐œ‘ โ†’ ((2 ยท ((๐ต / ๐ด)โ†‘3)) โˆ’ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) = (((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ†‘3)))
163150oveq2d 7378 . . . . . . . 8 (๐œ‘ โ†’ (((๐ดโ†‘2) ยท ๐ท) / (๐ดโ†‘3)) = (((๐ดโ†‘2) ยท ๐ท) / ((๐ดโ†‘2) ยท ๐ด)))
16413, 1, 57, 16, 104divcan5d 11964 . . . . . . . 8 (๐œ‘ โ†’ (((๐ดโ†‘2) ยท ๐ท) / ((๐ดโ†‘2) ยท ๐ด)) = (๐ท / ๐ด))
165163, 164eqtr2d 2778 . . . . . . 7 (๐œ‘ โ†’ (๐ท / ๐ด) = (((๐ดโ†‘2) ยท ๐ท) / (๐ดโ†‘3)))
166165oveq2d 7378 . . . . . 6 (๐œ‘ โ†’ (27 ยท (๐ท / ๐ด)) = (27 ยท (((๐ดโ†‘2) ยท ๐ท) / (๐ดโ†‘3))))
16756a1i 11 . . . . . . 7 (๐œ‘ โ†’ 27 โˆˆ โ„‚)
168167, 58, 67, 72divassd 11973 . . . . . 6 (๐œ‘ โ†’ ((27 ยท ((๐ดโ†‘2) ยท ๐ท)) / (๐ดโ†‘3)) = (27 ยท (((๐ดโ†‘2) ยท ๐ท) / (๐ดโ†‘3))))
169166, 168eqtr4d 2780 . . . . 5 (๐œ‘ โ†’ (27 ยท (๐ท / ๐ด)) = ((27 ยท ((๐ดโ†‘2) ยท ๐ท)) / (๐ดโ†‘3)))
170162, 169oveq12d 7380 . . . 4 (๐œ‘ โ†’ (((2 ยท ((๐ต / ๐ด)โ†‘3)) โˆ’ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) + (27 ยท (๐ท / ๐ด))) = ((((2 ยท (๐ตโ†‘3)) โˆ’ ((9 ยท ๐ด) ยท (๐ต ยท ๐ถ))) / (๐ดโ†‘3)) + ((27 ยท ((๐ดโ†‘2) ยท ๐ท)) / (๐ดโ†‘3))))
171134, 135, 1703eqtr4d 2787 . . 3 (๐œ‘ โ†’ (๐‘ / (๐ดโ†‘3)) = (((2 ยท ((๐ต / ๐ด)โ†‘3)) โˆ’ (9 ยท ((๐ต / ๐ด) ยท (๐ถ / ๐ด)))) + (27 ยท (๐ท / ๐ด))))
172 cubic2.0 . . . 4 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
17335, 1, 172, 16divne0d 11954 . . 3 (๐œ‘ โ†’ (๐‘‡ / ๐ด) โ‰  0)
17432, 33, 34, 2, 36, 77, 78, 120, 133, 171, 173mcubic 26213 . 2 (๐œ‘ โ†’ ((((๐‘‹โ†‘3) + ((๐ต / ๐ด) ยท (๐‘‹โ†‘2))) + (((๐ถ / ๐ด) ยท ๐‘‹) + (๐ท / ๐ด))) = 0 โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3))))
175 oveq1 7369 . . . . . . . 8 (๐‘Ÿ = 0 โ†’ (๐‘Ÿโ†‘3) = (0โ†‘3))
176 3nn 12239 . . . . . . . . 9 3 โˆˆ โ„•
177 0exp 14010 . . . . . . . . 9 (3 โˆˆ โ„• โ†’ (0โ†‘3) = 0)
178176, 177ax-mp 5 . . . . . . . 8 (0โ†‘3) = 0
179175, 178eqtrdi 2793 . . . . . . 7 (๐‘Ÿ = 0 โ†’ (๐‘Ÿโ†‘3) = 0)
180 0ne1 12231 . . . . . . . 8 0 โ‰  1
181180a1i 11 . . . . . . 7 (๐‘Ÿ = 0 โ†’ 0 โ‰  1)
182179, 181eqnetrd 3012 . . . . . 6 (๐‘Ÿ = 0 โ†’ (๐‘Ÿโ†‘3) โ‰  1)
183182necon2i 2979 . . . . 5 ((๐‘Ÿโ†‘3) = 1 โ†’ ๐‘Ÿ โ‰  0)
184 simprl 770 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘Ÿ โˆˆ โ„‚)
18535adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘‡ โˆˆ โ„‚)
1861adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐ด โˆˆ โ„‚)
18716adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐ด โ‰  0)
188184, 185, 186, 187divassd 11973 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘Ÿ ยท ๐‘‡) / ๐ด) = (๐‘Ÿ ยท (๐‘‡ / ๐ด)))
189188eqcomd 2743 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘Ÿ ยท (๐‘‡ / ๐ด)) = ((๐‘Ÿ ยท ๐‘‡) / ๐ด))
190189oveq2d 7378 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) = ((๐ต / ๐ด) + ((๐‘Ÿ ยท ๐‘‡) / ๐ด)))
1917adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐ต โˆˆ โ„‚)
192184, 185mulcld 11182 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘Ÿ ยท ๐‘‡) โˆˆ โ„‚)
193191, 192, 186, 187divdird 11976 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต + (๐‘Ÿ ยท ๐‘‡)) / ๐ด) = ((๐ต / ๐ด) + ((๐‘Ÿ ยท ๐‘‡) / ๐ด)))
194190, 193eqtr4d 2780 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) = ((๐ต + (๐‘Ÿ ยท ๐‘‡)) / ๐ด))
19591adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘€ โˆˆ โ„‚)
196195, 186, 187divcld 11938 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘€ / ๐ด) โˆˆ โ„‚)
197 simprr 772 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘Ÿ โ‰  0)
198172adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘‡ โ‰  0)
199184, 185, 197, 198mulne0d 11814 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘Ÿ ยท ๐‘‡) โ‰  0)
200196, 192, 186, 199, 187divcan7d 11966 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐‘€ / ๐ด) / ๐ด) / ((๐‘Ÿ ยท ๐‘‡) / ๐ด)) = ((๐‘€ / ๐ด) / (๐‘Ÿ ยท ๐‘‡)))
201195, 186, 186, 187, 187divdiv1d 11969 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / ๐ด) / ๐ด) = (๐‘€ / (๐ด ยท ๐ด)))
202186sqvald 14055 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐ดโ†‘2) = (๐ด ยท ๐ด))
203202oveq2d 7378 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘€ / (๐ดโ†‘2)) = (๐‘€ / (๐ด ยท ๐ด)))
204201, 203eqtr4d 2780 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / ๐ด) / ๐ด) = (๐‘€ / (๐ดโ†‘2)))
205204, 188oveq12d 7380 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐‘€ / ๐ด) / ๐ด) / ((๐‘Ÿ ยท ๐‘‡) / ๐ด)) = ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด))))
206195, 186, 192, 187, 199divdiv32d 11963 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / ๐ด) / (๐‘Ÿ ยท ๐‘‡)) = ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / ๐ด))
207200, 205, 2063eqtr3d 2785 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด))) = ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / ๐ด))
208194, 207oveq12d 7380 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) = (((๐ต + (๐‘Ÿ ยท ๐‘‡)) / ๐ด) + ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / ๐ด)))
209191, 192addcld 11181 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐ต + (๐‘Ÿ ยท ๐‘‡)) โˆˆ โ„‚)
210195, 192, 199divcld 11938 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘€ / (๐‘Ÿ ยท ๐‘‡)) โˆˆ โ„‚)
211209, 210, 186, 187divdird 11976 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / ๐ด) = (((๐ต + (๐‘Ÿ ยท ๐‘‡)) / ๐ด) + ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / ๐ด)))
212208, 211eqtr4d 2780 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) = (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / ๐ด))
213212oveq1d 7377 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3) = ((((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / ๐ด) / 3))
214209, 210addcld 11181 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) โˆˆ โ„‚)
21586a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ 3 โˆˆ โ„‚)
216 3ne0 12266 . . . . . . . . . . 11 3 โ‰  0
217216a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ 3 โ‰  0)
218214, 186, 215, 187, 217divdiv1d 11969 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / ๐ด) / 3) = (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (๐ด ยท 3)))
219 mulcom 11144 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚) โ†’ (๐ด ยท 3) = (3 ยท ๐ด))
220186, 86, 219sylancl 587 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐ด ยท 3) = (3 ยท ๐ด))
221220oveq2d 7378 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (๐ด ยท 3)) = (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))
222213, 218, 2213eqtrd 2781 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3) = (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))
223222negeqd 11402 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3) = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))
224223eqeq2d 2748 . . . . . 6 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘‹ = -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3) โ†” ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด))))
225224anassrs 469 . . . . 5 (((๐œ‘ โˆง ๐‘Ÿ โˆˆ โ„‚) โˆง ๐‘Ÿ โ‰  0) โ†’ (๐‘‹ = -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3) โ†” ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด))))
226183, 225sylan2 594 . . . 4 (((๐œ‘ โˆง ๐‘Ÿ โˆˆ โ„‚) โˆง (๐‘Ÿโ†‘3) = 1) โ†’ (๐‘‹ = -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3) โ†” ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด))))
227226pm5.32da 580 . . 3 ((๐œ‘ โˆง ๐‘Ÿ โˆˆ โ„‚) โ†’ (((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3)) โ†” ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))))
228227rexbidva 3174 . 2 (๐œ‘ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -((((๐ต / ๐ด) + (๐‘Ÿ ยท (๐‘‡ / ๐ด))) + ((๐‘€ / (๐ดโ†‘2)) / (๐‘Ÿ ยท (๐‘‡ / ๐ด)))) / 3)) โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))))
22931, 174, 2283bitrd 305 1 (๐œ‘ โ†’ ((((๐ด ยท (๐‘‹โ†‘3)) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / (3 ยท ๐ด)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074  (class class class)co 7362  โ„‚cc 11056  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   โˆ’ cmin 11392  -cneg 11393   / cdiv 11819  โ„•cn 12160  2c2 12215  3c3 12216  4c4 12217  7c7 12220  9c9 12222  โ„•0cn0 12420  โ„คcz 12506  cdc 12625  โ†‘cexp 13974
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 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
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 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-sup 9385  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-rp 12923  df-seq 13914  df-exp 13975  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-dvds 16144
This theorem is referenced by:  cubic  26215
  Copyright terms: Public domain W3C validator