Step |
Hyp |
Ref |
Expression |
1 |
|
quart.a |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
2 |
|
quart.b |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
3 |
|
quart.c |
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
4 |
|
quart.d |
⊢ ( 𝜑 → 𝐷 ∈ ℂ ) |
5 |
|
quart.x |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
6 |
|
quart.e |
⊢ ( 𝜑 → 𝐸 = - ( 𝐴 / 4 ) ) |
7 |
|
quart.p |
⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) ) |
8 |
|
quart.q |
⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) ) |
9 |
|
quart.r |
⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / ; 1 6 ) − ( ( 3 / ; ; 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) ) |
10 |
|
quart.u |
⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( ; 1 2 · 𝑅 ) ) ) |
11 |
|
quart.v |
⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( ; 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( ; 7 2 · ( 𝑃 · 𝑅 ) ) ) ) |
12 |
|
quart.w |
⊢ ( 𝜑 → 𝑊 = ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) ) |
13 |
|
quart.s |
⊢ ( 𝜑 → 𝑆 = ( ( √ ‘ 𝑀 ) / 2 ) ) |
14 |
|
quart.m |
⊢ ( 𝜑 → 𝑀 = - ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) ) |
15 |
|
quart.t |
⊢ ( 𝜑 → 𝑇 = ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ) |
16 |
|
quart.t0 |
⊢ ( 𝜑 → 𝑇 ≠ 0 ) |
17 |
|
quart.m0 |
⊢ ( 𝜑 → 𝑀 ≠ 0 ) |
18 |
|
quart.i |
⊢ ( 𝜑 → 𝐼 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ) |
19 |
|
quart.j |
⊢ ( 𝜑 → 𝐽 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ) |
20 |
1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16
|
quartlem3 |
⊢ ( 𝜑 → ( 𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ ) ) |
21 |
20
|
simp2d |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
22 |
21
|
sqrtcld |
⊢ ( 𝜑 → ( √ ‘ 𝑀 ) ∈ ℂ ) |
23 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
24 |
21
|
sqsqrtd |
⊢ ( 𝜑 → ( ( √ ‘ 𝑀 ) ↑ 2 ) = 𝑀 ) |
25 |
24 17
|
eqnetrd |
⊢ ( 𝜑 → ( ( √ ‘ 𝑀 ) ↑ 2 ) ≠ 0 ) |
26 |
|
sqne0 |
⊢ ( ( √ ‘ 𝑀 ) ∈ ℂ → ( ( ( √ ‘ 𝑀 ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ 𝑀 ) ≠ 0 ) ) |
27 |
22 26
|
syl |
⊢ ( 𝜑 → ( ( ( √ ‘ 𝑀 ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ 𝑀 ) ≠ 0 ) ) |
28 |
25 27
|
mpbid |
⊢ ( 𝜑 → ( √ ‘ 𝑀 ) ≠ 0 ) |
29 |
|
2ne0 |
⊢ 2 ≠ 0 |
30 |
29
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
31 |
22 23 28 30
|
divne0d |
⊢ ( 𝜑 → ( ( √ ‘ 𝑀 ) / 2 ) ≠ 0 ) |
32 |
13 31
|
eqnetrd |
⊢ ( 𝜑 → 𝑆 ≠ 0 ) |
33 |
20
|
simp1d |
⊢ ( 𝜑 → 𝑆 ∈ ℂ ) |
34 |
33
|
sqcld |
⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℂ ) |
35 |
34
|
negcld |
⊢ ( 𝜑 → - ( 𝑆 ↑ 2 ) ∈ ℂ ) |
36 |
1 2 3 4 7 8 9
|
quart1cl |
⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) ) |
37 |
36
|
simp1d |
⊢ ( 𝜑 → 𝑃 ∈ ℂ ) |
38 |
37
|
halfcld |
⊢ ( 𝜑 → ( 𝑃 / 2 ) ∈ ℂ ) |
39 |
35 38
|
subcld |
⊢ ( 𝜑 → ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) ∈ ℂ ) |
40 |
36
|
simp2d |
⊢ ( 𝜑 → 𝑄 ∈ ℂ ) |
41 |
|
4cn |
⊢ 4 ∈ ℂ |
42 |
41
|
a1i |
⊢ ( 𝜑 → 4 ∈ ℂ ) |
43 |
|
4ne0 |
⊢ 4 ≠ 0 |
44 |
43
|
a1i |
⊢ ( 𝜑 → 4 ≠ 0 ) |
45 |
40 42 44
|
divcld |
⊢ ( 𝜑 → ( 𝑄 / 4 ) ∈ ℂ ) |
46 |
45 33 32
|
divcld |
⊢ ( 𝜑 → ( ( 𝑄 / 4 ) / 𝑆 ) ∈ ℂ ) |
47 |
39 46
|
addcld |
⊢ ( 𝜑 → ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ∈ ℂ ) |
48 |
47
|
sqrtcld |
⊢ ( 𝜑 → ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ∈ ℂ ) |
49 |
18 48
|
eqeltrd |
⊢ ( 𝜑 → 𝐼 ∈ ℂ ) |
50 |
39 46
|
subcld |
⊢ ( 𝜑 → ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ∈ ℂ ) |
51 |
50
|
sqrtcld |
⊢ ( 𝜑 → ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ∈ ℂ ) |
52 |
19 51
|
eqeltrd |
⊢ ( 𝜑 → 𝐽 ∈ ℂ ) |
53 |
32 49 52
|
3jca |
⊢ ( 𝜑 → ( 𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ) ) |