Step | Hyp | Ref
| Expression |
1 | | dcubic2.u |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
2 | | 3nn0 12432 |
. . . . . . . . 9
โข 3 โ
โ0 |
3 | | expcl 13986 |
. . . . . . . . 9
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
4 | 1, 2, 3 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (๐โ3) โ โ) |
5 | 4 | sqvald 14049 |
. . . . . . 7
โข (๐ โ ((๐โ3)โ2) = ((๐โ3) ยท (๐โ3))) |
6 | 5 | oveq1d 7373 |
. . . . . 6
โข (๐ โ (((๐โ3)โ2) / (๐โ3)) = (((๐โ3) ยท (๐โ3)) / (๐โ3))) |
7 | | dcubic2.z |
. . . . . . . 8
โข (๐ โ ๐ โ 0) |
8 | | 3z 12537 |
. . . . . . . . 9
โข 3 โ
โค |
9 | 8 | a1i 11 |
. . . . . . . 8
โข (๐ โ 3 โ
โค) |
10 | 1, 7, 9 | expne0d 14058 |
. . . . . . 7
โข (๐ โ (๐โ3) โ 0) |
11 | 4, 4, 10 | divcan4d 11938 |
. . . . . 6
โข (๐ โ (((๐โ3) ยท (๐โ3)) / (๐โ3)) = (๐โ3)) |
12 | 6, 11 | eqtr2d 2778 |
. . . . 5
โข (๐ โ (๐โ3) = (((๐โ3)โ2) / (๐โ3))) |
13 | | dcubic.d |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
14 | | dcubic.m |
. . . . . . . . . . 11
โข (๐ โ ๐ = (๐ / 3)) |
15 | | dcubic.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
16 | | 3cn 12235 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 3 โ
โ) |
18 | | 3ne0 12260 |
. . . . . . . . . . . . 13
โข 3 โ
0 |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 3 โ 0) |
20 | 15, 17, 19 | divcld 11932 |
. . . . . . . . . . 11
โข (๐ โ (๐ / 3) โ โ) |
21 | 14, 20 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
22 | | expcl 13986 |
. . . . . . . . . 10
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
23 | 21, 2, 22 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (๐โ3) โ โ) |
24 | 23, 4, 10 | divcld 11932 |
. . . . . . . 8
โข (๐ โ ((๐โ3) / (๐โ3)) โ โ) |
25 | 13, 24 | negsubd 11519 |
. . . . . . 7
โข (๐ โ (๐ + -((๐โ3) / (๐โ3))) = (๐ โ ((๐โ3) / (๐โ3)))) |
26 | 13, 4, 10 | divcan4d 11938 |
. . . . . . . 8
โข (๐ โ ((๐ ยท (๐โ3)) / (๐โ3)) = ๐) |
27 | 26 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ (((๐ ยท (๐โ3)) / (๐โ3)) โ ((๐โ3) / (๐โ3))) = (๐ โ ((๐โ3) / (๐โ3)))) |
28 | 25, 27 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ (๐ + -((๐โ3) / (๐โ3))) = (((๐ ยท (๐โ3)) / (๐โ3)) โ ((๐โ3) / (๐โ3)))) |
29 | | dcubic.x |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
30 | 15, 29 | mulcld 11176 |
. . . . . . . . 9
โข (๐ โ (๐ ยท ๐) โ โ) |
31 | 30 | negcld 11500 |
. . . . . . . 8
โข (๐ โ -(๐ ยท ๐) โ โ) |
32 | 24 | negcld 11500 |
. . . . . . . 8
โข (๐ โ -((๐โ3) / (๐โ3)) โ โ) |
33 | 31, 32, 30, 13 | add42d 11385 |
. . . . . . 7
โข (๐ โ ((-(๐ ยท ๐) + -((๐โ3) / (๐โ3))) + ((๐ ยท ๐) + ๐)) = ((-(๐ ยท ๐) + (๐ ยท ๐)) + (๐ + -((๐โ3) / (๐โ3))))) |
34 | 15, 29 | mulneg2d 11610 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท -๐) = -(๐ ยท ๐)) |
35 | | dcubic2.2 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ = (๐ โ (๐ / ๐))) |
36 | 35 | negeqd 11396 |
. . . . . . . . . . . . . 14
โข (๐ โ -๐ = -(๐ โ (๐ / ๐))) |
37 | 21, 1, 7 | divcld 11932 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ / ๐) โ โ) |
38 | 1, 37 | negsubdid 11528 |
. . . . . . . . . . . . . 14
โข (๐ โ -(๐ โ (๐ / ๐)) = (-๐ + (๐ / ๐))) |
39 | 36, 38 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ -๐ = (-๐ + (๐ / ๐))) |
40 | 39 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท -๐) = (๐ ยท (-๐ + (๐ / ๐)))) |
41 | 34, 40 | eqtr3d 2779 |
. . . . . . . . . . 11
โข (๐ โ -(๐ ยท ๐) = (๐ ยท (-๐ + (๐ / ๐)))) |
42 | 1 | negcld 11500 |
. . . . . . . . . . . 12
โข (๐ โ -๐ โ โ) |
43 | 15, 42, 37 | adddid 11180 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท (-๐ + (๐ / ๐))) = ((๐ ยท -๐) + (๐ ยท (๐ / ๐)))) |
44 | 15, 1 | mulneg2d 11610 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท -๐) = -(๐ ยท ๐)) |
45 | 44 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ ((๐ ยท -๐) + (๐ ยท (๐ / ๐))) = (-(๐ ยท ๐) + (๐ ยท (๐ / ๐)))) |
46 | 41, 43, 45 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (๐ โ -(๐ ยท ๐) = (-(๐ ยท ๐) + (๐ ยท (๐ / ๐)))) |
47 | 46 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ (-(๐ ยท ๐) + -((๐โ3) / (๐โ3))) = ((-(๐ ยท ๐) + (๐ ยท (๐ / ๐))) + -((๐โ3) / (๐โ3)))) |
48 | 15, 1 | mulcld 11176 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท ๐) โ โ) |
49 | 48 | negcld 11500 |
. . . . . . . . . 10
โข (๐ โ -(๐ ยท ๐) โ โ) |
50 | 15, 37 | mulcld 11176 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท (๐ / ๐)) โ โ) |
51 | 49, 50, 32 | addassd 11178 |
. . . . . . . . 9
โข (๐ โ ((-(๐ ยท ๐) + (๐ ยท (๐ / ๐))) + -((๐โ3) / (๐โ3))) = (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))))) |
52 | 47, 51 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (-(๐ ยท ๐) + -((๐โ3) / (๐โ3))) = (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))))) |
53 | 52 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ ((-(๐ ยท ๐) + -((๐โ3) / (๐โ3))) + ((๐ ยท ๐) + ๐)) = ((-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) + ((๐ ยท ๐) + ๐))) |
54 | 31, 30 | addcomd 11358 |
. . . . . . . . . 10
โข (๐ โ (-(๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + -(๐ ยท ๐))) |
55 | 30 | negidd 11503 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐) + -(๐ ยท ๐)) = 0) |
56 | 54, 55 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ (-(๐ ยท ๐) + (๐ ยท ๐)) = 0) |
57 | 56 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ ((-(๐ ยท ๐) + (๐ ยท ๐)) + (๐ + -((๐โ3) / (๐โ3)))) = (0 + (๐ + -((๐โ3) / (๐โ3))))) |
58 | 13, 32 | addcld 11175 |
. . . . . . . . 9
โข (๐ โ (๐ + -((๐โ3) / (๐โ3))) โ โ) |
59 | 58 | addid2d 11357 |
. . . . . . . 8
โข (๐ โ (0 + (๐ + -((๐โ3) / (๐โ3)))) = (๐ + -((๐โ3) / (๐โ3)))) |
60 | 57, 59 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ ((-(๐ ยท ๐) + (๐ ยท ๐)) + (๐ + -((๐โ3) / (๐โ3)))) = (๐ + -((๐โ3) / (๐โ3)))) |
61 | 33, 53, 60 | 3eqtr3d 2785 |
. . . . . 6
โข (๐ โ ((-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) + ((๐ ยท ๐) + ๐)) = (๐ + -((๐โ3) / (๐โ3)))) |
62 | 13, 4 | mulcld 11176 |
. . . . . . 7
โข (๐ โ (๐ ยท (๐โ3)) โ โ) |
63 | 62, 23, 4, 10 | divsubdird 11971 |
. . . . . 6
โข (๐ โ (((๐ ยท (๐โ3)) โ (๐โ3)) / (๐โ3)) = (((๐ ยท (๐โ3)) / (๐โ3)) โ ((๐โ3) / (๐โ3)))) |
64 | 28, 61, 63 | 3eqtr4d 2787 |
. . . . 5
โข (๐ โ ((-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) + ((๐ ยท ๐) + ๐)) = (((๐ ยท (๐โ3)) โ (๐โ3)) / (๐โ3))) |
65 | 12, 64 | oveq12d 7376 |
. . . 4
โข (๐ โ ((๐โ3) + ((-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) + ((๐ ยท ๐) + ๐))) = ((((๐โ3)โ2) / (๐โ3)) + (((๐ ยท (๐โ3)) โ (๐โ3)) / (๐โ3)))) |
66 | 1, 37 | negsubd 11519 |
. . . . . . . . . 10
โข (๐ โ (๐ + -(๐ / ๐)) = (๐ โ (๐ / ๐))) |
67 | 35, 66 | eqtr4d 2780 |
. . . . . . . . 9
โข (๐ โ ๐ = (๐ + -(๐ / ๐))) |
68 | 67 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ (๐โ3) = ((๐ + -(๐ / ๐))โ3)) |
69 | 37 | negcld 11500 |
. . . . . . . . 9
โข (๐ โ -(๐ / ๐) โ โ) |
70 | | binom3 14128 |
. . . . . . . . 9
โข ((๐ โ โ โง -(๐ / ๐) โ โ) โ ((๐ + -(๐ / ๐))โ3) = (((๐โ3) + (3 ยท ((๐โ2) ยท -(๐ / ๐)))) + ((3 ยท (๐ ยท (-(๐ / ๐)โ2))) + (-(๐ / ๐)โ3)))) |
71 | 1, 69, 70 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((๐ + -(๐ / ๐))โ3) = (((๐โ3) + (3 ยท ((๐โ2) ยท -(๐ / ๐)))) + ((3 ยท (๐ ยท (-(๐ / ๐)โ2))) + (-(๐ / ๐)โ3)))) |
72 | 1 | sqcld 14050 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ2) โ โ) |
73 | 72, 37 | mulneg2d 11610 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐โ2) ยท -(๐ / ๐)) = -((๐โ2) ยท (๐ / ๐))) |
74 | 72, 21, 1, 7 | div12d 11968 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐โ2) ยท (๐ / ๐)) = (๐ ยท ((๐โ2) / ๐))) |
75 | 1 | sqvald 14049 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
76 | 75 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐โ2) / ๐) = ((๐ ยท ๐) / ๐)) |
77 | 1, 1, 7 | divcan4d 11938 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ ยท ๐) / ๐) = ๐) |
78 | 76, 77 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐โ2) / ๐) = ๐) |
79 | 78 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ ยท ((๐โ2) / ๐)) = (๐ ยท ๐)) |
80 | 74, 79 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐โ2) ยท (๐ / ๐)) = (๐ ยท ๐)) |
81 | 80 | negeqd 11396 |
. . . . . . . . . . . . 13
โข (๐ โ -((๐โ2) ยท (๐ / ๐)) = -(๐ ยท ๐)) |
82 | 73, 81 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) ยท -(๐ / ๐)) = -(๐ ยท ๐)) |
83 | 82 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ (3 ยท ((๐โ2) ยท -(๐ / ๐))) = (3 ยท -(๐ ยท ๐))) |
84 | 21, 1 | mulcld 11176 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท ๐) โ โ) |
85 | 17, 84 | mulneg2d 11610 |
. . . . . . . . . . 11
โข (๐ โ (3 ยท -(๐ ยท ๐)) = -(3 ยท (๐ ยท ๐))) |
86 | 17, 21, 1 | mulassd 11179 |
. . . . . . . . . . . . 13
โข (๐ โ ((3 ยท ๐) ยท ๐) = (3 ยท (๐ ยท ๐))) |
87 | 14 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ (3 ยท ๐) = (3 ยท (๐ / 3))) |
88 | 15, 17, 19 | divcan2d 11934 |
. . . . . . . . . . . . . . 15
โข (๐ โ (3 ยท (๐ / 3)) = ๐) |
89 | 87, 88 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (3 ยท ๐) = ๐) |
90 | 89 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ ((3 ยท ๐) ยท ๐) = (๐ ยท ๐)) |
91 | 86, 90 | eqtr3d 2779 |
. . . . . . . . . . . 12
โข (๐ โ (3 ยท (๐ ยท ๐)) = (๐ ยท ๐)) |
92 | 91 | negeqd 11396 |
. . . . . . . . . . 11
โข (๐ โ -(3 ยท (๐ ยท ๐)) = -(๐ ยท ๐)) |
93 | 83, 85, 92 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (๐ โ (3 ยท ((๐โ2) ยท -(๐ / ๐))) = -(๐ ยท ๐)) |
94 | 93 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ ((๐โ3) + (3 ยท ((๐โ2) ยท -(๐ / ๐)))) = ((๐โ3) + -(๐ ยท ๐))) |
95 | | sqneg 14022 |
. . . . . . . . . . . . . . . 16
โข ((๐ / ๐) โ โ โ (-(๐ / ๐)โ2) = ((๐ / ๐)โ2)) |
96 | 37, 95 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (-(๐ / ๐)โ2) = ((๐ / ๐)โ2)) |
97 | 37 | sqvald 14049 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ / ๐)โ2) = ((๐ / ๐) ยท (๐ / ๐))) |
98 | 96, 97 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (-(๐ / ๐)โ2) = ((๐ / ๐) ยท (๐ / ๐))) |
99 | 98 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท (-(๐ / ๐)โ2)) = (๐ ยท ((๐ / ๐) ยท (๐ / ๐)))) |
100 | 1, 37, 37 | mulassd 11179 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ ยท (๐ / ๐)) ยท (๐ / ๐)) = (๐ ยท ((๐ / ๐) ยท (๐ / ๐)))) |
101 | 21, 1, 7 | divcan2d 11934 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท (๐ / ๐)) = ๐) |
102 | 101 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ ยท (๐ / ๐)) ยท (๐ / ๐)) = (๐ ยท (๐ / ๐))) |
103 | 99, 100, 102 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท (-(๐ / ๐)โ2)) = (๐ ยท (๐ / ๐))) |
104 | 103 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ (3 ยท (๐ ยท (-(๐ / ๐)โ2))) = (3 ยท (๐ ยท (๐ / ๐)))) |
105 | 17, 21, 37 | mulassd 11179 |
. . . . . . . . . . 11
โข (๐ โ ((3 ยท ๐) ยท (๐ / ๐)) = (3 ยท (๐ ยท (๐ / ๐)))) |
106 | 89 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ ((3 ยท ๐) ยท (๐ / ๐)) = (๐ ยท (๐ / ๐))) |
107 | 104, 105,
106 | 3eqtr2d 2783 |
. . . . . . . . . 10
โข (๐ โ (3 ยท (๐ ยท (-(๐ / ๐)โ2))) = (๐ ยท (๐ / ๐))) |
108 | | 3nn 12233 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
109 | 108 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 3 โ
โ) |
110 | | n2dvds3 16254 |
. . . . . . . . . . . . 13
โข ยฌ 2
โฅ 3 |
111 | 110 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ ยฌ 2 โฅ
3) |
112 | | oexpneg 16228 |
. . . . . . . . . . . 12
โข (((๐ / ๐) โ โ โง 3 โ โ
โง ยฌ 2 โฅ 3) โ (-(๐ / ๐)โ3) = -((๐ / ๐)โ3)) |
113 | 37, 109, 111, 112 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ (-(๐ / ๐)โ3) = -((๐ / ๐)โ3)) |
114 | 2 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 3 โ
โ0) |
115 | 21, 1, 7, 114 | expdivd 14066 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ / ๐)โ3) = ((๐โ3) / (๐โ3))) |
116 | 115 | negeqd 11396 |
. . . . . . . . . . 11
โข (๐ โ -((๐ / ๐)โ3) = -((๐โ3) / (๐โ3))) |
117 | 113, 116 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (-(๐ / ๐)โ3) = -((๐โ3) / (๐โ3))) |
118 | 107, 117 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ โ ((3 ยท (๐ ยท (-(๐ / ๐)โ2))) + (-(๐ / ๐)โ3)) = ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) |
119 | 94, 118 | oveq12d 7376 |
. . . . . . . 8
โข (๐ โ (((๐โ3) + (3 ยท ((๐โ2) ยท -(๐ / ๐)))) + ((3 ยท (๐ ยท (-(๐ / ๐)โ2))) + (-(๐ / ๐)โ3))) = (((๐โ3) + -(๐ ยท ๐)) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))))) |
120 | 68, 71, 119 | 3eqtrd 2781 |
. . . . . . 7
โข (๐ โ (๐โ3) = (((๐โ3) + -(๐ ยท ๐)) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))))) |
121 | 50, 32 | addcld 11175 |
. . . . . . . 8
โข (๐ โ ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))) โ โ) |
122 | 4, 49, 121 | addassd 11178 |
. . . . . . 7
โข (๐ โ (((๐โ3) + -(๐ ยท ๐)) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) = ((๐โ3) + (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))))) |
123 | 120, 122 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (๐โ3) = ((๐โ3) + (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))))) |
124 | 123 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = (((๐โ3) + (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))))) + ((๐ ยท ๐) + ๐))) |
125 | 49, 121 | addcld 11175 |
. . . . . 6
โข (๐ โ (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) โ โ) |
126 | 30, 13 | addcld 11175 |
. . . . . 6
โข (๐ โ ((๐ ยท ๐) + ๐) โ โ) |
127 | 4, 125, 126 | addassd 11178 |
. . . . 5
โข (๐ โ (((๐โ3) + (-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3))))) + ((๐ ยท ๐) + ๐)) = ((๐โ3) + ((-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) + ((๐ ยท ๐) + ๐)))) |
128 | 124, 127 | eqtrd 2777 |
. . . 4
โข (๐ โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = ((๐โ3) + ((-(๐ ยท ๐) + ((๐ ยท (๐ / ๐)) + -((๐โ3) / (๐โ3)))) + ((๐ ยท ๐) + ๐)))) |
129 | 4 | sqcld 14050 |
. . . . 5
โข (๐ โ ((๐โ3)โ2) โ
โ) |
130 | 62, 23 | subcld 11513 |
. . . . 5
โข (๐ โ ((๐ ยท (๐โ3)) โ (๐โ3)) โ โ) |
131 | 129, 130,
4, 10 | divdird 11970 |
. . . 4
โข (๐ โ ((((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) / (๐โ3)) = ((((๐โ3)โ2) / (๐โ3)) + (((๐ ยท (๐โ3)) โ (๐โ3)) / (๐โ3)))) |
132 | 65, 128, 131 | 3eqtr4d 2787 |
. . 3
โข (๐ โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = ((((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) / (๐โ3))) |
133 | 132 | eqeq1d 2739 |
. 2
โข (๐ โ (((๐โ3) + ((๐ ยท ๐) + ๐)) = 0 โ ((((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) / (๐โ3)) = 0)) |
134 | 129, 130 | addcld 11175 |
. . 3
โข (๐ โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) โ โ) |
135 | 134, 4, 10 | diveq0ad 11942 |
. 2
โข (๐ โ (((((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) / (๐โ3)) = 0 โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = 0)) |
136 | 133, 135 | bitrd 279 |
1
โข (๐ โ (((๐โ3) + ((๐ ยท ๐) + ๐)) = 0 โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = 0)) |