Step |
Hyp |
Ref |
Expression |
1 |
|
mcubic.b |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
2 |
|
mcubic.c |
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
3 |
|
mcubic.d |
⊢ ( 𝜑 → 𝐷 ∈ ℂ ) |
4 |
|
mcubic.x |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
5 |
|
mcubic.t |
⊢ ( 𝜑 → 𝑇 ∈ ℂ ) |
6 |
|
mcubic.3 |
⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( 𝑁 + 𝐺 ) / 2 ) ) |
7 |
|
mcubic.g |
⊢ ( 𝜑 → 𝐺 ∈ ℂ ) |
8 |
|
mcubic.2 |
⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) ) |
9 |
|
mcubic.m |
⊢ ( 𝜑 → 𝑀 = ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) ) |
10 |
|
mcubic.n |
⊢ ( 𝜑 → 𝑁 = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) ) |
11 |
|
mcubic.0 |
⊢ ( 𝜑 → 𝑇 ≠ 0 ) |
12 |
1
|
sqcld |
⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ ) |
13 |
|
3cn |
⊢ 3 ∈ ℂ |
14 |
|
mulcl |
⊢ ( ( 3 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 3 · 𝐶 ) ∈ ℂ ) |
15 |
13 2 14
|
sylancr |
⊢ ( 𝜑 → ( 3 · 𝐶 ) ∈ ℂ ) |
16 |
12 15
|
subcld |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) ∈ ℂ ) |
17 |
9 16
|
eqeltrd |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
18 |
13
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℂ ) |
19 |
|
3ne0 |
⊢ 3 ≠ 0 |
20 |
19
|
a1i |
⊢ ( 𝜑 → 3 ≠ 0 ) |
21 |
17 18 20
|
divcld |
⊢ ( 𝜑 → ( 𝑀 / 3 ) ∈ ℂ ) |
22 |
21
|
negcld |
⊢ ( 𝜑 → - ( 𝑀 / 3 ) ∈ ℂ ) |
23 |
|
2cn |
⊢ 2 ∈ ℂ |
24 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
25 |
|
expcl |
⊢ ( ( 𝐵 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐵 ↑ 3 ) ∈ ℂ ) |
26 |
1 24 25
|
sylancl |
⊢ ( 𝜑 → ( 𝐵 ↑ 3 ) ∈ ℂ ) |
27 |
|
mulcl |
⊢ ( ( 2 ∈ ℂ ∧ ( 𝐵 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ ) |
28 |
23 26 27
|
sylancr |
⊢ ( 𝜑 → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ ) |
29 |
|
9cn |
⊢ 9 ∈ ℂ |
30 |
1 2
|
mulcld |
⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ ) |
31 |
|
mulcl |
⊢ ( ( 9 ∈ ℂ ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( 9 · ( 𝐵 · 𝐶 ) ) ∈ ℂ ) |
32 |
29 30 31
|
sylancr |
⊢ ( 𝜑 → ( 9 · ( 𝐵 · 𝐶 ) ) ∈ ℂ ) |
33 |
28 32
|
subcld |
⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) ∈ ℂ ) |
34 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
35 |
|
7nn |
⊢ 7 ∈ ℕ |
36 |
34 35
|
decnncl |
⊢ ; 2 7 ∈ ℕ |
37 |
36
|
nncni |
⊢ ; 2 7 ∈ ℂ |
38 |
|
mulcl |
⊢ ( ( ; 2 7 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ; 2 7 · 𝐷 ) ∈ ℂ ) |
39 |
37 3 38
|
sylancr |
⊢ ( 𝜑 → ( ; 2 7 · 𝐷 ) ∈ ℂ ) |
40 |
33 39
|
addcld |
⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) ∈ ℂ ) |
41 |
10 40
|
eqeltrd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
42 |
37
|
a1i |
⊢ ( 𝜑 → ; 2 7 ∈ ℂ ) |
43 |
36
|
nnne0i |
⊢ ; 2 7 ≠ 0 |
44 |
43
|
a1i |
⊢ ( 𝜑 → ; 2 7 ≠ 0 ) |
45 |
41 42 44
|
divcld |
⊢ ( 𝜑 → ( 𝑁 / ; 2 7 ) ∈ ℂ ) |
46 |
1 18 20
|
divcld |
⊢ ( 𝜑 → ( 𝐵 / 3 ) ∈ ℂ ) |
47 |
4 46
|
addcld |
⊢ ( 𝜑 → ( 𝑋 + ( 𝐵 / 3 ) ) ∈ ℂ ) |
48 |
5 18 20
|
divcld |
⊢ ( 𝜑 → ( 𝑇 / 3 ) ∈ ℂ ) |
49 |
48
|
negcld |
⊢ ( 𝜑 → - ( 𝑇 / 3 ) ∈ ℂ ) |
50 |
|
3nn |
⊢ 3 ∈ ℕ |
51 |
50
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℕ ) |
52 |
|
n2dvds3 |
⊢ ¬ 2 ∥ 3 |
53 |
52
|
a1i |
⊢ ( 𝜑 → ¬ 2 ∥ 3 ) |
54 |
|
oexpneg |
⊢ ( ( ( 𝑇 / 3 ) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3 ) → ( - ( 𝑇 / 3 ) ↑ 3 ) = - ( ( 𝑇 / 3 ) ↑ 3 ) ) |
55 |
48 51 53 54
|
syl3anc |
⊢ ( 𝜑 → ( - ( 𝑇 / 3 ) ↑ 3 ) = - ( ( 𝑇 / 3 ) ↑ 3 ) ) |
56 |
24
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℕ0 ) |
57 |
5 18 20 56
|
expdivd |
⊢ ( 𝜑 → ( ( 𝑇 / 3 ) ↑ 3 ) = ( ( 𝑇 ↑ 3 ) / ( 3 ↑ 3 ) ) ) |
58 |
|
3exp3 |
⊢ ( 3 ↑ 3 ) = ; 2 7 |
59 |
58
|
a1i |
⊢ ( 𝜑 → ( 3 ↑ 3 ) = ; 2 7 ) |
60 |
6 59
|
oveq12d |
⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) / ( 3 ↑ 3 ) ) = ( ( ( 𝑁 + 𝐺 ) / 2 ) / ; 2 7 ) ) |
61 |
41 7
|
addcld |
⊢ ( 𝜑 → ( 𝑁 + 𝐺 ) ∈ ℂ ) |
62 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
63 |
|
2ne0 |
⊢ 2 ≠ 0 |
64 |
63
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
65 |
61 62 42 64 44
|
divdiv32d |
⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / 2 ) / ; 2 7 ) = ( ( ( 𝑁 + 𝐺 ) / ; 2 7 ) / 2 ) ) |
66 |
41 7
|
addcomd |
⊢ ( 𝜑 → ( 𝑁 + 𝐺 ) = ( 𝐺 + 𝑁 ) ) |
67 |
66
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑁 + 𝐺 ) / ; 2 7 ) = ( ( 𝐺 + 𝑁 ) / ; 2 7 ) ) |
68 |
7 41 42 44
|
divdird |
⊢ ( 𝜑 → ( ( 𝐺 + 𝑁 ) / ; 2 7 ) = ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) ) |
69 |
67 68
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑁 + 𝐺 ) / ; 2 7 ) = ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) ) |
70 |
69
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / ; 2 7 ) / 2 ) = ( ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) / 2 ) ) |
71 |
7 42 44
|
divcld |
⊢ ( 𝜑 → ( 𝐺 / ; 2 7 ) ∈ ℂ ) |
72 |
71 45 62 64
|
divdird |
⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) / 2 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) ) |
73 |
65 70 72
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / 2 ) / ; 2 7 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) ) |
74 |
57 60 73
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝑇 / 3 ) ↑ 3 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) ) |
75 |
74
|
negeqd |
⊢ ( 𝜑 → - ( ( 𝑇 / 3 ) ↑ 3 ) = - ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) ) |
76 |
71
|
halfcld |
⊢ ( 𝜑 → ( ( 𝐺 / ; 2 7 ) / 2 ) ∈ ℂ ) |
77 |
45
|
halfcld |
⊢ ( 𝜑 → ( ( 𝑁 / ; 2 7 ) / 2 ) ∈ ℂ ) |
78 |
76 77
|
negdi2d |
⊢ ( 𝜑 → - ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) = ( - ( ( 𝐺 / ; 2 7 ) / 2 ) − ( ( 𝑁 / ; 2 7 ) / 2 ) ) ) |
79 |
55 75 78
|
3eqtrd |
⊢ ( 𝜑 → ( - ( 𝑇 / 3 ) ↑ 3 ) = ( - ( ( 𝐺 / ; 2 7 ) / 2 ) − ( ( 𝑁 / ; 2 7 ) / 2 ) ) ) |
80 |
76
|
negcld |
⊢ ( 𝜑 → - ( ( 𝐺 / ; 2 7 ) / 2 ) ∈ ℂ ) |
81 |
|
sqneg |
⊢ ( ( ( 𝐺 / ; 2 7 ) / 2 ) ∈ ℂ → ( - ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) ) |
82 |
76 81
|
syl |
⊢ ( 𝜑 → ( - ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) ) |
83 |
71 62 64
|
sqdivd |
⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝐺 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) ) |
84 |
45 62 64
|
sqdivd |
⊢ ( 𝜑 → ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝑁 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) ) |
85 |
41 42 44
|
sqdivd |
⊢ ( 𝜑 → ( ( 𝑁 / ; 2 7 ) ↑ 2 ) = ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) ) |
86 |
85
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑁 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) ) |
87 |
84 86
|
eqtr2d |
⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) = ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) ) |
88 |
|
4cn |
⊢ 4 ∈ ℂ |
89 |
88
|
a1i |
⊢ ( 𝜑 → 4 ∈ ℂ ) |
90 |
|
expcl |
⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑀 ↑ 3 ) ∈ ℂ ) |
91 |
17 24 90
|
sylancl |
⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ ) |
92 |
37
|
sqcli |
⊢ ( ; 2 7 ↑ 2 ) ∈ ℂ |
93 |
92
|
a1i |
⊢ ( 𝜑 → ( ; 2 7 ↑ 2 ) ∈ ℂ ) |
94 |
|
sqne0 |
⊢ ( ; 2 7 ∈ ℂ → ( ( ; 2 7 ↑ 2 ) ≠ 0 ↔ ; 2 7 ≠ 0 ) ) |
95 |
42 94
|
syl |
⊢ ( 𝜑 → ( ( ; 2 7 ↑ 2 ) ≠ 0 ↔ ; 2 7 ≠ 0 ) ) |
96 |
44 95
|
mpbird |
⊢ ( 𝜑 → ( ; 2 7 ↑ 2 ) ≠ 0 ) |
97 |
89 91 93 96
|
divassd |
⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) = ( 4 · ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) ) ) |
98 |
29
|
a1i |
⊢ ( 𝜑 → 9 ∈ ℂ ) |
99 |
|
9nn |
⊢ 9 ∈ ℕ |
100 |
99
|
nnne0i |
⊢ 9 ≠ 0 |
101 |
100
|
a1i |
⊢ ( 𝜑 → 9 ≠ 0 ) |
102 |
17 98 101 56
|
expdivd |
⊢ ( 𝜑 → ( ( 𝑀 / 9 ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( 9 ↑ 3 ) ) ) |
103 |
23 13
|
mulcomi |
⊢ ( 2 · 3 ) = ( 3 · 2 ) |
104 |
103
|
oveq2i |
⊢ ( 3 ↑ ( 2 · 3 ) ) = ( 3 ↑ ( 3 · 2 ) ) |
105 |
|
expmul |
⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( 3 ↑ ( 2 · 3 ) ) = ( ( 3 ↑ 2 ) ↑ 3 ) ) |
106 |
13 34 24 105
|
mp3an |
⊢ ( 3 ↑ ( 2 · 3 ) ) = ( ( 3 ↑ 2 ) ↑ 3 ) |
107 |
|
expmul |
⊢ ( ( 3 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 3 ↑ ( 3 · 2 ) ) = ( ( 3 ↑ 3 ) ↑ 2 ) ) |
108 |
13 24 34 107
|
mp3an |
⊢ ( 3 ↑ ( 3 · 2 ) ) = ( ( 3 ↑ 3 ) ↑ 2 ) |
109 |
104 106 108
|
3eqtr3i |
⊢ ( ( 3 ↑ 2 ) ↑ 3 ) = ( ( 3 ↑ 3 ) ↑ 2 ) |
110 |
|
sq3 |
⊢ ( 3 ↑ 2 ) = 9 |
111 |
110
|
oveq1i |
⊢ ( ( 3 ↑ 2 ) ↑ 3 ) = ( 9 ↑ 3 ) |
112 |
58
|
oveq1i |
⊢ ( ( 3 ↑ 3 ) ↑ 2 ) = ( ; 2 7 ↑ 2 ) |
113 |
109 111 112
|
3eqtr3i |
⊢ ( 9 ↑ 3 ) = ( ; 2 7 ↑ 2 ) |
114 |
113
|
oveq2i |
⊢ ( ( 𝑀 ↑ 3 ) / ( 9 ↑ 3 ) ) = ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) |
115 |
102 114
|
eqtrdi |
⊢ ( 𝜑 → ( ( 𝑀 / 9 ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) ) |
116 |
115
|
oveq2d |
⊢ ( 𝜑 → ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) = ( 4 · ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) ) ) |
117 |
97 116
|
eqtr4d |
⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) = ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) ) |
118 |
117
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) = ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / ( 2 ↑ 2 ) ) ) |
119 |
|
sq2 |
⊢ ( 2 ↑ 2 ) = 4 |
120 |
119
|
oveq2i |
⊢ ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / ( 2 ↑ 2 ) ) = ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / 4 ) |
121 |
17 98 101
|
divcld |
⊢ ( 𝜑 → ( 𝑀 / 9 ) ∈ ℂ ) |
122 |
|
expcl |
⊢ ( ( ( 𝑀 / 9 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( 𝑀 / 9 ) ↑ 3 ) ∈ ℂ ) |
123 |
121 24 122
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑀 / 9 ) ↑ 3 ) ∈ ℂ ) |
124 |
|
4ne0 |
⊢ 4 ≠ 0 |
125 |
124
|
a1i |
⊢ ( 𝜑 → 4 ≠ 0 ) |
126 |
123 89 125
|
divcan3d |
⊢ ( 𝜑 → ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / 4 ) = ( ( 𝑀 / 9 ) ↑ 3 ) ) |
127 |
120 126
|
eqtrid |
⊢ ( 𝜑 → ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / ( 2 ↑ 2 ) ) = ( ( 𝑀 / 9 ) ↑ 3 ) ) |
128 |
118 127
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) = ( ( 𝑀 / 9 ) ↑ 3 ) ) |
129 |
87 128
|
oveq12d |
⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) − ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) − ( ( 𝑀 / 9 ) ↑ 3 ) ) ) |
130 |
41
|
sqcld |
⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ ) |
131 |
130 93 96
|
divcld |
⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) ∈ ℂ ) |
132 |
|
mulcl |
⊢ ( ( 4 ∈ ℂ ∧ ( 𝑀 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ ) |
133 |
88 91 132
|
sylancr |
⊢ ( 𝜑 → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ ) |
134 |
133 93 96
|
divcld |
⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ∈ ℂ ) |
135 |
23
|
sqcli |
⊢ ( 2 ↑ 2 ) ∈ ℂ |
136 |
135
|
a1i |
⊢ ( 𝜑 → ( 2 ↑ 2 ) ∈ ℂ ) |
137 |
119 124
|
eqnetri |
⊢ ( 2 ↑ 2 ) ≠ 0 |
138 |
137
|
a1i |
⊢ ( 𝜑 → ( 2 ↑ 2 ) ≠ 0 ) |
139 |
131 134 136 138
|
divsubdird |
⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) − ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) ) ) |
140 |
77
|
sqcld |
⊢ ( 𝜑 → ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) ∈ ℂ ) |
141 |
140 123
|
negsubd |
⊢ ( 𝜑 → ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + - ( ( 𝑀 / 9 ) ↑ 3 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) − ( ( 𝑀 / 9 ) ↑ 3 ) ) ) |
142 |
129 139 141
|
3eqtr4d |
⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + - ( ( 𝑀 / 9 ) ↑ 3 ) ) ) |
143 |
7 42 44
|
sqdivd |
⊢ ( 𝜑 → ( ( 𝐺 / ; 2 7 ) ↑ 2 ) = ( ( 𝐺 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) ) |
144 |
8
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ; 2 7 ↑ 2 ) ) ) |
145 |
130 133 93 96
|
divsubdird |
⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ; 2 7 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) ) |
146 |
143 144 145
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝐺 / ; 2 7 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) ) |
147 |
146
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) / ( 2 ↑ 2 ) ) ) |
148 |
|
oexpneg |
⊢ ( ( ( 𝑀 / 9 ) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3 ) → ( - ( 𝑀 / 9 ) ↑ 3 ) = - ( ( 𝑀 / 9 ) ↑ 3 ) ) |
149 |
121 51 53 148
|
syl3anc |
⊢ ( 𝜑 → ( - ( 𝑀 / 9 ) ↑ 3 ) = - ( ( 𝑀 / 9 ) ↑ 3 ) ) |
150 |
149
|
oveq2d |
⊢ ( 𝜑 → ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + ( - ( 𝑀 / 9 ) ↑ 3 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + - ( ( 𝑀 / 9 ) ↑ 3 ) ) ) |
151 |
142 147 150
|
3eqtr4d |
⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + ( - ( 𝑀 / 9 ) ↑ 3 ) ) ) |
152 |
82 83 151
|
3eqtrd |
⊢ ( 𝜑 → ( - ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + ( - ( 𝑀 / 9 ) ↑ 3 ) ) ) |
153 |
17 18 18 20 20
|
divdiv1d |
⊢ ( 𝜑 → ( ( 𝑀 / 3 ) / 3 ) = ( 𝑀 / ( 3 · 3 ) ) ) |
154 |
|
3t3e9 |
⊢ ( 3 · 3 ) = 9 |
155 |
154
|
oveq2i |
⊢ ( 𝑀 / ( 3 · 3 ) ) = ( 𝑀 / 9 ) |
156 |
153 155
|
eqtrdi |
⊢ ( 𝜑 → ( ( 𝑀 / 3 ) / 3 ) = ( 𝑀 / 9 ) ) |
157 |
156
|
negeqd |
⊢ ( 𝜑 → - ( ( 𝑀 / 3 ) / 3 ) = - ( 𝑀 / 9 ) ) |
158 |
21 18 20
|
divnegd |
⊢ ( 𝜑 → - ( ( 𝑀 / 3 ) / 3 ) = ( - ( 𝑀 / 3 ) / 3 ) ) |
159 |
157 158
|
eqtr3d |
⊢ ( 𝜑 → - ( 𝑀 / 9 ) = ( - ( 𝑀 / 3 ) / 3 ) ) |
160 |
|
eqidd |
⊢ ( 𝜑 → ( ( 𝑁 / ; 2 7 ) / 2 ) = ( ( 𝑁 / ; 2 7 ) / 2 ) ) |
161 |
5 18 11 20
|
divne0d |
⊢ ( 𝜑 → ( 𝑇 / 3 ) ≠ 0 ) |
162 |
48 161
|
negne0d |
⊢ ( 𝜑 → - ( 𝑇 / 3 ) ≠ 0 ) |
163 |
22 45 47 49 79 80 152 159 160 162
|
dcubic |
⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ) ) |
164 |
|
binom3 |
⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝐵 / 3 ) ∈ ℂ ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) = ( ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
165 |
4 46 164
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) = ( ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
166 |
4
|
sqcld |
⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ ) |
167 |
18 166 46
|
mul12d |
⊢ ( 𝜑 → ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) = ( ( 𝑋 ↑ 2 ) · ( 3 · ( 𝐵 / 3 ) ) ) ) |
168 |
1 18 20
|
divcan2d |
⊢ ( 𝜑 → ( 3 · ( 𝐵 / 3 ) ) = 𝐵 ) |
169 |
168
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · ( 3 · ( 𝐵 / 3 ) ) ) = ( ( 𝑋 ↑ 2 ) · 𝐵 ) ) |
170 |
166 1
|
mulcomd |
⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · 𝐵 ) = ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) |
171 |
167 169 170
|
3eqtrd |
⊢ ( 𝜑 → ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) = ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) |
172 |
171
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) = ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) ) |
173 |
172
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
174 |
165 173
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
175 |
174
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) ) |
176 |
|
expcl |
⊢ ( ( 𝑋 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑋 ↑ 3 ) ∈ ℂ ) |
177 |
4 24 176
|
sylancl |
⊢ ( 𝜑 → ( 𝑋 ↑ 3 ) ∈ ℂ ) |
178 |
1 166
|
mulcld |
⊢ ( 𝜑 → ( 𝐵 · ( 𝑋 ↑ 2 ) ) ∈ ℂ ) |
179 |
177 178
|
addcld |
⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) ∈ ℂ ) |
180 |
46
|
sqcld |
⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 2 ) ∈ ℂ ) |
181 |
4 180
|
mulcld |
⊢ ( 𝜑 → ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ∈ ℂ ) |
182 |
18 181
|
mulcld |
⊢ ( 𝜑 → ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ∈ ℂ ) |
183 |
|
expcl |
⊢ ( ( ( 𝐵 / 3 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( 𝐵 / 3 ) ↑ 3 ) ∈ ℂ ) |
184 |
46 24 183
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 3 ) ∈ ℂ ) |
185 |
182 184
|
addcld |
⊢ ( 𝜑 → ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ∈ ℂ ) |
186 |
22 47
|
mulcld |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) ∈ ℂ ) |
187 |
186 45
|
addcld |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ∈ ℂ ) |
188 |
179 185 187
|
addassd |
⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) ) ) |
189 |
22 4 46
|
adddid |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) = ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ) ) |
190 |
189
|
oveq1d |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) |
191 |
22 4
|
mulcld |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · 𝑋 ) ∈ ℂ ) |
192 |
22 46
|
mulcld |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ∈ ℂ ) |
193 |
191 192 45
|
addassd |
⊢ ( 𝜑 → ( ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) ) ) |
194 |
9
|
oveq1d |
⊢ ( 𝜑 → ( 𝑀 / 3 ) = ( ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) / 3 ) ) |
195 |
12 15 18 20
|
divsubdird |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) / 3 ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) − ( ( 3 · 𝐶 ) / 3 ) ) ) |
196 |
2 18 20
|
divcan3d |
⊢ ( 𝜑 → ( ( 3 · 𝐶 ) / 3 ) = 𝐶 ) |
197 |
196
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) − ( ( 3 · 𝐶 ) / 3 ) ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) ) |
198 |
194 195 197
|
3eqtrd |
⊢ ( 𝜑 → ( 𝑀 / 3 ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) ) |
199 |
198
|
negeqd |
⊢ ( 𝜑 → - ( 𝑀 / 3 ) = - ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) ) |
200 |
12 18 20
|
divcld |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) / 3 ) ∈ ℂ ) |
201 |
200 2
|
negsubdi2d |
⊢ ( 𝜑 → - ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) = ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) ) |
202 |
199 201
|
eqtrd |
⊢ ( 𝜑 → - ( 𝑀 / 3 ) = ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) ) |
203 |
202
|
oveq1d |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · 𝑋 ) = ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · 𝑋 ) ) |
204 |
2 200 4
|
subdird |
⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · 𝑋 ) = ( ( 𝐶 · 𝑋 ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) ) ) |
205 |
200 4
|
mulcomd |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) = ( 𝑋 · ( ( 𝐵 ↑ 2 ) / 3 ) ) ) |
206 |
13
|
sqvali |
⊢ ( 3 ↑ 2 ) = ( 3 · 3 ) |
207 |
206
|
oveq2i |
⊢ ( ( 𝐵 ↑ 2 ) / ( 3 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) / ( 3 · 3 ) ) |
208 |
1 18 20
|
sqdivd |
⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( 3 ↑ 2 ) ) ) |
209 |
12 18 18 20 20
|
divdiv1d |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) = ( ( 𝐵 ↑ 2 ) / ( 3 · 3 ) ) ) |
210 |
207 208 209
|
3eqtr4a |
⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) ) |
211 |
210
|
oveq2d |
⊢ ( 𝜑 → ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) = ( 3 · ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) ) ) |
212 |
200 18 20
|
divcan2d |
⊢ ( 𝜑 → ( 3 · ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) ) = ( ( 𝐵 ↑ 2 ) / 3 ) ) |
213 |
211 212
|
eqtrd |
⊢ ( 𝜑 → ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) / 3 ) ) |
214 |
213
|
oveq2d |
⊢ ( 𝜑 → ( 𝑋 · ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) = ( 𝑋 · ( ( 𝐵 ↑ 2 ) / 3 ) ) ) |
215 |
4 18 180
|
mul12d |
⊢ ( 𝜑 → ( 𝑋 · ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) = ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) |
216 |
205 214 215
|
3eqtr2d |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) = ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) |
217 |
216
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) ) = ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) ) |
218 |
203 204 217
|
3eqtrd |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · 𝑋 ) = ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) ) |
219 |
202
|
oveq1d |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) = ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · ( 𝐵 / 3 ) ) ) |
220 |
2 200 46
|
subdird |
⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · ( 𝐵 / 3 ) ) = ( ( 𝐶 · ( 𝐵 / 3 ) ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) ) ) |
221 |
2 1 18 20
|
divassd |
⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) / 3 ) = ( 𝐶 · ( 𝐵 / 3 ) ) ) |
222 |
2 1
|
mulcomd |
⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) ) |
223 |
222
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) / 3 ) = ( ( 𝐵 · 𝐶 ) / 3 ) ) |
224 |
221 223
|
eqtr3d |
⊢ ( 𝜑 → ( 𝐶 · ( 𝐵 / 3 ) ) = ( ( 𝐵 · 𝐶 ) / 3 ) ) |
225 |
12 18 1 18 20 20
|
divmuldivd |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐵 ) / ( 3 · 3 ) ) ) |
226 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
227 |
226
|
oveq2i |
⊢ ( 𝐵 ↑ 3 ) = ( 𝐵 ↑ ( 2 + 1 ) ) |
228 |
|
expp1 |
⊢ ( ( 𝐵 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝐵 ↑ ( 2 + 1 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) ) |
229 |
1 34 228
|
sylancl |
⊢ ( 𝜑 → ( 𝐵 ↑ ( 2 + 1 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) ) |
230 |
227 229
|
eqtr2id |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) · 𝐵 ) = ( 𝐵 ↑ 3 ) ) |
231 |
154
|
a1i |
⊢ ( 𝜑 → ( 3 · 3 ) = 9 ) |
232 |
230 231
|
oveq12d |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) · 𝐵 ) / ( 3 · 3 ) ) = ( ( 𝐵 ↑ 3 ) / 9 ) ) |
233 |
225 232
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) = ( ( 𝐵 ↑ 3 ) / 9 ) ) |
234 |
224 233
|
oveq12d |
⊢ ( 𝜑 → ( ( 𝐶 · ( 𝐵 / 3 ) ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) ) = ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) ) |
235 |
219 220 234
|
3eqtrd |
⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) = ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) ) |
236 |
10
|
oveq1d |
⊢ ( 𝜑 → ( 𝑁 / ; 2 7 ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) / ; 2 7 ) ) |
237 |
33 39 42 44
|
divdird |
⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) / ; 2 7 ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) + ( ( ; 2 7 · 𝐷 ) / ; 2 7 ) ) ) |
238 |
28 32 42 44
|
divsubdird |
⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) ) ) |
239 |
|
9t3e27 |
⊢ ( 9 · 3 ) = ; 2 7 |
240 |
239
|
oveq2i |
⊢ ( ( 9 · ( 𝐵 · 𝐶 ) ) / ( 9 · 3 ) ) = ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) |
241 |
30 18 98 20 101
|
divcan5d |
⊢ ( 𝜑 → ( ( 9 · ( 𝐵 · 𝐶 ) ) / ( 9 · 3 ) ) = ( ( 𝐵 · 𝐶 ) / 3 ) ) |
242 |
240 241
|
eqtr3id |
⊢ ( 𝜑 → ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) = ( ( 𝐵 · 𝐶 ) / 3 ) ) |
243 |
242
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) |
244 |
238 243
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) |
245 |
3 42 44
|
divcan3d |
⊢ ( 𝜑 → ( ( ; 2 7 · 𝐷 ) / ; 2 7 ) = 𝐷 ) |
246 |
244 245
|
oveq12d |
⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) + ( ( ; 2 7 · 𝐷 ) / ; 2 7 ) ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) |
247 |
236 237 246
|
3eqtrd |
⊢ ( 𝜑 → ( 𝑁 / ; 2 7 ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) |
248 |
235 247
|
oveq12d |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) ) |
249 |
26 98 101
|
divcld |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / 9 ) ∈ ℂ ) |
250 |
28 42 44
|
divcld |
⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ∈ ℂ ) |
251 |
249 250
|
negsubdi2d |
⊢ ( 𝜑 → - ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) ) |
252 |
1 18 20 56
|
expdivd |
⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 3 ) = ( ( 𝐵 ↑ 3 ) / ( 3 ↑ 3 ) ) ) |
253 |
58
|
oveq2i |
⊢ ( ( 𝐵 ↑ 3 ) / ( 3 ↑ 3 ) ) = ( ( 𝐵 ↑ 3 ) / ; 2 7 ) |
254 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
255 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
256 |
13 23 254 255
|
subaddrii |
⊢ ( 3 − 2 ) = 1 |
257 |
256
|
oveq1i |
⊢ ( ( 3 − 2 ) · ( 𝐵 ↑ 3 ) ) = ( 1 · ( 𝐵 ↑ 3 ) ) |
258 |
26
|
mulid2d |
⊢ ( 𝜑 → ( 1 · ( 𝐵 ↑ 3 ) ) = ( 𝐵 ↑ 3 ) ) |
259 |
257 258
|
eqtrid |
⊢ ( 𝜑 → ( ( 3 − 2 ) · ( 𝐵 ↑ 3 ) ) = ( 𝐵 ↑ 3 ) ) |
260 |
18 62 26
|
subdird |
⊢ ( 𝜑 → ( ( 3 − 2 ) · ( 𝐵 ↑ 3 ) ) = ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) ) |
261 |
259 260
|
eqtr3d |
⊢ ( 𝜑 → ( 𝐵 ↑ 3 ) = ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) ) |
262 |
261
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / ; 2 7 ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) / ; 2 7 ) ) |
263 |
|
mulcl |
⊢ ( ( 3 ∈ ℂ ∧ ( 𝐵 ↑ 3 ) ∈ ℂ ) → ( 3 · ( 𝐵 ↑ 3 ) ) ∈ ℂ ) |
264 |
13 26 263
|
sylancr |
⊢ ( 𝜑 → ( 3 · ( 𝐵 ↑ 3 ) ) ∈ ℂ ) |
265 |
264 28 42 44
|
divsubdird |
⊢ ( 𝜑 → ( ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) / ; 2 7 ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) ) |
266 |
262 265
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / ; 2 7 ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) ) |
267 |
253 266
|
eqtrid |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / ( 3 ↑ 3 ) ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) ) |
268 |
29 13 239
|
mulcomli |
⊢ ( 3 · 9 ) = ; 2 7 |
269 |
268
|
oveq2i |
⊢ ( ( 3 · ( 𝐵 ↑ 3 ) ) / ( 3 · 9 ) ) = ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) |
270 |
26 98 18 101 20
|
divcan5d |
⊢ ( 𝜑 → ( ( 3 · ( 𝐵 ↑ 3 ) ) / ( 3 · 9 ) ) = ( ( 𝐵 ↑ 3 ) / 9 ) ) |
271 |
269 270
|
eqtr3id |
⊢ ( 𝜑 → ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) = ( ( 𝐵 ↑ 3 ) / 9 ) ) |
272 |
271
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) = ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) ) |
273 |
252 267 272
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 3 ) = ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) ) |
274 |
273
|
negeqd |
⊢ ( 𝜑 → - ( ( 𝐵 / 3 ) ↑ 3 ) = - ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) ) |
275 |
30 18 20
|
divcld |
⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) / 3 ) ∈ ℂ ) |
276 |
275 249 250
|
npncan3d |
⊢ ( 𝜑 → ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) ) |
277 |
251 274 276
|
3eqtr4d |
⊢ ( 𝜑 → - ( ( 𝐵 / 3 ) ↑ 3 ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) ) |
278 |
277
|
oveq1d |
⊢ ( 𝜑 → ( - ( ( 𝐵 / 3 ) ↑ 3 ) + 𝐷 ) = ( ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) + 𝐷 ) ) |
279 |
184
|
negcld |
⊢ ( 𝜑 → - ( ( 𝐵 / 3 ) ↑ 3 ) ∈ ℂ ) |
280 |
279 3
|
addcomd |
⊢ ( 𝜑 → ( - ( ( 𝐵 / 3 ) ↑ 3 ) + 𝐷 ) = ( 𝐷 + - ( ( 𝐵 / 3 ) ↑ 3 ) ) ) |
281 |
235 192
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) ∈ ℂ ) |
282 |
250 275
|
subcld |
⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ∈ ℂ ) |
283 |
281 282 3
|
addassd |
⊢ ( 𝜑 → ( ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) + 𝐷 ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) ) |
284 |
278 280 283
|
3eqtr3d |
⊢ ( 𝜑 → ( 𝐷 + - ( ( 𝐵 / 3 ) ↑ 3 ) ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) ) |
285 |
3 184
|
negsubd |
⊢ ( 𝜑 → ( 𝐷 + - ( ( 𝐵 / 3 ) ↑ 3 ) ) = ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) |
286 |
248 284 285
|
3eqtr2d |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) = ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) |
287 |
218 286
|
oveq12d |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) + ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
288 |
190 193 287
|
3eqtrd |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) + ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
289 |
2 4
|
mulcld |
⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ ℂ ) |
290 |
289 3 182 184
|
addsub4d |
⊢ ( 𝜑 → ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) = ( ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) + ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
291 |
288 290
|
eqtr4d |
⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) |
292 |
291
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) ) |
293 |
289 3
|
addcld |
⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) + 𝐷 ) ∈ ℂ ) |
294 |
185 293
|
pncan3d |
⊢ ( 𝜑 → ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) |
295 |
292 294
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) |
296 |
295
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) |
297 |
175 188 296
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) |
298 |
297
|
eqeq1d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = 0 ↔ ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ) ) |
299 |
|
oveq1 |
⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = ( 0 ↑ 3 ) ) |
300 |
|
0exp |
⊢ ( 3 ∈ ℕ → ( 0 ↑ 3 ) = 0 ) |
301 |
50 300
|
ax-mp |
⊢ ( 0 ↑ 3 ) = 0 |
302 |
299 301
|
eqtrdi |
⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = 0 ) |
303 |
|
0ne1 |
⊢ 0 ≠ 1 |
304 |
303
|
a1i |
⊢ ( 𝑟 = 0 → 0 ≠ 1 ) |
305 |
302 304
|
eqnetrd |
⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) ≠ 1 ) |
306 |
305
|
necon2i |
⊢ ( ( 𝑟 ↑ 3 ) = 1 → 𝑟 ≠ 0 ) |
307 |
|
eqcom |
⊢ ( 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ↔ - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = 𝑋 ) |
308 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝐵 ∈ ℂ ) |
309 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑟 ∈ ℂ ) |
310 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑇 ∈ ℂ ) |
311 |
309 310
|
mulcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · 𝑇 ) ∈ ℂ ) |
312 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑀 ∈ ℂ ) |
313 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑟 ≠ 0 ) |
314 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑇 ≠ 0 ) |
315 |
309 310 313 314
|
mulne0d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · 𝑇 ) ≠ 0 ) |
316 |
312 311 315
|
divcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / ( 𝑟 · 𝑇 ) ) ∈ ℂ ) |
317 |
311 316
|
addcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ∈ ℂ ) |
318 |
13
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 3 ∈ ℂ ) |
319 |
19
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 3 ≠ 0 ) |
320 |
308 317 318 319
|
divdird |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 + ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) / 3 ) = ( ( 𝐵 / 3 ) + ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
321 |
308 311 316
|
addassd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) = ( 𝐵 + ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) |
322 |
321
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( 𝐵 + ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) / 3 ) ) |
323 |
46
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝐵 / 3 ) ∈ ℂ ) |
324 |
317 318 319
|
divcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ∈ ℂ ) |
325 |
323 324
|
subnegd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) = ( ( 𝐵 / 3 ) + ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
326 |
320 322 325
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
327 |
326
|
negeqd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = - ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
328 |
324
|
negcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ∈ ℂ ) |
329 |
323 328
|
negsubdi2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) = ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) ) |
330 |
327 329
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) ) |
331 |
330
|
eqeq1d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = 𝑋 ↔ ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) = 𝑋 ) ) |
332 |
307 331
|
syl5bb |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ↔ ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) = 𝑋 ) ) |
333 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑋 ∈ ℂ ) |
334 |
328 323 333
|
subadd2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) = 𝑋 ↔ ( 𝑋 + ( 𝐵 / 3 ) ) = - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
335 |
311 316 318 319
|
divdird |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( ( 𝑟 · 𝑇 ) / 3 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) ) |
336 |
335
|
negeqd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = - ( ( ( 𝑟 · 𝑇 ) / 3 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) ) |
337 |
311 318 319
|
divcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 3 ) ∈ ℂ ) |
338 |
316 318 319
|
divcld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ∈ ℂ ) |
339 |
337 338
|
negdi2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) / 3 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) = ( - ( ( 𝑟 · 𝑇 ) / 3 ) − ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) ) |
340 |
309 310 318 319
|
divassd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 3 ) = ( 𝑟 · ( 𝑇 / 3 ) ) ) |
341 |
340
|
negeqd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( 𝑟 · 𝑇 ) / 3 ) = - ( 𝑟 · ( 𝑇 / 3 ) ) ) |
342 |
48
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑇 / 3 ) ∈ ℂ ) |
343 |
309 342
|
mulneg2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · - ( 𝑇 / 3 ) ) = - ( 𝑟 · ( 𝑇 / 3 ) ) ) |
344 |
341 343
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( 𝑟 · 𝑇 ) / 3 ) = ( 𝑟 · - ( 𝑇 / 3 ) ) ) |
345 |
312 311 318 315 319
|
divdiv32d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) = ( ( 𝑀 / 3 ) / ( 𝑟 · 𝑇 ) ) ) |
346 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / 3 ) ∈ ℂ ) |
347 |
346 311 318 315 319
|
divcan7d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑀 / 3 ) / 3 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 3 ) / ( 𝑟 · 𝑇 ) ) ) |
348 |
156
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑀 / 3 ) / 3 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) ) |
349 |
348
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑀 / 3 ) / 3 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) ) |
350 |
345 347 349
|
3eqtr2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) ) |
351 |
121
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / 9 ) ∈ ℂ ) |
352 |
311 318 315 319
|
divne0d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 3 ) ≠ 0 ) |
353 |
351 337 352
|
div2negd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( 𝑀 / 9 ) / - ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) ) |
354 |
344
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( 𝑀 / 9 ) / - ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) |
355 |
350 353 354
|
3eqtr2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) = ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) |
356 |
344 355
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( ( 𝑟 · 𝑇 ) / 3 ) − ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) |
357 |
336 339 356
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) |
358 |
357
|
eqeq2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ↔ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ) |
359 |
332 334 358
|
3bitrrd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
360 |
359
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ 𝑟 ≠ 0 ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
361 |
306 360
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( 𝑟 ↑ 3 ) = 1 ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) |
362 |
361
|
pm5.32da |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → ( ( ( 𝑟 ↑ 3 ) = 1 ∧ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ↔ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) ) |
363 |
362
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) ) |
364 |
163 298 363
|
3bitr3d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) ) |