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

Theorem mcubic 26200
Description: Solutions to a monic cubic equation, a special case of cubic 26202. (Contributed by Mario Carneiro, 24-Apr-2015.)
Hypotheses
Ref Expression
mcubic.b (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
mcubic.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
mcubic.d (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
mcubic.x (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
mcubic.t (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
mcubic.3 (๐œ‘ โ†’ (๐‘‡โ†‘3) = ((๐‘ + ๐บ) / 2))
mcubic.g (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
mcubic.2 (๐œ‘ โ†’ (๐บโ†‘2) = ((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))))
mcubic.m (๐œ‘ โ†’ ๐‘€ = ((๐ตโ†‘2) โˆ’ (3 ยท ๐ถ)))
mcubic.n (๐œ‘ โ†’ ๐‘ = (((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) + (27 ยท ๐ท)))
mcubic.0 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
Assertion
Ref Expression
mcubic (๐œ‘ โ†’ ((((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3))))
Distinct variable groups:   ๐ต,๐‘Ÿ   ๐‘€,๐‘Ÿ   ๐‘,๐‘Ÿ   ๐œ‘,๐‘Ÿ   ๐‘‡,๐‘Ÿ   ๐‘‹,๐‘Ÿ
Allowed substitution hints:   ๐ถ(๐‘Ÿ)   ๐ท(๐‘Ÿ)   ๐บ(๐‘Ÿ)

Proof of Theorem mcubic
StepHypRef Expression
1 mcubic.m . . . . . 6 (๐œ‘ โ†’ ๐‘€ = ((๐ตโ†‘2) โˆ’ (3 ยท ๐ถ)))
2 mcubic.b . . . . . . . 8 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
32sqcld 14050 . . . . . . 7 (๐œ‘ โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
4 3cn 12235 . . . . . . . 8 3 โˆˆ โ„‚
5 mcubic.c . . . . . . . 8 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
6 mulcl 11136 . . . . . . . 8 ((3 โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (3 ยท ๐ถ) โˆˆ โ„‚)
74, 5, 6sylancr 588 . . . . . . 7 (๐œ‘ โ†’ (3 ยท ๐ถ) โˆˆ โ„‚)
83, 7subcld 11513 . . . . . 6 (๐œ‘ โ†’ ((๐ตโ†‘2) โˆ’ (3 ยท ๐ถ)) โˆˆ โ„‚)
91, 8eqeltrd 2838 . . . . 5 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
104a1i 11 . . . . 5 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
11 3ne0 12260 . . . . . 6 3 โ‰  0
1211a1i 11 . . . . 5 (๐œ‘ โ†’ 3 โ‰  0)
139, 10, 12divcld 11932 . . . 4 (๐œ‘ โ†’ (๐‘€ / 3) โˆˆ โ„‚)
1413negcld 11500 . . 3 (๐œ‘ โ†’ -(๐‘€ / 3) โˆˆ โ„‚)
15 mcubic.n . . . . 5 (๐œ‘ โ†’ ๐‘ = (((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) + (27 ยท ๐ท)))
16 2cn 12229 . . . . . . . 8 2 โˆˆ โ„‚
17 3nn0 12432 . . . . . . . . 9 3 โˆˆ โ„•0
18 expcl 13986 . . . . . . . . 9 ((๐ต โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐ตโ†‘3) โˆˆ โ„‚)
192, 17, 18sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ (๐ตโ†‘3) โˆˆ โ„‚)
20 mulcl 11136 . . . . . . . 8 ((2 โˆˆ โ„‚ โˆง (๐ตโ†‘3) โˆˆ โ„‚) โ†’ (2 ยท (๐ตโ†‘3)) โˆˆ โ„‚)
2116, 19, 20sylancr 588 . . . . . . 7 (๐œ‘ โ†’ (2 ยท (๐ตโ†‘3)) โˆˆ โ„‚)
22 9cn 12254 . . . . . . . 8 9 โˆˆ โ„‚
232, 5mulcld 11176 . . . . . . . 8 (๐œ‘ โ†’ (๐ต ยท ๐ถ) โˆˆ โ„‚)
24 mulcl 11136 . . . . . . . 8 ((9 โˆˆ โ„‚ โˆง (๐ต ยท ๐ถ) โˆˆ โ„‚) โ†’ (9 ยท (๐ต ยท ๐ถ)) โˆˆ โ„‚)
2522, 23, 24sylancr 588 . . . . . . 7 (๐œ‘ โ†’ (9 ยท (๐ต ยท ๐ถ)) โˆˆ โ„‚)
2621, 25subcld 11513 . . . . . 6 (๐œ‘ โ†’ ((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) โˆˆ โ„‚)
27 2nn0 12431 . . . . . . . . 9 2 โˆˆ โ„•0
28 7nn 12246 . . . . . . . . 9 7 โˆˆ โ„•
2927, 28decnncl 12639 . . . . . . . 8 27 โˆˆ โ„•
3029nncni 12164 . . . . . . 7 27 โˆˆ โ„‚
31 mcubic.d . . . . . . 7 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
32 mulcl 11136 . . . . . . 7 ((27 โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚) โ†’ (27 ยท ๐ท) โˆˆ โ„‚)
3330, 31, 32sylancr 588 . . . . . 6 (๐œ‘ โ†’ (27 ยท ๐ท) โˆˆ โ„‚)
3426, 33addcld 11175 . . . . 5 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) + (27 ยท ๐ท)) โˆˆ โ„‚)
3515, 34eqeltrd 2838 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
3630a1i 11 . . . 4 (๐œ‘ โ†’ 27 โˆˆ โ„‚)
3729nnne0i 12194 . . . . 5 27 โ‰  0
3837a1i 11 . . . 4 (๐œ‘ โ†’ 27 โ‰  0)
3935, 36, 38divcld 11932 . . 3 (๐œ‘ โ†’ (๐‘ / 27) โˆˆ โ„‚)
40 mcubic.x . . . 4 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
412, 10, 12divcld 11932 . . . 4 (๐œ‘ โ†’ (๐ต / 3) โˆˆ โ„‚)
4240, 41addcld 11175 . . 3 (๐œ‘ โ†’ (๐‘‹ + (๐ต / 3)) โˆˆ โ„‚)
43 mcubic.t . . . . 5 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
4443, 10, 12divcld 11932 . . . 4 (๐œ‘ โ†’ (๐‘‡ / 3) โˆˆ โ„‚)
4544negcld 11500 . . 3 (๐œ‘ โ†’ -(๐‘‡ / 3) โˆˆ โ„‚)
46 3nn 12233 . . . . . 6 3 โˆˆ โ„•
4746a1i 11 . . . . 5 (๐œ‘ โ†’ 3 โˆˆ โ„•)
48 n2dvds3 16254 . . . . . 6 ยฌ 2 โˆฅ 3
4948a1i 11 . . . . 5 (๐œ‘ โ†’ ยฌ 2 โˆฅ 3)
50 oexpneg 16228 . . . . 5 (((๐‘‡ / 3) โˆˆ โ„‚ โˆง 3 โˆˆ โ„• โˆง ยฌ 2 โˆฅ 3) โ†’ (-(๐‘‡ / 3)โ†‘3) = -((๐‘‡ / 3)โ†‘3))
5144, 47, 49, 50syl3anc 1372 . . . 4 (๐œ‘ โ†’ (-(๐‘‡ / 3)โ†‘3) = -((๐‘‡ / 3)โ†‘3))
5217a1i 11 . . . . . . 7 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
5343, 10, 12, 52expdivd 14066 . . . . . 6 (๐œ‘ โ†’ ((๐‘‡ / 3)โ†‘3) = ((๐‘‡โ†‘3) / (3โ†‘3)))
54 mcubic.3 . . . . . . 7 (๐œ‘ โ†’ (๐‘‡โ†‘3) = ((๐‘ + ๐บ) / 2))
55 3exp3 16965 . . . . . . . 8 (3โ†‘3) = 27
5655a1i 11 . . . . . . 7 (๐œ‘ โ†’ (3โ†‘3) = 27)
5754, 56oveq12d 7376 . . . . . 6 (๐œ‘ โ†’ ((๐‘‡โ†‘3) / (3โ†‘3)) = (((๐‘ + ๐บ) / 2) / 27))
58 mcubic.g . . . . . . . . 9 (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
5935, 58addcld 11175 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ + ๐บ) โˆˆ โ„‚)
60 2cnd 12232 . . . . . . . 8 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
61 2ne0 12258 . . . . . . . . 9 2 โ‰  0
6261a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2 โ‰  0)
6359, 60, 36, 62, 38divdiv32d 11957 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ + ๐บ) / 2) / 27) = (((๐‘ + ๐บ) / 27) / 2))
6435, 58addcomd 11358 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ + ๐บ) = (๐บ + ๐‘))
6564oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ + ๐บ) / 27) = ((๐บ + ๐‘) / 27))
6658, 35, 36, 38divdird 11970 . . . . . . . . 9 (๐œ‘ โ†’ ((๐บ + ๐‘) / 27) = ((๐บ / 27) + (๐‘ / 27)))
6765, 66eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ + ๐บ) / 27) = ((๐บ / 27) + (๐‘ / 27)))
6867oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ + ๐บ) / 27) / 2) = (((๐บ / 27) + (๐‘ / 27)) / 2))
6958, 36, 38divcld 11932 . . . . . . . 8 (๐œ‘ โ†’ (๐บ / 27) โˆˆ โ„‚)
7069, 39, 60, 62divdird 11970 . . . . . . 7 (๐œ‘ โ†’ (((๐บ / 27) + (๐‘ / 27)) / 2) = (((๐บ / 27) / 2) + ((๐‘ / 27) / 2)))
7163, 68, 703eqtrd 2781 . . . . . 6 (๐œ‘ โ†’ (((๐‘ + ๐บ) / 2) / 27) = (((๐บ / 27) / 2) + ((๐‘ / 27) / 2)))
7253, 57, 713eqtrd 2781 . . . . 5 (๐œ‘ โ†’ ((๐‘‡ / 3)โ†‘3) = (((๐บ / 27) / 2) + ((๐‘ / 27) / 2)))
7372negeqd 11396 . . . 4 (๐œ‘ โ†’ -((๐‘‡ / 3)โ†‘3) = -(((๐บ / 27) / 2) + ((๐‘ / 27) / 2)))
7469halfcld 12399 . . . . 5 (๐œ‘ โ†’ ((๐บ / 27) / 2) โˆˆ โ„‚)
7539halfcld 12399 . . . . 5 (๐œ‘ โ†’ ((๐‘ / 27) / 2) โˆˆ โ„‚)
7674, 75negdi2d 11527 . . . 4 (๐œ‘ โ†’ -(((๐บ / 27) / 2) + ((๐‘ / 27) / 2)) = (-((๐บ / 27) / 2) โˆ’ ((๐‘ / 27) / 2)))
7751, 73, 763eqtrd 2781 . . 3 (๐œ‘ โ†’ (-(๐‘‡ / 3)โ†‘3) = (-((๐บ / 27) / 2) โˆ’ ((๐‘ / 27) / 2)))
7874negcld 11500 . . 3 (๐œ‘ โ†’ -((๐บ / 27) / 2) โˆˆ โ„‚)
79 sqneg 14022 . . . . 5 (((๐บ / 27) / 2) โˆˆ โ„‚ โ†’ (-((๐บ / 27) / 2)โ†‘2) = (((๐บ / 27) / 2)โ†‘2))
8074, 79syl 17 . . . 4 (๐œ‘ โ†’ (-((๐บ / 27) / 2)โ†‘2) = (((๐บ / 27) / 2)โ†‘2))
8169, 60, 62sqdivd 14065 . . . 4 (๐œ‘ โ†’ (((๐บ / 27) / 2)โ†‘2) = (((๐บ / 27)โ†‘2) / (2โ†‘2)))
8239, 60, 62sqdivd 14065 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ / 27) / 2)โ†‘2) = (((๐‘ / 27)โ†‘2) / (2โ†‘2)))
8335, 36, 38sqdivd 14065 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ / 27)โ†‘2) = ((๐‘โ†‘2) / (27โ†‘2)))
8483oveq1d 7373 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ / 27)โ†‘2) / (2โ†‘2)) = (((๐‘โ†‘2) / (27โ†‘2)) / (2โ†‘2)))
8582, 84eqtr2d 2778 . . . . . . 7 (๐œ‘ โ†’ (((๐‘โ†‘2) / (27โ†‘2)) / (2โ†‘2)) = (((๐‘ / 27) / 2)โ†‘2))
86 4cn 12239 . . . . . . . . . . . 12 4 โˆˆ โ„‚
8786a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 4 โˆˆ โ„‚)
88 expcl 13986 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘€โ†‘3) โˆˆ โ„‚)
899, 17, 88sylancl 587 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘€โ†‘3) โˆˆ โ„‚)
9030sqcli 14086 . . . . . . . . . . . 12 (27โ†‘2) โˆˆ โ„‚
9190a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (27โ†‘2) โˆˆ โ„‚)
92 sqne0 14029 . . . . . . . . . . . . 13 (27 โˆˆ โ„‚ โ†’ ((27โ†‘2) โ‰  0 โ†” 27 โ‰  0))
9336, 92syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((27โ†‘2) โ‰  0 โ†” 27 โ‰  0))
9438, 93mpbird 257 . . . . . . . . . . 11 (๐œ‘ โ†’ (27โ†‘2) โ‰  0)
9587, 89, 91, 94divassd 11967 . . . . . . . . . 10 (๐œ‘ โ†’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) = (4 ยท ((๐‘€โ†‘3) / (27โ†‘2))))
9622a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 9 โˆˆ โ„‚)
97 9nn 12252 . . . . . . . . . . . . . . 15 9 โˆˆ โ„•
9897nnne0i 12194 . . . . . . . . . . . . . 14 9 โ‰  0
9998a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 9 โ‰  0)
1009, 96, 99, 52expdivd 14066 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ / 9)โ†‘3) = ((๐‘€โ†‘3) / (9โ†‘3)))
10116, 4mulcomi 11164 . . . . . . . . . . . . . . . 16 (2 ยท 3) = (3 ยท 2)
102101oveq2i 7369 . . . . . . . . . . . . . . 15 (3โ†‘(2 ยท 3)) = (3โ†‘(3 ยท 2))
103 expmul 14014 . . . . . . . . . . . . . . . 16 ((3 โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 โˆง 3 โˆˆ โ„•0) โ†’ (3โ†‘(2 ยท 3)) = ((3โ†‘2)โ†‘3))
1044, 27, 17, 103mp3an 1462 . . . . . . . . . . . . . . 15 (3โ†‘(2 ยท 3)) = ((3โ†‘2)โ†‘3)
105 expmul 14014 . . . . . . . . . . . . . . . 16 ((3 โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0) โ†’ (3โ†‘(3 ยท 2)) = ((3โ†‘3)โ†‘2))
1064, 17, 27, 105mp3an 1462 . . . . . . . . . . . . . . 15 (3โ†‘(3 ยท 2)) = ((3โ†‘3)โ†‘2)
107102, 104, 1063eqtr3i 2773 . . . . . . . . . . . . . 14 ((3โ†‘2)โ†‘3) = ((3โ†‘3)โ†‘2)
108 sq3 14103 . . . . . . . . . . . . . . 15 (3โ†‘2) = 9
109108oveq1i 7368 . . . . . . . . . . . . . 14 ((3โ†‘2)โ†‘3) = (9โ†‘3)
11055oveq1i 7368 . . . . . . . . . . . . . 14 ((3โ†‘3)โ†‘2) = (27โ†‘2)
111107, 109, 1103eqtr3i 2773 . . . . . . . . . . . . 13 (9โ†‘3) = (27โ†‘2)
112111oveq2i 7369 . . . . . . . . . . . 12 ((๐‘€โ†‘3) / (9โ†‘3)) = ((๐‘€โ†‘3) / (27โ†‘2))
113100, 112eqtrdi 2793 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘€ / 9)โ†‘3) = ((๐‘€โ†‘3) / (27โ†‘2)))
114113oveq2d 7374 . . . . . . . . . 10 (๐œ‘ โ†’ (4 ยท ((๐‘€ / 9)โ†‘3)) = (4 ยท ((๐‘€โ†‘3) / (27โ†‘2))))
11595, 114eqtr4d 2780 . . . . . . . . 9 (๐œ‘ โ†’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) = (4 ยท ((๐‘€ / 9)โ†‘3)))
116115oveq1d 7373 . . . . . . . 8 (๐œ‘ โ†’ (((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) / (2โ†‘2)) = ((4 ยท ((๐‘€ / 9)โ†‘3)) / (2โ†‘2)))
117 sq2 14102 . . . . . . . . . 10 (2โ†‘2) = 4
118117oveq2i 7369 . . . . . . . . 9 ((4 ยท ((๐‘€ / 9)โ†‘3)) / (2โ†‘2)) = ((4 ยท ((๐‘€ / 9)โ†‘3)) / 4)
1199, 96, 99divcld 11932 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘€ / 9) โˆˆ โ„‚)
120 expcl 13986 . . . . . . . . . . 11 (((๐‘€ / 9) โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ ((๐‘€ / 9)โ†‘3) โˆˆ โ„‚)
121119, 17, 120sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘€ / 9)โ†‘3) โˆˆ โ„‚)
122 4ne0 12262 . . . . . . . . . . 11 4 โ‰  0
123122a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 4 โ‰  0)
124121, 87, 123divcan3d 11937 . . . . . . . . 9 (๐œ‘ โ†’ ((4 ยท ((๐‘€ / 9)โ†‘3)) / 4) = ((๐‘€ / 9)โ†‘3))
125118, 124eqtrid 2789 . . . . . . . 8 (๐œ‘ โ†’ ((4 ยท ((๐‘€ / 9)โ†‘3)) / (2โ†‘2)) = ((๐‘€ / 9)โ†‘3))
126116, 125eqtrd 2777 . . . . . . 7 (๐œ‘ โ†’ (((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) / (2โ†‘2)) = ((๐‘€ / 9)โ†‘3))
12785, 126oveq12d 7376 . . . . . 6 (๐œ‘ โ†’ ((((๐‘โ†‘2) / (27โ†‘2)) / (2โ†‘2)) โˆ’ (((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) / (2โ†‘2))) = ((((๐‘ / 27) / 2)โ†‘2) โˆ’ ((๐‘€ / 9)โ†‘3)))
12835sqcld 14050 . . . . . . . 8 (๐œ‘ โ†’ (๐‘โ†‘2) โˆˆ โ„‚)
129128, 91, 94divcld 11932 . . . . . . 7 (๐œ‘ โ†’ ((๐‘โ†‘2) / (27โ†‘2)) โˆˆ โ„‚)
130 mulcl 11136 . . . . . . . . 9 ((4 โˆˆ โ„‚ โˆง (๐‘€โ†‘3) โˆˆ โ„‚) โ†’ (4 ยท (๐‘€โ†‘3)) โˆˆ โ„‚)
13186, 89, 130sylancr 588 . . . . . . . 8 (๐œ‘ โ†’ (4 ยท (๐‘€โ†‘3)) โˆˆ โ„‚)
132131, 91, 94divcld 11932 . . . . . . 7 (๐œ‘ โ†’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) โˆˆ โ„‚)
13316sqcli 14086 . . . . . . . 8 (2โ†‘2) โˆˆ โ„‚
134133a1i 11 . . . . . . 7 (๐œ‘ โ†’ (2โ†‘2) โˆˆ โ„‚)
135117, 122eqnetri 3015 . . . . . . . 8 (2โ†‘2) โ‰  0
136135a1i 11 . . . . . . 7 (๐œ‘ โ†’ (2โ†‘2) โ‰  0)
137129, 132, 134, 136divsubdird 11971 . . . . . 6 (๐œ‘ โ†’ ((((๐‘โ†‘2) / (27โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2))) / (2โ†‘2)) = ((((๐‘โ†‘2) / (27โ†‘2)) / (2โ†‘2)) โˆ’ (((4 ยท (๐‘€โ†‘3)) / (27โ†‘2)) / (2โ†‘2))))
13875sqcld 14050 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ / 27) / 2)โ†‘2) โˆˆ โ„‚)
139138, 121negsubd 11519 . . . . . 6 (๐œ‘ โ†’ ((((๐‘ / 27) / 2)โ†‘2) + -((๐‘€ / 9)โ†‘3)) = ((((๐‘ / 27) / 2)โ†‘2) โˆ’ ((๐‘€ / 9)โ†‘3)))
140127, 137, 1393eqtr4d 2787 . . . . 5 (๐œ‘ โ†’ ((((๐‘โ†‘2) / (27โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2))) / (2โ†‘2)) = ((((๐‘ / 27) / 2)โ†‘2) + -((๐‘€ / 9)โ†‘3)))
14158, 36, 38sqdivd 14065 . . . . . . 7 (๐œ‘ โ†’ ((๐บ / 27)โ†‘2) = ((๐บโ†‘2) / (27โ†‘2)))
142 mcubic.2 . . . . . . . 8 (๐œ‘ โ†’ (๐บโ†‘2) = ((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))))
143142oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ ((๐บโ†‘2) / (27โ†‘2)) = (((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))) / (27โ†‘2)))
144128, 131, 91, 94divsubdird 11971 . . . . . . 7 (๐œ‘ โ†’ (((๐‘โ†‘2) โˆ’ (4 ยท (๐‘€โ†‘3))) / (27โ†‘2)) = (((๐‘โ†‘2) / (27โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2))))
145141, 143, 1443eqtrd 2781 . . . . . 6 (๐œ‘ โ†’ ((๐บ / 27)โ†‘2) = (((๐‘โ†‘2) / (27โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2))))
146145oveq1d 7373 . . . . 5 (๐œ‘ โ†’ (((๐บ / 27)โ†‘2) / (2โ†‘2)) = ((((๐‘โ†‘2) / (27โ†‘2)) โˆ’ ((4 ยท (๐‘€โ†‘3)) / (27โ†‘2))) / (2โ†‘2)))
147 oexpneg 16228 . . . . . . 7 (((๐‘€ / 9) โˆˆ โ„‚ โˆง 3 โˆˆ โ„• โˆง ยฌ 2 โˆฅ 3) โ†’ (-(๐‘€ / 9)โ†‘3) = -((๐‘€ / 9)โ†‘3))
148119, 47, 49, 147syl3anc 1372 . . . . . 6 (๐œ‘ โ†’ (-(๐‘€ / 9)โ†‘3) = -((๐‘€ / 9)โ†‘3))
149148oveq2d 7374 . . . . 5 (๐œ‘ โ†’ ((((๐‘ / 27) / 2)โ†‘2) + (-(๐‘€ / 9)โ†‘3)) = ((((๐‘ / 27) / 2)โ†‘2) + -((๐‘€ / 9)โ†‘3)))
150140, 146, 1493eqtr4d 2787 . . . 4 (๐œ‘ โ†’ (((๐บ / 27)โ†‘2) / (2โ†‘2)) = ((((๐‘ / 27) / 2)โ†‘2) + (-(๐‘€ / 9)โ†‘3)))
15180, 81, 1503eqtrd 2781 . . 3 (๐œ‘ โ†’ (-((๐บ / 27) / 2)โ†‘2) = ((((๐‘ / 27) / 2)โ†‘2) + (-(๐‘€ / 9)โ†‘3)))
1529, 10, 10, 12, 12divdiv1d 11963 . . . . . 6 (๐œ‘ โ†’ ((๐‘€ / 3) / 3) = (๐‘€ / (3 ยท 3)))
153 3t3e9 12321 . . . . . . 7 (3 ยท 3) = 9
154153oveq2i 7369 . . . . . 6 (๐‘€ / (3 ยท 3)) = (๐‘€ / 9)
155152, 154eqtrdi 2793 . . . . 5 (๐œ‘ โ†’ ((๐‘€ / 3) / 3) = (๐‘€ / 9))
156155negeqd 11396 . . . 4 (๐œ‘ โ†’ -((๐‘€ / 3) / 3) = -(๐‘€ / 9))
15713, 10, 12divnegd 11945 . . . 4 (๐œ‘ โ†’ -((๐‘€ / 3) / 3) = (-(๐‘€ / 3) / 3))
158156, 157eqtr3d 2779 . . 3 (๐œ‘ โ†’ -(๐‘€ / 9) = (-(๐‘€ / 3) / 3))
159 eqidd 2738 . . 3 (๐œ‘ โ†’ ((๐‘ / 27) / 2) = ((๐‘ / 27) / 2))
160 mcubic.0 . . . . 5 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
16143, 10, 160, 12divne0d 11948 . . . 4 (๐œ‘ โ†’ (๐‘‡ / 3) โ‰  0)
16244, 161negne0d 11511 . . 3 (๐œ‘ โ†’ -(๐‘‡ / 3) โ‰  0)
16314, 39, 42, 45, 77, 78, 151, 158, 159, 162dcubic 26199 . 2 (๐œ‘ โ†’ ((((๐‘‹ + (๐ต / 3))โ†‘3) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = 0 โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง (๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3)))))))
164 binom3 14128 . . . . . . 7 ((๐‘‹ โˆˆ โ„‚ โˆง (๐ต / 3) โˆˆ โ„‚) โ†’ ((๐‘‹ + (๐ต / 3))โ†‘3) = (((๐‘‹โ†‘3) + (3 ยท ((๐‘‹โ†‘2) ยท (๐ต / 3)))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))))
16540, 41, 164syl2anc 585 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ + (๐ต / 3))โ†‘3) = (((๐‘‹โ†‘3) + (3 ยท ((๐‘‹โ†‘2) ยท (๐ต / 3)))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))))
16640sqcld 14050 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‹โ†‘2) โˆˆ โ„‚)
16710, 166, 41mul12d 11365 . . . . . . . . 9 (๐œ‘ โ†’ (3 ยท ((๐‘‹โ†‘2) ยท (๐ต / 3))) = ((๐‘‹โ†‘2) ยท (3 ยท (๐ต / 3))))
1682, 10, 12divcan2d 11934 . . . . . . . . . 10 (๐œ‘ โ†’ (3 ยท (๐ต / 3)) = ๐ต)
169168oveq2d 7374 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‹โ†‘2) ยท (3 ยท (๐ต / 3))) = ((๐‘‹โ†‘2) ยท ๐ต))
170166, 2mulcomd 11177 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‹โ†‘2) ยท ๐ต) = (๐ต ยท (๐‘‹โ†‘2)))
171167, 169, 1703eqtrd 2781 . . . . . . . 8 (๐œ‘ โ†’ (3 ยท ((๐‘‹โ†‘2) ยท (๐ต / 3))) = (๐ต ยท (๐‘‹โ†‘2)))
172171oveq2d 7374 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‹โ†‘3) + (3 ยท ((๐‘‹โ†‘2) ยท (๐ต / 3)))) = ((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))))
173172oveq1d 7373 . . . . . 6 (๐œ‘ โ†’ (((๐‘‹โ†‘3) + (3 ยท ((๐‘‹โ†‘2) ยท (๐ต / 3)))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))) = (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))))
174165, 173eqtrd 2777 . . . . 5 (๐œ‘ โ†’ ((๐‘‹ + (๐ต / 3))โ†‘3) = (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))))
175174oveq1d 7373 . . . 4 (๐œ‘ โ†’ (((๐‘‹ + (๐ต / 3))โ†‘3) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = ((((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))))
176 expcl 13986 . . . . . . 7 ((๐‘‹ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
17740, 17, 176sylancl 587 . . . . . 6 (๐œ‘ โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
1782, 166mulcld 11176 . . . . . 6 (๐œ‘ โ†’ (๐ต ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
179177, 178addcld 11175 . . . . 5 (๐œ‘ โ†’ ((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) โˆˆ โ„‚)
18041sqcld 14050 . . . . . . . 8 (๐œ‘ โ†’ ((๐ต / 3)โ†‘2) โˆˆ โ„‚)
18140, 180mulcld 11176 . . . . . . 7 (๐œ‘ โ†’ (๐‘‹ ยท ((๐ต / 3)โ†‘2)) โˆˆ โ„‚)
18210, 181mulcld 11176 . . . . . 6 (๐œ‘ โ†’ (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) โˆˆ โ„‚)
183 expcl 13986 . . . . . . 7 (((๐ต / 3) โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ ((๐ต / 3)โ†‘3) โˆˆ โ„‚)
18441, 17, 183sylancl 587 . . . . . 6 (๐œ‘ โ†’ ((๐ต / 3)โ†‘3) โˆˆ โ„‚)
185182, 184addcld 11175 . . . . 5 (๐œ‘ โ†’ ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) โˆˆ โ„‚)
18614, 42mulcld 11176 . . . . . 6 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) โˆˆ โ„‚)
187186, 39addcld 11175 . . . . 5 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27)) โˆˆ โ„‚)
188179, 185, 187addassd 11178 . . . 4 (๐œ‘ โ†’ ((((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + (((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27)))))
18914, 40, 41adddid 11180 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) = ((-(๐‘€ / 3) ยท ๐‘‹) + (-(๐‘€ / 3) ยท (๐ต / 3))))
190189oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27)) = (((-(๐‘€ / 3) ยท ๐‘‹) + (-(๐‘€ / 3) ยท (๐ต / 3))) + (๐‘ / 27)))
19114, 40mulcld 11176 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท ๐‘‹) โˆˆ โ„‚)
19214, 41mulcld 11176 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท (๐ต / 3)) โˆˆ โ„‚)
193191, 192, 39addassd 11178 . . . . . . . . 9 (๐œ‘ โ†’ (((-(๐‘€ / 3) ยท ๐‘‹) + (-(๐‘€ / 3) ยท (๐ต / 3))) + (๐‘ / 27)) = ((-(๐‘€ / 3) ยท ๐‘‹) + ((-(๐‘€ / 3) ยท (๐ต / 3)) + (๐‘ / 27))))
1941oveq1d 7373 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘€ / 3) = (((๐ตโ†‘2) โˆ’ (3 ยท ๐ถ)) / 3))
1953, 7, 10, 12divsubdird 11971 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ตโ†‘2) โˆ’ (3 ยท ๐ถ)) / 3) = (((๐ตโ†‘2) / 3) โˆ’ ((3 ยท ๐ถ) / 3)))
1965, 10, 12divcan3d 11937 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((3 ยท ๐ถ) / 3) = ๐ถ)
197196oveq2d 7374 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ตโ†‘2) / 3) โˆ’ ((3 ยท ๐ถ) / 3)) = (((๐ตโ†‘2) / 3) โˆ’ ๐ถ))
198194, 195, 1973eqtrd 2781 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘€ / 3) = (((๐ตโ†‘2) / 3) โˆ’ ๐ถ))
199198negeqd 11396 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -(๐‘€ / 3) = -(((๐ตโ†‘2) / 3) โˆ’ ๐ถ))
2003, 10, 12divcld 11932 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ตโ†‘2) / 3) โˆˆ โ„‚)
201200, 5negsubdi2d 11529 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -(((๐ตโ†‘2) / 3) โˆ’ ๐ถ) = (๐ถ โˆ’ ((๐ตโ†‘2) / 3)))
202199, 201eqtrd 2777 . . . . . . . . . . . 12 (๐œ‘ โ†’ -(๐‘€ / 3) = (๐ถ โˆ’ ((๐ตโ†‘2) / 3)))
203202oveq1d 7373 . . . . . . . . . . 11 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท ๐‘‹) = ((๐ถ โˆ’ ((๐ตโ†‘2) / 3)) ยท ๐‘‹))
2045, 200, 40subdird 11613 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ถ โˆ’ ((๐ตโ†‘2) / 3)) ยท ๐‘‹) = ((๐ถ ยท ๐‘‹) โˆ’ (((๐ตโ†‘2) / 3) ยท ๐‘‹)))
205200, 40mulcomd 11177 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ตโ†‘2) / 3) ยท ๐‘‹) = (๐‘‹ ยท ((๐ตโ†‘2) / 3)))
2064sqvali 14085 . . . . . . . . . . . . . . . . . 18 (3โ†‘2) = (3 ยท 3)
207206oveq2i 7369 . . . . . . . . . . . . . . . . 17 ((๐ตโ†‘2) / (3โ†‘2)) = ((๐ตโ†‘2) / (3 ยท 3))
2082, 10, 12sqdivd 14065 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ต / 3)โ†‘2) = ((๐ตโ†‘2) / (3โ†‘2)))
2093, 10, 10, 12, 12divdiv1d 11963 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((๐ตโ†‘2) / 3) / 3) = ((๐ตโ†‘2) / (3 ยท 3)))
210207, 208, 2093eqtr4a 2803 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ต / 3)โ†‘2) = (((๐ตโ†‘2) / 3) / 3))
211210oveq2d 7374 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (3 ยท ((๐ต / 3)โ†‘2)) = (3 ยท (((๐ตโ†‘2) / 3) / 3)))
212200, 10, 12divcan2d 11934 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (3 ยท (((๐ตโ†‘2) / 3) / 3)) = ((๐ตโ†‘2) / 3))
213211, 212eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3 ยท ((๐ต / 3)โ†‘2)) = ((๐ตโ†‘2) / 3))
214213oveq2d 7374 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ ยท (3 ยท ((๐ต / 3)โ†‘2))) = (๐‘‹ ยท ((๐ตโ†‘2) / 3)))
21540, 10, 180mul12d 11365 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ ยท (3 ยท ((๐ต / 3)โ†‘2))) = (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))))
216205, 214, 2153eqtr2d 2783 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ตโ†‘2) / 3) ยท ๐‘‹) = (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))))
217216oveq2d 7374 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ถ ยท ๐‘‹) โˆ’ (((๐ตโ†‘2) / 3) ยท ๐‘‹)) = ((๐ถ ยท ๐‘‹) โˆ’ (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2)))))
218203, 204, 2173eqtrd 2781 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท ๐‘‹) = ((๐ถ ยท ๐‘‹) โˆ’ (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2)))))
219202oveq1d 7373 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท (๐ต / 3)) = ((๐ถ โˆ’ ((๐ตโ†‘2) / 3)) ยท (๐ต / 3)))
2205, 200, 41subdird 11613 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ถ โˆ’ ((๐ตโ†‘2) / 3)) ยท (๐ต / 3)) = ((๐ถ ยท (๐ต / 3)) โˆ’ (((๐ตโ†‘2) / 3) ยท (๐ต / 3))))
2215, 2, 10, 12divassd 11967 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ถ ยท ๐ต) / 3) = (๐ถ ยท (๐ต / 3)))
2225, 2mulcomd 11177 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ถ ยท ๐ต) = (๐ต ยท ๐ถ))
223222oveq1d 7373 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ถ ยท ๐ต) / 3) = ((๐ต ยท ๐ถ) / 3))
224221, 223eqtr3d 2779 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ถ ยท (๐ต / 3)) = ((๐ต ยท ๐ถ) / 3))
2253, 10, 2, 10, 12, 12divmuldivd 11973 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ตโ†‘2) / 3) ยท (๐ต / 3)) = (((๐ตโ†‘2) ยท ๐ต) / (3 ยท 3)))
226 df-3 12218 . . . . . . . . . . . . . . . . . 18 3 = (2 + 1)
227226oveq2i 7369 . . . . . . . . . . . . . . . . 17 (๐ตโ†‘3) = (๐ตโ†‘(2 + 1))
228 expp1 13975 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (๐ตโ†‘(2 + 1)) = ((๐ตโ†‘2) ยท ๐ต))
2292, 27, 228sylancl 587 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ตโ†‘(2 + 1)) = ((๐ตโ†‘2) ยท ๐ต))
230227, 229eqtr2id 2790 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ตโ†‘2) ยท ๐ต) = (๐ตโ†‘3))
231153a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (3 ยท 3) = 9)
232230, 231oveq12d 7376 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ตโ†‘2) ยท ๐ต) / (3 ยท 3)) = ((๐ตโ†‘3) / 9))
233225, 232eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ตโ†‘2) / 3) ยท (๐ต / 3)) = ((๐ตโ†‘3) / 9))
234224, 233oveq12d 7376 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ถ ยท (๐ต / 3)) โˆ’ (((๐ตโ†‘2) / 3) ยท (๐ต / 3))) = (((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)))
235219, 220, 2343eqtrd 2781 . . . . . . . . . . . 12 (๐œ‘ โ†’ (-(๐‘€ / 3) ยท (๐ต / 3)) = (((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)))
23615oveq1d 7373 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ / 27) = ((((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) + (27 ยท ๐ท)) / 27))
23726, 33, 36, 38divdird 11970 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) + (27 ยท ๐ท)) / 27) = ((((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) / 27) + ((27 ยท ๐ท) / 27)))
23821, 25, 36, 38divsubdird 11971 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) / 27) = (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((9 ยท (๐ต ยท ๐ถ)) / 27)))
239 9t3e27 12742 . . . . . . . . . . . . . . . . . 18 (9 ยท 3) = 27
240239oveq2i 7369 . . . . . . . . . . . . . . . . 17 ((9 ยท (๐ต ยท ๐ถ)) / (9 ยท 3)) = ((9 ยท (๐ต ยท ๐ถ)) / 27)
24123, 10, 96, 12, 99divcan5d 11958 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((9 ยท (๐ต ยท ๐ถ)) / (9 ยท 3)) = ((๐ต ยท ๐ถ) / 3))
242240, 241eqtr3id 2791 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((9 ยท (๐ต ยท ๐ถ)) / 27) = ((๐ต ยท ๐ถ) / 3))
243242oveq2d 7374 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((9 ยท (๐ต ยท ๐ถ)) / 27)) = (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)))
244238, 243eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) / 27) = (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)))
24531, 36, 38divcan3d 11937 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((27 ยท ๐ท) / 27) = ๐ท)
246244, 245oveq12d 7376 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((2 ยท (๐ตโ†‘3)) โˆ’ (9 ยท (๐ต ยท ๐ถ))) / 27) + ((27 ยท ๐ท) / 27)) = ((((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)) + ๐ท))
247236, 237, 2463eqtrd 2781 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ / 27) = ((((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)) + ๐ท))
248235, 247oveq12d 7376 . . . . . . . . . . 11 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท (๐ต / 3)) + (๐‘ / 27)) = ((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + ((((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)) + ๐ท)))
24919, 96, 99divcld 11932 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ตโ†‘3) / 9) โˆˆ โ„‚)
25021, 36, 38divcld 11932 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 ยท (๐ตโ†‘3)) / 27) โˆˆ โ„‚)
251249, 250negsubdi2d 11529 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ -(((๐ตโ†‘3) / 9) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)) = (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ตโ†‘3) / 9)))
2522, 10, 12, 52expdivd 14066 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ต / 3)โ†‘3) = ((๐ตโ†‘3) / (3โ†‘3)))
25355oveq2i 7369 . . . . . . . . . . . . . . . . 17 ((๐ตโ†‘3) / (3โ†‘3)) = ((๐ตโ†‘3) / 27)
254 ax-1cn 11110 . . . . . . . . . . . . . . . . . . . . . . 23 1 โˆˆ โ„‚
255 2p1e3 12296 . . . . . . . . . . . . . . . . . . . . . . 23 (2 + 1) = 3
2564, 16, 254, 255subaddrii 11491 . . . . . . . . . . . . . . . . . . . . . 22 (3 โˆ’ 2) = 1
257256oveq1i 7368 . . . . . . . . . . . . . . . . . . . . 21 ((3 โˆ’ 2) ยท (๐ตโ†‘3)) = (1 ยท (๐ตโ†‘3))
25819mulid2d 11174 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (1 ยท (๐ตโ†‘3)) = (๐ตโ†‘3))
259257, 258eqtrid 2789 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((3 โˆ’ 2) ยท (๐ตโ†‘3)) = (๐ตโ†‘3))
26010, 60, 19subdird 11613 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((3 โˆ’ 2) ยท (๐ตโ†‘3)) = ((3 ยท (๐ตโ†‘3)) โˆ’ (2 ยท (๐ตโ†‘3))))
261259, 260eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ตโ†‘3) = ((3 ยท (๐ตโ†‘3)) โˆ’ (2 ยท (๐ตโ†‘3))))
262261oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ตโ†‘3) / 27) = (((3 ยท (๐ตโ†‘3)) โˆ’ (2 ยท (๐ตโ†‘3))) / 27))
263 mulcl 11136 . . . . . . . . . . . . . . . . . . . 20 ((3 โˆˆ โ„‚ โˆง (๐ตโ†‘3) โˆˆ โ„‚) โ†’ (3 ยท (๐ตโ†‘3)) โˆˆ โ„‚)
2644, 19, 263sylancr 588 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (3 ยท (๐ตโ†‘3)) โˆˆ โ„‚)
265264, 21, 36, 38divsubdird 11971 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((3 ยท (๐ตโ†‘3)) โˆ’ (2 ยท (๐ตโ†‘3))) / 27) = (((3 ยท (๐ตโ†‘3)) / 27) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)))
266262, 265eqtrd 2777 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ตโ†‘3) / 27) = (((3 ยท (๐ตโ†‘3)) / 27) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)))
267253, 266eqtrid 2789 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ตโ†‘3) / (3โ†‘3)) = (((3 ยท (๐ตโ†‘3)) / 27) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)))
26822, 4, 239mulcomli 11165 . . . . . . . . . . . . . . . . . . 19 (3 ยท 9) = 27
269268oveq2i 7369 . . . . . . . . . . . . . . . . . 18 ((3 ยท (๐ตโ†‘3)) / (3 ยท 9)) = ((3 ยท (๐ตโ†‘3)) / 27)
27019, 96, 10, 99, 12divcan5d 11958 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((3 ยท (๐ตโ†‘3)) / (3 ยท 9)) = ((๐ตโ†‘3) / 9))
271269, 270eqtr3id 2791 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((3 ยท (๐ตโ†‘3)) / 27) = ((๐ตโ†‘3) / 9))
272271oveq1d 7373 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((3 ยท (๐ตโ†‘3)) / 27) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)) = (((๐ตโ†‘3) / 9) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)))
273252, 267, 2723eqtrd 2781 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต / 3)โ†‘3) = (((๐ตโ†‘3) / 9) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)))
274273negeqd 11396 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ -((๐ต / 3)โ†‘3) = -(((๐ตโ†‘3) / 9) โˆ’ ((2 ยท (๐ตโ†‘3)) / 27)))
27523, 10, 12divcld 11932 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต ยท ๐ถ) / 3) โˆˆ โ„‚)
276275, 249, 250npncan3d 11549 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3))) = (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ตโ†‘3) / 9)))
277251, 274, 2763eqtr4d 2787 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -((๐ต / 3)โ†‘3) = ((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3))))
278277oveq1d 7373 . . . . . . . . . . . 12 (๐œ‘ โ†’ (-((๐ต / 3)โ†‘3) + ๐ท) = (((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3))) + ๐ท))
279184negcld 11500 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -((๐ต / 3)โ†‘3) โˆˆ โ„‚)
280279, 31addcomd 11358 . . . . . . . . . . . 12 (๐œ‘ โ†’ (-((๐ต / 3)โ†‘3) + ๐ท) = (๐ท + -((๐ต / 3)โ†‘3)))
281235, 192eqeltrrd 2839 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) โˆˆ โ„‚)
282250, 275subcld 11513 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)) โˆˆ โ„‚)
283281, 282, 31addassd 11178 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + (((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3))) + ๐ท) = ((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + ((((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)) + ๐ท)))
284278, 280, 2833eqtr3d 2785 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ท + -((๐ต / 3)โ†‘3)) = ((((๐ต ยท ๐ถ) / 3) โˆ’ ((๐ตโ†‘3) / 9)) + ((((2 ยท (๐ตโ†‘3)) / 27) โˆ’ ((๐ต ยท ๐ถ) / 3)) + ๐ท)))
28531, 184negsubd 11519 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ท + -((๐ต / 3)โ†‘3)) = (๐ท โˆ’ ((๐ต / 3)โ†‘3)))
286248, 284, 2853eqtr2d 2783 . . . . . . . . . 10 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท (๐ต / 3)) + (๐‘ / 27)) = (๐ท โˆ’ ((๐ต / 3)โ†‘3)))
287218, 286oveq12d 7376 . . . . . . . . 9 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท ๐‘‹) + ((-(๐‘€ / 3) ยท (๐ต / 3)) + (๐‘ / 27))) = (((๐ถ ยท ๐‘‹) โˆ’ (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2)))) + (๐ท โˆ’ ((๐ต / 3)โ†‘3))))
288190, 193, 2873eqtrd 2781 . . . . . . . 8 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27)) = (((๐ถ ยท ๐‘‹) โˆ’ (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2)))) + (๐ท โˆ’ ((๐ต / 3)โ†‘3))))
2895, 40mulcld 11176 . . . . . . . . 9 (๐œ‘ โ†’ (๐ถ ยท ๐‘‹) โˆˆ โ„‚)
290289, 31, 182, 184addsub4d 11560 . . . . . . . 8 (๐œ‘ โ†’ (((๐ถ ยท ๐‘‹) + ๐ท) โˆ’ ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))) = (((๐ถ ยท ๐‘‹) โˆ’ (3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2)))) + (๐ท โˆ’ ((๐ต / 3)โ†‘3))))
291288, 290eqtr4d 2780 . . . . . . 7 (๐œ‘ โ†’ ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27)) = (((๐ถ ยท ๐‘‹) + ๐ท) โˆ’ ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3))))
292291oveq2d 7374 . . . . . 6 (๐œ‘ โ†’ (((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = (((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) + (((๐ถ ยท ๐‘‹) + ๐ท) โˆ’ ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)))))
293289, 31addcld 11175 . . . . . . 7 (๐œ‘ โ†’ ((๐ถ ยท ๐‘‹) + ๐ท) โˆˆ โ„‚)
294185, 293pncan3d 11516 . . . . . 6 (๐œ‘ โ†’ (((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) + (((๐ถ ยท ๐‘‹) + ๐ท) โˆ’ ((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)))) = ((๐ถ ยท ๐‘‹) + ๐ท))
295292, 294eqtrd 2777 . . . . 5 (๐œ‘ โ†’ (((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = ((๐ถ ยท ๐‘‹) + ๐ท))
296295oveq2d 7374 . . . 4 (๐œ‘ โ†’ (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + (((3 ยท (๐‘‹ ยท ((๐ต / 3)โ†‘2))) + ((๐ต / 3)โ†‘3)) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27)))) = (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)))
297175, 188, 2963eqtrd 2781 . . 3 (๐œ‘ โ†’ (((๐‘‹ + (๐ต / 3))โ†‘3) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)))
298297eqeq1d 2739 . 2 (๐œ‘ โ†’ ((((๐‘‹ + (๐ต / 3))โ†‘3) + ((-(๐‘€ / 3) ยท (๐‘‹ + (๐ต / 3))) + (๐‘ / 27))) = 0 โ†” (((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0))
299 oveq1 7365 . . . . . . . 8 (๐‘Ÿ = 0 โ†’ (๐‘Ÿโ†‘3) = (0โ†‘3))
300 0exp 14004 . . . . . . . . 9 (3 โˆˆ โ„• โ†’ (0โ†‘3) = 0)
30146, 300ax-mp 5 . . . . . . . 8 (0โ†‘3) = 0
302299, 301eqtrdi 2793 . . . . . . 7 (๐‘Ÿ = 0 โ†’ (๐‘Ÿโ†‘3) = 0)
303 0ne1 12225 . . . . . . . 8 0 โ‰  1
304303a1i 11 . . . . . . 7 (๐‘Ÿ = 0 โ†’ 0 โ‰  1)
305302, 304eqnetrd 3012 . . . . . 6 (๐‘Ÿ = 0 โ†’ (๐‘Ÿโ†‘3) โ‰  1)
306305necon2i 2979 . . . . 5 ((๐‘Ÿโ†‘3) = 1 โ†’ ๐‘Ÿ โ‰  0)
307 eqcom 2744 . . . . . . . 8 (๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โ†” -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = ๐‘‹)
3082adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐ต โˆˆ โ„‚)
309 simprl 770 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘Ÿ โˆˆ โ„‚)
31043adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘‡ โˆˆ โ„‚)
311309, 310mulcld 11176 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘Ÿ ยท ๐‘‡) โˆˆ โ„‚)
3129adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘€ โˆˆ โ„‚)
313 simprr 772 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘Ÿ โ‰  0)
314160adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘‡ โ‰  0)
315309, 310, 313, 314mulne0d 11808 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘Ÿ ยท ๐‘‡) โ‰  0)
316312, 311, 315divcld 11932 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘€ / (๐‘Ÿ ยท ๐‘‡)) โˆˆ โ„‚)
317311, 316addcld 11175 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) โˆˆ โ„‚)
3184a1i 11 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ 3 โˆˆ โ„‚)
31911a1i 11 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ 3 โ‰  0)
320308, 317, 318, 319divdird 11970 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต + ((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡)))) / 3) = ((๐ต / 3) + (((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
321308, 311, 316addassd 11178 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) = (๐ต + ((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡)))))
322321oveq1d 7373 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = ((๐ต + ((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡)))) / 3))
32341adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐ต / 3) โˆˆ โ„‚)
324317, 318, 319divcld 11932 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆˆ โ„‚)
325323, 324subnegd 11520 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐ต / 3) โˆ’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)) = ((๐ต / 3) + (((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
326320, 322, 3253eqtr4d 2787 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = ((๐ต / 3) โˆ’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
327326negeqd 11396 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = -((๐ต / 3) โˆ’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
328324negcld 11500 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆˆ โ„‚)
329323, 328negsubdi2d 11529 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -((๐ต / 3) โˆ’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)) = (-(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆ’ (๐ต / 3)))
330327, 329eqtrd 2777 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = (-(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆ’ (๐ต / 3)))
331330eqeq1d 2739 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (-(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = ๐‘‹ โ†” (-(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆ’ (๐ต / 3)) = ๐‘‹))
332307, 331bitrid 283 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โ†” (-(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆ’ (๐ต / 3)) = ๐‘‹))
33340adantr 482 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ๐‘‹ โˆˆ โ„‚)
334328, 323, 333subadd2d 11532 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((-(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โˆ’ (๐ต / 3)) = ๐‘‹ โ†” (๐‘‹ + (๐ต / 3)) = -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
335311, 316, 318, 319divdird 11970 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = (((๐‘Ÿ ยท ๐‘‡) / 3) + ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3)))
336335negeqd 11396 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = -(((๐‘Ÿ ยท ๐‘‡) / 3) + ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3)))
337311, 318, 319divcld 11932 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘Ÿ ยท ๐‘‡) / 3) โˆˆ โ„‚)
338316, 318, 319divcld 11932 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3) โˆˆ โ„‚)
339337, 338negdi2d 11527 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -(((๐‘Ÿ ยท ๐‘‡) / 3) + ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3)) = (-((๐‘Ÿ ยท ๐‘‡) / 3) โˆ’ ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3)))
340309, 310, 318, 319divassd 11967 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘Ÿ ยท ๐‘‡) / 3) = (๐‘Ÿ ยท (๐‘‡ / 3)))
341340negeqd 11396 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -((๐‘Ÿ ยท ๐‘‡) / 3) = -(๐‘Ÿ ยท (๐‘‡ / 3)))
34244adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘‡ / 3) โˆˆ โ„‚)
343309, 342mulneg2d 11610 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘Ÿ ยท -(๐‘‡ / 3)) = -(๐‘Ÿ ยท (๐‘‡ / 3)))
344341, 343eqtr4d 2780 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -((๐‘Ÿ ยท ๐‘‡) / 3) = (๐‘Ÿ ยท -(๐‘‡ / 3)))
345312, 311, 318, 315, 319divdiv32d 11957 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3) = ((๐‘€ / 3) / (๐‘Ÿ ยท ๐‘‡)))
34613adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘€ / 3) โˆˆ โ„‚)
347346, 311, 318, 315, 319divcan7d 11960 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐‘€ / 3) / 3) / ((๐‘Ÿ ยท ๐‘‡) / 3)) = ((๐‘€ / 3) / (๐‘Ÿ ยท ๐‘‡)))
348155oveq1d 7373 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐‘€ / 3) / 3) / ((๐‘Ÿ ยท ๐‘‡) / 3)) = ((๐‘€ / 9) / ((๐‘Ÿ ยท ๐‘‡) / 3)))
349348adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (((๐‘€ / 3) / 3) / ((๐‘Ÿ ยท ๐‘‡) / 3)) = ((๐‘€ / 9) / ((๐‘Ÿ ยท ๐‘‡) / 3)))
350345, 347, 3493eqtr2d 2783 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3) = ((๐‘€ / 9) / ((๐‘Ÿ ยท ๐‘‡) / 3)))
351119adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (๐‘€ / 9) โˆˆ โ„‚)
352311, 318, 315, 319divne0d 11948 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘Ÿ ยท ๐‘‡) / 3) โ‰  0)
353351, 337, 352div2negd 11947 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (-(๐‘€ / 9) / -((๐‘Ÿ ยท ๐‘‡) / 3)) = ((๐‘€ / 9) / ((๐‘Ÿ ยท ๐‘‡) / 3)))
354344oveq2d 7374 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (-(๐‘€ / 9) / -((๐‘Ÿ ยท ๐‘‡) / 3)) = (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3))))
355350, 353, 3543eqtr2d 2783 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3) = (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3))))
356344, 355oveq12d 7376 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ (-((๐‘Ÿ ยท ๐‘‡) / 3) โˆ’ ((๐‘€ / (๐‘Ÿ ยท ๐‘‡)) / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3)))))
357336, 339, 3563eqtrd 2781 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3)))))
358357eqeq2d 2748 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘‹ + (๐ต / 3)) = -(((๐‘Ÿ ยท ๐‘‡) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3) โ†” (๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3))))))
359332, 334, 3583bitrrd 306 . . . . . 6 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ โ„‚ โˆง ๐‘Ÿ โ‰  0)) โ†’ ((๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3)))) โ†” ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
360359anassrs 469 . . . . 5 (((๐œ‘ โˆง ๐‘Ÿ โˆˆ โ„‚) โˆง ๐‘Ÿ โ‰  0) โ†’ ((๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3)))) โ†” ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
361306, 360sylan2 594 . . . 4 (((๐œ‘ โˆง ๐‘Ÿ โˆˆ โ„‚) โˆง (๐‘Ÿโ†‘3) = 1) โ†’ ((๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3)))) โ†” ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3)))
362361pm5.32da 580 . . 3 ((๐œ‘ โˆง ๐‘Ÿ โˆˆ โ„‚) โ†’ (((๐‘Ÿโ†‘3) = 1 โˆง (๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3))))) โ†” ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3))))
363362rexbidva 3174 . 2 (๐œ‘ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง (๐‘‹ + (๐ต / 3)) = ((๐‘Ÿ ยท -(๐‘‡ / 3)) โˆ’ (-(๐‘€ / 9) / (๐‘Ÿ ยท -(๐‘‡ / 3))))) โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3))))
364163, 298, 3633bitr3d 309 1 (๐œ‘ โ†’ ((((๐‘‹โ†‘3) + (๐ต ยท (๐‘‹โ†‘2))) + ((๐ถ ยท ๐‘‹) + ๐ท)) = 0 โ†” โˆƒ๐‘Ÿ โˆˆ โ„‚ ((๐‘Ÿโ†‘3) = 1 โˆง ๐‘‹ = -(((๐ต + (๐‘Ÿ ยท ๐‘‡)) + (๐‘€ / (๐‘Ÿ ยท ๐‘‡))) / 3))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074   class class class wbr 5106  (class class class)co 7358  โ„‚cc 11050  0cc0 11052  1c1 11053   + caddc 11055   ยท cmul 11057   โˆ’ cmin 11386  -cneg 11387   / cdiv 11813  โ„•cn 12154  2c2 12209  3c3 12210  4c4 12211  7c7 12214  9c9 12216  โ„•0cn0 12414  cdc 12619  โ†‘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  ax-pre-sup 11130
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-sup 9379  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-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-z 12501  df-dec 12620  df-uz 12765  df-rp 12917  df-seq 13908  df-exp 13969  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-dvds 16138
This theorem is referenced by:  cubic2  26201  quart  26214
  Copyright terms: Public domain W3C validator