Metamath Proof Explorer

Theorem quartlem2

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 ) ) ) ) )
Assertion quartlem2 ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ ) )

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 1 2 3 4 7 8 9 quart1cl ⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
14 13 simp1d ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
15 14 sqcld ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℂ )
16 1nn0 ⊢ 1 ∈ ℕ0
17 2nn ⊢ 2 ∈ ℕ
18 16 17 decnncl ⊢ 1 2 ∈ ℕ
19 18 nncni ⊢ 1 2 ∈ ℂ
20 13 simp3d ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
21 mulcl ⊢ ( ( 1 2 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 1 2 · 𝑅 ) ∈ ℂ )
22 19 20 21 sylancr ⊢ ( 𝜑 → ( 1 2 · 𝑅 ) ∈ ℂ )
23 15 22 addcld ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) ∈ ℂ )
24 10 23 eqeltrd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
25 2cn ⊢ 2 ∈ ℂ
26 3nn0 ⊢ 3 ∈ ℕ0
27 expcl ⊢ ( ( 𝑃 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑃 ↑ 3 ) ∈ ℂ )
28 14 26 27 sylancl ⊢ ( 𝜑 → ( 𝑃 ↑ 3 ) ∈ ℂ )
29 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑃 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
30 25 28 29 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
31 30 negcld ⊢ ( 𝜑 → - ( 2 · ( 𝑃 ↑ 3 ) ) ∈ ℂ )
32 2nn0 ⊢ 2 ∈ ℕ0
33 7nn ⊢ 7 ∈ ℕ
34 32 33 decnncl ⊢ 2 7 ∈ ℕ
35 34 nncni ⊢ 2 7 ∈ ℂ
36 13 simp2d ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
37 36 sqcld ⊢ ( 𝜑 → ( 𝑄 ↑ 2 ) ∈ ℂ )
38 mulcl ⊢ ( ( 2 7 ∈ ℂ ∧ ( 𝑄 ↑ 2 ) ∈ ℂ ) → ( 2 7 · ( 𝑄 ↑ 2 ) ) ∈ ℂ )
39 35 37 38 sylancr ⊢ ( 𝜑 → ( 2 7 · ( 𝑄 ↑ 2 ) ) ∈ ℂ )
40 31 39 subcld ⊢ ( 𝜑 → ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) ∈ ℂ )
41 7nn0 ⊢ 7 ∈ ℕ0
42 41 17 decnncl ⊢ 7 2 ∈ ℕ
43 42 nncni ⊢ 7 2 ∈ ℂ
44 14 20 mulcld ⊢ ( 𝜑 → ( 𝑃 · 𝑅 ) ∈ ℂ )
45 mulcl ⊢ ( ( 7 2 ∈ ℂ ∧ ( 𝑃 · 𝑅 ) ∈ ℂ ) → ( 7 2 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
46 43 44 45 sylancr ⊢ ( 𝜑 → ( 7 2 · ( 𝑃 · 𝑅 ) ) ∈ ℂ )
47 40 46 addcld ⊢ ( 𝜑 → ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) ∈ ℂ )
48 11 47 eqeltrd ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
49 48 sqcld ⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℂ )
50 4cn ⊢ 4 ∈ ℂ
51 expcl ⊢ ( ( 𝑈 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑈 ↑ 3 ) ∈ ℂ )
52 24 26 51 sylancl ⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ∈ ℂ )
53 mulcl ⊢ ( ( 4 ∈ ℂ ∧ ( 𝑈 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
54 50 52 53 sylancr ⊢ ( 𝜑 → ( 4 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
55 49 54 subcld ⊢ ( 𝜑 → ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ∈ ℂ )
56 55 sqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) ∈ ℂ )
57 12 56 eqeltrd ⊢ ( 𝜑 → 𝑊 ∈ ℂ )
58 24 48 57 3jca ⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ ) )