Metamath Proof Explorer

Theorem quartlem3

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 )
Assertion quartlem3 ( 𝜑 → ( 𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ ) )

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 2cn ⊢ 2 ∈ ℂ
18 1 2 3 4 7 8 9 quart1cl ⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
19 18 simp1d ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
20 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( 2 · 𝑃 ) ∈ ℂ )
21 17 19 20 sylancr ⊢ ( 𝜑 → ( 2 · 𝑃 ) ∈ ℂ )
22 1 2 3 4 1 6 7 8 9 10 11 12 quartlem2 ⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ ) )
23 22 simp2d ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
24 22 simp3d ⊢ ( 𝜑 → 𝑊 ∈ ℂ )
25 23 24 addcld ⊢ ( 𝜑 → ( 𝑉 + 𝑊 ) ∈ ℂ )
26 25 halfcld ⊢ ( 𝜑 → ( ( 𝑉 + 𝑊 ) / 2 ) ∈ ℂ )
27 3nn ⊢ 3 ∈ ℕ
28 nnrecre ⊢ ( 3 ∈ ℕ → ( 1 / 3 ) ∈ ℝ )
29 27 28 ax-mp ⊢ ( 1 / 3 ) ∈ ℝ
30 29 recni ⊢ ( 1 / 3 ) ∈ ℂ
31 cxpcl ⊢ ( ( ( ( 𝑉 + 𝑊 ) / 2 ) ∈ ℂ ∧ ( 1 / 3 ) ∈ ℂ ) → ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
32 26 30 31 sylancl ⊢ ( 𝜑 → ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
33 15 32 eqeltrd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
34 21 33 addcld ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) + 𝑇 ) ∈ ℂ )
35 22 simp1d ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
36 35 33 16 divcld ⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) ∈ ℂ )
37 34 36 addcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) ∈ ℂ )
38 3cn ⊢ 3 ∈ ℂ
39 38 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
40 3ne0 ⊢ 3 ≠ 0
41 40 a1i ⊢ ( 𝜑 → 3 ≠ 0 )
42 37 39 41 divcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) ∈ ℂ )
43 42 negcld ⊢ ( 𝜑 → - ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) ∈ ℂ )
44 14 43 eqeltrd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
45 44 sqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑀 ) ∈ ℂ )
46 45 halfcld ⊢ ( 𝜑 → ( ( √ ‘ 𝑀 ) / 2 ) ∈ ℂ )
47 13 46 eqeltrd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
48 47 44 33 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ ) )