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