Step | Hyp | Ref
| Expression |
1 | | dcubic2.u |
. . . . 5
โข (๐ โ ๐ โ โ) |
2 | | dcubic.t |
. . . . 5
โข (๐ โ ๐ โ โ) |
3 | | dcubic.0 |
. . . . 5
โข (๐ โ ๐ โ 0) |
4 | 1, 2, 3 | divcld 11932 |
. . . 4
โข (๐ โ (๐ / ๐) โ โ) |
5 | 4 | adantr 482 |
. . 3
โข ((๐ โง (๐โ3) = (๐บ โ ๐)) โ (๐ / ๐) โ โ) |
6 | | 3nn0 12432 |
. . . . . . 7
โข 3 โ
โ0 |
7 | 6 | a1i 11 |
. . . . . 6
โข (๐ โ 3 โ
โ0) |
8 | 1, 2, 3, 7 | expdivd 14066 |
. . . . 5
โข (๐ โ ((๐ / ๐)โ3) = ((๐โ3) / (๐โ3))) |
9 | 8 | adantr 482 |
. . . 4
โข ((๐ โง (๐โ3) = (๐บ โ ๐)) โ ((๐ / ๐)โ3) = ((๐โ3) / (๐โ3))) |
10 | | oveq1 7365 |
. . . . 5
โข ((๐โ3) = (๐บ โ ๐) โ ((๐โ3) / (๐โ3)) = ((๐บ โ ๐) / (๐โ3))) |
11 | | dcubic.3 |
. . . . . . 7
โข (๐ โ (๐โ3) = (๐บ โ ๐)) |
12 | 11 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((๐โ3) / (๐โ3)) = ((๐บ โ ๐) / (๐โ3))) |
13 | | expcl 13986 |
. . . . . . . 8
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
14 | 2, 6, 13 | sylancl 587 |
. . . . . . 7
โข (๐ โ (๐โ3) โ โ) |
15 | | 3z 12537 |
. . . . . . . . 9
โข 3 โ
โค |
16 | 15 | a1i 11 |
. . . . . . . 8
โข (๐ โ 3 โ
โค) |
17 | 2, 3, 16 | expne0d 14058 |
. . . . . . 7
โข (๐ โ (๐โ3) โ 0) |
18 | 14, 17 | dividd 11930 |
. . . . . 6
โข (๐ โ ((๐โ3) / (๐โ3)) = 1) |
19 | 12, 18 | eqtr3d 2779 |
. . . . 5
โข (๐ โ ((๐บ โ ๐) / (๐โ3)) = 1) |
20 | 10, 19 | sylan9eqr 2799 |
. . . 4
โข ((๐ โง (๐โ3) = (๐บ โ ๐)) โ ((๐โ3) / (๐โ3)) = 1) |
21 | 9, 20 | eqtrd 2777 |
. . 3
โข ((๐ โง (๐โ3) = (๐บ โ ๐)) โ ((๐ / ๐)โ3) = 1) |
22 | | dcubic2.2 |
. . . . 5
โข (๐ โ ๐ = (๐ โ (๐ / ๐))) |
23 | 1, 2, 3 | divcan1d 11933 |
. . . . . 6
โข (๐ โ ((๐ / ๐) ยท ๐) = ๐) |
24 | 23 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (๐ / ((๐ / ๐) ยท ๐)) = (๐ / ๐)) |
25 | 23, 24 | oveq12d 7376 |
. . . . 5
โข (๐ โ (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐))) = (๐ โ (๐ / ๐))) |
26 | 22, 25 | eqtr4d 2780 |
. . . 4
โข (๐ โ ๐ = (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐)))) |
27 | 26 | adantr 482 |
. . 3
โข ((๐ โง (๐โ3) = (๐บ โ ๐)) โ ๐ = (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐)))) |
28 | | oveq1 7365 |
. . . . . 6
โข (๐ = (๐ / ๐) โ (๐โ3) = ((๐ / ๐)โ3)) |
29 | 28 | eqeq1d 2739 |
. . . . 5
โข (๐ = (๐ / ๐) โ ((๐โ3) = 1 โ ((๐ / ๐)โ3) = 1)) |
30 | | oveq1 7365 |
. . . . . . 7
โข (๐ = (๐ / ๐) โ (๐ ยท ๐) = ((๐ / ๐) ยท ๐)) |
31 | 30 | oveq2d 7374 |
. . . . . . 7
โข (๐ = (๐ / ๐) โ (๐ / (๐ ยท ๐)) = (๐ / ((๐ / ๐) ยท ๐))) |
32 | 30, 31 | oveq12d 7376 |
. . . . . 6
โข (๐ = (๐ / ๐) โ ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))) = (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐)))) |
33 | 32 | eqeq2d 2748 |
. . . . 5
โข (๐ = (๐ / ๐) โ (๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))) โ ๐ = (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐))))) |
34 | 29, 33 | anbi12d 632 |
. . . 4
โข (๐ = (๐ / ๐) โ (((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐)))) โ (((๐ / ๐)โ3) = 1 โง ๐ = (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐)))))) |
35 | 34 | rspcev 3582 |
. . 3
โข (((๐ / ๐) โ โ โง (((๐ / ๐)โ3) = 1 โง ๐ = (((๐ / ๐) ยท ๐) โ (๐ / ((๐ / ๐) ยท ๐))))) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |
36 | 5, 21, 27, 35 | syl12anc 836 |
. 2
โข ((๐ โง (๐โ3) = (๐บ โ ๐)) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |
37 | | dcubic.m |
. . . . . . . 8
โข (๐ โ ๐ = (๐ / 3)) |
38 | | dcubic.c |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
39 | | 3cn 12235 |
. . . . . . . . . 10
โข 3 โ
โ |
40 | 39 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 3 โ
โ) |
41 | | 3ne0 12260 |
. . . . . . . . . 10
โข 3 โ
0 |
42 | 41 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 3 โ 0) |
43 | 38, 40, 42 | divcld 11932 |
. . . . . . . 8
โข (๐ โ (๐ / 3) โ โ) |
44 | 37, 43 | eqeltrd 2838 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
45 | | dcubic2.z |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
46 | 44, 1, 45 | divcld 11932 |
. . . . . 6
โข (๐ โ (๐ / ๐) โ โ) |
47 | 46 | negcld 11500 |
. . . . 5
โข (๐ โ -(๐ / ๐) โ โ) |
48 | 47, 2, 3 | divcld 11932 |
. . . 4
โข (๐ โ (-(๐ / ๐) / ๐) โ โ) |
49 | 48 | adantr 482 |
. . 3
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (-(๐ / ๐) / ๐) โ โ) |
50 | 47, 2, 3, 7 | expdivd 14066 |
. . . . . 6
โข (๐ โ ((-(๐ / ๐) / ๐)โ3) = ((-(๐ / ๐)โ3) / (๐โ3))) |
51 | 44, 1, 45 | divnegd 11945 |
. . . . . . . . 9
โข (๐ โ -(๐ / ๐) = (-๐ / ๐)) |
52 | 51 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ (-(๐ / ๐)โ3) = ((-๐ / ๐)โ3)) |
53 | 44 | negcld 11500 |
. . . . . . . . 9
โข (๐ โ -๐ โ โ) |
54 | 53, 1, 45, 7 | expdivd 14066 |
. . . . . . . 8
โข (๐ โ ((-๐ / ๐)โ3) = ((-๐โ3) / (๐โ3))) |
55 | 11 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐บ + ๐) ยท (๐โ3)) = ((๐บ + ๐) ยท (๐บ โ ๐))) |
56 | | dcubic.g |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐บ โ โ) |
57 | | dcubic.n |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ = (๐ / 2)) |
58 | | dcubic.d |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
59 | 58 | halfcld 12399 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ / 2) โ โ) |
60 | 57, 59 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
61 | | subsq 14115 |
. . . . . . . . . . . . . . 15
โข ((๐บ โ โ โง ๐ โ โ) โ ((๐บโ2) โ (๐โ2)) = ((๐บ + ๐) ยท (๐บ โ ๐))) |
62 | 56, 60, 61 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐บโ2) โ (๐โ2)) = ((๐บ + ๐) ยท (๐บ โ ๐))) |
63 | 55, 62 | eqtr4d 2780 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐บ + ๐) ยท (๐โ3)) = ((๐บโ2) โ (๐โ2))) |
64 | | dcubic.2 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐บโ2) = ((๐โ2) + (๐โ3))) |
65 | 64 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐บโ2) โ (๐โ2)) = (((๐โ2) + (๐โ3)) โ (๐โ2))) |
66 | 60 | sqcld 14050 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ2) โ โ) |
67 | | expcl 13986 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
68 | 44, 6, 67 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ3) โ โ) |
69 | 66, 68 | pncan2d 11515 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐โ2) + (๐โ3)) โ (๐โ2)) = (๐โ3)) |
70 | 63, 65, 69 | 3eqtrd 2781 |
. . . . . . . . . . . 12
โข (๐ โ ((๐บ + ๐) ยท (๐โ3)) = (๐โ3)) |
71 | 70 | negeqd 11396 |
. . . . . . . . . . 11
โข (๐ โ -((๐บ + ๐) ยท (๐โ3)) = -(๐โ3)) |
72 | 56, 60 | addcld 11175 |
. . . . . . . . . . . 12
โข (๐ โ (๐บ + ๐) โ โ) |
73 | 72, 14 | mulneg1d 11609 |
. . . . . . . . . . 11
โข (๐ โ (-(๐บ + ๐) ยท (๐โ3)) = -((๐บ + ๐) ยท (๐โ3))) |
74 | | 3nn 12233 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
75 | 74 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 3 โ
โ) |
76 | | n2dvds3 16254 |
. . . . . . . . . . . . 13
โข ยฌ 2
โฅ 3 |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ ยฌ 2 โฅ
3) |
78 | | oexpneg 16228 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 3 โ
โ โง ยฌ 2 โฅ 3) โ (-๐โ3) = -(๐โ3)) |
79 | 44, 75, 77, 78 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ (-๐โ3) = -(๐โ3)) |
80 | 71, 73, 79 | 3eqtr4d 2787 |
. . . . . . . . . 10
โข (๐ โ (-(๐บ + ๐) ยท (๐โ3)) = (-๐โ3)) |
81 | 80 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((-(๐บ + ๐) ยท (๐โ3)) / (๐โ3)) = ((-๐โ3) / (๐โ3))) |
82 | 72 | negcld 11500 |
. . . . . . . . . 10
โข (๐ โ -(๐บ + ๐) โ โ) |
83 | | expcl 13986 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
84 | 1, 6, 83 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ (๐โ3) โ โ) |
85 | 1, 45, 16 | expne0d 14058 |
. . . . . . . . . 10
โข (๐ โ (๐โ3) โ 0) |
86 | 82, 14, 84, 85 | div23d 11969 |
. . . . . . . . 9
โข (๐ โ ((-(๐บ + ๐) ยท (๐โ3)) / (๐โ3)) = ((-(๐บ + ๐) / (๐โ3)) ยท (๐โ3))) |
87 | 81, 86 | eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ ((-๐โ3) / (๐โ3)) = ((-(๐บ + ๐) / (๐โ3)) ยท (๐โ3))) |
88 | 52, 54, 87 | 3eqtrd 2781 |
. . . . . . 7
โข (๐ โ (-(๐ / ๐)โ3) = ((-(๐บ + ๐) / (๐โ3)) ยท (๐โ3))) |
89 | 88 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((-(๐ / ๐)โ3) / (๐โ3)) = (((-(๐บ + ๐) / (๐โ3)) ยท (๐โ3)) / (๐โ3))) |
90 | 82, 84, 85 | divcld 11932 |
. . . . . . 7
โข (๐ โ (-(๐บ + ๐) / (๐โ3)) โ โ) |
91 | 90, 14, 17 | divcan4d 11938 |
. . . . . 6
โข (๐ โ (((-(๐บ + ๐) / (๐โ3)) ยท (๐โ3)) / (๐โ3)) = (-(๐บ + ๐) / (๐โ3))) |
92 | 50, 89, 91 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ ((-(๐ / ๐) / ๐)โ3) = (-(๐บ + ๐) / (๐โ3))) |
93 | 92 | adantr 482 |
. . . 4
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ((-(๐ / ๐) / ๐)โ3) = (-(๐บ + ๐) / (๐โ3))) |
94 | | oveq1 7365 |
. . . . . 6
โข ((๐โ3) = -(๐บ + ๐) โ ((๐โ3) / (๐โ3)) = (-(๐บ + ๐) / (๐โ3))) |
95 | 94 | eqcomd 2743 |
. . . . 5
โข ((๐โ3) = -(๐บ + ๐) โ (-(๐บ + ๐) / (๐โ3)) = ((๐โ3) / (๐โ3))) |
96 | 84, 85 | dividd 11930 |
. . . . 5
โข (๐ โ ((๐โ3) / (๐โ3)) = 1) |
97 | 95, 96 | sylan9eqr 2799 |
. . . 4
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (-(๐บ + ๐) / (๐โ3)) = 1) |
98 | 93, 97 | eqtrd 2777 |
. . 3
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ((-(๐ / ๐) / ๐)โ3) = 1) |
99 | 46, 1 | neg2subd 11530 |
. . . . . 6
โข (๐ โ (-(๐ / ๐) โ -๐) = (๐ โ (๐ / ๐))) |
100 | 22, 99 | eqtr4d 2780 |
. . . . 5
โข (๐ โ ๐ = (-(๐ / ๐) โ -๐)) |
101 | 100 | adantr 482 |
. . . 4
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ๐ = (-(๐ / ๐) โ -๐)) |
102 | 47, 2, 3 | divcan1d 11933 |
. . . . . 6
โข (๐ โ ((-(๐ / ๐) / ๐) ยท ๐) = -(๐ / ๐)) |
103 | 102 | adantr 482 |
. . . . 5
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ((-(๐ / ๐) / ๐) ยท ๐) = -(๐ / ๐)) |
104 | 44, 1, 45 | divneg2d 11946 |
. . . . . . . . 9
โข (๐ โ -(๐ / ๐) = (๐ / -๐)) |
105 | 102, 104 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((-(๐ / ๐) / ๐) ยท ๐) = (๐ / -๐)) |
106 | 105 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ((-(๐ / ๐) / ๐) ยท ๐) = (๐ / -๐)) |
107 | 106 | oveq2d 7374 |
. . . . . 6
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐)) = (๐ / (๐ / -๐))) |
108 | 44 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ๐ โ โ) |
109 | 1 | negcld 11500 |
. . . . . . . 8
โข (๐ โ -๐ โ โ) |
110 | 109 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ -๐ โ โ) |
111 | 73, 71 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (-(๐บ + ๐) ยท (๐โ3)) = -(๐โ3)) |
112 | 111 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (-(๐บ + ๐) ยท (๐โ3)) = -(๐โ3)) |
113 | 82 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ -(๐บ + ๐) โ โ) |
114 | 14 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐โ3) โ โ) |
115 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐โ3) = -(๐บ + ๐)) |
116 | 85 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐โ3) โ 0) |
117 | 115, 116 | eqnetrrd 3013 |
. . . . . . . . . 10
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ -(๐บ + ๐) โ 0) |
118 | 17 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐โ3) โ 0) |
119 | 113, 114,
117, 118 | mulne0d 11808 |
. . . . . . . . 9
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (-(๐บ + ๐) ยท (๐โ3)) โ 0) |
120 | 112, 119 | eqnetrrd 3013 |
. . . . . . . 8
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ -(๐โ3) โ 0) |
121 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (๐โ3) = (0โ3)) |
122 | | 0exp 14004 |
. . . . . . . . . . . . 13
โข (3 โ
โ โ (0โ3) = 0) |
123 | 74, 122 | ax-mp 5 |
. . . . . . . . . . . 12
โข
(0โ3) = 0 |
124 | 121, 123 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐โ3) = 0) |
125 | 124 | negeqd 11396 |
. . . . . . . . . 10
โข (๐ = 0 โ -(๐โ3) = -0) |
126 | | neg0 11448 |
. . . . . . . . . 10
โข -0 =
0 |
127 | 125, 126 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ = 0 โ -(๐โ3) = 0) |
128 | 127 | necon3i 2977 |
. . . . . . . 8
โข (-(๐โ3) โ 0 โ ๐ โ 0) |
129 | 120, 128 | syl 17 |
. . . . . . 7
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ๐ โ 0) |
130 | 1, 45 | negne0d 11511 |
. . . . . . . 8
โข (๐ โ -๐ โ 0) |
131 | 130 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ -๐ โ 0) |
132 | 108, 110,
129, 131 | ddcand 11952 |
. . . . . 6
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐ / (๐ / -๐)) = -๐) |
133 | 107, 132 | eqtrd 2777 |
. . . . 5
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐)) = -๐) |
134 | 103, 133 | oveq12d 7376 |
. . . 4
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ (((-(๐ / ๐) / ๐) ยท ๐) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐))) = (-(๐ / ๐) โ -๐)) |
135 | 101, 134 | eqtr4d 2780 |
. . 3
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ ๐ = (((-(๐ / ๐) / ๐) ยท ๐) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐)))) |
136 | | oveq1 7365 |
. . . . . 6
โข (๐ = (-(๐ / ๐) / ๐) โ (๐โ3) = ((-(๐ / ๐) / ๐)โ3)) |
137 | 136 | eqeq1d 2739 |
. . . . 5
โข (๐ = (-(๐ / ๐) / ๐) โ ((๐โ3) = 1 โ ((-(๐ / ๐) / ๐)โ3) = 1)) |
138 | | oveq1 7365 |
. . . . . . 7
โข (๐ = (-(๐ / ๐) / ๐) โ (๐ ยท ๐) = ((-(๐ / ๐) / ๐) ยท ๐)) |
139 | 138 | oveq2d 7374 |
. . . . . . 7
โข (๐ = (-(๐ / ๐) / ๐) โ (๐ / (๐ ยท ๐)) = (๐ / ((-(๐ / ๐) / ๐) ยท ๐))) |
140 | 138, 139 | oveq12d 7376 |
. . . . . 6
โข (๐ = (-(๐ / ๐) / ๐) โ ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))) = (((-(๐ / ๐) / ๐) ยท ๐) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐)))) |
141 | 140 | eqeq2d 2748 |
. . . . 5
โข (๐ = (-(๐ / ๐) / ๐) โ (๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))) โ ๐ = (((-(๐ / ๐) / ๐) ยท ๐) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐))))) |
142 | 137, 141 | anbi12d 632 |
. . . 4
โข (๐ = (-(๐ / ๐) / ๐) โ (((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐)))) โ (((-(๐ / ๐) / ๐)โ3) = 1 โง ๐ = (((-(๐ / ๐) / ๐) ยท ๐) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐)))))) |
143 | 142 | rspcev 3582 |
. . 3
โข
(((-(๐ / ๐) / ๐) โ โ โง (((-(๐ / ๐) / ๐)โ3) = 1 โง ๐ = (((-(๐ / ๐) / ๐) ยท ๐) โ (๐ / ((-(๐ / ๐) / ๐) ยท ๐))))) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |
144 | 49, 98, 135, 143 | syl12anc 836 |
. 2
โข ((๐ โง (๐โ3) = -(๐บ + ๐)) โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |
145 | 84 | sqcld 14050 |
. . . . . . 7
โข (๐ โ ((๐โ3)โ2) โ
โ) |
146 | 145 | mulid2d 11174 |
. . . . . 6
โข (๐ โ (1 ยท ((๐โ3)โ2)) = ((๐โ3)โ2)) |
147 | 58, 84 | mulcld 11176 |
. . . . . . 7
โข (๐ โ (๐ ยท (๐โ3)) โ โ) |
148 | 147, 68 | negsubd 11519 |
. . . . . 6
โข (๐ โ ((๐ ยท (๐โ3)) + -(๐โ3)) = ((๐ ยท (๐โ3)) โ (๐โ3))) |
149 | 146, 148 | oveq12d 7376 |
. . . . 5
โข (๐ โ ((1 ยท ((๐โ3)โ2)) + ((๐ ยท (๐โ3)) + -(๐โ3))) = (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3)))) |
150 | | dcubic2.x |
. . . . . 6
โข (๐ โ ((๐โ3) + ((๐ ยท ๐) + ๐)) = 0) |
151 | | dcubic.x |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
152 | 38, 58, 151, 2, 11, 56, 64, 37, 57, 3, 1, 45, 22 | dcubic1lem 26196 |
. . . . . 6
โข (๐ โ (((๐โ3) + ((๐ ยท ๐) + ๐)) = 0 โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = 0)) |
153 | 150, 152 | mpbid 231 |
. . . . 5
โข (๐ โ (((๐โ3)โ2) + ((๐ ยท (๐โ3)) โ (๐โ3))) = 0) |
154 | 149, 153 | eqtrd 2777 |
. . . 4
โข (๐ โ ((1 ยท ((๐โ3)โ2)) + ((๐ ยท (๐โ3)) + -(๐โ3))) = 0) |
155 | | 1cnd 11151 |
. . . . 5
โข (๐ โ 1 โ
โ) |
156 | | ax-1ne0 11121 |
. . . . . 6
โข 1 โ
0 |
157 | 156 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ 0) |
158 | 68 | negcld 11500 |
. . . . 5
โข (๐ โ -(๐โ3) โ โ) |
159 | | 2cn 12229 |
. . . . . 6
โข 2 โ
โ |
160 | | mulcl 11136 |
. . . . . 6
โข ((2
โ โ โง ๐บ
โ โ) โ (2 ยท ๐บ) โ โ) |
161 | 159, 56, 160 | sylancr 588 |
. . . . 5
โข (๐ โ (2 ยท ๐บ) โ
โ) |
162 | | sqmul 14025 |
. . . . . . 7
โข ((2
โ โ โง ๐บ
โ โ) โ ((2 ยท ๐บ)โ2) = ((2โ2) ยท (๐บโ2))) |
163 | 159, 56, 162 | sylancr 588 |
. . . . . 6
โข (๐ โ ((2 ยท ๐บ)โ2) = ((2โ2) ยท
(๐บโ2))) |
164 | 64 | oveq2d 7374 |
. . . . . 6
โข (๐ โ ((2โ2) ยท
(๐บโ2)) = ((2โ2)
ยท ((๐โ2) +
(๐โ3)))) |
165 | 159 | sqcli 14086 |
. . . . . . . . 9
โข
(2โ2) โ โ |
166 | | mulcl 11136 |
. . . . . . . . 9
โข
(((2โ2) โ โ โง (๐โ2) โ โ) โ ((2โ2)
ยท (๐โ2)) โ
โ) |
167 | 165, 66, 166 | sylancr 588 |
. . . . . . . 8
โข (๐ โ ((2โ2) ยท
(๐โ2)) โ
โ) |
168 | | mulcl 11136 |
. . . . . . . . 9
โข
(((2โ2) โ โ โง (๐โ3) โ โ) โ ((2โ2)
ยท (๐โ3)) โ
โ) |
169 | 165, 68, 168 | sylancr 588 |
. . . . . . . 8
โข (๐ โ ((2โ2) ยท
(๐โ3)) โ
โ) |
170 | 167, 169 | subnegd 11520 |
. . . . . . 7
โข (๐ โ (((2โ2) ยท
(๐โ2)) โ
-((2โ2) ยท (๐โ3))) = (((2โ2) ยท (๐โ2)) + ((2โ2) ยท
(๐โ3)))) |
171 | 57 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) = (2 ยท (๐ / 2))) |
172 | 159 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
173 | | 2ne0 12258 |
. . . . . . . . . . . . 13
โข 2 โ
0 |
174 | 173 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ 0) |
175 | 58, 172, 174 | divcan2d 11934 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (๐ / 2)) = ๐) |
176 | 171, 175 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) = ๐) |
177 | 176 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ2) = (๐โ2)) |
178 | | sqmul 14025 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ) โ ((2 ยท ๐)โ2) = ((2โ2) ยท (๐โ2))) |
179 | 159, 60, 178 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ2) = ((2โ2) ยท
(๐โ2))) |
180 | 177, 179 | eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ (๐โ2) = ((2โ2) ยท (๐โ2))) |
181 | 158 | mulid2d 11174 |
. . . . . . . . . . 11
โข (๐ โ (1 ยท -(๐โ3)) = -(๐โ3)) |
182 | 181 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ โ (4 ยท (1 ยท
-(๐โ3))) = (4 ยท
-(๐โ3))) |
183 | | 4cn 12239 |
. . . . . . . . . . 11
โข 4 โ
โ |
184 | | mulneg2 11593 |
. . . . . . . . . . 11
โข ((4
โ โ โง (๐โ3) โ โ) โ (4 ยท
-(๐โ3)) = -(4 ยท
(๐โ3))) |
185 | 183, 68, 184 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (4 ยท -(๐โ3)) = -(4 ยท (๐โ3))) |
186 | 182, 185 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ (4 ยท (1 ยท
-(๐โ3))) = -(4
ยท (๐โ3))) |
187 | | sq2 14102 |
. . . . . . . . . . 11
โข
(2โ2) = 4 |
188 | 187 | oveq1i 7368 |
. . . . . . . . . 10
โข
((2โ2) ยท (๐โ3)) = (4 ยท (๐โ3)) |
189 | 188 | negeqi 11395 |
. . . . . . . . 9
โข
-((2โ2) ยท (๐โ3)) = -(4 ยท (๐โ3)) |
190 | 186, 189 | eqtr4di 2795 |
. . . . . . . 8
โข (๐ โ (4 ยท (1 ยท
-(๐โ3))) =
-((2โ2) ยท (๐โ3))) |
191 | 180, 190 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ ((๐โ2) โ (4 ยท (1 ยท
-(๐โ3)))) =
(((2โ2) ยท (๐โ2)) โ -((2โ2) ยท
(๐โ3)))) |
192 | 165 | a1i 11 |
. . . . . . . 8
โข (๐ โ (2โ2) โ
โ) |
193 | 192, 66, 68 | adddid 11180 |
. . . . . . 7
โข (๐ โ ((2โ2) ยท
((๐โ2) + (๐โ3))) = (((2โ2)
ยท (๐โ2)) +
((2โ2) ยท (๐โ3)))) |
194 | 170, 191,
193 | 3eqtr4rd 2788 |
. . . . . 6
โข (๐ โ ((2โ2) ยท
((๐โ2) + (๐โ3))) = ((๐โ2) โ (4 ยท (1 ยท
-(๐โ3))))) |
195 | 163, 164,
194 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ ((2 ยท ๐บ)โ2) = ((๐โ2) โ (4 ยท (1 ยท
-(๐โ3))))) |
196 | 155, 157,
58, 158, 84, 161, 195 | quad2 26192 |
. . . 4
โข (๐ โ (((1 ยท ((๐โ3)โ2)) + ((๐ ยท (๐โ3)) + -(๐โ3))) = 0 โ ((๐โ3) = ((-๐ + (2 ยท ๐บ)) / (2 ยท 1)) โจ (๐โ3) = ((-๐ โ (2 ยท ๐บ)) / (2 ยท 1))))) |
197 | 154, 196 | mpbid 231 |
. . 3
โข (๐ โ ((๐โ3) = ((-๐ + (2 ยท ๐บ)) / (2 ยท 1)) โจ (๐โ3) = ((-๐ โ (2 ยท ๐บ)) / (2 ยท 1)))) |
198 | | 2t1e2 12317 |
. . . . . . 7
โข (2
ยท 1) = 2 |
199 | 198 | oveq2i 7369 |
. . . . . 6
โข ((-๐ + (2 ยท ๐บ)) / (2 ยท 1)) = ((-๐ + (2 ยท ๐บ)) / 2) |
200 | 58 | negcld 11500 |
. . . . . . . 8
โข (๐ โ -๐ โ โ) |
201 | 200, 161,
172, 174 | divdird 11970 |
. . . . . . 7
โข (๐ โ ((-๐ + (2 ยท ๐บ)) / 2) = ((-๐ / 2) + ((2 ยท ๐บ) / 2))) |
202 | 57 | negeqd 11396 |
. . . . . . . . 9
โข (๐ โ -๐ = -(๐ / 2)) |
203 | 58, 172, 174 | divnegd 11945 |
. . . . . . . . 9
โข (๐ โ -(๐ / 2) = (-๐ / 2)) |
204 | 202, 203 | eqtr2d 2778 |
. . . . . . . 8
โข (๐ โ (-๐ / 2) = -๐) |
205 | 56, 172, 174 | divcan3d 11937 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐บ) / 2) = ๐บ) |
206 | 204, 205 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ ((-๐ / 2) + ((2 ยท ๐บ) / 2)) = (-๐ + ๐บ)) |
207 | 60 | negcld 11500 |
. . . . . . . . 9
โข (๐ โ -๐ โ โ) |
208 | 207, 56 | addcomd 11358 |
. . . . . . . 8
โข (๐ โ (-๐ + ๐บ) = (๐บ + -๐)) |
209 | 56, 60 | negsubd 11519 |
. . . . . . . 8
โข (๐ โ (๐บ + -๐) = (๐บ โ ๐)) |
210 | 208, 209 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (-๐ + ๐บ) = (๐บ โ ๐)) |
211 | 201, 206,
210 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ ((-๐ + (2 ยท ๐บ)) / 2) = (๐บ โ ๐)) |
212 | 199, 211 | eqtrid 2789 |
. . . . 5
โข (๐ โ ((-๐ + (2 ยท ๐บ)) / (2 ยท 1)) = (๐บ โ ๐)) |
213 | 212 | eqeq2d 2748 |
. . . 4
โข (๐ โ ((๐โ3) = ((-๐ + (2 ยท ๐บ)) / (2 ยท 1)) โ (๐โ3) = (๐บ โ ๐))) |
214 | 198 | oveq2i 7369 |
. . . . . 6
โข ((-๐ โ (2 ยท ๐บ)) / (2 ยท 1)) = ((-๐ โ (2 ยท ๐บ)) / 2) |
215 | 204, 205 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ ((-๐ / 2) โ ((2 ยท ๐บ) / 2)) = (-๐ โ ๐บ)) |
216 | 200, 161,
172, 174 | divsubdird 11971 |
. . . . . . 7
โข (๐ โ ((-๐ โ (2 ยท ๐บ)) / 2) = ((-๐ / 2) โ ((2 ยท ๐บ) / 2))) |
217 | 56, 60 | addcomd 11358 |
. . . . . . . . 9
โข (๐ โ (๐บ + ๐) = (๐ + ๐บ)) |
218 | 217 | negeqd 11396 |
. . . . . . . 8
โข (๐ โ -(๐บ + ๐) = -(๐ + ๐บ)) |
219 | 60, 56 | negdi2d 11527 |
. . . . . . . 8
โข (๐ โ -(๐ + ๐บ) = (-๐ โ ๐บ)) |
220 | 218, 219 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ -(๐บ + ๐) = (-๐ โ ๐บ)) |
221 | 215, 216,
220 | 3eqtr4d 2787 |
. . . . . 6
โข (๐ โ ((-๐ โ (2 ยท ๐บ)) / 2) = -(๐บ + ๐)) |
222 | 214, 221 | eqtrid 2789 |
. . . . 5
โข (๐ โ ((-๐ โ (2 ยท ๐บ)) / (2 ยท 1)) = -(๐บ + ๐)) |
223 | 222 | eqeq2d 2748 |
. . . 4
โข (๐ โ ((๐โ3) = ((-๐ โ (2 ยท ๐บ)) / (2 ยท 1)) โ (๐โ3) = -(๐บ + ๐))) |
224 | 213, 223 | orbi12d 918 |
. . 3
โข (๐ โ (((๐โ3) = ((-๐ + (2 ยท ๐บ)) / (2 ยท 1)) โจ (๐โ3) = ((-๐ โ (2 ยท ๐บ)) / (2 ยท 1))) โ ((๐โ3) = (๐บ โ ๐) โจ (๐โ3) = -(๐บ + ๐)))) |
225 | 197, 224 | mpbid 231 |
. 2
โข (๐ โ ((๐โ3) = (๐บ โ ๐) โจ (๐โ3) = -(๐บ + ๐))) |
226 | 36, 144, 225 | mpjaodan 958 |
1
โข (๐ โ โ๐ โ โ ((๐โ3) = 1 โง ๐ = ((๐ ยท ๐) โ (๐ / (๐ ยท ๐))))) |