Metamath Proof Explorer


Theorem quart

Description: The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull ) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quart.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
quart.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
quart.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
quart.d โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„‚ )
quart.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚ )
quart.e โŠข ( ๐œ‘ โ†’ ๐ธ = - ( ๐ด / 4 ) )
quart.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( ๐ต โˆ’ ( ( 3 / 8 ) ยท ( ๐ด โ†‘ 2 ) ) ) )
quart.q โŠข ( ๐œ‘ โ†’ ๐‘„ = ( ( ๐ถ โˆ’ ( ( ๐ด ยท ๐ต ) / 2 ) ) + ( ( ๐ด โ†‘ 3 ) / 8 ) ) )
quart.r โŠข ( ๐œ‘ โ†’ ๐‘… = ( ( ๐ท โˆ’ ( ( ๐ถ ยท ๐ด ) / 4 ) ) + ( ( ( ( ๐ด โ†‘ 2 ) ยท ๐ต ) / 1 6 ) โˆ’ ( ( 3 / 2 5 6 ) ยท ( ๐ด โ†‘ 4 ) ) ) ) )
quart.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ( ๐‘ƒ โ†‘ 2 ) + ( 1 2 ยท ๐‘… ) ) )
quart.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
quart.w โŠข ( ๐œ‘ โ†’ ๐‘Š = ( โˆš โ€˜ ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) ) )
quart.s โŠข ( ๐œ‘ โ†’ ๐‘† = ( ( โˆš โ€˜ ๐‘€ ) / 2 ) )
quart.m โŠข ( ๐œ‘ โ†’ ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ๐‘‡ ) + ( ๐‘ˆ / ๐‘‡ ) ) / 3 ) )
quart.t โŠข ( ๐œ‘ โ†’ ๐‘‡ = ( ( ( ๐‘‰ + ๐‘Š ) / 2 ) โ†‘๐‘ ( 1 / 3 ) ) )
quart.t0 โŠข ( ๐œ‘ โ†’ ๐‘‡ โ‰  0 )
quart.m0 โŠข ( ๐œ‘ โ†’ ๐‘€ โ‰  0 )
quart.i โŠข ( ๐œ‘ โ†’ ๐ผ = ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) )
quart.j โŠข ( ๐œ‘ โ†’ ๐ฝ = ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) )
Assertion quart ( ๐œ‘ โ†’ ( ( ( ( ๐‘‹ โ†‘ 4 ) + ( ๐ด ยท ( ๐‘‹ โ†‘ 3 ) ) ) + ( ( ๐ต ยท ( ๐‘‹ โ†‘ 2 ) ) + ( ( ๐ถ ยท ๐‘‹ ) + ๐ท ) ) ) = 0 โ†” ( ( ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) โˆจ ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) ) โˆจ ( ๐‘‹ = ( ( ๐ธ + ๐‘† ) + ๐ฝ ) โˆจ ๐‘‹ = ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quart.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 quart.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
3 quart.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
4 quart.d โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„‚ )
5 quart.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚ )
6 quart.e โŠข ( ๐œ‘ โ†’ ๐ธ = - ( ๐ด / 4 ) )
7 quart.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( ๐ต โˆ’ ( ( 3 / 8 ) ยท ( ๐ด โ†‘ 2 ) ) ) )
8 quart.q โŠข ( ๐œ‘ โ†’ ๐‘„ = ( ( ๐ถ โˆ’ ( ( ๐ด ยท ๐ต ) / 2 ) ) + ( ( ๐ด โ†‘ 3 ) / 8 ) ) )
9 quart.r โŠข ( ๐œ‘ โ†’ ๐‘… = ( ( ๐ท โˆ’ ( ( ๐ถ ยท ๐ด ) / 4 ) ) + ( ( ( ( ๐ด โ†‘ 2 ) ยท ๐ต ) / 1 6 ) โˆ’ ( ( 3 / 2 5 6 ) ยท ( ๐ด โ†‘ 4 ) ) ) ) )
10 quart.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ( ๐‘ƒ โ†‘ 2 ) + ( 1 2 ยท ๐‘… ) ) )
11 quart.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
12 quart.w โŠข ( ๐œ‘ โ†’ ๐‘Š = ( โˆš โ€˜ ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) ) )
13 quart.s โŠข ( ๐œ‘ โ†’ ๐‘† = ( ( โˆš โ€˜ ๐‘€ ) / 2 ) )
14 quart.m โŠข ( ๐œ‘ โ†’ ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ๐‘‡ ) + ( ๐‘ˆ / ๐‘‡ ) ) / 3 ) )
15 quart.t โŠข ( ๐œ‘ โ†’ ๐‘‡ = ( ( ( ๐‘‰ + ๐‘Š ) / 2 ) โ†‘๐‘ ( 1 / 3 ) ) )
16 quart.t0 โŠข ( ๐œ‘ โ†’ ๐‘‡ โ‰  0 )
17 quart.m0 โŠข ( ๐œ‘ โ†’ ๐‘€ โ‰  0 )
18 quart.i โŠข ( ๐œ‘ โ†’ ๐ผ = ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) )
19 quart.j โŠข ( ๐œ‘ โ†’ ๐ฝ = ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) )
20 6 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘‹ โˆ’ - ( ๐ด / 4 ) ) )
21 4cn โŠข 4 โˆˆ โ„‚
22 21 a1i โŠข ( ๐œ‘ โ†’ 4 โˆˆ โ„‚ )
23 4ne0 โŠข 4 โ‰  0
24 23 a1i โŠข ( ๐œ‘ โ†’ 4 โ‰  0 )
25 1 22 24 divcld โŠข ( ๐œ‘ โ†’ ( ๐ด / 4 ) โˆˆ โ„‚ )
26 5 25 subnegd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆ’ - ( ๐ด / 4 ) ) = ( ๐‘‹ + ( ๐ด / 4 ) ) )
27 20 26 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘‹ + ( ๐ด / 4 ) ) )
28 1 2 3 4 7 8 9 5 27 quart1 โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‹ โ†‘ 4 ) + ( ๐ด ยท ( ๐‘‹ โ†‘ 3 ) ) ) + ( ( ๐ต ยท ( ๐‘‹ โ†‘ 2 ) ) + ( ( ๐ถ ยท ๐‘‹ ) + ๐ท ) ) ) = ( ( ( ( ๐‘‹ โˆ’ ๐ธ ) โ†‘ 4 ) + ( ๐‘ƒ ยท ( ( ๐‘‹ โˆ’ ๐ธ ) โ†‘ 2 ) ) ) + ( ( ๐‘„ ยท ( ๐‘‹ โˆ’ ๐ธ ) ) + ๐‘… ) ) )
29 28 eqeq1d โŠข ( ๐œ‘ โ†’ ( ( ( ( ๐‘‹ โ†‘ 4 ) + ( ๐ด ยท ( ๐‘‹ โ†‘ 3 ) ) ) + ( ( ๐ต ยท ( ๐‘‹ โ†‘ 2 ) ) + ( ( ๐ถ ยท ๐‘‹ ) + ๐ท ) ) ) = 0 โ†” ( ( ( ( ๐‘‹ โˆ’ ๐ธ ) โ†‘ 4 ) + ( ๐‘ƒ ยท ( ( ๐‘‹ โˆ’ ๐ธ ) โ†‘ 2 ) ) ) + ( ( ๐‘„ ยท ( ๐‘‹ โˆ’ ๐ธ ) ) + ๐‘… ) ) = 0 ) )
30 1 2 3 4 7 8 9 quart1cl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆˆ โ„‚ โˆง ๐‘„ โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚ ) )
31 30 simp1d โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚ )
32 30 simp2d โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚ )
33 25 negcld โŠข ( ๐œ‘ โ†’ - ( ๐ด / 4 ) โˆˆ โ„‚ )
34 6 33 eqeltrd โŠข ( ๐œ‘ โ†’ ๐ธ โˆˆ โ„‚ )
35 5 34 subcld โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆ’ ๐ธ ) โˆˆ โ„‚ )
36 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 quartlem3 โŠข ( ๐œ‘ โ†’ ( ๐‘† โˆˆ โ„‚ โˆง ๐‘€ โˆˆ โ„‚ โˆง ๐‘‡ โˆˆ โ„‚ ) )
37 36 simp1d โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ โ„‚ )
38 13 oveq2d โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘† ) = ( 2 ยท ( ( โˆš โ€˜ ๐‘€ ) / 2 ) ) )
39 36 simp2d โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚ )
40 39 sqrtcld โŠข ( ๐œ‘ โ†’ ( โˆš โ€˜ ๐‘€ ) โˆˆ โ„‚ )
41 2cnd โŠข ( ๐œ‘ โ†’ 2 โˆˆ โ„‚ )
42 2ne0 โŠข 2 โ‰  0
43 42 a1i โŠข ( ๐œ‘ โ†’ 2 โ‰  0 )
44 40 41 43 divcan2d โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ( โˆš โ€˜ ๐‘€ ) / 2 ) ) = ( โˆš โ€˜ ๐‘€ ) )
45 38 44 eqtrd โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘† ) = ( โˆš โ€˜ ๐‘€ ) )
46 45 oveq1d โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘† ) โ†‘ 2 ) = ( ( โˆš โ€˜ ๐‘€ ) โ†‘ 2 ) )
47 39 sqsqrtd โŠข ( ๐œ‘ โ†’ ( ( โˆš โ€˜ ๐‘€ ) โ†‘ 2 ) = ๐‘€ )
48 46 47 eqtr2d โŠข ( ๐œ‘ โ†’ ๐‘€ = ( ( 2 ยท ๐‘† ) โ†‘ 2 ) )
49 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 17 18 19 quartlem4 โŠข ( ๐œ‘ โ†’ ( ๐‘† โ‰  0 โˆง ๐ผ โˆˆ โ„‚ โˆง ๐ฝ โˆˆ โ„‚ ) )
50 49 simp2d โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ โ„‚ )
51 18 oveq1d โŠข ( ๐œ‘ โ†’ ( ๐ผ โ†‘ 2 ) = ( ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) โ†‘ 2 ) )
52 37 sqcld โŠข ( ๐œ‘ โ†’ ( ๐‘† โ†‘ 2 ) โˆˆ โ„‚ )
53 52 negcld โŠข ( ๐œ‘ โ†’ - ( ๐‘† โ†‘ 2 ) โˆˆ โ„‚ )
54 31 halfcld โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ / 2 ) โˆˆ โ„‚ )
55 53 54 subcld โŠข ( ๐œ‘ โ†’ ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆˆ โ„‚ )
56 32 22 24 divcld โŠข ( ๐œ‘ โ†’ ( ๐‘„ / 4 ) โˆˆ โ„‚ )
57 49 simp1d โŠข ( ๐œ‘ โ†’ ๐‘† โ‰  0 )
58 56 37 57 divcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘„ / 4 ) / ๐‘† ) โˆˆ โ„‚ )
59 55 58 addcld โŠข ( ๐œ‘ โ†’ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) โˆˆ โ„‚ )
60 59 sqsqrtd โŠข ( ๐œ‘ โ†’ ( ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) โ†‘ 2 ) = ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) )
61 51 60 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ผ โ†‘ 2 ) = ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) + ( ( ๐‘„ / 4 ) / ๐‘† ) ) )
62 30 simp3d โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„‚ )
63 1cnd โŠข ( ๐œ‘ โ†’ 1 โˆˆ โ„‚ )
64 3z โŠข 3 โˆˆ โ„ค
65 1exp โŠข ( 3 โˆˆ โ„ค โ†’ ( 1 โ†‘ 3 ) = 1 )
66 64 65 mp1i โŠข ( ๐œ‘ โ†’ ( 1 โ†‘ 3 ) = 1 )
67 36 simp3d โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚ )
68 67 mulid2d โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘‡ ) = ๐‘‡ )
69 68 oveq2d โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) = ( ( 2 ยท ๐‘ƒ ) + ๐‘‡ ) )
70 68 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) = ( ๐‘ˆ / ๐‘‡ ) )
71 69 70 oveq12d โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) = ( ( ( 2 ยท ๐‘ƒ ) + ๐‘‡ ) + ( ๐‘ˆ / ๐‘‡ ) ) )
72 71 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) = ( ( ( ( 2 ยท ๐‘ƒ ) + ๐‘‡ ) + ( ๐‘ˆ / ๐‘‡ ) ) / 3 ) )
73 72 negeqd โŠข ( ๐œ‘ โ†’ - ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) = - ( ( ( ( 2 ยท ๐‘ƒ ) + ๐‘‡ ) + ( ๐‘ˆ / ๐‘‡ ) ) / 3 ) )
74 14 73 eqtr4d โŠข ( ๐œ‘ โ†’ ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) )
75 oveq1 โŠข ( ๐‘ฅ = 1 โ†’ ( ๐‘ฅ โ†‘ 3 ) = ( 1 โ†‘ 3 ) )
76 75 eqeq1d โŠข ( ๐‘ฅ = 1 โ†’ ( ( ๐‘ฅ โ†‘ 3 ) = 1 โ†” ( 1 โ†‘ 3 ) = 1 ) )
77 oveq1 โŠข ( ๐‘ฅ = 1 โ†’ ( ๐‘ฅ ยท ๐‘‡ ) = ( 1 ยท ๐‘‡ ) )
78 77 oveq2d โŠข ( ๐‘ฅ = 1 โ†’ ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) = ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) )
79 77 oveq2d โŠข ( ๐‘ฅ = 1 โ†’ ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) = ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) )
80 78 79 oveq12d โŠข ( ๐‘ฅ = 1 โ†’ ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) = ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) )
81 80 oveq1d โŠข ( ๐‘ฅ = 1 โ†’ ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) = ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) )
82 81 negeqd โŠข ( ๐‘ฅ = 1 โ†’ - ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) )
83 82 eqeq2d โŠข ( ๐‘ฅ = 1 โ†’ ( ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) โ†” ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) ) )
84 76 83 anbi12d โŠข ( ๐‘ฅ = 1 โ†’ ( ( ( ๐‘ฅ โ†‘ 3 ) = 1 โˆง ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) ) โ†” ( ( 1 โ†‘ 3 ) = 1 โˆง ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) ) ) )
85 84 rspcev โŠข ( ( 1 โˆˆ โ„‚ โˆง ( ( 1 โ†‘ 3 ) = 1 โˆง ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( 1 ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( 1 ยท ๐‘‡ ) ) ) / 3 ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ( ๐‘ฅ โ†‘ 3 ) = 1 โˆง ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) ) )
86 63 66 74 85 syl12anc โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ( ๐‘ฅ โ†‘ 3 ) = 1 โˆง ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) ) )
87 2cn โŠข 2 โˆˆ โ„‚
88 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ ) โ†’ ( 2 ยท ๐‘ƒ ) โˆˆ โ„‚ )
89 87 31 88 sylancr โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ƒ ) โˆˆ โ„‚ )
90 31 sqcld โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โ†‘ 2 ) โˆˆ โ„‚ )
91 mulcl โŠข ( ( 4 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚ ) โ†’ ( 4 ยท ๐‘… ) โˆˆ โ„‚ )
92 21 62 91 sylancr โŠข ( ๐œ‘ โ†’ ( 4 ยท ๐‘… ) โˆˆ โ„‚ )
93 90 92 subcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) โˆˆ โ„‚ )
94 32 sqcld โŠข ( ๐œ‘ โ†’ ( ๐‘„ โ†‘ 2 ) โˆˆ โ„‚ )
95 94 negcld โŠข ( ๐œ‘ โ†’ - ( ๐‘„ โ†‘ 2 ) โˆˆ โ„‚ )
96 15 oveq1d โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ†‘ 3 ) = ( ( ( ( ๐‘‰ + ๐‘Š ) / 2 ) โ†‘๐‘ ( 1 / 3 ) ) โ†‘ 3 ) )
97 1 2 3 4 1 6 7 8 9 10 11 12 quartlem2 โŠข ( ๐œ‘ โ†’ ( ๐‘ˆ โˆˆ โ„‚ โˆง ๐‘‰ โˆˆ โ„‚ โˆง ๐‘Š โˆˆ โ„‚ ) )
98 97 simp2d โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ โ„‚ )
99 97 simp3d โŠข ( ๐œ‘ โ†’ ๐‘Š โˆˆ โ„‚ )
100 98 99 addcld โŠข ( ๐œ‘ โ†’ ( ๐‘‰ + ๐‘Š ) โˆˆ โ„‚ )
101 100 halfcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‰ + ๐‘Š ) / 2 ) โˆˆ โ„‚ )
102 3nn โŠข 3 โˆˆ โ„•
103 cxproot โŠข ( ( ( ( ๐‘‰ + ๐‘Š ) / 2 ) โˆˆ โ„‚ โˆง 3 โˆˆ โ„• ) โ†’ ( ( ( ( ๐‘‰ + ๐‘Š ) / 2 ) โ†‘๐‘ ( 1 / 3 ) ) โ†‘ 3 ) = ( ( ๐‘‰ + ๐‘Š ) / 2 ) )
104 101 102 103 sylancl โŠข ( ๐œ‘ โ†’ ( ( ( ( ๐‘‰ + ๐‘Š ) / 2 ) โ†‘๐‘ ( 1 / 3 ) ) โ†‘ 3 ) = ( ( ๐‘‰ + ๐‘Š ) / 2 ) )
105 96 104 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ†‘ 3 ) = ( ( ๐‘‰ + ๐‘Š ) / 2 ) )
106 12 oveq1d โŠข ( ๐œ‘ โ†’ ( ๐‘Š โ†‘ 2 ) = ( ( โˆš โ€˜ ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) ) โ†‘ 2 ) )
107 98 sqcld โŠข ( ๐œ‘ โ†’ ( ๐‘‰ โ†‘ 2 ) โˆˆ โ„‚ )
108 97 simp1d โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„‚ )
109 3nn0 โŠข 3 โˆˆ โ„•0
110 expcl โŠข ( ( ๐‘ˆ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0 ) โ†’ ( ๐‘ˆ โ†‘ 3 ) โˆˆ โ„‚ )
111 108 109 110 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘ˆ โ†‘ 3 ) โˆˆ โ„‚ )
112 mulcl โŠข ( ( 4 โˆˆ โ„‚ โˆง ( ๐‘ˆ โ†‘ 3 ) โˆˆ โ„‚ ) โ†’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) โˆˆ โ„‚ )
113 21 111 112 sylancr โŠข ( ๐œ‘ โ†’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) โˆˆ โ„‚ )
114 107 113 subcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) โˆˆ โ„‚ )
115 114 sqsqrtd โŠข ( ๐œ‘ โ†’ ( ( โˆš โ€˜ ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) ) โ†‘ 2 ) = ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) )
116 106 115 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘Š โ†‘ 2 ) = ( ( ๐‘‰ โ†‘ 2 ) โˆ’ ( 4 ยท ( ๐‘ˆ โ†‘ 3 ) ) ) )
117 31 32 62 10 11 quartlem1 โŠข ( ๐œ‘ โ†’ ( ๐‘ˆ = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) โˆง ๐‘‰ = ( ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) + ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) ) ) )
118 117 simpld โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) )
119 117 simprd โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) + ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) ) )
120 89 93 95 39 67 105 99 116 118 119 16 mcubic โŠข ( ๐œ‘ โ†’ ( ( ( ( ๐‘€ โ†‘ 3 ) + ( ( 2 ยท ๐‘ƒ ) ยท ( ๐‘€ โ†‘ 2 ) ) ) + ( ( ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ยท ๐‘€ ) + - ( ๐‘„ โ†‘ 2 ) ) ) = 0 โ†” โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ( ๐‘ฅ โ†‘ 3 ) = 1 โˆง ๐‘€ = - ( ( ( ( 2 ยท ๐‘ƒ ) + ( ๐‘ฅ ยท ๐‘‡ ) ) + ( ๐‘ˆ / ( ๐‘ฅ ยท ๐‘‡ ) ) ) / 3 ) ) ) )
121 86 120 mpbird โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘€ โ†‘ 3 ) + ( ( 2 ยท ๐‘ƒ ) ยท ( ๐‘€ โ†‘ 2 ) ) ) + ( ( ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ยท ๐‘€ ) + - ( ๐‘„ โ†‘ 2 ) ) ) = 0 )
122 49 simp3d โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚ )
123 19 oveq1d โŠข ( ๐œ‘ โ†’ ( ๐ฝ โ†‘ 2 ) = ( ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) โ†‘ 2 ) )
124 55 58 subcld โŠข ( ๐œ‘ โ†’ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) โˆˆ โ„‚ )
125 124 sqsqrtd โŠข ( ๐œ‘ โ†’ ( ( โˆš โ€˜ ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) ) โ†‘ 2 ) = ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) )
126 123 125 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ฝ โ†‘ 2 ) = ( ( - ( ๐‘† โ†‘ 2 ) โˆ’ ( ๐‘ƒ / 2 ) ) โˆ’ ( ( ๐‘„ / 4 ) / ๐‘† ) ) )
127 31 32 35 37 48 17 50 61 62 121 122 126 dquart โŠข ( ๐œ‘ โ†’ ( ( ( ( ( ๐‘‹ โˆ’ ๐ธ ) โ†‘ 4 ) + ( ๐‘ƒ ยท ( ( ๐‘‹ โˆ’ ๐ธ ) โ†‘ 2 ) ) ) + ( ( ๐‘„ ยท ( ๐‘‹ โˆ’ ๐ธ ) ) + ๐‘… ) ) = 0 โ†” ( ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† + ๐ผ ) โˆจ ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† โˆ’ ๐ผ ) ) โˆจ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† + ๐ฝ ) โˆจ ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† โˆ’ ๐ฝ ) ) ) ) )
128 37 negcld โŠข ( ๐œ‘ โ†’ - ๐‘† โˆˆ โ„‚ )
129 128 50 addcld โŠข ( ๐œ‘ โ†’ ( - ๐‘† + ๐ผ ) โˆˆ โ„‚ )
130 5 34 129 subaddd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† + ๐ผ ) โ†” ( ๐ธ + ( - ๐‘† + ๐ผ ) ) = ๐‘‹ ) )
131 34 37 negsubd โŠข ( ๐œ‘ โ†’ ( ๐ธ + - ๐‘† ) = ( ๐ธ โˆ’ ๐‘† ) )
132 131 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐ธ + - ๐‘† ) + ๐ผ ) = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) )
133 34 128 50 addassd โŠข ( ๐œ‘ โ†’ ( ( ๐ธ + - ๐‘† ) + ๐ผ ) = ( ๐ธ + ( - ๐‘† + ๐ผ ) ) )
134 132 133 eqtr3d โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) = ( ๐ธ + ( - ๐‘† + ๐ผ ) ) )
135 134 eqeq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) = ๐‘‹ โ†” ( ๐ธ + ( - ๐‘† + ๐ผ ) ) = ๐‘‹ ) )
136 130 135 bitr4d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† + ๐ผ ) โ†” ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) = ๐‘‹ ) )
137 eqcom โŠข ( ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) = ๐‘‹ โ†” ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) )
138 136 137 bitrdi โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† + ๐ผ ) โ†” ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) ) )
139 128 50 subcld โŠข ( ๐œ‘ โ†’ ( - ๐‘† โˆ’ ๐ผ ) โˆˆ โ„‚ )
140 5 34 139 subaddd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† โˆ’ ๐ผ ) โ†” ( ๐ธ + ( - ๐‘† โˆ’ ๐ผ ) ) = ๐‘‹ ) )
141 131 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐ธ + - ๐‘† ) โˆ’ ๐ผ ) = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) )
142 34 128 50 addsubassd โŠข ( ๐œ‘ โ†’ ( ( ๐ธ + - ๐‘† ) โˆ’ ๐ผ ) = ( ๐ธ + ( - ๐‘† โˆ’ ๐ผ ) ) )
143 141 142 eqtr3d โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) = ( ๐ธ + ( - ๐‘† โˆ’ ๐ผ ) ) )
144 143 eqeq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) = ๐‘‹ โ†” ( ๐ธ + ( - ๐‘† โˆ’ ๐ผ ) ) = ๐‘‹ ) )
145 140 144 bitr4d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† โˆ’ ๐ผ ) โ†” ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) = ๐‘‹ ) )
146 eqcom โŠข ( ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) = ๐‘‹ โ†” ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) )
147 145 146 bitrdi โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† โˆ’ ๐ผ ) โ†” ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) ) )
148 138 147 orbi12d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† + ๐ผ ) โˆจ ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† โˆ’ ๐ผ ) ) โ†” ( ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) โˆจ ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) ) ) )
149 37 122 addcld โŠข ( ๐œ‘ โ†’ ( ๐‘† + ๐ฝ ) โˆˆ โ„‚ )
150 5 34 149 subaddd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† + ๐ฝ ) โ†” ( ๐ธ + ( ๐‘† + ๐ฝ ) ) = ๐‘‹ ) )
151 34 37 122 addassd โŠข ( ๐œ‘ โ†’ ( ( ๐ธ + ๐‘† ) + ๐ฝ ) = ( ๐ธ + ( ๐‘† + ๐ฝ ) ) )
152 151 eqeq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ + ๐‘† ) + ๐ฝ ) = ๐‘‹ โ†” ( ๐ธ + ( ๐‘† + ๐ฝ ) ) = ๐‘‹ ) )
153 150 152 bitr4d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† + ๐ฝ ) โ†” ( ( ๐ธ + ๐‘† ) + ๐ฝ ) = ๐‘‹ ) )
154 eqcom โŠข ( ( ( ๐ธ + ๐‘† ) + ๐ฝ ) = ๐‘‹ โ†” ๐‘‹ = ( ( ๐ธ + ๐‘† ) + ๐ฝ ) )
155 153 154 bitrdi โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† + ๐ฝ ) โ†” ๐‘‹ = ( ( ๐ธ + ๐‘† ) + ๐ฝ ) ) )
156 37 122 subcld โŠข ( ๐œ‘ โ†’ ( ๐‘† โˆ’ ๐ฝ ) โˆˆ โ„‚ )
157 5 34 156 subaddd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† โˆ’ ๐ฝ ) โ†” ( ๐ธ + ( ๐‘† โˆ’ ๐ฝ ) ) = ๐‘‹ ) )
158 34 37 122 addsubassd โŠข ( ๐œ‘ โ†’ ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) = ( ๐ธ + ( ๐‘† โˆ’ ๐ฝ ) ) )
159 158 eqeq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) = ๐‘‹ โ†” ( ๐ธ + ( ๐‘† โˆ’ ๐ฝ ) ) = ๐‘‹ ) )
160 157 159 bitr4d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† โˆ’ ๐ฝ ) โ†” ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) = ๐‘‹ ) )
161 eqcom โŠข ( ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) = ๐‘‹ โ†” ๐‘‹ = ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) )
162 160 161 bitrdi โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† โˆ’ ๐ฝ ) โ†” ๐‘‹ = ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) ) )
163 155 162 orbi12d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† + ๐ฝ ) โˆจ ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† โˆ’ ๐ฝ ) ) โ†” ( ๐‘‹ = ( ( ๐ธ + ๐‘† ) + ๐ฝ ) โˆจ ๐‘‹ = ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) ) ) )
164 148 163 orbi12d โŠข ( ๐œ‘ โ†’ ( ( ( ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† + ๐ผ ) โˆจ ( ๐‘‹ โˆ’ ๐ธ ) = ( - ๐‘† โˆ’ ๐ผ ) ) โˆจ ( ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† + ๐ฝ ) โˆจ ( ๐‘‹ โˆ’ ๐ธ ) = ( ๐‘† โˆ’ ๐ฝ ) ) ) โ†” ( ( ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) โˆจ ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) ) โˆจ ( ๐‘‹ = ( ( ๐ธ + ๐‘† ) + ๐ฝ ) โˆจ ๐‘‹ = ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) ) ) ) )
165 29 127 164 3bitrd โŠข ( ๐œ‘ โ†’ ( ( ( ( ๐‘‹ โ†‘ 4 ) + ( ๐ด ยท ( ๐‘‹ โ†‘ 3 ) ) ) + ( ( ๐ต ยท ( ๐‘‹ โ†‘ 2 ) ) + ( ( ๐ถ ยท ๐‘‹ ) + ๐ท ) ) ) = 0 โ†” ( ( ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) + ๐ผ ) โˆจ ๐‘‹ = ( ( ๐ธ โˆ’ ๐‘† ) โˆ’ ๐ผ ) ) โˆจ ( ๐‘‹ = ( ( ๐ธ + ๐‘† ) + ๐ฝ ) โˆจ ๐‘‹ = ( ( ๐ธ + ๐‘† ) โˆ’ ๐ฝ ) ) ) ) )