Metamath Proof Explorer


Theorem quartlem4

Description: Closure lemmas for quart . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses quart.a ( 𝜑𝐴 ∈ ℂ )
quart.b ( 𝜑𝐵 ∈ ℂ )
quart.c ( 𝜑𝐶 ∈ ℂ )
quart.d ( 𝜑𝐷 ∈ ℂ )
quart.x ( 𝜑𝑋 ∈ ℂ )
quart.e ( 𝜑𝐸 = - ( 𝐴 / 4 ) )
quart.p ( 𝜑𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
quart.q ( 𝜑𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
quart.r ( 𝜑𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 1 6 ) − ( ( 3 / 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
quart.u ( 𝜑𝑈 = ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) )
quart.v ( 𝜑𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
quart.w ( 𝜑𝑊 = ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) )
quart.s ( 𝜑𝑆 = ( ( √ ‘ 𝑀 ) / 2 ) )
quart.m ( 𝜑𝑀 = - ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) )
quart.t ( 𝜑𝑇 = ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) )
quart.t0 ( 𝜑𝑇 ≠ 0 )
quart.m0 ( 𝜑𝑀 ≠ 0 )
quart.i ( 𝜑𝐼 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) )
quart.j ( 𝜑𝐽 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) )
Assertion quartlem4 ( 𝜑 → ( 𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ) )

Proof

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 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ) )