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

Theorem dquart 26798
Description: Solve a depressed quartic equation. To eliminate ๐‘†, which is the square root of a solution ๐‘€ to the resolvent cubic equation, apply cubic 26794 or one of its variants. (Contributed by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
dquart.b (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
dquart.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
dquart.x (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
dquart.s (๐œ‘ โ†’ ๐‘† โˆˆ โ„‚)
dquart.m (๐œ‘ โ†’ ๐‘€ = ((2 ยท ๐‘†)โ†‘2))
dquart.m0 (๐œ‘ โ†’ ๐‘€ โ‰  0)
dquart.i (๐œ‘ โ†’ ๐ผ โˆˆ โ„‚)
dquart.i2 (๐œ‘ โ†’ (๐ผโ†‘2) = ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) + ((๐ถ / 4) / ๐‘†)))
dquart.d (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
dquart.3 (๐œ‘ โ†’ (((๐‘€โ†‘3) + ((2 ยท ๐ต) ยท (๐‘€โ†‘2))) + ((((๐ตโ†‘2) โˆ’ (4 ยท ๐ท)) ยท ๐‘€) + -(๐ถโ†‘2))) = 0)
dquart.j (๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚)
dquart.j2 (๐œ‘ โ†’ (๐ฝโ†‘2) = ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) โˆ’ ((๐ถ / 4) / ๐‘†)))
Assertion
Ref Expression
dquart (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” ((๐‘‹ = (-๐‘† + ๐ผ) โˆจ ๐‘‹ = (-๐‘† โˆ’ ๐ผ)) โˆจ (๐‘‹ = (๐‘† + ๐ฝ) โˆจ ๐‘‹ = (๐‘† โˆ’ ๐ฝ)))))

Proof of Theorem dquart
StepHypRef Expression
1 dquart.x . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
21sqcld 14141 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‹โ†‘2) โˆˆ โ„‚)
3 dquart.m . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ = ((2 ยท ๐‘†)โ†‘2))
4 2cn 12318 . . . . . . . . . . . . 13 2 โˆˆ โ„‚
5 dquart.s . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘† โˆˆ โ„‚)
6 mulcl 11223 . . . . . . . . . . . . 13 ((2 โˆˆ โ„‚ โˆง ๐‘† โˆˆ โ„‚) โ†’ (2 ยท ๐‘†) โˆˆ โ„‚)
74, 5, 6sylancr 586 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘†) โˆˆ โ„‚)
87sqcld 14141 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘†)โ†‘2) โˆˆ โ„‚)
93, 8eqeltrd 2829 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
10 dquart.b . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
119, 10addcld 11264 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€ + ๐ต) โˆˆ โ„‚)
1211halfcld 12488 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘€ + ๐ต) / 2) โˆˆ โ„‚)
13 binom2 14213 . . . . . . . 8 (((๐‘‹โ†‘2) โˆˆ โ„‚ โˆง ((๐‘€ + ๐ต) / 2) โˆˆ โ„‚) โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) = ((((๐‘‹โ†‘2)โ†‘2) + (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2)))) + (((๐‘€ + ๐ต) / 2)โ†‘2)))
142, 12, 13syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) = ((((๐‘‹โ†‘2)โ†‘2) + (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2)))) + (((๐‘€ + ๐ต) / 2)โ†‘2)))
15 2nn0 12520 . . . . . . . . . . . . 13 2 โˆˆ โ„•0
1615a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆˆ โ„•0)
171, 16, 16expmuld 14146 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹โ†‘(2 ยท 2)) = ((๐‘‹โ†‘2)โ†‘2))
18 2t2e4 12407 . . . . . . . . . . . 12 (2 ยท 2) = 4
1918oveq2i 7431 . . . . . . . . . . 11 (๐‘‹โ†‘(2 ยท 2)) = (๐‘‹โ†‘4)
2017, 19eqtr3di 2783 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‹โ†‘2)โ†‘2) = (๐‘‹โ†‘4))
214a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
2221, 2, 12mul12d 11454 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2))) = ((๐‘‹โ†‘2) ยท (2 ยท ((๐‘€ + ๐ต) / 2))))
23 2ne0 12347 . . . . . . . . . . . . . . 15 2 โ‰  0
2423a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰  0)
2511, 21, 24divcan2d 12023 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท ((๐‘€ + ๐ต) / 2)) = (๐‘€ + ๐ต))
2625oveq2d 7436 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹โ†‘2) ยท (2 ยท ((๐‘€ + ๐ต) / 2))) = ((๐‘‹โ†‘2) ยท (๐‘€ + ๐ต)))
272, 11mulcomd 11266 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹โ†‘2) ยท (๐‘€ + ๐ต)) = ((๐‘€ + ๐ต) ยท (๐‘‹โ†‘2)))
2826, 27eqtrd 2768 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘‹โ†‘2) ยท (2 ยท ((๐‘€ + ๐ต) / 2))) = ((๐‘€ + ๐ต) ยท (๐‘‹โ†‘2)))
299, 10, 2adddird 11270 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘€ + ๐ต) ยท (๐‘‹โ†‘2)) = ((๐‘€ ยท (๐‘‹โ†‘2)) + (๐ต ยท (๐‘‹โ†‘2))))
3022, 28, 293eqtrd 2772 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2))) = ((๐‘€ ยท (๐‘‹โ†‘2)) + (๐ต ยท (๐‘‹โ†‘2))))
3120, 30oveq12d 7438 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘‹โ†‘2)โ†‘2) + (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2)))) = ((๐‘‹โ†‘4) + ((๐‘€ ยท (๐‘‹โ†‘2)) + (๐ต ยท (๐‘‹โ†‘2)))))
32 4nn0 12522 . . . . . . . . . . 11 4 โˆˆ โ„•0
33 expcl 14077 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„‚ โˆง 4 โˆˆ โ„•0) โ†’ (๐‘‹โ†‘4) โˆˆ โ„‚)
341, 32, 33sylancl 585 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‹โ†‘4) โˆˆ โ„‚)
359, 2mulcld 11265 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘€ ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
3610, 2mulcld 11265 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ต ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
3734, 35, 36add12d 11471 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‹โ†‘4) + ((๐‘€ ยท (๐‘‹โ†‘2)) + (๐ต ยท (๐‘‹โ†‘2)))) = ((๐‘€ ยท (๐‘‹โ†‘2)) + ((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2)))))
3831, 37eqtrd 2768 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘‹โ†‘2)โ†‘2) + (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2)))) = ((๐‘€ ยท (๐‘‹โ†‘2)) + ((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2)))))
3938oveq1d 7435 . . . . . . 7 (๐œ‘ โ†’ ((((๐‘‹โ†‘2)โ†‘2) + (2 ยท ((๐‘‹โ†‘2) ยท ((๐‘€ + ๐ต) / 2)))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) = (((๐‘€ ยท (๐‘‹โ†‘2)) + ((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2)))) + (((๐‘€ + ๐ต) / 2)โ†‘2)))
4034, 36addcld 11264 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) โˆˆ โ„‚)
4112sqcld 14141 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘€ + ๐ต) / 2)โ†‘2) โˆˆ โ„‚)
4235, 40, 41addassd 11267 . . . . . . 7 (๐œ‘ โ†’ (((๐‘€ ยท (๐‘‹โ†‘2)) + ((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2)))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) = ((๐‘€ ยท (๐‘‹โ†‘2)) + (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2))))
4314, 39, 423eqtrd 2772 . . . . . 6 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) = ((๐‘€ ยท (๐‘‹โ†‘2)) + (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2))))
449halfcld 12488 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘€ / 2) โˆˆ โ„‚)
4544, 1mulcld 11265 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘€ / 2) ยท ๐‘‹) โˆˆ โ„‚)
46 dquart.c . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
47 4cn 12328 . . . . . . . . . . . . 13 4 โˆˆ โ„‚
4847a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 4 โˆˆ โ„‚)
49 4ne0 12351 . . . . . . . . . . . . 13 4 โ‰  0
5049a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ 4 โ‰  0)
5146, 48, 50divcld 12021 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ถ / 4) โˆˆ โ„‚)
5245, 51subcld 11602 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) โˆˆ โ„‚)
53 dquart.m0 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘€ โ‰  0)
543, 53eqnetrrd 3006 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2 ยท ๐‘†)โ†‘2) โ‰  0)
55 sqne0 14120 . . . . . . . . . . . . . 14 ((2 ยท ๐‘†) โˆˆ โ„‚ โ†’ (((2 ยท ๐‘†)โ†‘2) โ‰  0 โ†” (2 ยท ๐‘†) โ‰  0))
567, 55syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((2 ยท ๐‘†)โ†‘2) โ‰  0 โ†” (2 ยท ๐‘†) โ‰  0))
5754, 56mpbid 231 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘†) โ‰  0)
58 mulne0b 11886 . . . . . . . . . . . . 13 ((2 โˆˆ โ„‚ โˆง ๐‘† โˆˆ โ„‚) โ†’ ((2 โ‰  0 โˆง ๐‘† โ‰  0) โ†” (2 ยท ๐‘†) โ‰  0))
594, 5, 58sylancr 586 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((2 โ‰  0 โˆง ๐‘† โ‰  0) โ†” (2 ยท ๐‘†) โ‰  0))
6057, 59mpbird 257 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 โ‰  0 โˆง ๐‘† โ‰  0))
6160simprd 495 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘† โ‰  0)
6252, 5, 21, 61, 24divcan5d 12047 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท (((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4))) / (2 ยท ๐‘†)) = ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†))
6321, 45, 51subdid 11701 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4))) = ((2 ยท ((๐‘€ / 2) ยท ๐‘‹)) โˆ’ (2 ยท (๐ถ / 4))))
6421, 44, 1mulassd 11268 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2 ยท (๐‘€ / 2)) ยท ๐‘‹) = (2 ยท ((๐‘€ / 2) ยท ๐‘‹)))
659, 21, 24divcan2d 12023 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 ยท (๐‘€ / 2)) = ๐‘€)
6665oveq1d 7435 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2 ยท (๐‘€ / 2)) ยท ๐‘‹) = (๐‘€ ยท ๐‘‹))
6764, 66eqtr3d 2770 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ((๐‘€ / 2) ยท ๐‘‹)) = (๐‘€ ยท ๐‘‹))
6821, 46, 48, 50divassd 12056 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2 ยท ๐ถ) / 4) = (2 ยท (๐ถ / 4)))
6918oveq2i 7431 . . . . . . . . . . . . . 14 ((2 ยท ๐ถ) / (2 ยท 2)) = ((2 ยท ๐ถ) / 4)
7046, 21, 21, 24, 24divcan5d 12047 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 ยท ๐ถ) / (2 ยท 2)) = (๐ถ / 2))
7169, 70eqtr3id 2782 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2 ยท ๐ถ) / 4) = (๐ถ / 2))
7268, 71eqtr3d 2770 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท (๐ถ / 4)) = (๐ถ / 2))
7367, 72oveq12d 7438 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ((๐‘€ / 2) ยท ๐‘‹)) โˆ’ (2 ยท (๐ถ / 4))) = ((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)))
7463, 73eqtrd 2768 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท (((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4))) = ((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)))
7574oveq1d 7435 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท (((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4))) / (2 ยท ๐‘†)) = (((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)) / (2 ยท ๐‘†)))
7662, 75eqtr3d 2770 . . . . . . . 8 (๐œ‘ โ†’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†) = (((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)) / (2 ยท ๐‘†)))
7776oveq1d 7435 . . . . . . 7 (๐œ‘ โ†’ (((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)โ†‘2) = ((((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)) / (2 ยท ๐‘†))โ†‘2))
789, 1mulcld 11265 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€ ยท ๐‘‹) โˆˆ โ„‚)
7946halfcld 12488 . . . . . . . . 9 (๐œ‘ โ†’ (๐ถ / 2) โˆˆ โ„‚)
8078, 79subcld 11602 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)) โˆˆ โ„‚)
8180, 7, 57sqdivd 14156 . . . . . . 7 (๐œ‘ โ†’ ((((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2)) / (2 ยท ๐‘†))โ†‘2) = ((((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2))โ†‘2) / ((2 ยท ๐‘†)โ†‘2)))
829sqcld 14141 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘€โ†‘2) โˆˆ โ„‚)
8382, 2mulcld 11265 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
8478, 46mulcld 11265 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ) โˆˆ โ„‚)
8583, 84subcld 11602 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) โˆˆ โ„‚)
8646sqcld 14141 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ถโ†‘2) โˆˆ โ„‚)
8786, 48, 50divcld 12021 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ถโ†‘2) / 4) โˆˆ โ„‚)
8885, 87, 9, 53divdird 12059 . . . . . . . 8 (๐œ‘ โ†’ (((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) + ((๐ถโ†‘2) / 4)) / ๐‘€) = (((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) / ๐‘€) + (((๐ถโ†‘2) / 4) / ๐‘€)))
89 binom2sub 14215 . . . . . . . . . . 11 (((๐‘€ ยท ๐‘‹) โˆˆ โ„‚ โˆง (๐ถ / 2) โˆˆ โ„‚) โ†’ (((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2))โ†‘2) = ((((๐‘€ ยท ๐‘‹)โ†‘2) โˆ’ (2 ยท ((๐‘€ ยท ๐‘‹) ยท (๐ถ / 2)))) + ((๐ถ / 2)โ†‘2)))
9078, 79, 89syl2anc 583 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2))โ†‘2) = ((((๐‘€ ยท ๐‘‹)โ†‘2) โˆ’ (2 ยท ((๐‘€ ยท ๐‘‹) ยท (๐ถ / 2)))) + ((๐ถ / 2)โ†‘2)))
919, 1sqmuld 14155 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘‹)โ†‘2) = ((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)))
9221, 78, 79mul12d 11454 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท ((๐‘€ ยท ๐‘‹) ยท (๐ถ / 2))) = ((๐‘€ ยท ๐‘‹) ยท (2 ยท (๐ถ / 2))))
9346, 21, 24divcan2d 12023 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 ยท (๐ถ / 2)) = ๐ถ)
9493oveq2d 7436 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘‹) ยท (2 ยท (๐ถ / 2))) = ((๐‘€ ยท ๐‘‹) ยท ๐ถ))
9592, 94eqtrd 2768 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ((๐‘€ ยท ๐‘‹) ยท (๐ถ / 2))) = ((๐‘€ ยท ๐‘‹) ยท ๐ถ))
9691, 95oveq12d 7438 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐‘€ ยท ๐‘‹)โ†‘2) โˆ’ (2 ยท ((๐‘€ ยท ๐‘‹) ยท (๐ถ / 2)))) = (((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)))
9746, 21, 24sqdivd 14156 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ถ / 2)โ†‘2) = ((๐ถโ†‘2) / (2โ†‘2)))
98 sq2 14193 . . . . . . . . . . . . 13 (2โ†‘2) = 4
9998oveq2i 7431 . . . . . . . . . . . 12 ((๐ถโ†‘2) / (2โ†‘2)) = ((๐ถโ†‘2) / 4)
10097, 99eqtrdi 2784 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ถ / 2)โ†‘2) = ((๐ถโ†‘2) / 4))
10196, 100oveq12d 7438 . . . . . . . . . 10 (๐œ‘ โ†’ ((((๐‘€ ยท ๐‘‹)โ†‘2) โˆ’ (2 ยท ((๐‘€ ยท ๐‘‹) ยท (๐ถ / 2)))) + ((๐ถ / 2)โ†‘2)) = ((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) + ((๐ถโ†‘2) / 4)))
10290, 101eqtr2d 2769 . . . . . . . . 9 (๐œ‘ โ†’ ((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) + ((๐ถโ†‘2) / 4)) = (((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2))โ†‘2))
103102, 3oveq12d 7438 . . . . . . . 8 (๐œ‘ โ†’ (((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) + ((๐ถโ†‘2) / 4)) / ๐‘€) = ((((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2))โ†‘2) / ((2 ยท ๐‘†)โ†‘2)))
10483, 84, 9, 53divsubdird 12060 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) / ๐‘€) = ((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) / ๐‘€) โˆ’ (((๐‘€ ยท ๐‘‹) ยท ๐ถ) / ๐‘€)))
10582, 2, 9, 53div23d 12058 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) / ๐‘€) = (((๐‘€โ†‘2) / ๐‘€) ยท (๐‘‹โ†‘2)))
1069sqvald 14140 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘€โ†‘2) = (๐‘€ ยท ๐‘€))
107106oveq1d 7435 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘€โ†‘2) / ๐‘€) = ((๐‘€ ยท ๐‘€) / ๐‘€))
1089, 9, 53divcan3d 12026 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘€) / ๐‘€) = ๐‘€)
109107, 108eqtrd 2768 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐‘€โ†‘2) / ๐‘€) = ๐‘€)
110109oveq1d 7435 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐‘€โ†‘2) / ๐‘€) ยท (๐‘‹โ†‘2)) = (๐‘€ ยท (๐‘‹โ†‘2)))
111105, 110eqtrd 2768 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) / ๐‘€) = (๐‘€ ยท (๐‘‹โ†‘2)))
1129, 1, 46mul32d 11455 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ) = ((๐‘€ ยท ๐ถ) ยท ๐‘‹))
1139, 46, 1mulassd 11268 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘€ ยท ๐ถ) ยท ๐‘‹) = (๐‘€ ยท (๐ถ ยท ๐‘‹)))
114112, 113eqtrd 2768 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ) = (๐‘€ ยท (๐ถ ยท ๐‘‹)))
115114oveq1d 7435 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐‘€ ยท ๐‘‹) ยท ๐ถ) / ๐‘€) = ((๐‘€ ยท (๐ถ ยท ๐‘‹)) / ๐‘€))
11646, 1mulcld 11265 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ถ ยท ๐‘‹) โˆˆ โ„‚)
117116, 9, 53divcan3d 12026 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘€ ยท (๐ถ ยท ๐‘‹)) / ๐‘€) = (๐ถ ยท ๐‘‹))
118115, 117eqtrd 2768 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐‘€ ยท ๐‘‹) ยท ๐ถ) / ๐‘€) = (๐ถ ยท ๐‘‹))
119111, 118oveq12d 7438 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) / ๐‘€) โˆ’ (((๐‘€ ยท ๐‘‹) ยท ๐ถ) / ๐‘€)) = ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ (๐ถ ยท ๐‘‹)))
120104, 119eqtrd 2768 . . . . . . . . . 10 (๐œ‘ โ†’ ((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) / ๐‘€) = ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ (๐ถ ยท ๐‘‹)))
121120oveq1d 7435 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) / ๐‘€) + (((๐ถโ†‘2) / 4) / ๐‘€)) = (((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ (๐ถ ยท ๐‘‹)) + (((๐ถโ†‘2) / 4) / ๐‘€)))
12287, 9, 53divcld 12021 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ถโ†‘2) / 4) / ๐‘€) โˆˆ โ„‚)
12335, 116, 122subsubd 11630 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))) = (((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ (๐ถ ยท ๐‘‹)) + (((๐ถโ†‘2) / 4) / ๐‘€)))
124121, 123eqtr4d 2771 . . . . . . . 8 (๐œ‘ โ†’ (((((๐‘€โ†‘2) ยท (๐‘‹โ†‘2)) โˆ’ ((๐‘€ ยท ๐‘‹) ยท ๐ถ)) / ๐‘€) + (((๐ถโ†‘2) / 4) / ๐‘€)) = ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))))
12588, 103, 1243eqtr3d 2776 . . . . . . 7 (๐œ‘ โ†’ ((((๐‘€ ยท ๐‘‹) โˆ’ (๐ถ / 2))โ†‘2) / ((2 ยท ๐‘†)โ†‘2)) = ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))))
12677, 81, 1253eqtrd 2772 . . . . . 6 (๐œ‘ โ†’ (((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)โ†‘2) = ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))))
12743, 126oveq12d 7438 . . . . 5 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) โˆ’ (((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)โ†‘2)) = (((๐‘€ ยท (๐‘‹โ†‘2)) + (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2))) โˆ’ ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€)))))
12840, 41addcld 11264 . . . . . 6 (๐œ‘ โ†’ (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) โˆˆ โ„‚)
129116, 122subcld 11602 . . . . . 6 (๐œ‘ โ†’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€)) โˆˆ โ„‚)
13035, 128, 129pnncand 11641 . . . . 5 (๐œ‘ โ†’ (((๐‘€ ยท (๐‘‹โ†‘2)) + (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2))) โˆ’ ((๐‘€ ยท (๐‘‹โ†‘2)) โˆ’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€)))) = ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) + ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))))
131122negcld 11589 . . . . . . 7 (๐œ‘ โ†’ -(((๐ถโ†‘2) / 4) / ๐‘€) โˆˆ โ„‚)
13240, 41, 116, 131add4d 11473 . . . . . 6 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) + ((๐ถ ยท ๐‘‹) + -(((๐ถโ†‘2) / 4) / ๐‘€))) = ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (๐ถ ยท ๐‘‹)) + ((((๐‘€ + ๐ต) / 2)โ†‘2) + -(((๐ถโ†‘2) / 4) / ๐‘€))))
133116, 122negsubd 11608 . . . . . . 7 (๐œ‘ โ†’ ((๐ถ ยท ๐‘‹) + -(((๐ถโ†‘2) / 4) / ๐‘€)) = ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€)))
134133oveq2d 7436 . . . . . 6 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) + ((๐ถ ยท ๐‘‹) + -(((๐ถโ†‘2) / 4) / ๐‘€))) = ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) + ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))))
13541, 122negsubd 11608 . . . . . . . . 9 (๐œ‘ โ†’ ((((๐‘€ + ๐ต) / 2)โ†‘2) + -(((๐ถโ†‘2) / 4) / ๐‘€)) = ((((๐‘€ + ๐ต) / 2)โ†‘2) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€)))
136 dquart.i . . . . . . . . . 10 (๐œ‘ โ†’ ๐ผ โˆˆ โ„‚)
137 dquart.i2 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ผโ†‘2) = ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) + ((๐ถ / 4) / ๐‘†)))
138 dquart.d . . . . . . . . . 10 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
139 dquart.3 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐‘€โ†‘3) + ((2 ยท ๐ต) ยท (๐‘€โ†‘2))) + ((((๐ตโ†‘2) โˆ’ (4 ยท ๐ท)) ยท ๐‘€) + -(๐ถโ†‘2))) = 0)
14010, 46, 1, 5, 3, 53, 136, 137, 138, 139dquartlem2 26797 . . . . . . . . 9 (๐œ‘ โ†’ ((((๐‘€ + ๐ต) / 2)โ†‘2) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€)) = ๐ท)
141135, 140eqtrd 2768 . . . . . . . 8 (๐œ‘ โ†’ ((((๐‘€ + ๐ต) / 2)โ†‘2) + -(((๐ถโ†‘2) / 4) / ๐‘€)) = ๐ท)
142141oveq2d 7436 . . . . . . 7 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (๐ถ ยท ๐‘‹)) + ((((๐‘€ + ๐ต) / 2)โ†‘2) + -(((๐ถโ†‘2) / 4) / ๐‘€))) = ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (๐ถ ยท ๐‘‹)) + ๐ท))
14340, 116, 138addassd 11267 . . . . . . 7 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (๐ถ ยท ๐‘‹)) + ๐ท) = (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)))
144142, 143eqtrd 2768 . . . . . 6 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (๐ถ ยท ๐‘‹)) + ((((๐‘€ + ๐ต) / 2)โ†‘2) + -(((๐ถโ†‘2) / 4) / ๐‘€))) = (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)))
145132, 134, 1443eqtr3d 2776 . . . . 5 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + (((๐‘€ + ๐ต) / 2)โ†‘2)) + ((๐ถ ยท ๐‘‹) โˆ’ (((๐ถโ†‘2) / 4) / ๐‘€))) = (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)))
146127, 130, 1453eqtrd 2772 . . . 4 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) โˆ’ (((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)โ†‘2)) = (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)))
1472, 12addcld 11264 . . . . 5 (๐œ‘ โ†’ ((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆˆ โ„‚)
14852, 5, 61divcld 12021 . . . . 5 (๐œ‘ โ†’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†) โˆˆ โ„‚)
149 subsq 14206 . . . . 5 ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆˆ โ„‚ โˆง ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†) โˆˆ โ„‚) โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) โˆ’ (((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)โ†‘2)) = ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) ยท (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†))))
150147, 148, 149syl2anc 583 . . . 4 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2))โ†‘2) โˆ’ (((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)โ†‘2)) = ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) ยท (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†))))
151146, 150eqtr3d 2770 . . 3 (๐œ‘ โ†’ (((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) ยท (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†))))
152151eqeq1d 2730 . 2 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) ยท (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†))) = 0))
153147, 148addcld 11264 . . 3 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) โˆˆ โ„‚)
154147, 148subcld 11602 . . 3 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) โˆˆ โ„‚)
155153, 154mul0ord 11895 . 2 (๐œ‘ โ†’ (((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) ยท (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†))) = 0 โ†” ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0 โˆจ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0)))
15610, 46, 1, 5, 3, 53, 136, 137dquartlem1 26796 . . 3 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0 โ†” (๐‘‹ = (-๐‘† + ๐ผ) โˆจ ๐‘‹ = (-๐‘† โˆ’ ๐ผ))))
1575negcld 11589 . . . . 5 (๐œ‘ โ†’ -๐‘† โˆˆ โ„‚)
158 sqneg 14113 . . . . . . . 8 ((2 ยท ๐‘†) โˆˆ โ„‚ โ†’ (-(2 ยท ๐‘†)โ†‘2) = ((2 ยท ๐‘†)โ†‘2))
1597, 158syl 17 . . . . . . 7 (๐œ‘ โ†’ (-(2 ยท ๐‘†)โ†‘2) = ((2 ยท ๐‘†)โ†‘2))
1603, 159eqtr4d 2771 . . . . . 6 (๐œ‘ โ†’ ๐‘€ = (-(2 ยท ๐‘†)โ†‘2))
161 mulneg2 11682 . . . . . . . 8 ((2 โˆˆ โ„‚ โˆง ๐‘† โˆˆ โ„‚) โ†’ (2 ยท -๐‘†) = -(2 ยท ๐‘†))
1624, 5, 161sylancr 586 . . . . . . 7 (๐œ‘ โ†’ (2 ยท -๐‘†) = -(2 ยท ๐‘†))
163162oveq1d 7435 . . . . . 6 (๐œ‘ โ†’ ((2 ยท -๐‘†)โ†‘2) = (-(2 ยท ๐‘†)โ†‘2))
164160, 163eqtr4d 2771 . . . . 5 (๐œ‘ โ†’ ๐‘€ = ((2 ยท -๐‘†)โ†‘2))
165 dquart.j . . . . 5 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚)
166 dquart.j2 . . . . . 6 (๐œ‘ โ†’ (๐ฝโ†‘2) = ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) โˆ’ ((๐ถ / 4) / ๐‘†)))
1675sqcld 14141 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘†โ†‘2) โˆˆ โ„‚)
168167negcld 11589 . . . . . . . 8 (๐œ‘ โ†’ -(๐‘†โ†‘2) โˆˆ โ„‚)
16910halfcld 12488 . . . . . . . 8 (๐œ‘ โ†’ (๐ต / 2) โˆˆ โ„‚)
170168, 169subcld 11602 . . . . . . 7 (๐œ‘ โ†’ (-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) โˆˆ โ„‚)
17151, 5, 61divcld 12021 . . . . . . 7 (๐œ‘ โ†’ ((๐ถ / 4) / ๐‘†) โˆˆ โ„‚)
172170, 171negsubd 11608 . . . . . 6 (๐œ‘ โ†’ ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) + -((๐ถ / 4) / ๐‘†)) = ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) โˆ’ ((๐ถ / 4) / ๐‘†)))
173 sqneg 14113 . . . . . . . . . . 11 (๐‘† โˆˆ โ„‚ โ†’ (-๐‘†โ†‘2) = (๐‘†โ†‘2))
1745, 173syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (-๐‘†โ†‘2) = (๐‘†โ†‘2))
175174eqcomd 2734 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘†โ†‘2) = (-๐‘†โ†‘2))
176175negeqd 11485 . . . . . . . 8 (๐œ‘ โ†’ -(๐‘†โ†‘2) = -(-๐‘†โ†‘2))
177176oveq1d 7435 . . . . . . 7 (๐œ‘ โ†’ (-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) = (-(-๐‘†โ†‘2) โˆ’ (๐ต / 2)))
17851, 5, 61divneg2d 12035 . . . . . . 7 (๐œ‘ โ†’ -((๐ถ / 4) / ๐‘†) = ((๐ถ / 4) / -๐‘†))
179177, 178oveq12d 7438 . . . . . 6 (๐œ‘ โ†’ ((-(๐‘†โ†‘2) โˆ’ (๐ต / 2)) + -((๐ถ / 4) / ๐‘†)) = ((-(-๐‘†โ†‘2) โˆ’ (๐ต / 2)) + ((๐ถ / 4) / -๐‘†)))
180166, 172, 1793eqtr2d 2774 . . . . 5 (๐œ‘ โ†’ (๐ฝโ†‘2) = ((-(-๐‘†โ†‘2) โˆ’ (๐ต / 2)) + ((๐ถ / 4) / -๐‘†)))
18110, 46, 1, 157, 164, 53, 165, 180dquartlem1 26796 . . . 4 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / -๐‘†)) = 0 โ†” (๐‘‹ = (--๐‘† + ๐ฝ) โˆจ ๐‘‹ = (--๐‘† โˆ’ ๐ฝ))))
18252, 5, 61divneg2d 12035 . . . . . . 7 (๐œ‘ โ†’ -((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†) = ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / -๐‘†))
183182oveq2d 7436 . . . . . 6 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + -((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / -๐‘†)))
184147, 148negsubd 11608 . . . . . 6 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + -((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)))
185183, 184eqtr3d 2770 . . . . 5 (๐œ‘ โ†’ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / -๐‘†)) = (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)))
186185eqeq1d 2730 . . . 4 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / -๐‘†)) = 0 โ†” (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0))
1875negnegd 11593 . . . . . . 7 (๐œ‘ โ†’ --๐‘† = ๐‘†)
188187oveq1d 7435 . . . . . 6 (๐œ‘ โ†’ (--๐‘† + ๐ฝ) = (๐‘† + ๐ฝ))
189188eqeq2d 2739 . . . . 5 (๐œ‘ โ†’ (๐‘‹ = (--๐‘† + ๐ฝ) โ†” ๐‘‹ = (๐‘† + ๐ฝ)))
190187oveq1d 7435 . . . . . 6 (๐œ‘ โ†’ (--๐‘† โˆ’ ๐ฝ) = (๐‘† โˆ’ ๐ฝ))
191190eqeq2d 2739 . . . . 5 (๐œ‘ โ†’ (๐‘‹ = (--๐‘† โˆ’ ๐ฝ) โ†” ๐‘‹ = (๐‘† โˆ’ ๐ฝ)))
192189, 191orbi12d 917 . . . 4 (๐œ‘ โ†’ ((๐‘‹ = (--๐‘† + ๐ฝ) โˆจ ๐‘‹ = (--๐‘† โˆ’ ๐ฝ)) โ†” (๐‘‹ = (๐‘† + ๐ฝ) โˆจ ๐‘‹ = (๐‘† โˆ’ ๐ฝ))))
193181, 186, 1923bitr3d 309 . . 3 (๐œ‘ โ†’ ((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0 โ†” (๐‘‹ = (๐‘† + ๐ฝ) โˆจ ๐‘‹ = (๐‘† โˆ’ ๐ฝ))))
194156, 193orbi12d 917 . 2 (๐œ‘ โ†’ (((((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) + ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0 โˆจ (((๐‘‹โ†‘2) + ((๐‘€ + ๐ต) / 2)) โˆ’ ((((๐‘€ / 2) ยท ๐‘‹) โˆ’ (๐ถ / 4)) / ๐‘†)) = 0) โ†” ((๐‘‹ = (-๐‘† + ๐ผ) โˆจ ๐‘‹ = (-๐‘† โˆ’ ๐ผ)) โˆจ (๐‘‹ = (๐‘† + ๐ฝ) โˆจ ๐‘‹ = (๐‘† โˆ’ ๐ฝ)))))
195152, 155, 1943bitrd 305 1 (๐œ‘ โ†’ ((((๐‘‹โ†‘4) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” ((๐‘‹ = (-๐‘† + ๐ผ) โˆจ ๐‘‹ = (-๐‘† โˆ’ ๐ผ)) โˆจ (๐‘‹ = (๐‘† + ๐ฝ) โˆจ ๐‘‹ = (๐‘† โˆ’ ๐ฝ)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 846   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2937  (class class class)co 7420  โ„‚cc 11137  0cc0 11139   + caddc 11142   ยท cmul 11144   โˆ’ cmin 11475  -cneg 11476   / cdiv 11902  2c2 12298  3c3 12299  4c4 12300  โ„•0cn0 12503  โ†‘cexp 14059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-2nd 7994  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-div 11903  df-nn 12244  df-2 12306  df-3 12307  df-4 12308  df-n0 12504  df-z 12590  df-uz 12854  df-seq 14000  df-exp 14060
This theorem is referenced by:  quart  26806
  Copyright terms: Public domain W3C validator