Step | Hyp | Ref
| Expression |
1 | | dcubic.0 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
2 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ ๐ โ 0) |
3 | | dcubic.t |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
4 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ ๐ โ โ) |
5 | | 3z 12543 |
. . . . . . . . . 10
โข 3 โ
โค |
6 | | expne0i 14007 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ 0 โง 3 โ โค)
โ (๐โ3) โ
0) |
7 | 5, 6 | mp3an3 1451 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ 0) โ (๐โ3) โ
0) |
8 | 7 | ex 414 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 0 โ (๐โ3) โ
0)) |
9 | 4, 8 | syl 17 |
. . . . . . 7
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ (๐ โ 0 โ (๐โ3) โ 0)) |
10 | | dcubic.3 |
. . . . . . . . . . 11
โข (๐ โ (๐โ3) = (๐บ โ ๐)) |
11 | 10 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ3) = (๐บ โ ๐)) |
12 | | dcubic.g |
. . . . . . . . . . . . . 14
โข (๐ โ ๐บ โ โ) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐บ โ
โ) |
14 | | dcubic.2 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐บโ2) = ((๐โ2) + (๐โ3))) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐บโ2) = ((๐โ2) + (๐โ3))) |
16 | | dcubic.n |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ = (๐ / 2)) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ = (๐ / 2)) |
18 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ = 0) |
19 | 18 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐ ยท ๐) = (๐ ยท 0)) |
20 | | dcubic.c |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ๐ โ โ) |
21 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ โ
โ) |
22 | 21 | mul01d 11361 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐ ยท 0) =
0) |
23 | 19, 22 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐ ยท ๐) = 0) |
24 | 23 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐ ยท ๐) + ๐) = (0 + ๐)) |
25 | 18 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ3) =
(0โ3)) |
26 | | 3nn 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 3 โ
โ |
27 | | 0exp 14010 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (3 โ
โ โ (0โ3) = 0) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(0โ3) = 0 |
29 | 25, 28 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ3) = 0) |
30 | 29 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = (0 + ((๐ ยท ๐) + ๐))) |
31 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) |
32 | | 0cnd 11155 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ 0 โ
โ) |
33 | 23, 32 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐ ยท ๐) โ โ) |
34 | | dcubic.d |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ๐ โ โ) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ โ
โ) |
36 | 33, 35 | addcld 11181 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐ ยท ๐) + ๐) โ โ) |
37 | 36 | addid2d 11363 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (0 + ((๐ ยท ๐) + ๐)) = ((๐ ยท ๐) + ๐)) |
38 | 30, 31, 37 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐ ยท ๐) + ๐) = 0) |
39 | 35 | addid2d 11363 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (0 + ๐) = ๐) |
40 | 24, 38, 39 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ = 0) |
41 | 40 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐ / 2) = (0 /
2)) |
42 | | 2cn 12235 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
โ |
43 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
0 |
44 | 42, 43 | div0i 11896 |
. . . . . . . . . . . . . . . . . . 19
โข (0 / 2) =
0 |
45 | 41, 44 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐ / 2) = 0) |
46 | 17, 45 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ = 0) |
47 | 46 | sq0id 14105 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ2) = 0) |
48 | | dcubic.m |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ = (๐ / 3)) |
49 | | 3cn 12241 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 3 โ
โ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 3 โ
โ) |
51 | | 3ne0 12266 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 3 โ
0 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 3 โ 0) |
53 | 20, 50, 52 | divcld 11938 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ / 3) โ โ) |
54 | 48, 53 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ โ โ) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ โ
โ) |
56 | | 4cn 12245 |
. . . . . . . . . . . . . . . . . . . 20
โข 4 โ
โ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ 4 โ
โ) |
58 | | 4ne0 12268 |
. . . . . . . . . . . . . . . . . . . 20
โข 4 โ
0 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ 4 โ
0) |
60 | 18 | sq0id 14105 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ2) = 0) |
61 | 60 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ2) + (4 ยท ๐)) = (0 + (4 ยท ๐))) |
62 | | dcubic.x |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ๐ โ โ) |
63 | 62 | sqcld 14056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐โ2) โ โ) |
64 | | mulcl 11142 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((4
โ โ โง ๐
โ โ) โ (4 ยท ๐) โ โ) |
65 | 56, 54, 64 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (4 ยท ๐) โ
โ) |
66 | 63, 65 | addcld 11181 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((๐โ2) + (4 ยท ๐)) โ โ) |
67 | 66 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ2) + (4 ยท ๐)) โ
โ) |
68 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ
(โโ((๐โ2)
+ (4 ยท ๐))) =
0) |
69 | 67, 68 | sqr00d 15333 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ2) + (4 ยท ๐)) = 0) |
70 | 65 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (4 ยท
๐) โ
โ) |
71 | 70 | addid2d 11363 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (0 + (4
ยท ๐)) = (4 ยท
๐)) |
72 | 61, 69, 71 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (4 ยท
๐) = 0) |
73 | 56 | mul01i 11352 |
. . . . . . . . . . . . . . . . . . . 20
โข (4
ยท 0) = 0 |
74 | 72, 73 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (4 ยท
๐) = (4 ยท
0)) |
75 | 55, 32, 57, 59, 74 | mulcanad 11797 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐ = 0) |
76 | 75 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ3) =
(0โ3)) |
77 | 76, 28 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ3) = 0) |
78 | 47, 77 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ2) + (๐โ3)) = (0 + 0)) |
79 | | 00id 11337 |
. . . . . . . . . . . . . . 15
โข (0 + 0) =
0 |
80 | 78, 79 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ((๐โ2) + (๐โ3)) = 0) |
81 | 15, 80 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐บโ2) = 0) |
82 | 13, 81 | sqeq0d 14057 |
. . . . . . . . . . . 12
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ ๐บ = 0) |
83 | 82, 46 | oveq12d 7380 |
. . . . . . . . . . 11
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐บ โ ๐) = (0 โ 0)) |
84 | | 0m0e0 12280 |
. . . . . . . . . . 11
โข (0
โ 0) = 0 |
85 | 83, 84 | eqtrdi 2793 |
. . . . . . . . . 10
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐บ โ ๐) = 0) |
86 | 11, 85 | eqtrd 2777 |
. . . . . . . . 9
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ (๐โ3) = 0) |
87 | 86 | ex 414 |
. . . . . . . 8
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ ((๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0) โ (๐โ3) = 0)) |
88 | 87 | necon3ad 2957 |
. . . . . . 7
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ ((๐โ3) โ 0 โ ยฌ (๐ = 0 โง
(โโ((๐โ2)
+ (4 ยท ๐))) =
0))) |
89 | 9, 88 | syld 47 |
. . . . . 6
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ (๐ โ 0 โ ยฌ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0))) |
90 | 2, 89 | mpd 15 |
. . . . 5
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ ยฌ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) |
91 | | oveq12 7371 |
. . . . . . . . . . 11
โข ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0) โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = (0 + 0)) |
92 | 91, 79 | eqtrdi 2793 |
. . . . . . . . . 10
โข ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0) โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0) |
93 | | oveq12 7371 |
. . . . . . . . . . 11
โข ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0) โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = (0 โ
0)) |
94 | 93, 84 | eqtrdi 2793 |
. . . . . . . . . 10
โข ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0) โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0) |
95 | 92, 94 | jca 513 |
. . . . . . . . 9
โข ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0) โ ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0 โง (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0)) |
96 | 66 | sqrtcld 15329 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((๐โ2) + (4 ยท ๐))) โ
โ) |
97 | | halfaddsub 12393 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง
(โโ((๐โ2)
+ (4 ยท ๐))) โ
โ) โ ((((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2) +
((๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)) =
๐ โง (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) =
(โโ((๐โ2)
+ (4 ยท ๐))))) |
98 | 62, 96, 97 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = ๐ โง (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = (โโ((๐โ2) + (4 ยท ๐))))) |
99 | 98 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = ๐) |
100 | 99 | eqeq1d 2739 |
. . . . . . . . . 10
โข (๐ โ ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0 โ ๐ = 0)) |
101 | 98 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = (โโ((๐โ2) + (4 ยท ๐)))) |
102 | 101 | eqeq1d 2739 |
. . . . . . . . . 10
โข (๐ โ ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0 โ (โโ((๐โ2) + (4 ยท ๐))) = 0)) |
103 | 100, 102 | anbi12d 632 |
. . . . . . . . 9
โข (๐ โ (((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) + ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0 โง (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) = 0) โ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0))) |
104 | 95, 103 | imbitrid 243 |
. . . . . . . 8
โข (๐ โ ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0) โ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0))) |
105 | 104 | con3d 152 |
. . . . . . 7
โข (๐ โ (ยฌ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0) โ ยฌ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) =
0))) |
106 | | eldifi 4091 |
. . . . . . . . . . . . . 14
โข (๐ข โ (โ โ {0})
โ ๐ข โ
โ) |
107 | 106 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ๐ข โ
โ) |
108 | 54 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ ๐ โ
โ) |
109 | | eldifsni 4755 |
. . . . . . . . . . . . . . 15
โข (๐ข โ (โ โ {0})
โ ๐ข โ
0) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ ๐ข โ 0) |
111 | 108, 107,
110 | divcld 11938 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ / ๐ข) โ โ) |
112 | 62 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ๐ โ
โ) |
113 | 107, 111,
112 | subaddd 11537 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ข โ (๐ / ๐ข)) = ๐ โ ((๐ / ๐ข) + ๐) = ๐ข)) |
114 | | eqcom 2744 |
. . . . . . . . . . . 12
โข (๐ = (๐ข โ (๐ / ๐ข)) โ (๐ข โ (๐ / ๐ข)) = ๐) |
115 | | eqcom 2744 |
. . . . . . . . . . . 12
โข (๐ข = ((๐ / ๐ข) + ๐) โ ((๐ / ๐ข) + ๐) = ๐ข) |
116 | 113, 114,
115 | 3bitr4g 314 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ = (๐ข โ (๐ / ๐ข)) โ ๐ข = ((๐ / ๐ข) + ๐))) |
117 | 107 | sqcld 14056 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ขโ2) โ
โ) |
118 | 112, 107 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ ยท ๐ข) โ โ) |
119 | 118, 108 | addcld 11181 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ ยท ๐ข) + ๐) โ โ) |
120 | 117, 119 | subeq0ad 11529 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(((๐ขโ2) โ
((๐ ยท ๐ข) + ๐)) = 0 โ (๐ขโ2) = ((๐ ยท ๐ข) + ๐))) |
121 | 107 | sqvald 14055 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ขโ2) = (๐ข ยท ๐ข)) |
122 | 111, 112,
107 | adddird 11187 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(((๐ / ๐ข) + ๐) ยท ๐ข) = (((๐ / ๐ข) ยท ๐ข) + (๐ ยท ๐ข))) |
123 | 108, 107,
110 | divcan1d 11939 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ / ๐ข) ยท ๐ข) = ๐) |
124 | 123 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(((๐ / ๐ข) ยท ๐ข) + (๐ ยท ๐ข)) = (๐ + (๐ ยท ๐ข))) |
125 | 108, 118 | addcomd 11364 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ + (๐ ยท ๐ข)) = ((๐ ยท ๐ข) + ๐)) |
126 | 122, 124,
125 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ ยท ๐ข) + ๐) = (((๐ / ๐ข) + ๐) ยท ๐ข)) |
127 | 121, 126 | eqeq12d 2753 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ขโ2) = ((๐ ยท ๐ข) + ๐) โ (๐ข ยท ๐ข) = (((๐ / ๐ข) + ๐) ยท ๐ข))) |
128 | 111, 112 | addcld 11181 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ / ๐ข) + ๐) โ โ) |
129 | 107, 128,
107, 110 | mulcan2d 11796 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ข ยท ๐ข) = (((๐ / ๐ข) + ๐) ยท ๐ข) โ ๐ข = ((๐ / ๐ข) + ๐))) |
130 | 120, 127,
129 | 3bitrd 305 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(((๐ขโ2) โ
((๐ ยท ๐ข) + ๐)) = 0 โ ๐ข = ((๐ / ๐ข) + ๐))) |
131 | | 1cnd 11157 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ 1
โ โ) |
132 | | ax-1ne0 11127 |
. . . . . . . . . . . . . 14
โข 1 โ
0 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ 1 โ
0) |
134 | 62 | negcld 11506 |
. . . . . . . . . . . . . 14
โข (๐ โ -๐ โ โ) |
135 | 134 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ -๐ โ
โ) |
136 | 54 | negcld 11506 |
. . . . . . . . . . . . . 14
โข (๐ โ -๐ โ โ) |
137 | 136 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ -๐ โ
โ) |
138 | | sqneg 14028 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (-๐โ2) = (๐โ2)) |
139 | 112, 138 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ (-๐โ2) = (๐โ2)) |
140 | 137 | mulid2d 11180 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ข โ (โ โ {0})) โ (1
ยท -๐) = -๐) |
141 | 140 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ข โ (โ โ {0})) โ (4
ยท (1 ยท -๐)) =
(4 ยท -๐)) |
142 | | mulneg2 11599 |
. . . . . . . . . . . . . . . . 17
โข ((4
โ โ โง ๐
โ โ) โ (4 ยท -๐) = -(4 ยท ๐)) |
143 | 56, 108, 142 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ข โ (โ โ {0})) โ (4
ยท -๐) = -(4 ยท
๐)) |
144 | 141, 143 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ (4
ยท (1 ยท -๐)) =
-(4 ยท ๐)) |
145 | 139, 144 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ
((-๐โ2) โ (4
ยท (1 ยท -๐)))
= ((๐โ2) โ -(4
ยท ๐))) |
146 | 63 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐โ2) โ
โ) |
147 | 65 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ (4
ยท ๐) โ
โ) |
148 | 146, 147 | subnegd 11526 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐โ2) โ -(4 ยท
๐)) = ((๐โ2) + (4 ยท ๐))) |
149 | 145, 148 | eqtr2d 2778 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐โ2) + (4 ยท ๐)) = ((-๐โ2) โ (4 ยท (1 ยท
-๐)))) |
150 | 131, 133,
135, 137, 107, 149 | quad 26206 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ (((1
ยท (๐ขโ2)) +
((-๐ ยท ๐ข) + -๐)) = 0 โ (๐ข = ((--๐ + (โโ((๐โ2) + (4 ยท ๐)))) / (2 ยท 1)) โจ ๐ข = ((--๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / (2 ยท 1))))) |
151 | 117 | mulid2d 11180 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ (1
ยท (๐ขโ2)) =
(๐ขโ2)) |
152 | 112, 107 | mulneg1d 11615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ข โ (โ โ {0})) โ (-๐ ยท ๐ข) = -(๐ ยท ๐ข)) |
153 | 152 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ข โ (โ โ {0})) โ
((-๐ ยท ๐ข) + -๐) = (-(๐ ยท ๐ข) + -๐)) |
154 | 118, 108 | negdid 11532 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ข โ (โ โ {0})) โ
-((๐ ยท ๐ข) + ๐) = (-(๐ ยท ๐ข) + -๐)) |
155 | 153, 154 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ
((-๐ ยท ๐ข) + -๐) = -((๐ ยท ๐ข) + ๐)) |
156 | 151, 155 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((1
ยท (๐ขโ2)) +
((-๐ ยท ๐ข) + -๐)) = ((๐ขโ2) + -((๐ ยท ๐ข) + ๐))) |
157 | 117, 119 | negsubd 11525 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ขโ2) + -((๐ ยท ๐ข) + ๐)) = ((๐ขโ2) โ ((๐ ยท ๐ข) + ๐))) |
158 | 156, 157 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((1
ยท (๐ขโ2)) +
((-๐ ยท ๐ข) + -๐)) = ((๐ขโ2) โ ((๐ ยท ๐ข) + ๐))) |
159 | 158 | eqeq1d 2739 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ (((1
ยท (๐ขโ2)) +
((-๐ ยท ๐ข) + -๐)) = 0 โ ((๐ขโ2) โ ((๐ ยท ๐ข) + ๐)) = 0)) |
160 | 112 | negnegd 11510 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ข โ (โ โ {0})) โ --๐ = ๐) |
161 | 160 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(--๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) =
(๐ + (โโ((๐โ2) + (4 ยท ๐))))) |
162 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . 16
โข (2
ยท 1) = 2 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ (2
ยท 1) = 2) |
164 | 161, 163 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ
((--๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / (2
ยท 1)) = ((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) /
2)) |
165 | 164 | eqeq2d 2748 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ข = ((--๐ + (โโ((๐โ2) + (4 ยท ๐)))) / (2 ยท 1)) โ ๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2))) |
166 | 160 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(--๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) =
(๐ โ
(โโ((๐โ2)
+ (4 ยท ๐))))) |
167 | 166, 163 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ข โ (โ โ {0})) โ
((--๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) / (2
ยท 1)) = ((๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) /
2)) |
168 | 167 | eqeq2d 2748 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ข = ((--๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / (2 ยท 1)) โ ๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2))) |
169 | 165, 168 | orbi12d 918 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (โ โ {0})) โ ((๐ข = ((--๐ + (โโ((๐โ2) + (4 ยท ๐)))) / (2 ยท 1)) โจ ๐ข = ((--๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / (2 ยท 1))) โ (๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ ๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)))) |
170 | 150, 159,
169 | 3bitr3d 309 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (โ โ {0})) โ
(((๐ขโ2) โ
((๐ ยท ๐ข) + ๐)) = 0 โ (๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ ๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)))) |
171 | 116, 130,
170 | 3bitr2d 307 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ (โ โ {0})) โ (๐ = (๐ข โ (๐ / ๐ข)) โ (๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ ๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)))) |
172 | 171 | rexbidva 3174 |
. . . . . . . . 9
โข (๐ โ (โ๐ข โ (โ โ {0})๐ = (๐ข โ (๐ / ๐ข)) โ โ๐ข โ (โ โ {0})(๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ ๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)))) |
173 | | r19.43 3126 |
. . . . . . . . 9
โข
(โ๐ข โ
(โ โ {0})(๐ข =
((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โจ ๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) โ (โ๐ข โ (โ โ
{0})๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ โ๐ข โ (โ โ {0})๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2))) |
174 | 172, 173 | bitrdi 287 |
. . . . . . . 8
โข (๐ โ (โ๐ข โ (โ โ {0})๐ = (๐ข โ (๐ / ๐ข)) โ (โ๐ข โ (โ โ {0})๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ โ๐ข โ (โ โ {0})๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)))) |
175 | | risset 3224 |
. . . . . . . . . . 11
โข (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ (โ
โ {0}) โ โ๐ข โ (โ โ {0})๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2)) |
176 | 62, 96 | addcld 11181 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ + (โโ((๐โ2) + (4 ยท ๐)))) โ โ) |
177 | 176 | halfcld 12405 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ โ) |
178 | | eldifsn 4752 |
. . . . . . . . . . . . 13
โข (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ (โ
โ {0}) โ (((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โ โ โง ((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โ 0)) |
179 | 178 | baib 537 |
. . . . . . . . . . . 12
โข (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ โ โ
(((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โ (โ โ {0}) โ ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0)) |
180 | 177, 179 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ (โ โ {0})
โ ((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โ 0)) |
181 | 175, 180 | bitr3id 285 |
. . . . . . . . . 10
โข (๐ โ (โ๐ข โ (โ โ {0})๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0)) |
182 | | risset 3224 |
. . . . . . . . . . 11
โข (((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ (โ
โ {0}) โ โ๐ข โ (โ โ {0})๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) |
183 | 62, 96 | subcld 11519 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ (โโ((๐โ2) + (4 ยท ๐)))) โ โ) |
184 | 183 | halfcld 12405 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ โ) |
185 | | eldifsn 4752 |
. . . . . . . . . . . . 13
โข (((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ (โ
โ {0}) โ (((๐
โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ โ โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ
0)) |
186 | 185 | baib 537 |
. . . . . . . . . . . 12
โข (((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ โ โ
(((๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โ (โ โ {0}) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0)) |
187 | 184, 186 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ (โ โ {0})
โ ((๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2)
โ 0)) |
188 | 182, 187 | bitr3id 285 |
. . . . . . . . . 10
โข (๐ โ (โ๐ข โ (โ โ {0})๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0)) |
189 | 181, 188 | orbi12d 918 |
. . . . . . . . 9
โข (๐ โ ((โ๐ข โ (โ โ
{0})๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ โ๐ข โ (โ โ {0})๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) โ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0 โจ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0))) |
190 | | neorian 3040 |
. . . . . . . . 9
โข ((((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0 โจ ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) โ 0) โ ยฌ
(((๐ +
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2) =
0 โง ((๐ โ
(โโ((๐โ2)
+ (4 ยท ๐)))) / 2) =
0)) |
191 | 189, 190 | bitrdi 287 |
. . . . . . . 8
โข (๐ โ ((โ๐ข โ (โ โ
{0})๐ข = ((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) โจ โ๐ข โ (โ โ {0})๐ข = ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2)) โ ยฌ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0))) |
192 | 174, 191 | bitrd 279 |
. . . . . . 7
โข (๐ โ (โ๐ข โ (โ โ {0})๐ = (๐ข โ (๐ / ๐ข)) โ ยฌ (((๐ + (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0 โง ((๐ โ (โโ((๐โ2) + (4 ยท ๐)))) / 2) = 0))) |
193 | 105, 192 | sylibrd 259 |
. . . . . 6
โข (๐ โ (ยฌ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0) โ โ๐ข โ (โ โ
{0})๐ = (๐ข โ (๐ / ๐ข)))) |
194 | 193 | imp 408 |
. . . . 5
โข ((๐ โง ยฌ (๐ = 0 โง (โโ((๐โ2) + (4 ยท ๐))) = 0)) โ โ๐ข โ (โ โ
{0})๐ = (๐ข โ (๐ / ๐ข))) |
195 | 90, 194 | syldan 592 |
. . . 4
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ โ๐ข โ (โ โ {0})๐ = (๐ข โ (๐ / ๐ข))) |
196 | 20 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ โ โ) |
197 | 34 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ โ โ) |
198 | 62 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ โ โ) |
199 | 3 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ โ โ) |
200 | 10 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ (๐โ3) = (๐บ โ ๐)) |
201 | 12 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐บ โ โ) |
202 | 14 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ (๐บโ2) = ((๐โ2) + (๐โ3))) |
203 | 48 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ = (๐ / 3)) |
204 | 16 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ = (๐ / 2)) |
205 | 1 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ โ 0) |
206 | 106 | ad2antrl 727 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ข โ โ) |
207 | 109 | ad2antrl 727 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ข โ 0) |
208 | | simprr 772 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ๐ = (๐ข โ (๐ / ๐ข))) |
209 | | simplr 768 |
. . . . 5
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) |
210 | 196, 197,
198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209 | dcubic2 26210 |
. . . 4
โข (((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โง (๐ข โ (โ โ {0}) โง ๐ = (๐ข โ (๐ / ๐ข)))) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |
211 | 195, 210 | rexlimddv 3159 |
. . 3
โข ((๐ โง ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |
212 | 211 | ex 414 |
. 2
โข (๐ โ (((๐โ3) + ((๐ ยท ๐) + ๐)) = 0 โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐)))))) |
213 | 20 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ โ) |
214 | 34 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ โ) |
215 | 62 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ โ) |
216 | | simplr 768 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ โ) |
217 | 3 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ โ) |
218 | 216, 217 | mulcld 11182 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ (๐ ยท ๐) โ โ) |
219 | | 3nn0 12438 |
. . . . . . 7
โข 3 โ
โ0 |
220 | 219 | a1i 11 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ 3 โ
โ0) |
221 | 216, 217,
220 | mulexpd 14073 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ((๐ ยท ๐)โ3) = ((๐โ3) ยท (๐โ3))) |
222 | | simprl 770 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ (๐โ3) = 1) |
223 | 222 | oveq1d 7377 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ((๐โ3) ยท (๐โ3)) = (1 ยท (๐โ3))) |
224 | | expcl 13992 |
. . . . . . . . 9
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
225 | 3, 219, 224 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (๐โ3) โ โ) |
226 | 225 | mulid2d 11180 |
. . . . . . 7
โข (๐ โ (1 ยท (๐โ3)) = (๐โ3)) |
227 | 226, 10 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (1 ยท (๐โ3)) = (๐บ โ ๐)) |
228 | 227 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ (1 ยท (๐โ3)) = (๐บ โ ๐)) |
229 | 221, 223,
228 | 3eqtrd 2781 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ((๐ ยท ๐)โ3) = (๐บ โ ๐)) |
230 | 12 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐บ โ โ) |
231 | 14 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ (๐บโ2) = ((๐โ2) + (๐โ3))) |
232 | 48 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ = (๐ / 3)) |
233 | 16 | ad2antrr 725 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ = (๐ / 2)) |
234 | 132 | a1i 11 |
. . . . . . 7
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ 1 โ 0) |
235 | 222, 234 | eqnetrd 3012 |
. . . . . 6
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ (๐โ3) โ 0) |
236 | | oveq1 7369 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ3) = (0โ3)) |
237 | 236, 28 | eqtrdi 2793 |
. . . . . . 7
โข (๐ = 0 โ (๐โ3) = 0) |
238 | 237 | necon3i 2977 |
. . . . . 6
โข ((๐โ3) โ 0 โ ๐ โ 0) |
239 | 235, 238 | syl 17 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ 0) |
240 | 1 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ โ 0) |
241 | 216, 217,
239, 240 | mulne0d 11814 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ (๐ ยท ๐) โ 0) |
242 | | simprr 772 |
. . . 4
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐)))) |
243 | 213, 214,
215, 218, 229, 230, 231, 232, 233, 241, 242 | dcubic1 26211 |
. . 3
โข (((๐ โง ๐ โ โ) โง ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) |
244 | 243 | rexlimdva2 3155 |
. 2
โข (๐ โ (โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐)))) โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0)) |
245 | 212, 244 | impbid 211 |
1
โข (๐ โ (((๐โ3) + ((๐ ยท ๐) + ๐)) = 0 โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐)))))) |